[reaperhulk]

Trust change (lean/VerifiedGarbage/TCB/). It adds a property and a check, and weakens no model, contract or Verified. Nothing proves the property yet: every x86-64 function is on the allowlist, so the generated code does not change.

The property

TCB/X86_64/Residue.lean defines NoResidue c k retBits. Like ConstantTime, it is a property of two runs. Take any two runs of c from states that:

• satisfy k.pre,
• agree on what k.pub says is public,
• agree on everything outside the buffers (Outside 0).

They end in states that agree on everything outside the buffers but the result (Outside retBits). "Everything outside the buffers" means:

• every general-purpose register, and the flags;
• every vector register, including the upper halves of ymm/zmm and zmm16–zmm31;
• MXCSR;
• every byte of memory outside the regions the function may read or write, in particular the stack below the caller's stack pointer, where the function's frames and return addresses were.

So what the function leaves where its Rust caller cannot clear it depends only on what the caller left there and on public data. Clearing a location and leaving its entry value are equally fine; no choice can carry a secret.

What was there on entry is taken as given: a secret the caller left in a register is the caller's. So are the return addresses the code's calls push (State.unknowns), which are code addresses.

Not covered, because the model does not have them:

• the opmask register k1;
• the parity and adjust flags;
• microarchitectural state.

The enforcement

• Target.noResidue (TCB/Artifact.lean) is what a target means by the property: some NoResidue on x86-64, none elsewhere.

• Artifact.residue and Registration.residue (TCB/Registration.lean) carry an optional proof of it for the artifact's code, contract and result width. None is possible on a target that does not define the property.

• The emitter (Rust.checkResidue, run by Emit.run) refuses:

  • an artifact of such a target that has no proof, unless ci/residue_allowlist.txt lists it;
  • in a full run (--part, which has all of a target's artifacts), a listed function that has a proof or no longer exists.

  Converting a function therefore removes its line, and every problem is reported at once.

• The generated documentation of a function that proves it, and of a dispatcher all of whose implementations do, says so (Rust.residueDoc).

A follow-up PR adds the framework that proves the property (a residue analysis, and a verified scrub of what it finds), the first conversions, and a CI check that the list only shrinks. Until then, a new x86-64 function gets a line, which the emitter requires.

Review

What to read:

• TCB/X86_64/Residue.lean (60 lines): Outside and NoResidue.
• In TCB/Artifact.lean: the new Target field. Contract moved above Target, unchanged, since the field's type uses it.
• In TCB/Registration.lean: the two residue fields and Api.artifact passing it.
• In TCB/Rust.lean: parseResidueAllowlist, checkResidue and residueDoc.
• In TCB/Emit.lean: the call in run.

Changing Target rebuilds every Lean module once.

Checks

Locally, on the commit before its rebase onto #4678 (which touched only PPC64LE in TCB/):

• lake build, Emit.lean (every x86-64 function listed; no generated file changes), the Static checks job, check_lean_public_imports.py: pass.
• cargo test with Wycheproof: pass.

The rebase dropped 10 lines for AES-GCM-SIV variants main removed since.

No benchmark: no generated code changes.

---

Generated by Claude Code

[github-actions]

This pull request has conflicts with main, found after e4c4e66 landed on main: rebase it to resolve them. Before rebasing, see CLAUDE.md on checking how much Lean main changed, and on restacking a stacked pull request.

_{Posted by .github/workflows/conflicts.yml, once per push to a conflicting pull request.}