Agent
Measurement boundary (2026-08-11, origin/main at b068e565a). The current planning denominator is 973 definitions across 365 source files under Programs/ and Dispatch.lean, enumerated by python3 scripts/asmtoprogram.py coverage and its generated docs/4ch8f-asm-to-program-coverage.md report: 406 ALREADY-STRUCTURED, 140…
Agent
Registry of unverified EvmAsm/Codegen/Programs/ modules that still define RISC-V assembly-string probes but are linked into no zisk BuildUnit, so they are deadweight a future PR can git rm. The list is generated and reproducible by committed scripts/scandeadprobes.py (re-run it to refresh); entries are cross-checked…
Agent
Status: phase-2 design drafted; implementation is held for maintainer review. Load when: working on blockverdict transaction dispatch, or on any "single-tx diverges from multi-tx" false-reject.
Agent
Moved out of AGENTS.md to keep the agent guide compact. Load this when.
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.