Repository navigation
Support lean4 - #8
Closed
Koukyosyumei wants to merge 196 commits into
Closed
Koukyosyumei wants to merge 196 commits into
Koukyosyumei wants to merge 196 commits into
Conversation
Inherited from the previous agent's handoff, reviewed and committed as found: the strict e5r-verify ELF exporter, the bounded RV32I Lean model, an independent Lean ELF reader, the assembly and no_std Rust clamp fixtures with finite (all byte inputs) kernel-checked proofs, negative controls, the QEMU differential oracle and the checking runner. Known baseline problem, fixed in the next commit: the runner writes into fixtures/build/lean-rv32, which makes the absent fixture corpus look present, so five e5r-analysis cache tests panic with "fixture" instead of skipping. Separately, 21 corpus-gated tests fail by design on this host because scripts/build-fixtures.sh needs an AArch64 cross gcc, llvm-mc and llvm-pdbutil, none of which are installed here. CI builds that corpus.
The corpus-gated workspace tests take the existence of fixtures/build as 'the fixture corpus was built'. The V0 runner created fixtures/build/lean-rv32, so on a checkout without the corpus five e5r-analysis cache tests panicked on a missing fixture instead of skipping. Build output now goes to the ignored verification/rv32/build/. The cache suite passes 9/9 again and the V0 checker passes end to end from the new location.
The first product target: an unmodified Embassy 0.10 thread-mode executor on the SiFive FE310-G002 (HiFive1 Rev B, RV32IMAC), built with the stable riscv32imac-unknown-none-elf target and plain cargo. A CLINT time driver (embassy-time-driver + embassy-time-queue-utils, the documented route for a chip without an Embassy HAL) drives a 10 ms sampler task that reads UART0 and sends through an embassy-sync Channel to an actuator task, which keeps a moving window and writes a clamped duty to PWM0 pwmcmp1. Cargo.lock pins every dependency. Debug info is off so the ELF is byte-identical from any checkout path (checked from two paths). It runs on QEMU 8.2.2 sifive_e,revb=true: duty values follow mean+7 clamped at 100.
…EMU replay Theories/Hart.lean: RV32IMAC + Zicsr + Zifencei + MRET/WFI decoding (including the RV32C expansion) and an instruction semantics that returns a first-order effect tree, following the ISA/memory split of Theorem Labs' rocq-linux-process-semantics (design only, nothing copied). Architectural traps and 'the model declines' are separate outcomes. Machine-mode CSRs are limited to the fields the scope needs; anything else fails closed. Theories/Platform.lean: RAM, a read-only executable flash image and a device register table interpret those effects. Device reads, interrupts at enabled boundaries and SC success are environmental choices; the platform is an over-approximation in exactly those places and unsupported elsewhere. Step, Escapes and Reach define what a safety proof has to cover. boards/hifive1-revb.json is the machine-readable board description (memory map, device registers, boot assumptions, exclusions). tools/gen_board.py generates Theories/Board/Hifive1Revb.lean from it. e5r-verify flash exports the flash contents a board boots from (file bytes at p_paddr; RAM arbitrary), cross-checked against e5r's loader, and Theories/FlashElf.lean is an independent Lean reader of the same rules. tools/qemu_trace.py + tools/Replay.lean (native, via lake build replay) replay a QEMU sifive_e single-instruction trace in the model. On the Embassy firmware: 43297 transitions, 118 timer interrupts and 716 device writes with every GPR and modeled CSR equal after every transition. The replay found and this commit fixes a lost pc advance after environmental CSR reads.
ROADMAP section F records the owner's expansion of V0 into a staged product for one board, with an acceptance criterion per milestone (F1 accepted, F2-F8 open) and the explicit non-scope list. docs/firmware-verification.md states the supported configuration, the shape of a guarantee, the environmental over-approximations, boot assumptions, exclusions and trusted computing base, in the same terms as boards/hifive1-revb.json.
…re binary Theories/Logic.lean adds the program logic the symbolic proofs use: deterministic steps (the same result under every environment, no events), the fetch/decode/execute bridge, per-instruction effect lemmas, register get/set and CSR frame lemmas, and RAM load/store interpretation. Projects/hifive1/Duty.lean proves duty() as rustc emitted it in the checked flash image: from every state meeting the calling convention (a0 points at 8 bytes of RAM), it returns to ra with a0 = min(sum/8 + 7, 100) -- the source-level expression, related to the compiler's min(sum/8, 93) + 7 -- RAM unchanged, only a1-a3 clobbered and every CSR preserved. The loop is proved by an invariant over the iteration count. Axioms: propext, Classical.choice, Quot.sound.
Projects/hifive1/clamp: the V0 clamp source on the HiFive1 memory map, compiled for riscv32imac with the pinned rustc (opt-level 1, 2 and s emit identical bytes). clamp_all proves, from every boot state with the pc at the entry point (all registers, CSRs and RAM arbitrary), that the binary reaches its idle loop having stored input.wrapping_add(7).min(100) -- for all 2^32 inputs, without enumeration -- and changed no other RAM byte or CSR. wraps exhibits the overflow case (0xfffffffa -> 1) that a non-wrapping reading of the source would get wrong. Axioms: propext, Quot.sound. ramRead/ramWrite are restated arithmetically (same values) so that read-after-write and RAM frame lemmas, added to Theories/Logic.lean, are linear facts.
With interrupts enabled first, every task the interrupt handler can wake spends some time half-initialized (a null poll function), which any sound whole-program invariant has to admit and the executor's run loop then cannot be shown safe. Spawning first is the natural order anyway. duty() keeps its address and its contract still checks; the QEMU replay of the rebuilt binary (input 'AzB\xff\x00Q') agrees with the model on 62773 transitions, 170 timer interrupts and 1032 device writes.
Not a result yet: nothing here is proved sound and the analyzer does not yet produce a certificate for the Embassy firmware. Committed so the design and the measured state are reviewable. Theories/Absint.lean defines the checker the whole-firmware proof will rest on: value sets / ranges / symbolic handler-entry values, memory cells with guarded facts (enough for Option<Waker>'s null niche), a transfer function that mirrors Hart.exec, split edges, a global static-RAM invariant G for interruptible nodes, and a handler summary relative to the interrupted registers and sp, with a pinned region for main's never-returning frame (where the Embassy executor lives). tools/Analyze.lean is the untrusted search that produces certificates with the same transfer function. On the firmware it currently explores ~30k nodes and stops with ~119 possible faults, almost all one imprecision: the timer queue's waker vtable/data correlation is lost on some handler path, so wake() is reachable with a null task. Remaining: fix that, shrink the certificate (function summaries) to a size the kernel can check, and prove check_sound.
…-result detection A job file (e5r.verify.job.v1) names the ELF and how to build it, its reviewed SHA-256, the board, the Lean modules and the theorems to audit, and time/memory limits. e5r-verify check rebuilds the ELF, refuses a stale generated board, exports the flash image, generates a per-job image-fidelity theorem (the independent Lean ELF reader must reconstruct the exported image from the original bytes), scans every module for proof escapes, compiles each from source with one worker under a resident-memory watchdog and a timeout, and audits every named theorem's axioms. The result (e5r.verify.result.v1) records the status -- proved, failed, unsupported, resource_exhausted or error; a failed proof is never reported as a counterexample -- with SHA-256 identities of the job, board, ELF and every model and proof source, the Lean and e5r-verify versions, the allowed axioms, and per-stage time and peak RSS. e5r-verify verify-result says whether a stored result still describes the current inputs. Jobs for the firmware's duty() contract and the 32-bit clamp both check (proved; duty_contract: propext, Classical.choice, Quot.sound; clamp_all: propext, Quot.sound; image fidelity: propext). tools/test_job_controls.py runs six negative controls (changed ELF identity, false theorem, sorry, memory limit, non-ELF input, unknown theorem) and each gets the status it should. SHA-256 is implemented in-crate with the FIPS 180 vectors; the board schema is renamed e5r.board.v1 to follow e5r's JSON convention.
…ault class tools/run_isa_differential.py generates seeded random RV32IMAC programs (tools/gen_isa_test.py: every base ALU op and shift, upper immediates, all branches both ways, JAL/JALR including bit-0 clearing, every load/store width, all of M with zero divisors and overflow, every AMO, LR/SC, fences and the RV32C forms), runs them under qemu-riscv32 one instruction per block, and replays QEMU's register trace in the model (lake exe replay_isa, which reads the program through the independent Lean ELF reader). Seeds 1-4: about 30k instructions, every register equal after every one, all 84 required instruction kinds executed (tools/isa_coverage.py), and a trace with one flipped bit is rejected. The replay code is now a library shared with the firmware replay. Projects/Controls.lean: 30 kernel-checked controls on the platform model -- misaligned loads/stores, unmapped and past-RAM addresses, stores to flash, device width and direction, atomics outside RAM, illegal encodings (F, the zero halfword, C.FLD), ecall/ebreak/c.ebreak, unmodeled CSRs, read-only CSR writes, unmodeled mstatus/mtvec fields, mret to U-mode, SC with and without a reservation, fetch outside the image and from an odd pc, JALR bit clearing, interrupt enabling, and that an accepted device write is exactly one event. The firmware job audits them (E5R.Controls.*: job theorem patterns now expand over a namespace) and proves: 33 theorems. Image modules set maxHeartbeats 0 so a large ELF literal can be compiled natively for the replay tools; that affects elaboration only.
…amespaces duty: from a concrete calling-convention state with a window of eight 10s, the emitted function returns 17. clamp: a concrete boot state with input 0xfffffffa reaches the idle loop having stored the wrapped result 1. Both jobs now audit every theorem their modules declare: hifive1-clamp32 proves 15 theorems (20 s, 596 MiB peak), hifive1-duty 50 including the 30 model controls (40 s, 957 MiB peak).
scripts/check-firmware-verification.sh refuses stale generated boards, runs every verification job fresh and confirms each result is current, then runs the runner's negative controls, the instruction-level QEMU differential test and the whole-firmware sifive_e replay (tools/run_firmware_replay.py, which also checks the duty values against the UART input). On the development host: every job proved, every control and test passed, 903 s, about 1 GB peak. The new firmware-verification CI job runs the same script on ubuntu-24.04 with a dev-profile e5r-verify, the pinned rustc for the fixtures, elan for Lean and Ubuntu's binutils 2.42 / QEMU 8.2.2, and uploads the results. It has not yet run on a GitHub runner. e5r-verify bundle writes a self-contained directory whose recheck.sh rechecks a proved job with nothing but the pinned Lean: SHA-256 sums, every module recompiled, the axiom report diffed against the recorded one (checked: the clamp bundle, 11 MB, rechecks offline). check --resume reuses a module's olean only when the chained hash of its source, every earlier module's source and the Lean version is unchanged. docs/firmware-verification.md now states the status plainly (function-level proofs done; the whole-firmware theorem not proved), how to run and read jobs and results, how to add a target, the current results and the validation evidence; docs/firmware-verification-install.md covers a fresh machine. ROADMAP F2, F3, F4 and F6 are accepted; F5 and F8 list what is done and open; F7 is open.
Joining kept only the left state's facts, so a guarded fact that the left state implied through plain facts (after the vtable and data words were rewritten in sequence inside a critical section) was dropped. The firmware analysis still reports the same possible faults (wake() with a null task in the handler); the investigation continues in the next session.
A separate review of the trusted base against the RISC-V specifications found: - SC without a reservation returned 'fail' without checking its address, so a misaligned or non-RAM SC did not trap (Zalrsc requires it). SC now probes its address with an atomic load first; Absint mirrors it; two controls added. - A proof module could add a theorem with kernel checking switched off via run_cmd and an option name built from strings; the word scan and the axiom audit both accepted it. Metaprogramming commands are now forbidden, character literals no longer hide code from the scan, and every module is replayed through a fresh kernel with leanchecker after compiling. The exploit is a permanent runner control. - Vectored mtvec with a base not aligned enough computes a different vector on SiFive cores (they OR the cause in). Vectored mode now needs a 128-byte-aligned base, else unsupported; controls added. - The flash window was the whole 512 MiB XIP alias; it is now the 4 MiB physical flash after the 64 KiB bootloader. - Runner: an import outside the job's checked modules is refused; the e5r-verify binary and gen_board.py are part of a result's identity; a change to the inputs during a run is an error; Ns.* sees attributed and modified theorems; jobs can pin hard-coded addresses to ELF symbols (the duty job pins 0x200102a0 to duty). - The docs overstated the literal check and the duty address binding; corrected, and the review is recorded in firmware-verification.md. After the fixes: hifive1-clamp32 proves 15 theorems, hifive1-duty 54 (with the new controls), and all 8 runner controls get their expected status.
Concretization of abstract values and the first soundness lemmas: value-set normalization, mkVals, constants, small ranges, the order (leq_sound), bounds, the exact set lift (lift2_sound) and addition of a constant (addC_sound) with and without wraparound. Proof-only; nothing depends on it yet and no whole-firmware claim is made.
add (exact sets, constants, non-wrapping ranges), sub, and, or, xor, shifts by constants (logical, arithmetic for non-negative ranges, left without overflow), slt and sltu (exact sets, and ranges decided by their bounds); alu_sound ties them to Hart's alu. Proof-only WIP.
canTake_sound: a branch direction is reported possible whenever a described pair of operands takes it (exact sets, the symbolic equal-operand case, and bounds for all six conditions, signed ones when both ranges are non-negative). refineL_sound / refineR_sound: narrowing an operand by the outcome of a comparison with a constant keeps every value that takes that outcome. The checker's refinement is factored into topRng, a core refinement and small (same behavior) so each piece has its own lemma.
extend_sound: an unsigned byte or halfword load is the raw value (it fits its width), a signed one is exact on value sets and unchanged on ranges below the width's sign bit. The checker's signed limit is a named function (same values) so the proof does not depend on how an if-chain reduces.
What a cell means (absolute or relative to the interrupted sp, with its guard), and soundness of the checker's reads: plain facts, guard evaluation, guarded lookup and loadCell (with the byte/halfword range defaults, since a loaded byte or halfword always fits). Proof-only WIP.
… proof) absStore recorded the abstract value of the whole register for sb/sh, but memory keeps only the low 8/16 bits: after sb of 0x1ff the checker would have described a following lbu as 0x1ff instead of 0xff. Narrow stores now record the value masked to their width. Found while writing the store lemmas of the soundness proof; the checker had not yet been used for any result. Also re-ran the full one-command check after the independent review's fixes: every job proved, every control and differential test passed (the firmware replay: 47021 transitions, 126 interrupts, duty values matching the input; 880 s).
ramWrite leaves every byte it does not touch; a read whose bytes are disjoint from a write is unchanged; reading a write back at its own address and width gives the stored value masked to the width. Proof-only WIP.
join_sound_left/right; storeStrong_sound (a strong store's new fact holds after the write and every kept fact still holds, given the store's separation from the cells it keeps -- including the guarded fact made vacuous by storing exactly the guard value); storeWeak_weakens and storeWeak_write (a store to one of several candidate addresses); setPlain_sound (pinning a just-loaded value). Proof-only WIP.
Absolute cells and guards must lie inside RAM, relative cells within the handler's budget below the interrupted sp, main-thread states may hold only absolute cells, and RAM must lie inside the 32-bit space. The soundness proof uses these to turn the checker's numeric overlap tests into byte disjointness (no access wraps).
…ss lemmas absLoad/absStore are now folds of loadAt/storeAt over the candidate addresses (same results; the analyzer explores the same 30476 nodes with the same 119 open reports), which is the shape the soundness proof needs. The checker also requires every interrupted sp to be word aligned and the stack to start at or above RAM. Logic gains the platform's ROM-load, device-load and device-store interpretation lemmas.
classify's answers as concrete facts, a fold lemma for the per-address joins, ROM reads bounded by their width, and absLoad_vals_sound: for every candidate address the platform takes the RAM, ROM or device branch without faulting and hands on a value the abstract load describes, which fits the access width. The checker now also requires image bytes to be bytes (a segment's Nat list could otherwise make a ROM byte load inexact).
storeSep_abs derives a store's separation obligations from the checker's well-formedness and overlap tests; EvOk states the device-write property; writeOk_sound; storeAt_written: at the address actually written the platform either writes RAM (and the abstract memory still holds) or emits one event the property allows.
….., 0x80003f58..) and 5 generated segments (next call, None -> tail call, Some -> park call, bounds check -> request decoder call, after tail)
…ounds check -> request decoder call, or None: tail; conditional on CopyContract Composes next_from_copy, park_from_copy and tail_from_copy at their real call sites (CallEnv from the session's fixed bases and sp), no panic for any buffer contents, writes confined (deframer, buffer, 0x70 stack, s6+0x2db). Not SessionSafe: dispatch, response, unpark, UART future and executor are not covered. 3.4 s; leanchecker ok; standard axioms.
…tes and delimiter were consumed); proved in call_case Needed by the session: from_decoded's length argument is 488 - parked, and k < consumed gives parked <= 485. Dependents recompile; leanchecker ok.
…o 0x80003e70; its length panic is not taken (parked <= 484 from next's k < consumed) 13 kernel-checked facts, one generated segment (sfrom), recv_step's Some outcome now records the message (buffer, 488 - parked >= 3, k). Still conditional on CopyContract; still NOT SessionSafe (dispatch from 0x80003e70, response, unpark, UART future, executor). leanchecker ok; standard axioms.
…oved); the session loop needs it to re-establish SessPre
…ing -> loop head with SessPre), callEnv_of; session map from the bytes Conditional on CopyContract. The map records what is proved (recv_step, unpark_step) and what is not: dispatch/response 0x80003e70..0x80003fd4 (yields to the executor) and the None path's UART read future (device oracle reads). No new assumptions. 7 facts, 2 generated segments; leanchecker ok; standard axioms.
…ts expansion at all 23 uses; reword 'axiom' in four header comments (runner word scan) No proof changed. All 36 Deframer/Cobs modules pass the runner's FORBIDDEN word scan (same tokenizer); fresh rebuild 205 s; leanchecker ok on every Deframer module; main theorems: propext, Classical.choice, Quot.sound only.
…erministic runs between checkpoints => every reachable machine, under any oracle) Every machine Reach-able from a checkpoint set whose members all start a quiet deterministic run back to the set emits nothing and is on such a run; an absorbing pc region with no checkpoint is never reached. Not for segments with device reads or enabled interrupts. lc ok; propext, Quot.sound.
…ail, panic_bounds_check, panic_fmt and the rust_begin_unwind loop never return 90 kernel-checked facts; next-pc lemmas per instruction kind from DetStep alone; generated step-closure proof (tools/gen_panic_region.py). With reach_on_runs: checkpoint runs ending off the panic path => no reachable machine at a panic pc, using only run endpoints. Map/roadmap: both session gaps do UART I/O, which these lemmas do not cover yet. lc ok; propext, Quot.sound.
…each_no_escape, lands_seq, lands_of_qrun) and panic avoidance with device I/O (lands_panic, reach_no_panic_io) Lands P m: every Step behaviour from m (every oracle, so any device-read value; device writes emitted as events) reaches a checkpoint; at each node the machine is Quiet and faults under no oracle (per-node obligations, proved where used). Reach from checkpoints rooted in such trees never escapes and never reaches a panic pc. Next-pc lemmas generalized from DetStep to any successful stepInstr; rg_ok generated. lc ok; propext, Quot.sound; word scan clean.
…om_none, lands_of_qrun_lands); UART receive poll facts and segments (RxFetch, RxSegs) lands_lbu_dev: an lbu from a readable byte-wide device register outside RAM and the image faults under no oracle, and its successors are exactly one per value the device may return. 24 facts for the receive poll 0x80004374..0x800043a8 and assert_offset; 6 generated segments between the two device reads. Clean rebuild from source of all 58 dependent modules (Theories, image, memmove, Cobs, Deframer, Reach/Trees/Panic): 534 s, leanchecker ok on all; the .lake cache had stale Logic/Absint/AbsintSound oleans, which earlier /dev/shm checks loaded; nothing changed under the fresh ones.
…ery behaviour from 0x80004374 reaches 0x800043a8 Induction over cap - i through assert_offset, the LSR read node, the RBR read node and the byte store, via Lands trees: never faults, never takes an interrupt, i <= cap, registers outside ra/s0/s1/a0-a2 kept, RAM changed only in buf[dst..dst+cap) and assert_offset's stack byte. Explicit RxEnv preconditions (UART RBR/LSR addresses in s3/s5, read from the Uart16550 struct: assumed). No CopyContract. 3.8 s; leanchecker ok; standard axioms; word scan clean.
…ion, alignment); CopyContract discharged (copy_contract); deframer methods and session steps unconditional Peer files from 60d2f96..89ab0a6 (Projects/rmk: Copy, Merge, MemmoveMis*, MemmoveBwd*, MemmoveFull, gen_path, check_rmk, test_controls, results). Deframer/CopyDischarge.lean: CopyEnv -> PreM field by field (frame/separation from the 48-byte frame; no size bound needed), PostF = CopyPost; tail_contract, park_contract, unpark_contract, next_contract, recv_step', unpark_step'. Fresh source build of 74 modules (786 s), leanchecker ok on all, standard axioms; word scan clean.
…); recv_step None outcome exports the read-poll inputs None outcome now also gives: s2 = buffer + filled, s4 = 488 - filled (tail's result), discarding <= 1, s9 = discarding, s5/s8 = consumed/filled before tail (difference = filled), s3 = the word at 0x8002a784 (the Uart16550 pointer) from the entry RAM. Dependents recompile; leanchecker ok.
… generated segments (discarding / nothing pending / full exits, future state stores, Uart16550 register addresses, filled += n and back to the loop head)
…viour (every UART value) returns to the loop head with SessPre (filled += n <= 488) or stops at an explicit read-future boundary (0x80003ff2 / 0x80004428) NoneAt's explicit assumptions: the Uart16550 struct (base at +0x1c, stride 1 at +0x20), outside the future-state words; the task flag pointer at sp+0x24 in RAM outside the deframer; 0x28 stack bytes above sp. RxOut now records Quiet. Composes nGo1/nGo2, rx_loop (via lands_seq), nZero/nCommit. leanchecker ok; standard axioms.
…struct/flag/stack extras; none_of_recv derives NoneAt; session_round: SessInv => Lands1 to loop head with SessInv or explicit boundaries (read future 0x80003ff2/0x80004428, Some point 0x80003e70); unpark_round back to the loop head with SessInv. none_step now carries its RAM frame (NoneQ/NW). Initialization, dispatch/response and executor/Quiet across polls not proved.
…ation, Some gap, executor still open
…header goes straight to the unpark site and back to the loop head with SessInv. ParkPost.hdisc (park keeps the discarding byte); recv_step Some outcome exports parked <= 484 and discarding <= 1; session_round's Some boundary now carries SomeAt; SomeFetch (103 facts 0x80003e70..0x80003fd8), SomeSegs generator. Dispatch/encode/send/executor not proved.
…n): DispatchContract / EncodeContract (Lands, ABI frame, Kept session cells; encode result tag 1 or len <= 7) are hypotheses only. some_round (hD hE, h26: s10 = 0x8002a7f0): from SomeAt every behaviour reaches the loop head with SessInv (empty response via the unpark site; slice-check panic not taken) or an explicit boundary: 0x80004204 Pending -> executor, 0x80003fa6 (0xff), 0x8000429e (send loop). SW widened to the poll's Some-path writes, Extras.spTop to sp+0x148; SomeSegs split into short segments with generated Csr lemmas. Fresh 80-module build 818 s, leanchecker ok.
…ot a hypothesis of some_round recv_step's RecvOut, none_step's NoneQ and unpark_step now export that x26 is kept (callee-saved in next/tail/park/unpark, written by no segment); extras_keep takes that equality. some_pos/some_round take only the two NAMED, undischarged contracts (DispatchContract, EncodeContract); SomeAt is unchanged in statement (s10 comes from SomeAt.ext). Whether SessInv, now including s10, holds when the task first reaches the loop head (initialization) is still open, as are dispatch/encode, the 0xff path, the send loop, and the executor / Quiet across polls. Fresh 80-module build 845 s ALL OK; leanchecker ok on Session, NonePath, SessionLoop, CopyDischarge, SessionInv, SomePath, SomeRound; axioms propext/Classical.choice/Quot.sound only.
`Uart16550<MmioBackend>::send_bytes` (0x800098a6) with its `assert_offset` calls: from SendEnv (struct base 0x10000000 / stride 1, buffer and 0x50-byte frame in RAM), every behaviour of the model, for every LSR/MCR/MSR value, reaches the return address with SendPost: quiet, sp and every callee-saved register, RAM changed only in [sp-0x50, sp), count 0 or 1..min(len,16). The THR stores are device-write events (new lands_sb_dev step lemma); the loop is by induction on the count. This is the transmit primitive under both the 0xff path's write_all future and the send loop; those callers are not proved yet. New: SendFetch (95 kernel-checked decode facts), SendSegs (generated by tools/gen_seg_send.py, regeneration byte-identical), SendBytes. Fresh build into a clean dir; leanchecker ok on all three; axioms propext/Classical.choice/Quot.sound only.
…und under the 07a17e5 contracts is vacuous; proposed DispEnv/EncEnv/Extras/SomeAt repairs with observed real layout; ownership (dispatch: main, encode: peer, send glue: exporter)
…US until EncEnv is repaired The peer refuted both 07a17e5 contracts (dispatch faults with service pointer word 0; encode_frame's buffer may alias Kept UART bytes). Dispatch side repaired with facts the session actually carries: - recv_step's Some outcome exports s9 = msgA (s7+0x1b1); SomeAt gains s9. - Extras gains svc ([0x8002a780] = 0x8002a4c0), tx ([0x8002a788] = 0x8002a1e4) with the TX struct's base/stride (0x8002a200/0x8002a204, needed by Uart.SendEnv), and the flag byte's separation from them; values observed on QEMU virt (monitor xp), stores at 0x80003da6..0x80003dae. - DispEnv gains svc, s9, the message, the non-negative header. DispatchContract now takes an explicit world predicate W (what dispatch dereferences beyond DispEnv; OPEN), and some_pos/some_round take W, hD, hE and WAt W m0. Kept gains the TX struct cells. - SomeWitness.lean: someAt_real / dispEnv_real (the repaired SomeAt/DispEnv hold at the observed layout) and svc_zero_not_someAt / svc_zero_not_dispEnv (the audit's counterexample is excluded). EncEnv is unchanged (peer owns encode_frame, interface in rmk/some-interfaces.md), so its refutation still applies and some_round remains vacuous. Initialization still open. Fresh 84-module build from this tree ALL OK 875 s; leanchecker ok on Session, SessionInv, SomePath, SomeRound, SomeWitness; axioms propext/Classical.choice/Quot.sound (witnesses: propext/Quot.sound).
… NAMED TopicsNewContract; memset proved - Init/Memset.lean memset_words PROVED: compiler_builtins memset word path (aligned dst, len >= 16 and a multiple of 4): returns, callee-saved kept, RAM changed only in [dst, dst+len). - Init/InitPath.lean init_round: from InitAt at 0x80003b38 (s6/s7, stack above the PubSub statics, the async fn's UART pointer arguments, flag pointer word 0x8002a7c9, both UART structs' base/stride), through the session-static stores, TopicSubscribers::new (NAMED, NOT proved: TopicsNewContract, frame = its struct, the PubSub statics, its 0x40 frame), memset(bufA, 0, 0x1e8) (proved) and the deframer reset, every behaviour reaches 0x80003e1a with SessInv (including s10, svc, tx). - Init/InitWitness.lean initAt_real: InitAt holds at the observed values. - tools/gen_seg.py: muldiv support (SendSegs/SomeSegs regeneration byte-identical); generators gen_seg_memset.py, gen_seg_init.py (byte-identical). Open: TopicsNewContract; that the first poll reaches InitAt; the encode contract; executor/Quiet. Fresh build of the 7 modules on the clean 84-module tree; leanchecker ok; std axioms.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.