Agent
GuestAddrs.lean is generated and high-churn: every linked layout change can rewrite it. Its import graph is deliberately wide (186 direct importers in the #12068 measurement), but importer count is not the defect and is not the success metric. Codegen.Layout is the useful contrast: it has more importers (332) but only…
Agent
On 2026-08-02, the hourly Lake artifact-cache eviction job had been failing for weeks while appearing to be installed correctly. The crontab entry was present, the script was executable, and the cache path was valid. The failure happened before argument parsing because the script tried to locate lake through PATH…
Agent
Guest layout changes regenerate GuestAddrs and linked address facts. A Lean file importing either one is rebuilt, together with every proof bundled in that file. This note records the safe split rule for keeping genuinely layout-independent proof content out of that rebuild cone.
Agent
For any change that moves the guest memory layout (arena capacities, section bases, row strides). Written after GH #10836 / PR #10878, whose CI caught a pin casualty the local build never saw.
Agent
Current shipped slice #10520 routes MTx direct precompiles through the shared scalar kernel. It is fault removal, not FR clearance: exact-parent A/B attributed 22670 and 22671 FAULT-to-OK; post-rebase shipping sweep measured FA=0, FR=68, FAULT=0. Reclassify (iff bar, 2026-08-15): those FR=68 are not "acceptable…
Agent
The output address (0xa0010000) is not a single ABI. Claims on offsets are meaningful only with the build unit that emits them. In particular, a bare "highest output offset" is not an allocation boundary.
Agent
The single entry point for turning one unverified guest routine into a verified, deployed one. Follow it top to bottom; every step points at ONE exemplar to copy and ONE reference section for trouble. Do not read the long docs end-to-end — this page routes you to the paragraph you need.
Agent
Moved out of AGENTS.md to keep the agent guide compact. Load this when a proof you are writing hits one of these symptoms; do not read end-to-end.
Agent
Status: LATENT (measured). The defect fires on every failing post-preparation transaction and is unobservable in the post-state. This gate pins the mechanism so an unrelated change cannot silently make it live.
Agent
Audience: the agent reviewing any PR in this repo. The review's job is NOT to re-run CI (it runs build, tactic/TCB scans, axiom audit of registered witnesses, layering, region-map, etc. — full list in docs/agents/roadmap-4ch8f.md §3). The review's job is (a) the gates CI does not run, and (b) adversarial reading of…
Agent
Audience: the agent (any capability tier) picking up the next bead of epic evm-asm-4ch8f. This page is the map; it tells you which bead to pick, which recipe applies, which gates you must run, and where every load-bearing definition lives. Read it top-to-bottom once; afterwards jump via §7.
Agent
What this is. An independent verification of the P2 "core migration done" hand-off (sail-phase3-bootstrap.md), run against the actual repo rather than the bootstrap's prose. Every claim below is backed by a command run this session. TL;DR: the migration is real and green, but three trust claims are overstated and two…
Agent
For: the next session. Goal: turn the 11 conditional MemProofs sailequiv lemmas (each assumes hexec) into lemmas proven from a concrete bare-mode precondition bundle, by writing the layered vmemread/write reduction the original authors deferred. This is the largest remaining tier of the P4 consolidated theorem.
Agent
For: the next session. Goal of P1: prove out scoped Lean generation for the zkVM RISC-V target on a throwaway branch, produce a go/no-go report, and hand P2 a validated SAILMODULES + config + version triple. No changes to the main project in P1.
Agent
For: the next session. Goal of P2: vendor the (now-proven) current-upstream scoped RV64IM Lean model into evm-asm, build it in-project, drop the moving dhsorens fork, and re-establish the 51 sailequiv lemmas against it.
Agent
For: the next session. Context: P2's core migration is DONE and green (see sail-phase2-bootstrap.md). The project builds against the vendored, release-pinned, scoped RV64IM model (require out from "vendor/sail-riscv-zkvm-lean"); dhsorens is gone from the build; all 51 sailequiv lemmas pass; full lake build EvmAsm =…
Agent
For: the next session. Supersedes the ordering in sail-phase3-bootstrap.md (whose "start with P4" was corrected by the review, and whose item-0 trust-hygiene is now done). Read sail-adversarial-review.md first — it is the evidence base for why the P4 exit criterion below is what it is.
Agent
Verdict: 🟢 GO — proven end-to-end. The current-upstream model generates AND builds, patch-free, on the project's toolchain: Sail 0.20.2 (built on OCaml ≥5.2) generates the scoped model (113 files); that model + external lean-sail v4 builds on the project's lean4 v4.30.0-rc1 — lake build 84/84 jobs, exit 0, including…
Agent
Date: 2026-06-29. Scope: the unconditional ldsailequiv discharge in EvmAsm/Rv64/SailEquiv/VmemReduction.lean (+ SailStepAttr.lean; MemProofs.lean placeholder removal). Independent read-only adversarial pass. Build green (2987/2987).
Agent
For: the next session. Status going in: Tier A (LD, doubleword) is DONE — ldsailequiv is now an unconditional theorem (no hexec), committed e34e4b918 on feat/sail-zkvm-integration. Build lake build EvmAsm = 2987/2987, exit 0, sorry-free, no nativedecide/bvdecide.
Agent
This is the pre-wiring evidence ledger for the bounded, fixed-allocation post-state MPT builder. The builder is temporarily routed only on the unmerged validation branch; no production wiring claim exists until every row marked required has a clean-build result and the routed full-guest evidence below exists.
Agent
Load when: a fix touches guest state/gas semantics and you have a choice between mirroring execution-specs and patching the guest's own reconstruction; or when a fix would break a formal proof; or when you are about to add guest state that has "no obvious spec counterpart." This page is the why behind several Critical…
Agent
Load when: you are about to declare a guest routine or family "done"; you are changing a decoder, encoder, or validator that has an execution-specs counterpart; or you are starting a correspondence audit for a new family.
Agent
Scoping document for bead evm-asm-s1d19 (P0): replace SpecRef's placeholder executeAlwaysOk with a real ExecutionSeam, so that verifystatelessnewpayload's successfulvalidation verdict matches execution-specs @ bd8c673 ([email protected]) on every fixture — including the 974 succ=0 EEST fixtures where SpecRef…