Notes from a Claude review

[gaynor-anthropic]

The kernel can be switched off, and nothing replays

import VerifiedGarbage.TCB.Axioms
set_option debug.skipKernelTC true in
theorem bad : False := by decide +kernel
#assert_standard_axioms bad
With the lakefile's options, lake build exits 0 and prints "bad depends only on the standard axioms []". Both ci/check_lean_*.py scripts exit 0. The same works through run_cmd … addDecl with no set_option in the text, and it was carried through the real registry to ship wrong code.

This looks like the likeliest accident for an LLM author. CLAUDE.md says the kernel was most of the build time and forbids raising limits, and this option is on no list.

Fix, one CI line: lake env leanchecker VerifiedGarbage. It ships in the 4.34.1 toolchain and refuses both forms. On the honest tree it exits 0 in 97 s with a 24 GB peak at 8 threads, or 166 s and 14 GB at 4.

The emitter runs compiled code, which need not equal the proved term

def addFast : Prog isa := .block [.mov .rax (.reg .rdi), .alu .sub .rax (.reg .rsi)]

@[implemented_by addFast]
def add : Prog isa := .block [.mov .rax (.reg .rdi), .alu .add .rax (.reg .rsi)]
No proof is touched. After the author regenerates src/asm, lake build, Emit.lean --check and both lints exit 0, the audit reports the three standard axioms, and selftest.rs holds sub rax, rsi. The kernel sees the honest definition while the emitter runs the substitute.

The unit test in src/lib.rs would catch this crude case. A subtler swap might pass. @[csimp] on an axiom outside the audited closure does the same to Rust.files itself.

Fix: refuse implemented_by, extern, export, csimp and init entries in the project's compiled modules. That is nine lines of the prototype below. One honest implemented_by exists, under Proof/Framework/Taint.

Nothing ties an entry's contract and sig to Spec/, or to each other

A namespace is not a directory. A Proof/ file may declare VG.Spec.X.fooContract with postcondition True, and the entry reads as if it came from Spec/.
Artifact.sig and .contract are separate fields. Lean and the emitter accepted a pair with swapped arguments and a shorter buffer. All 69 shipped entries pair up correctly.
Fix that removes trusted text: let Artifact hold pre, post, stack and leak, and compute contract := sig.contract target.abi ….

doc is hand-kept prose that must match contract.pre

It is 785 lines, 230 of them safety bullets. Deleting the scratch bullet from vg_sha256_compress passes everything. None of the 48 docs on 64-bit targets states the derived no-wrap clause, and all 21 on 32-bit targets do.

Fix: generate the bullets that are functions of sig, stack and writeArgs in TCB/Rust.lean, as featureDoc already does for CPU features. It would delete a large part of Artifacts.lean.

Endianness and pointer width are assumed and not enforced

rustCfg is target_arch = "aarch64", which also holds on aarch64_be and ILP32 targets (likewise x32 and armeb). The real crate compiles for aarch64_be and returns a wrong SHA-256 for "abc". ChaCha20 is right on both.

Fix: add target_endian = "little" and target_pointer_width to rustCfg, or two compile_error! lines.

[alex]

One PR per finding (the second and third share one):

1. Kernel can be switched off: CI: replay every declaration through the kernel with leanchecker #245 adds lake env leanchecker VerifiedGarbage to CI, plus a lint against debug.skipKernelTC. Both of the issue's forms (set_option and a run_cmd … addDecl) are rejected. The CI step first removes cached .oleans of deleted modules, which leanchecker otherwise replays and fails on.
2. Emitter runs compiled code and 3. contract/sig not tied to Spec/: TCB: the emitter audits that its compiled code is what the kernel checked, and where Spec names come from #246 (merged). #assert_no_compiler_overrides all run refuses implemented_by/extern/export on anything of the project that the artifacts or run use, transitively, and any csimp or initialize in a project module. That leaves the taint_decide tactic's unsafe term alone, since the emitter never runs it. #assert_spec_origin refuses a VG.Spec definition declared outside Spec/. The sig/contract pairing was already enforced by Artifact.ofSig: a swapped, shorter-buffer sig fails to elaborate.
3. Hand-kept safety prose: TCB: generate what memory each buffer must be valid for in the Safety docs #252. The emitter now generates each buffer's "must be valid for … bytes" item from the signature (Sig.validDoc), and rejects docs that state it themselves. The overlap and no-wrap items were already generated on every target by Sig.layoutDoc.
4. Endianness and pointer width: TCB: compile the assembly only on little-endian targets with the ABI's pointer width #248. src/asm/mod.rs gates each target on target_endian = "little" and the ABI's pointer width, and src/lib.rs has a compile_error! for aarch64_be, x32 and the like.

---

Generated by Claude Code

[alex]

Closing as complete. Where each finding ended up:

1. Kernel can be switched off: not addressed, by decision. CI: replay every declaration through the kernel with leanchecker #245 added a full leanchecker replay, but it cost ~7.5 minutes per CI run and was reverted in Revert "CI: replay every declaration through the kernel with leanchecker (#245)" #253. The only thing a replay adds beyond a lint is protection against deliberately adversarial proof code, which is out of scope here.
2. Emitter runs compiled code: fixed in TCB: the emitter audits that its compiled code is what the kernel checked, and where Spec names come from #246 (#assert_no_compiler_overrides).
3. Contract and sig not tied to Spec/: fixed in TCB: the emitter audits that its compiled code is what the kernel checked, and where Spec names come from #246 (#assert_spec_origin). The sig/contract pairing was already enforced by Artifact.ofSig.
4. Hand-kept safety prose: fixed in TCB: generate what memory each buffer must be valid for in the Safety docs #252. Each buffer's "must be valid for" item is generated from the signature, and the overlap and no-wrap items were already generated by Sig.layoutDoc.
5. Endianness and pointer width: fixed in TCB: compile the assembly only on little-endian targets with the ABI's pointer width #248, with per-target rustCfg and a compile_error! for aarch64_be, armeb, x32 and aarch64 ILP32.

---

Generated by Claude Code