saymrwulf/pasta-pallas-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/pasta-pallas-verified.git synced 2026-09-03 19:53:39 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
pasta-pallas-verified/TRUSTED-BASE.md
mrwulf f13707254f docs: estate-wide consistency pass (workflow audit, 36 findings, all verified before fixing) 
Nine parallel readers audited every doc against measured ground truth; every
finding was re-verified against the file before any edit, and the sweep fixed
by PROPERTY, not by flag — wording the readers caught in one repo was hunted
in all siblings (the two-button README sentence existed in all four forks,
not the three flagged; likewise the cone-overclaim in TRUSTED-BASE item 1).

This repo: see the diff. Records were not rewritten; clarifications are
dated. Doc-only except where noted in the estate summary; every gated doc
change was followed by a green button run.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-07 16:00:54 +02:00

1.6 KiB
Raw Permalink Blame History

Trusted base

What you must believe for the theorems in this repository to transfer to the running Rust code. Everything else is machine-checked.

  1. Lean 4 kernel (v4.30.0-rc2) and its three foundational axioms [propext, Classical.choice, Quot.sound]. Three representative certificates (P_prime, sub_spec, INV_spec) are #print axioms-audited against exactly this list; the remaining foundation theorems are protected by the no-axiom-declaration grep over Proofs/ only, which is weaker — it does not audit their cones.
  2. mathlib (prebuilt oleans fetched by lake exe cache get).
  3. Charon + Aeneas (pinned 9dd7f23c / bf13c42e): the translation from Rust MIR to the Lean model is assumed faithful. The generated gen/ files are never edited (comments only); proofs are stated ABOUT them.
  4. External-function models (gen/*/FunsExternal.lean): Rust items that Aeneas cannot translate (constant-time subtle primitives, iterator plumbing, formatting) are axiomatized as opaque symbols. The axiom audit proves none of these axioms enters the dependency cone of any certificate, except where a model is explicitly listed below.
  5. u64 primitive helpers (adc/sbb/mac, if not translatable): where a helper must be modeled externally, its model is a definition with proven arithmetic content (not an opaque axiom), or an axiom provably outside every certificate cone. The axiom audit enforces this.
  6. Compilation of Rust to machine code (rustc backend) is out of scope, as is side-channel behaviour (timing, speculation). The proofs are about functional correctness at the MIR/LLBC level.