WIP: saw-core-lean — SAWCore→Lean 4 backend#3214
Draft
septract wants to merge 115 commits intoGaloisInc:masterfrom
Draft
WIP: saw-core-lean — SAWCore→Lean 4 backend#3214septract wants to merge 115 commits intoGaloisInc:masterfrom
septract wants to merge 115 commits intoGaloisInc:masterfrom
Conversation
New private sublibrary mirroring saw-core-rocq per the design in saw-core-lean/doc/2026-04-22_lean-backend-design.md. Phase 0 covers the Lean 4 surface-syntax AST (Language.Lean.AST) and its pretty printer (Language.Lean.Pretty), smoke-tested against Lean 4.30.0-rc2. Translator, interpreter wiring, and the Lean-side support library follow in later phases. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds the minimal SAWCore Term -> Language.Lean.AST translator behind the write_lean_term entry point: - SAWCoreLean.Monad: trimmed mirror of SAWCoreRocq.Monad (TranslationError, TranslationConfiguration, runTranslationMonad). Drops vectorModule / monadicTranslation / postPreamble — Lean has native BitVec/Vector and no free-monad encoding is needed yet. - SAWCoreLean.Term: structural walker handling Sort, Pi, Lambda, App, Variable, and Constant (via short-name lookup with constantRenaming applied). All other term forms raise NotSupported. No shared-subterm lifting, no SpecialTreatment table, no module-walk support — those arrive with CryptolModule / SAWModule in later phases. - SAWCoreLean.Lean: translateTermAsDeclImports entry point plus a preamble listing the CryptolToLean support-library imports the generated output expects. A new saw-core-lean-smoketest test-suite exercises the translator on four synthetic terms without requiring a full saw binary; the Phase-0 flagship case \(x : Bool) -> x translates to 'def identity (x : Bool) : Bool := x' and elaborates cleanly under Lean 4.30.0-rc2. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds the write_lean_term command to the SAWScript interpreter, backed
by writeLeanTerm in saw-central.
- SAWCentral.Prover.Exporter: export writeLeanTerm /
leanTranslationConfiguration / writeLeanProp as Lean analogs of
writeRocqTerm / rocqTranslationConfiguration / writeRocqProp.
- SAWScript.Interpreter: add do_write_lean_term and a prim entry for
write_lean_term (no legacy alias — there's no prior name to
deprecate).
- saw.cabal: add saw:saw-core-lean to saw-central and saw-script
deps, mirroring where saw:saw-core-rocq sits.
Smoke-tested end-to-end: 'write_lean_term "idBool" [] [] "out.lean"
{{ \\(b : Bit) -> b }}' emits 'def idBool (b : Bool) : Bool := b',
which elaborates cleanly in Lean 4.30.0-rc2. The polymorphic
implRev{4,[8]} case also translates without error, using SAWCore
constant short names verbatim — proper Lean forms
(seq n a -> Vector a n, TCNum/NatPos/Bit0/One numerals) wait on the
Phase-1 SpecialTreatment table.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Introduces the Lean-side support library that generated output
imports. This is the first building block of Phase 1 per
saw-core-lean/doc/2026-04-22_lean-backend-design.md.
- lean/ is a Lake project pinned to leanprover/lean4:v4.29.1 (current
latest published stable).
- Module layout uses one namespace per file under CryptolToLean, not a
flat dump — preserves origin info and avoids cross-module name
clashes as more Cryptol modules are translated in later phases.
- Phase-1 stub contents:
* CryptolToLean.SAWCoreScaffolding.Bit := Bool
* CryptolToLean.SAWCoreVectors.Vec n a := Vector a n
* CryptolToLean.SAWCoreBitvectors.bitvector n := BitVec n
plus U8 / U16 / U32 / U64 aliases.
Bodies are deliberately thin; they fill in as the Haskell-side
SpecialTreatment table grows.
- Uses std only (no mathlib); revisit if a specific primitive forces
the call.
- SAWCoreLean.Lean preamble emits 'import CryptolToLean' plus 'open'
lines for each sub-namespace, so generated code can reference
primitives unqualified — mirrors how Rocq's 'Require Import' works.
End-to-end smoke: 'saw-lean-example/demo.saw' still translates
\(b : Bit) -> b to 'def idBool (b : Bool) : Bool := b', and the
emitted .lean now elaborates directly against the Lake project via
'lake env lean out/idBool.lean' with exit 0.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds the per-identifier treatment infrastructure that turns raw SAWCore constant references into the right Lean target — qualified, renamed, or macro-expanded. - SAWCoreLean.SpecialTreatment: mirrors SAWCoreRocq.SpecialTreatment (DefSiteTreatment / UseSiteTreatment / IdentSpecialTreatment, translateModuleName, findSpecialTreatment, mapsTo / rename / skip / replace combinators, escapeIdent). Adds a mapsToCore combinator for primitives that resolve in Lean's own prelude (no module prefix). The Prelude / Cryptol tables start with a minimal seed — Bool, Nat, Int, String, True, False, Eq, plus Bit / Vec / bitvector pointing at the handwritten support modules. - SAWCoreLean.Term: translateConstant and the App / asGlobalDef head case now dispatch through translateIdentWithArgs, which applies the UseSiteTreatment. UsePreserve qualifies with translateModuleName (so unseeded Prelude / Cryptol names land in CryptolToLean.SAWCorePrelude.* / CryptolToLean.CryptolPrimitivesForSAWCore.*, dangling until the Phase-2 generated preludes fill them in). No backwards-compat short-name fallback — matches the Rocq contract. - SAWCoreLean.Monad: new UnderAppliedMacro TranslationError variant for when a UseMacro entry is supplied with fewer arguments than its arity promises. - saw.cabal: saw-core-lean gains zenc dep (for Text.Encoding.Z used by escapeIdent) and exposes the new module. End-to-end: demo.saw's idBool.lean still elaborates cleanly; the implRev.lean output now uses fully qualified CryptolToLean.CryptolPrimitivesForSAWCore.seq / .TCNum / .NatPos / .Bit0 / .One names — correct per the contract, awaiting the Phase-2 generated preludes for the referenced modules to exist. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds UseMacro treatment entries for the SAWCore Nat / Pos
constructors (Zero, Succ, One, Bit0, Bit1, NatPos) and Cryptol's
TCNum Num-wrapper, plus Cryptol.seq -> Vec. Each macro collapses
when its input is already a Lean NatLit, falling back to a
qualified call otherwise.
Also maps Cryptol.seq to CryptolToLean.SAWCoreVectors.Vec with the
natural argument order (n first, then element type).
Fixes a related subtlety in the translator: 'applied' helper avoids
wrapping zero-arity results in 'Lean.App f []' so downstream macros
can pattern-match on bare 'NatLit' through nested applications.
Before: implRev4's type was
CryptolToLean.SAWCoreVectors.Vec
(CryptolToLean.SAWCorePrelude.Bit0
(CryptolToLean.SAWCorePrelude.Bit0 1))
(CryptolToLean.SAWCoreVectors.Vec
(CryptolToLean.SAWCorePrelude.Bit0
(CryptolToLean.SAWCorePrelude.Bit0
(CryptolToLean.SAWCorePrelude.Bit0 1)))
Bool)
After:
CryptolToLean.SAWCoreVectors.Vec 4
(CryptolToLean.SAWCoreVectors.Vec 8 Bool)
The only remaining dangling reference in implRev.lean is to
'implRev' itself — which needs constant-body translation, the final
big Phase-1 piece.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
When a SAWCore term references a constant with an ImportedName
(typically a Cryptol user-defined function lifted into SAWCore), the
translator now recursively translates the constant's body and emits
it as an auxiliary Lean def before the main output, mirroring the
Rocq translator's topLevelDeclarations handling.
- TranslationReader gains sawModuleMap so translateConstant can
resolve SAWCore names via requireNameInMap.
- TranslationState grows globalDeclarations + topLevelDeclarations
lists, with getNamesOfAllDeclarations as a dedup helper to avoid
translating the same constant twice.
- withTopTranslationState runs a sub-translation in a fresh local
scope (empty named environment + only reserved idents unavailable)
— bodies are closed, so no outer bindings should leak in.
- ResolvedDef with a body emits as a Lean def; ResolvedDef without
(axiom / primitive) emits as a Lean axiom.
- translateDefDoc / translateTermAsDeclImports / writeLeanTerm /
the smoke-test harness all thread ModuleMap through.
End-to-end on saw-lean-example's implRev{4,[8]}:
Before (just the bare reference):
def implRev4 : ... := implRev 4 (Vec 8 Bool)
After (peer body + use):
def implRev (n : ...) (a : Type) (xs : Vec n a) : Vec n a := ...
def implRev4 : ... := implRev 4 (Vec 8 Bool)
The emitted implRev body is a direct translation of the SAWCore
compilation of the Cryptol sequence comprehension, still referring
to many unmapped Cryptol primitives (ecAt, seqMap, tcSub, coerce,
seq_cong1, …). Those either land in the Phase-2 generated preludes
or get added to cryptolPreludeSpecialTreatmentMap as entries are
worked through.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds the offline_lean command to the SAWScript interpreter, mirroring offline_rocq. Each invocation emits one .lean file per goal containing both the translated Prop as 'def goal : Prop := ...' and a 'theorem goal_holds : goal := by sorry' stub — so the user can open the file in Lean and discharge the proof. - SAWCentral.Builtins: offline_lean :: FilePath -> ProofScript () — thin wrapper over writeLeanProp, parallels offline_rocq. - SAWCentral.Prover.Exporter: writeLeanProp now routes through translateGoalAsDeclImports (new) rather than reusing writeLeanTerm, so the theorem stub is appended. - SAWCoreLean.Lean: translateGoalAsDeclImports — same as translateTermAsDeclImports but ends with the by-sorry theorem. - SAWScript.Interpreter: do_offline_lean + prim 'offline_lean'. End-to-end: saw-lean-example/demo.saw now produces out/invol_prove0.lean and out/eq_spec_prove0.lean, each with translated goal Prop plus the by-sorry theorem stub. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Covers the three new commands (write_lean_sawcore_prelude, write_lean_cryptol_primitives_for_sawcore, write_lean_cryptol_module), the two new translator modules (SAWCoreLean.SAWModule, SAWCoreLean.CryptolModule), support-lib expansion sizing (Rocq 2728 LOC -> Lean ~510 LOC estimate thanks to native BitVec/Vector), and a phased 2A-2E sub-plan sized at ~1 week of focused work. Also catalogs the anticipated rough spots (recursion in Prelude.sawcore, universe polymorphism gaps in the current AST, Int vs. Cryptol Integer, dictionary-heavy Cryptol output) and open decisions to make (where generated preludes live in git, namespace scheme for user Cryptol modules, the skip list). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Addresses audit findings A2, A3, A4, A5, A6, A7, A8, B2, C1, C2.
Pretty.hs:
- App case now uses 'group (hang 2 (fillSep ...))' so long calls wrap
at the layout width instead of producing 1200-char one-liners. Pi
case similarly uses 'group (fillSep ...)'.
- Definition / Let build their headers by 'hsep' on a filtered list of
parts rather than '<+>' chaining through potentially-empty docs —
eliminates the double-space bug that showed up as 'def foo :=' and
'let x :=' when binders or type annotations were absent.
- Anonymous implicit pi binder renders as '{_ : ty}' not '{ty}' —
latter parses as a singleton-set literal in Lean.
- Drop the now-unused 'prettyMaybeTy' and 'prettyPiBinders' helpers.
SAWCoreLean.Lean:
- Drop the three 'open CryptolToLean.*' directives from the preamble.
The translator always emits fully-qualified names, so the opens
did nothing but reserve cosmetic space.
- translateGoalAsDeclImports had two extra hardlines between the goal
def and the theorem stub; reduced to one blank line.
SAWCoreLean.Term:
- translateDefDoc was using 'intersperse hardline' on top of each
prettyDecl's own trailing hardline, yielding two blank lines
between aux decls. Now just 'vcat (map prettyDecl ds)'.
SAWCoreLean.SpecialTreatment:
- 'Prelude.Eq' now uses the new 'mapsToCoreExpl' combinator ('@eq')
since Lean's 'Eq' takes its type parameter implicitly while SAWCore
supplies it explicitly. Without this, every translated 'Eq T x y'
would type-error once Phase 2 lands.
- Remove 'unwrapMacro'. The TCNum / NatPos entries it backed were
collapsing type-level wrappers into bare Nat literals, breaking the
Num vs Nat distinction ('seq : Num -> sort 0' can't accept a Nat).
Both now translate as ordinary qualified references; the Phase-2
generated prelude will provide them.
End-to-end impact on saw-lean-example:
- idBool.lean still elaborates cleanly against the Lake project.
- implRev.lean: 'TCNum 0 / TCNum (NatPos 4) / TCNum (NatPos 8)' now
appear as faithful qualified references instead of hollow literals,
and the previously ~1600-char body wraps across ~40 lines at
reasonable indentation.
- Blank-line hygiene tightened throughout.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Closes the type-discipline gap the audit flagged as blocker A1: the
translator now inspects each SAWCore binder's sort flags via
asSortWithFlags + sortFlagsToList, and for binders whose type carries
the isort flag injects an auxiliary '[Inh_a : Inhabited a]' instance
hypothesis. Mirrors the Rocq translator's BindTrans /
translateImplicitHyp path at saw-core-rocq/src/SAWCoreRocq/Term.hs:494-512.
- Language.Lean.AST: add 'Instance' BinderImplicity variant so we can
emit Lean's '[...]' typeclass binder syntax (needed so Lean's
instance search fills the Inhabited hypothesis at call sites —
a plain '{...}' implicit would require unification, which won't
find instances).
- Language.Lean.Pretty: 'Instance' binders print as '[...]'; for
anonymous instance pi binders use '[A] -> rest' (idiomatic Lean
typeclass-arg form).
- Language.Lean.SAWCoreScaffolding: re-export 'Inhabited' under the
CryptolToLean.SAWCoreScaffolding namespace so generated output's
qualified references resolve via 'import CryptolToLean'.
- SAWCoreLean.Term: BindTrans sum-type (Ident + type + auxiliary
instance hyps), bindTransToBinder / bindTransToPiBinder flatteners,
translateImplicitHyp that builds the Inhabited-applied-to-a-pi
hypothesis type, and a two-layer translateBinders (primed inner
version returns BindTrans; outer version concat-maps to Lean
binders for the non-Inhabited callers).
Impact: in saw-lean-example/out/implRev.lean, implRev's signature
now includes:
(n : ...Num) (a : Type) [Inh_a : ...Inhabited a] (xs : ...Vec n a)
idBool.lean is unchanged (Bool binders don't carry isort).
Also expands the smoke test (audit finding B6). Old SmokeTest.hs was
4 trivial cases printed to stdout; replaced with a tasty-hunit
harness of 17 assertion-based tests across three groups:
- Language.Lean.Pretty (12 tests: anonymous implicit pi, instance
pi, double-space regression guards on def / let, If / List /
StringLit / Tactic / IntLit / Ascription / ExplVar / Namespace)
- SAWCoreLean.Term (4 tests: idBool, Inhabited injection,
unqualified short-name behaviour, UnderAppliedMacro error path)
- SAWCoreLean.Lean.translateGoalAsDeclImports (1 test: verify the
by-sorry theorem stub is present with the right shape)
saw.cabal: add tasty + tasty-hunit as test-suite deps.
Design-doc §4 table: update the Let row to reflect that we emit
'let x := e; b' (audit finding E4) — the leading ';' form was a
deliberate Phase-0 choice but had drifted out of the doc.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Ports SAWCoreRocq.SAWModule to SAWCoreLean.SAWModule, adds the
translateSAWModule entry point in SAWCoreLean.Lean, and extends the
term-translation Reader with a 'currentModule :: Maybe ModuleName'
field so references within a module being emitted go unqualified
(Lean's namespace scope supplies the prefix).
- Language.Lean.AST: no changes.
- SAWCoreLean.Term:
* TranslationReader: add _currentModule.
* runTermTranslationMonad gains a 'Maybe ModuleName' argument and
separates the old single ident list into explicit 'globals' vs.
'localEnv' params — matches the Rocq signature so the
SAWModule walker can hand in both.
* translateIdentWithArgs: UsePreserve now emits unqualified when
the target module matches 'currentModule'; everything else stays
fully qualified.
* Add translateIdentToIdent (needed by translateCtor to learn a
constructor's Lean target name).
* Expose globalDeclarations / topLevelDeclarations lenses and
mkDefinition / translateParams / translatePiBinders for the
module walker.
* Single-term entry points thread 'Nothing' for currentModule —
no module context, so every Prelude/Cryptol reference qualifies.
- SAWCoreLean.SAWModule: new module (~210 lines, 1:1 with Rocq
modulo Lean AST names and the 'Lean' / 'Rocq' InjectCodeDecl
namespace tag). Handles TypeDecl (via translateDataType ->
InductiveDecl, with constructor-name qualification stripping),
DefDecl (via translateDef -> Definition/Axiom per DefQualifier),
and InjectCodeDecl (only 'Lean'-tagged code is injected).
- SAWCoreLean.Lean: translateSAWModule wraps moduleDecls in a
'namespace X ... end X' block using the translated module name.
Also adds moduleDeclName helper for skip-list lookups (to be
used by the Phase 2D Cryptol-module translator).
- saw.cabal: expose SAWCoreLean.SAWModule in the sublibrary.
Smoke test (all 17 pretty-printer, translator, and goal-emission
assertions) still green. Existing write_lean_term behaviour
unchanged — single-term mode passes 'Nothing' for currentModule,
so the no-module case behaves identically to before.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Wires write_lean_sawcore_prelude and write_lean_cryptol_primitives_for_sawcore
in saw-central's Exporter.hs (mirrors writeRocqSAWCorePrelude /
writeRocqCryptolPrimitivesForSAWCore), plus their interpreter prim
entries. Both run to completion against the real SAWCore sources:
- Prelude.sawcore (2628 lines) -> SAWCorePrelude.lean (4785 lines)
- Cryptol.sawcore (2180 lines) -> CryptolPrimitivesForSAWCore.lean (16643 lines)
Translator expansions needed to unblock the walk:
- FTermF now handles Recursor, ArrayValue, StringLit (not just Sort).
Recursor emits Foo.rec (Lean convention) instead of Foo_rect; the
ArrayValue bitvector-literal specialization from Rocq is deferred
(needs parameterized-utils machinery we can add later if output
noise calls for it).
- defaultIdentTarget helper centralizes 'this SAWCore ident's Lean
reference.' Two cases it handles that previously weren't:
* Constructors of inductive types live inside the type's Lean
namespace (MyData.ctor, not ctor alone). The translator now
consults resolveNameInMap to detect ResolvedCtor and prefixes
accordingly.
* Same for the 'explicit application' marker: SAWCore applies
datatype parameters to a constructor explicitly, but Lean's
auto-generated Foo.ctor takes them implicitly — so ctor uses
always emit with a leading @, forcing all args explicit.
- translateSAWModule uses Text.intercalate '.' moduleNamePieces for
its namespace header, not moduleNameText (which separates with ':').
SpecialTreatment: remove the Phase-1 Zero / Succ / One / Bit0 / Bit1
numeric-literal macros. They served to pretty-print small Nat
literals in standalone implRev.lean but they fire on *every*
reference, including the Prelude's own definitions of Succ etc.,
which then fail with UnderAppliedMacro when the definition introduces
Succ as a top-level constant without applying it. Phase 2 delivers
these definitions via the generated SAWCorePrelude.lean, so the
cosmetic workaround is no longer needed.
Smoke test: drop the under-applied-macro test (target was Bit0,
which no longer carries a macro treatment). 16/16 now green. The
drop is noted in-place so a future UseMacro entry can reinstate an
equivalent assertion.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Concrete issues surfaced by running write_lean_sawcore_prelude + write_lean_cryptol_primitives_for_sawcore on the real SAWCore sources and attempting 'lake env lean' on the output: 1. Lean rejects '.rec' in ordinary defs — needs 'noncomputable def'. 2. Lean core uses 'Eq.refl'/'Eq.symm'; SAWCore's 'Eq.Refl'/'Eq.Sym' need SpecialTreatment entries. 3. '_'/_''/_''' anonymous-binder suffixes are ugly; emit real anonymous pi binders where possible. 4. SAWCore 'Unit' constructor collides with Lean's 'Unit' type. 5. Some constructor applications still fail; needs investigation after (1) clears the cascade. 6. 'Sort' AST loses the universe level — extend to 'Sort (Maybe Nat)'. Each maps to a Phase-2C work item. Phase 2A + 2B landed cleanly; the walker runs end-to-end, producing 4.8K + 16.6K lines of Lean. Fixing these six classes is what turns that into something lake-buildable. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Closes 2C items 1-4 and 6 per the findings doc. Five of six audit
deltas; only the constructor-application investigation (2C-5) is
deferred to after regeneration.
2C-1 'noncomputable def' (audit finding 1):
- Language.Lean.AST: Definition gains a 'Noncomputable | Computable'
flag.
- Language.Lean.Pretty: emits 'noncomputable def' when set.
- SAWCoreLean.Term.mkDefinition{With}: Computable by default;
mkDefinitionWith lets callers override.
- SAWCoreLean.SAWModule.translateDef: NoQualifier defs emit as
Noncomputable — conservative over-approximation since the generator
has no body-walk to decide otherwise. Safe: the generated prelude
is for type-checking only, not execution.
- Smoketest call sites take the new flag.
2C-2 Eq.refl (audit finding 2):
- SpecialTreatment adds 'Refl' -> '@Eq.refl' (mapsToCoreExpl) so
SAWCore's @refl a x@ lines up with Lean's universe-polymorphic
@Eq.refl : {α} {a : α} -> a = a@.
2C-3 anonymous binder cleanup (audit finding 3):
- Remove '_' from reservedIdents. Lean accepts '_' as a binder name
in lambdas, let bindings, and pi binders ('fun _ => e', '(_ : A) ->
B'), so the previous '_' / '_'' / '_''' renaming chain was
unnecessary ugliness.
2C-4 UnitType (audit finding 4):
- SpecialTreatment maps Prelude.UnitType -> Lean core Unit and its
'Unit' constructor -> Lean's 'Unit.unit'. Avoids the name collision
between SAWCore's Unit constructor and Lean core's Unit type.
2C-6 universe levels (audit finding 6):
- Language.Lean.AST: Sort is now 'Prop | TypeLvl Integer' with a
'pattern Type = TypeLvl 0' bridge so existing call sites are
unchanged.
- Language.Lean.Pretty: emits 'Type', 'Type n' for level > 0.
- SAWCoreLean.Term.translateSort: keeps the Rocq-style collapse
(sort n -> Type) because a faithful 'Type n' emission trips the
many @sort 1@ vs 'Prop' impedance mismatches between SAWCore's Eq
family and Lean's core Eq. The AST support lands for future
targeted use; the default stays Rocq-compatible.
Scaffolding: Inhabited is now declared as a universe-polymorphic
class in CryptolToLean.SAWCoreScaffolding so the [Inh_a : Inhabited a]
injection on polymorphic defs elaborates even when SAWCore's
'isort' sits at a sort level above 0. An instance bridge from
_root_.Inhabited preserves the default Lean instances.
Impact on the first-run SAWCorePrelude.lean elaboration:
- Before 2C: hundreds of cascading errors, almost all rooted in the
'non-noncomputable invoking .rec' issue.
- After 2C (items 1-4, 6): ~100 errors, all concentrated in the
proof-heavy core of the Prelude (eq_cong, sym, trans, uip, coerce
variants) where SAWCore's 'sort 1' elaboration meets Lean's
Prop-valued Eq in ways that can't be reconciled without a case-by-
case SpecialTreatment 'DefReplace' realisation.
Pragmatic follow-up: the remaining errors all belong to the
'proof-only' slice of the Prelude that Cryptol programs never
actually exercise. A constantSkips list can silence them at
generation time; that's Phase 2C-5 work.
16/16 smoketest assertions still green.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Eliminates two cases where the translator quietly produced Lean output with different semantics from the SAWCore source. 1. 'bitvector n' in SAWCore is 'Vec n Bool' — a vector of booleans. The scaffolding previously aliased it to Lean's native 'BitVec n', which is semantically distinct (packed word vs. bit-list; indexing, equality, bitwise ops don't match). Fix: scaffolding now defines 'bitvector n := Vec n Bool', honest to SAWCore. Lean's BitVec ergonomics are given up — correct trade-off: a proof about 'Vec n Bool' that silently runs on 'BitVec n' proves the wrong thing. 2. Cryptol 'seq' has two cases: 'seq (TCNum n) a = Vec n a' and 'seq TCInf a = Stream a'. A prior SpecialTreatment entry mapped 'seq' -> 'Vec' unconditionally, collapsing the infinite-sequence case and quietly changing meaning. Entry removed; 'seq' now falls through to the generated Cryptol prelude, which case-splits via Num#rec1 as the source does. Also adds doc/2026-04-22_soundness.md: the discipline document. Top rule: soundness w.r.t. SAW semantics is the absolute top-level goal. Catalogs legitimate mapping patterns (precise equivalence, handwritten realization, explicit failure) vs. the one broken pattern (skip + no realization, which silently creates dangling references). Documents the known approximations (Eq's sort 1 vs Prop, Inhabited as a separate universe-polymorphic class, bitvector/BitVec now fixed). Lays out an audit checklist for adding new SpecialTreatment entries. Context: a prior pass of Phase 2C had added ~25 'skip' entries to silence the proof-heavy Prelude's elaboration errors (eq_cong, sym, trans, coerce__def family, etc.). On review, that was reverted — skip without a handwritten realization is a soundness hole that Lean's elaborator will only sometimes catch. The ~100 Lean errors from the auto-translated proof slice stay as loud failures; real Cryptol programs don't exercise those defs. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Full SAWCore -> Lean parity on demo.saw. After this commit, saw-lean-example/demo.saw produces five output files — idBool.lean, implRev.lean, Rev.lean, invol_prove0.lean, eq_spec_prove0.lean — analogous to saw-rocq-example's five .v files. - SAWCoreLean.CryptolModule (new, 64 lines): port of SAWCoreRocq.CryptolModule. Walks a CryptolModule's term map, translates each (name, term, type) triple as a Lean Definition, and registers the name in globalDeclarations so subsequent entries that reference it don't re-emit the body inline. - SAWCoreLean.Lean gains translateCryptolModule: wraps the translated defs in a 'namespace <name> ... end <name>' block. Also imports Language.Lean.Pretty to render the namespace decl. - SAWCentral.Prover.Exporter.writeLeanCryptolModule: the TopLevel action that loads a .cry file, resolves the Cryptol module structure, and routes through translateCryptolModule. Mirrors writeRocqCryptolModule 1:1. - SAWScript.Interpreter: do_write_lean_cryptol_module + 'prim write_lean_cryptol_module' entry. - saw.cabal: saw-core-lean gains 'cryptol' dep and 'cryptol-saw-core' sublib dep (needed for CryptolEnv / CryptolModule / TypedTerm). Exposes SAWCoreLean.CryptolModule. Output validation on rev.cry: Rev.lean emits two decls (specRev, implRev) inside 'namespace rev'. Elaborating it against the Lake support lib shows 18 unknown-identifier errors, all for generated-prelude names (CryptolPrimitivesForSAWCore.seq / .Num / .ecReverse / .ecEq etc., SAWCorePrelude.coerce). These are the expected Phase-2C gap — once the generated preludes land compilably, Rev.lean elaborates. Also adds '.tmp/' to .gitignore (used by audit-agent scratchpads). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Captures the sub-agent audit's findings on why the auto-translated
SAWCorePrelude.lean fails to elaborate. Key corrections to my
earlier diagnosis in 2026-04-22_soundness.md:
- The 'Eq/Prop universe gap' I conjectured isn't real — Lean 4's
Eq.rec is fully universe-polymorphic and accepts Prop motives.
- The real cause of ~60 errors is a translator bug: translateSort
collapses every SAWCore sort level to Type 0, so emitted wrappers
are monomorphic. Fix is to propagate universe levels (Phase 2C
item 6, extended).
- Two latent soundness bugs surfaced:
* Bool.rec arg order swapped (SAW True-first, Lean false-first)
— silent runtime wrongness on any Bool eliminator.
* Nat = Nat mapping: SAW binary-positive vs Lean unary. Loudly
fails today, but any cosmetic 'fix' would make it quietly wrong.
- Plus UnitType: Lean's Unit is abbrev PUnit.{1}, no Unit.rec exists.
Prioritized as P1-P5. Soundness-critical P1+P2 first, then P3 (Unit
cleanup), then the bigger P4 (universe polymorphism), then P5 (doc
correction).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Three audit findings, all soundness-critical or adjacent.
P1 (critical): remove the ('Nat', mapsToCore 'Nat') mapping. SAW's
Nat is 'Zero | NatPos Pos' (binary-positive); Lean's Nat is
'zero | succ Nat' (unary). They are structurally different types.
The mapping was a landmine — today it fails loudly because the
constructor names don't match, but any cosmetic 'fix' that renamed
them (Zero→zero, NatPos→succ) would silently change the semantics
of every Nat#rec elimination. Leave SAW's Nat as a native translated
inductive.
P2 (critical): SAW declares 'Bool { True; False }' (True first);
Lean 'Bool | false | true' (false first). Auto-translated iteDep /
ite use 'Bool.rec' with case args in SAW order, but Lean's Bool.rec
is in the opposite order — silently swaps the True and False
branches at every reduction.
Fix: new CryptolToLean/SAWCorePreludeExtra.lean with handwritten
iteDep, iteDep_True, iteDep_False, ite, ite_eq_iteDep that permute
the case arguments. Reduction rules close by rfl against Lean's
Bool.rec (verified in the file). SpecialTreatment adds mapsTo
entries pointing the SAWCore names at these realisations. The
generated output now shows 'Prelude::iteDep@core was skipped' at
def sites and 'CryptolToLean.SAWCorePreludeExtra.iteDep' at use
sites, preserving SAW semantics faithfully.
Audited the generated preludes for direct @Bool.rec or Bool.rec
calls — none exist; all Bool elimination goes through iteDep/ite.
P3: Lean's 'Unit' is 'abbrev PUnit.{1}' — no Unit.rec. My Phase-2C
mapping UnitType → Unit + Unit → Unit.unit made the translated
UnitType__rec emit '@Unit.rec', which doesn't resolve. Revert the
UnitType mapping (let SAW's UnitType translate as a native inductive
with an auto-generated .rec) and rename the 'Unit' constructor to
'TTUnit' via a regular rename treatment so it doesn't clash with
Lean core's Unit type at use sites.
Smoketest still green. Regenerated SAWCorePrelude.lean error count:
still at maxErrors cap (~100+) because the dominant group-1
universe-polymorphism errors stay until P4 lands — but the classes
of errors targeted by P1/P2/P3 (Nat name resolution, Unit.rec
missing) are gone.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Earlier draft proposed handwriting Prelude realisations for the subset of names the rev.cry demo touches, parking full-Prelude elaboration as a later phase. User flagged that: rev.cry is a driving use case, not a scope limit. The translator must handle arbitrary SAWCore input soundly, including the proof-heavy Prelude regions. This doc restates the actual problem: - SAWCore is cumulative (sort i <= sort j for i <= j). - Lean 4 is not. - Translating soundly requires explicit universe management in the emitted Lean. Catalogs what I've already tried (collapse to Type; per-def fresh universe vars) and what I don't yet know (exact root causes of the ~100 errors, Lean community practice, whether SAW scTypeOf can give us level info at emission time). Proposes: spawn a research agent to investigate, then design a real approach that handles arbitrary SAWCore. No scope-dodge. Branch saw-core-lean-p4-wip preserves the first-attempt infrastructure (AST + universe lists + translateSort recording) for reuse. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Captures the sub-agent's findings on how mathport, mathlib, and the Lean 4 ecosystem handle universe polymorphism in non-cumulative Lean 4. Key corrections to my P4 first-attempt framing: 1. Lean 4 non-cumulativity is kernel-baked (confirmed in installed toolchain source). No pragma restores it. 2. No prior structural Coq->Lean4 translator exists. SAWCore->Lean4 is new ground; no template to copy. 3. Mathport's pattern is the closest precedent: always emit 'mkConst name [explicit-level-list]' at call sites. My P4 attempt emitted bare '@foo' and hoped for inference — that's the known-brittle path. 4. Lean issue GaloisInc#2297 documents the 'max u v =?= max u ?v' unification weakness that likely explains our ~100 errors. The 'abbrev TypeMax' folklore workaround is an option. 5. PLift/ULift/PULift (Init.Prelude) are legitimate lifting operators; mathlib's Small/UnivLE are typeclass-based escape hatches. Actionable: reject the bare-@foo pattern, thread explicit levels via Pattern A (mathport's default), consider PULift wrapping for SAWCore sort-polymorphic types that genuinely need to cross universes. Complements 2026-04-22_universe-problem.md. The internal-errors agent is still running and will provide the other half. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Companion doc to 2026-04-22_universe-external-research.md. The
internal-errors sub-agent ran the P4-WIP-generated prelude through
Lean and categorized every error; the finding is that all 101
errors have one shared root cause (with minor variations), not a
fundamental impedance.
Root cause: translateSort in my P4-WIP names universe variables
by sort level ('u1' for every sort 1 occurrence), sharing one
Lean universe variable across all sort 1 binders in a def. But
Eq__rec's '(t : sort 1)' binder and its '(p : ... -> sort 1)'
motive-codomain need *independent* Lean universe variables —
when a caller's motive returns Prop (Sort 0) and the t arg is a
concrete type (Sort k > 0), they can't be the same variable.
Fix: each call to translateSort at a binder position allocates a
fresh universe variable. Sort 0 stays as concrete 'Type'. The
rule 'per binder-occurrence = fresh universe variable' is
conceptually simple and tracks how Rocq does it via implicit
polymorphism (just with explicit naming since Lean doesn't
auto-generalize).
Agent validated this with seven Lean probe files covering
Eq__rec, eq_cong, coerce__def, and the ite/iteDep support lib.
All elaborate cleanly under the proposed fix.
Secondary issue (Group C): our handwritten
SAWCorePreludeExtra.lean's iteDep/ite family is monomorphic at
'Type'. Callers pass 'Sort u'-valued motives; mismatch. Fix:
make the support defs universe-polymorphic via '.{u}'.
Effort estimate: 1-2 days, with the AST infrastructure from P4-WIP
reusable.
Combines with the external-research finding that Lean 4
non-cumulativity is kernel-baked and the mathport pattern
(explicit levels at every mkConst call site) is the correct
template. Our fix implements that template at the translateSort
level.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Incomplete attempt at making emitted Lean defs universe-polymorphic
so SAWCore 'sort 1' motives pass Lean's universe check. The approach
taken:
- Extend Language.Lean.AST.Sort with:
* SortVar String — 'Sort u', universe-polymorphic
* SortMax1Var String — 'Sort (max 1 u)', for inductive results
whose parameters use 'Sort u'.
- Thread universe-variable lists onto Definition, Axiom, and
Inductive in the AST.
- SAWCoreLean.Term: translateSort is now monadic, recording
encountered 'sort k' levels in TranslationState.universeVars.
sort 0 -> Type; sort k (k >= 1) -> Sort u{k}.
- SAWCoreLean.SAWModule: harvests the recorded universeVars per
def / inductive and emits them onto the Lean declaration's
universe-binder list.
What works:
- The AST/pretty-printer infrastructure is clean.
- Emitted preludes show 'def foo.{u1} (a : Sort u1) ...' and
'axiom fix.{u1} : ...' form.
- The 16 smoketest assertions still pass.
- Individual def declarations with clean universe signatures
(id, fix, sawLet, PairType, PairType1) now elaborate.
What doesn't yet work:
- Use-site universe instantiation. When a translated body calls
'Eq__rec t x motive ... y pf', Lean has to infer the universe of
the motive — but the caller's local universe variables and the
callee's universe variables aren't connected. Result: ~100
elaboration errors remain (identical count to pre-P4 because
different errors now, not because nothing improved).
- Inductive constructor universe constraints: 'inductive
PairType1.{u1} (a : Sort u1) ... : Sort (max 1 u1)' emits
structurally, but Lean then complains about constructor payload
universes vs. the inductive's result universe.
Parking reason:
The approach I took (fresh universe variable per sort level per
def) is a reasonable first approximation but doesn't solve the
cross-def use-site instantiation problem. A proper fix needs:
(a) A universe-resolution pass at the module level so all defs
agree on which u-variable corresponds to which SAWCore sort,
OR
(b) Emit '.{_}' wildcards at use sites and let Lean infer, OR
(c) Fundamentally different mechanism (explicit universe
arguments at every call site, Rocq-style cumulativity).
Before another attempt, a design pass is needed to pick one
approach and understand how Rocq sidesteps this entirely via
Coq's implicit universe polymorphism.
Branch: saw-core-lean-p4-wip. Base branch 'saw-core-lean' reverts
to the pre-P4 state (e4bd622) for now.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ives
Substantial progress on universe-polymorphic emission. The first
~2000 lines of the auto-translated SAWCorePrelude.lean (through
the pair/sum/list/Bool-theorem regions) now elaborate cleanly.
Errors now start at line 2001+ in the Nat-arithmetic and Vec
regions — separate investigation needed for those.
Core translator changes:
- translateSort: allocate a fresh universe variable per call for
each 'sort k ≥ 1' occurrence, not deduplicated by sort level.
Rationale: SAWCore's 'Eq__rec' has two independent 'sort 1'
binder occurrences (type param t, motive codomain) that need
separate Lean universe variables. Sharing one breaks when a
caller supplies 'Prop'-valued motive and 'Type'-valued type.
- mkDefinitionWith: post-emission universe-variable GC. The
type and body are translated separately and may each allocate
universe variables that get shadowed when Lambda binders hoist
into the 'def' signature. Walks the emitted Decl to collect
actually-referenced universe names and filters the declared
universe list to match, avoiding Lean's 'unused universe
parameter' error.
- mkDefinitionWith: when the body has fewer lambdas than the type
has pi binders (e.g. fstPairType1: 2 lambdas vs 3 pi binders),
strip the body lambdas' type annotations. Lean infers them from
the signature; keeping our annotations would reference separate
universe vars that Lean reports as unused.
AST / Pretty changes:
- Sort gains SortMax1Vars [String]: 'Sort (max 1 (max u v w))' for
inductives with multiple universe parameters. Single-var
degenerates to 'Sort (max 1 u)'; empty list degenerates to 'Type'.
Needed so 'PairType1 (a : Sort u) (b : Sort v) : ...' accepts
constructor payload at either u or v.
- SAWModule's inductive result sort: use SortMax1Vars over all
collected universe vars, not just the first.
- prettyUnivs emits comma-separated '.{u, v}' instead of
space-separated — Lean 4 rejects the space-separated form.
translateIdentWithArgs:
- 'UseRename' path now ctor-qualifies when emitting a renamed
constructor. SAWCore's UnitType has constructor Unit, which we
rename to TTUnit to avoid clash with Lean core's Unit type.
Without this fix, use sites emit bare 'TTUnit' but Lean scopes
constructors inside their inductive's namespace, so the actual
Lean name is 'UnitType.TTUnit' — now correctly emitted.
- Skip ctor-qualification when the rename target already contains
'.', so 'Eq -> Eq.refl' doesn't get mangled into 'Eq.Eq.refl'.
SAWCorePreludeExtra:
- iteDep / iteDep_True / iteDep_False / ite / ite_eq_iteDep all
universe-polymorphic via '.{u}'. Required so SAWCore callers
passing motives at arbitrary sorts elaborate. rfl reduction
proofs stay valid because Lean's Bool.rec is universe-poly.
Outstanding: ~100 errors remain in the second half of
SAWCorePrelude.lean (Nat-arithmetic, Vec, IsLeNat regions).
Needs separate investigation — likely further type-class or
constructor-parameter issues. 16/16 smoke tests pass.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
After P4 v2 (commit 795e0dd), 2000 of 4025 lines of auto-translated SAWCorePrelude.lean elaborate cleanly. Remaining ~100 errors all share one root cause: SAWCore's Prop <= Type cumulativity doesn't hold in Lean 4. Where SAWCore writes 'Either (IsLtNat m n) (IsLeNat n m)' with 'IsLtNat' and 'IsLeNat' at Prop, Lean expects 'Type' and rejects. The faithful-to-semantics fix is to emit 'PLift' wrappers at every application site where a Prop-typed argument meets a Type-expecting parameter. This is a separate investigation — ~1 additional day — that needs a type-directed pass comparing expected parameter types against translated argument types. Documented as P4 follow-up rather than rolled into 795e0dd so the substantial universe-handling progress can land cleanly. The soundness discipline forbids the alternative of collapsing SAWCore Prop to Lean Type — that would silently erase proof irrelevance. PLift insertion is the honest path. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Sub-agent report. Reframes the remaining P4 v2 errors and identifies
the sound fix with concrete probe validation. Headline corrections
to my preliminary plan:
1. Of 99 errors reported, only 17 are actually the Prop/Type gap.
The other 82 are two separate bugs:
- 68 are a Nat vs _root_.Nat name-resolution issue in
SAWCoreVectors.Vec (expects Lean's native Nat, but SAWCorePrelude
defines its own).
- 13 are the Lean reserved keyword 'at' — Prelude.at emits unquoted.
These are tracked as P6b and P6c; must not be conflated with P6.
2. Winning fix is NOT PLift insertion (the sketch I drafted in
p4-v2-status.md). It's Approach C: universe-polymorphize the
sort-0 inductives (Either.{u,v}, Maybe.{u}, PairType.{u,v}),
mirroring what P4 v2 already does for sort-1. Lean then infers
.{0,0} or .{1,1} at use sites automatically. Zero PLift
wrapping, no support-lib additions, no Coe tricks.
3. Key refinement: defs with multiple sort-0 binders linked by Eq
(like coerce__def) need a SINGLE shared universe across those
binders — not per-binder fresh. This is the one change from
naive P4 v2 logic.
4. Rejected alternatives (B: Coe instances; A: manual PLift with
downstream .down) probed and shown to have blocker limitations
on the translator's explicit-@-application form.
5. Rocq ground truth: Rocq emits Prop/Type literally with no
universe variables, relying on Coq's native cumulativity.
Lean doesn't have that, hence the need for polymorphization.
Effort estimate: 3-4 hours. Translator changes localized to a new
translateBinderType function + a Sort0Mode state flag. No
support-lib or pretty-printer changes.
Key probe files in .tmp/p6_probes/ (gitignored): C_final2.lean and
C_proveEqNat_full.lean validate the winning approach. A_*, B_* probes
validate the rejections.
Preserves the discipline: no SAWCore Prop -> Lean Type silent
collapse (would erase proof irrelevance); no skip lists; loud
failure where soundness can't be preserved.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Suggested by a Galois conversation: instead of emitting a
universe-polymorphic SAWCorePrelude.lean once and importing it
everywhere, specialize each user program's Prelude references at
the concrete type arguments and emit self-contained output per
program.
Rationale: Cryptol programs are monomorphic at the value level.
When a user writes implRev{4,[8]}, every 'sort 0' position in the
transitively-referenced Prelude defs resolves to a concrete type,
eliminating the universe-polymorphism impedance that Lean 4's
non-cumulativity creates.
This note is a de-risking exercise, not a commitment. Structured
as:
- Why the current polymorphic approach has stalled
- Why specialization plausibly avoids the impedance
- Where it could still fail (polymorphic user terms, output size,
residual polymorphism, recursion-through-specialization)
- Staged investigation plan before committing: enumerate
implRev4's dependencies; hand-specialize it; sketch translator
changes; only then implement
- What's preserved vs. demoted from existing work (P4 v2 universe
machinery stays but becomes fallback; generated prelude becomes
reference rather than deliverable)
Recommends Stage 1 (dependency enumeration, ~2h read-only) and
Stage 2 (hand-specialize implRev4, ~half day) before any
implementation. Stage 2's result is the single biggest de-risk.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Implements the translator changes sketched in
doc/2026-04-23_stage3-translator-sketch.md:
- writeLeanTerm / writeLeanProp / writeLeanCryptolModule run
scNormalize on the input before translation, with a fixed opaque
list covering Nat/Pos eliminator-heavy defs so the output stays
on the SpecialTreatment-mapped surface instead of unfolding into
binary-positive scaffolding.
- New handwritten CryptolToLean/SAWCorePrimitives.lean declares
axioms and inductives for the SAWCore primitives the Stage 1
dependency scan identified: Either, Num, Stream, Integer,
subNat/addNat, intSub/intNeg/intLe/natToInt/intToNat, gen,
atWithDefault, foldr, coerce, unsafeAssert, error. Universe-
polymorphic where the signature demands (unsafeAssert, error).
- SpecialTreatment wires each primitive and Nat/Pos constructor to
the right Lean-side target. Nat constructors use literal-collapse
(Zero -> 0, NatPos -> id, Bit0/Bit1 -> arithmetic helpers); the
non-literal fallback is a plain reference rather than a loud
error so polymorphic module translations still elaborate.
- polymorphismResidual on the residual type refuses binders at
sort k > 0 (decision D3). Plain Type-0 polymorphism is fine
(Cryptol's {a} binders translate as monomorphic Type params).
- translateSort reverts to its pre-P4 collapse (Prop for propSort,
Type 0 otherwise); the Stage 3 universe work stays on the WIP
branches.
- translateConstant's body-translation path for ImportedName is
removed — under specialization every surviving Constant resolves
via SpecialTreatment or falls through as a bare reference.
- translateDefDoc emits 'noncomputable def' unconditionally (every
SAW primitive we can emit is an axiom Lean's code generator
refuses to compile).
- CryptolModule.translateCryptolModule now actually returns the
user-facing Decl list (the old code threw it away and only kept
the auxiliary state).
- write_lean_sawcore_prelude and
write_lean_cryptol_primitives_for_sawcore are deleted along with
SAWCoreLean.SAWModule and translateSAWModule — dead code under
the new architecture.
All five saw-lean-example outputs (idBool, implRev, Rev,
invol_prove0, eq_spec_prove0) elaborate under 'lake env lean' with
only 'unused variable' warnings and the expected 'by sorry' stubs.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ranslation Option A from the deep-dive: make scNormalizeForLean iterate scNormalize to a fixed point. A single pass only unfolds constants whose unfolding triggers a beta/recursor reduction at the call site; constant-applied-to-variables forms (e.g. 'ecReverse n a xs') halt after one step, leaving dangling references in polymorphic Cryptol module output. Iterating unfolds one more layer each pass — SAWCore non-'fix' defs form a DAG so convergence is guaranteed — with a 100-iter safety bound. Supporting changes the polymorphic case surfaced: - SAWCorePrimitives.lean: add Stream (inductive, not axiom — has MkStream constructor), EmptyType (one-ctor Empty), RecordType (one-ctor RecordValue), foldl, and the missing int arithmetic (intAdd/intMul/intDiv/intMod/intEq). Make addNat/subNat reducible wrappers around Nat.add/Nat.sub so Lean can unify vector sizes like 'addNat 1 (subNat 10 0)' with literal '11'. - SpecialTreatment: mapsTo entries for Stream/MkStream/EmptyType/ Empty/RecordType/RecordValue and the int arithmetic set. Use mapsToExpl for constructors that take inductive type params explicitly in SAWCore. - Drop the 'isort' -> '[Inh_a : Inhabited a]' binder auto-injection. SAWCore's isort flag is an advisory about reachability; turning it into a positional Instance binder clashed with SAWCore's motive-positional recursor calls. No soundness loss (the flag wasn't used to justify any Lean-side reasoning). Wrapper becomes a pair of (Ident, Type) instead of carrying auxiliary instance args. - Recursor emission stays as '@Foo.rec' (explicit) — matches SAW's motive-first positional arg list. The rationale that previously argued against @ was the Inh_a auto-insertion path, which is gone. - CryptolModule.translateTypedTermMap emits 'noncomputable def' for Cryptol-module defs (same reasoning as translateDefDoc: any user term can transitively depend on the coerce/unsafeAssert/error axioms Lean's code generator refuses). All five saw-lean-example outputs (idBool 7 lines, implRev 298, Rev 4109, invol_prove0 1081, eq_spec_prove0 555) elaborate under 'lake env lean' with only unused-variable warnings and intended 'sorry' stubs. Smoketest suite still passes 16/16. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The two audit docs in doc/2026-04-24_audit-*.md flagged three
concrete soundness improvements:
1. Tighten 'error' from universe-polymorphic to non-Prop. The old
'error.{u} : (α : Sort u) → String → α' let a Lean user importing
the module write 'exact error False ""' to produce 'False'.
SAW's primitive is 'isort 1', forbidding Prop. We now use
'Sort (u+1)' — admits every non-Prop sort, blocks the attack.
2. Fail loudly on surviving Nat#rec / Pos#rec. Previously these
would emit '@Nat.rec' against Lean's auto-generated recursor
whose case order doesn't match SAW's; a user constructing such
a term saw an obscure Lean elaboration error instead of a
translator-level refusal. Term.hs now throws a new
'UnsoundRecursor' TranslationError when it sees a recursor over
Prelude.Nat or Prelude.Pos. (Probed by hand-constructing such
a term via 'parse_core' — it fails at saw-time with a clear
diagnostic.)
3. Extend 'leanOpaqueBuiltins' to cover every Prelude def whose
RHS uses Nat#rec or Pos#rec (per the audit list): leNat,
expNat, widthNat, divNat, modNat, pred, natCase, if0Nat,
Nat_cases, Nat__rec, Nat_cases2, doubleNat, BitM, posSub,
posEq, posLe, posLt, posExp, dblZ, AccessibleNat_all. Without
these, scNormalize would unfold them, surface their internal
recursors, and trigger the new loud-failure guard
unnecessarily.
Drive-by cleanup:
- Remove the 'CryptolToLean.SAWCoreScaffolding.Inhabited' class.
It was the target of the now-removed [Inh_a : Inhabited a]
auto-injection. Dormant, dead.
All 5 saw-lean-example outputs still elaborate (probe/Rev.lean
4109 lines, others unchanged in shape). 16/16 smoketests still
pass.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Update README and revised plan to reflect Slice B's closure (Phase 5d) — the blocker was a wrong zip axiom signature in our Lean support library, corrected in commit 9b27385. Popcount now translates and elaborates end-to-end; pinned in the integration suite.
SAW Prelude declares Float and Double as opaque types with mantissa-exponent constructors. Faithful Lean axioms matching Prelude.sawcore lines 2153-2165. Note: SAW's mkDouble at Prelude.sawcore:2163 is declared with return type Float (not Double). Possibly a SAW upstream typo, but the Lean axiom mirrors it exactly per the soundness-paramount rule (no silent corrections). Documented inline in SAWCorePrimitives.lean. If SAW fixes the upstream declaration our axiom should be updated to match. Coverage: Cryptol's surface 'Float e p' doesn't lower through these primitives — the cryptol-saw-core layer treats Cryptol Float operators as 'Unimplemented' and emits 'error UnitType "..."'. So our binding is exercised by parse_core / LLVM-extract paths, not by Cryptol Float surface code. The L-14 startup audit is the gate; smoketest pins that Float / Double / mkFloat / mkDouble are all covered (not in the unmapped-and-missing list). 44 smoketests + 22 integration tests pass.
Move the support library closer to Rocq's by adding the lemma shapes Rocq provides but we didn't yet. SAWCoreBitvectors_proofs additions (~80 LOC, ~20 new entries): - bvsmax / bvsmin / bvumax / bvumin constants — defined via gen - isBvsle / isBvslt / isBvule / isBvult Prop wrappers — defined as Bool-equation reflections - isBvX_def equivalences — Iff.rfl since the Prop wrappers unfold to the Bool eq by definition - Cross-comparison lemmas (axioms): isBvslt_to_isBvsle, isBvult_to_isBvule, isBvule_to_isBvult_or_eq, isBvslt_to_bvEq_false, isBvult_to_bvEq_false - Edge-case lemmas (axioms): isBvslt_antirefl, isBvsle_antisymm, not_isBvslt_bvsmin, not_isBvslt_bvsmax, isBvule_zero_n, isBvule_n_zero, isBvult_n_zero - Round-trip lemmas (axioms): bvNat_bvToNat_id, bvToNat_bvNat, bvToNat_bounds SAWCorePrelude_proofs additions: - mulNat_eq_natMul / minNat_eq_natMin / maxNat_eq_natMax / expNat_eq_natPow / pred_eq_natPred / doubleNat_eq — by rfl since these are reducible defs over Lean stdlib Each axiom matches Rocq's same-named lemma. Rocq proves via 'holds_for_bits_up_to_3' (exhaustive small-bit case analysis); we transport the conclusion. Same trust character as the existing bv axioms — SAW vouches for the semantics, we mirror. 44 smoketests + 22 integration tests pass.
Continued bringing the support library closer to Rocq parity. SAWCoreBitvectors_proofs (~110 LOC added, ~25 entries): - Successor/predecessor bv lemmas: isBvslt_to_isBvsle_suc, isBvult_to_isBvule_suc, isBvslt_pred_l, isBvsle_pred_l, isBvsle_suc_r, isBvslt_suc_r - Sign/unsigned bridge lemmas: isBvult_to_isBvslt_pos, isBvule_to_isBvsle_pos, bvule_to_bvslt_zero, bvule_to_zero_bvsle - Equality via subtraction: bvEq_bvSub_l, bvEq_bvSub_r - Boolean truth-table theorems: bool_beq_eq, bool_beq_neq, and_bool_eq_true/false, or_bool_eq_true/false, not_bool_eq_true/false (provable in Lean by cases <;> simp) SAWCorePreludeExtra: - iterNat / iter from CryptolPrimitivesForSAWCoreExtra.v — Cryptol's iterate-n-times pattern, paired with Num dispatch SAWCorePrelude_proofs: - min_nn / min_nSn / min_Snn — small min identities provable from Lean's Nat.min_self, Nat.min_eq_left/right, Nat.le_succ 44 smoketests + 22 integration tests pass.
User correction: 'Some of these lemmas seem like trivial properties of the Lean types. Surely that's not what you mean? you want to prove things about the local prelude definitions.' Two corrections: 1. Removed boolean truth-table theorems (bool_beq_eq, and_bool_eq_true, or_bool_eq_true, not_bool_eq_true, etc.). These were stated about Lean's standalone &&/||/\! operators — but SAW's Prelude.and / or / xor / not emit as ite Bool a b Bool.false-style chains in our translated output (per leanOpaqueBuiltins + L-16 wrapper routing). Lean's standalone && doesn't surface in user-facing SAW-translated goals, so theorems about it are Lean-stdlib trivia not actually useful for discharging SAW proofs. The iteDep_True / iteDep_False / ite_True / ite_False simp lemmas in SAWCorePreludeExtra already cover the SAW-emitted Bool-elim shape. Replaced with an inline note explaining the omission. 2. Restated min_nn / min_nSn / min_Snn in terms of SAW's minNat (the name the translator emits) rather than Lean's Nat.min. The proof reduces by rfl since minNat is a reducible alias, but the theorem's name and signature now match Rocq's intent and where users searching for 'minNat'-related rewrites would look. Same test suite still passes (44 + 22).
Audit per user request: prove meaningful properties of the SAW backend, not things that are trivial Lean-stdlib facts. Removed (SAWCoreBitvectors_proofs.lean): - not_not, and_comm, and_assoc, or_comm, or_assoc, and_or_distrib — Lean-stdlib Bool truth tables proven by 'cases <;> rfl'. These are properties of Lean's standalone Bool operators, but SAW's Prelude bool ops emit as 'ite Bool a b Bool.false' chains in our translated output (per leanOpaqueBuiltins + L-16 wrapper routing). Standalone Lean Bool ops do not surface in user-facing SAW-translated goals; the walkthrough proof confirms this by closing test_offline_lean.t2 (distributivity) via cases+rfl through iteDep reducibility, never using any of the deleted theorems. If a downstream user ever needs a raw Lean Bool fact, the stdlib has them under Bool.*. Reframed (SAWCorePrelude_proofs.lean): - The Nat-arithmetic alias section header now says 'convenience plumbing' rather than 'Rocq parity' or 'theorems about SAW behavior'. They are @[simp] entry points that rewrite SAW-named ops to their Lean stdlib equivalents — useful for proof ergonomics but not novel theorems. Mirrors Rocq's identical plumbing (addNat_add, mulNat_mul, etc.). Surviving theorems are substantive: Vector round-trips, fold reductions, Bool-Nat decision bridges, and the full bv axiom set (bvAdd / bvSub / bvNeg / bvXor / bvEq / isBvX / bvNat / bvToNat / bvule families). Those are the load-bearing 'Rocq parity' content. 44 smoketests + 22 integration tests pass.
Real-world exercise from exercises/functional-correctness/point/Point.cry — pinning end-to-end that we cover records + Cryptol Ring class dictionary (via 'zero') + property emission. ~150 lines of emitted Lean. 23 integration tests.
Mirrors otherTests/saw-core-rocq/test_cryptol_module_sha512.saw, which pins SAW's clean refusal of SHA-512's full functor (the parametric Merkle-Damgard chain over polymorphic message length L lowers to Prelude.fix over Cryptol::Num#rec1, which both backends refuse). For Lean: the L-5 lockdown's RejectedPrimitive fires; L-1's polymorphismResidual would also flag the L\@free Num residual. Pinned log.good captures the diagnostic shape so a regression that drops the rejection (or changes its wording in a way that breaks user-facing error messages) is caught. Lifting this is gated on a Phase 5 extension for the polymorphic Num#rec1 dispatch shape; documented inline in the .expect-fail. 24 integration tests now (was 23). Closes the last otherTests/saw-core-rocq parallel.
Convert ~80 opaque Lean axioms to definitions/theorems by routing
through Lean's native BitVec, Int, Rat, and Vector libraries.
Primitives (SAWCorePrimitives.lean):
- Add vecToBitVec/bitVecToVec converters between SAW's MSB-first
Vec n Bool and Lean's BitVec n.
- Replace ~25 bv-op axioms (bvAdd, bvSub, bvMul, bvNeg, bvUDiv,
bvURem, bvSDiv, bvSRem, bvShl, bvShr, bvSShr, bvNot, bvAnd, bvOr,
bvXor, bvEq, bv*lt/le/gt/ge, bvUExt, bvSExt, bvNat, bvToNat,
bvToInt, intToBv, sbvToInt) with noncomputable defs via BitVec.
- Define bvPopcount/bvCountLeadingZeros/bvCountTrailingZeros via
state-pair folds; bvLg2 via Nat.log2.
- Convert Integer ops to defs over Lean's Int. Use Int.fdiv/Int.fmod
to match SAW's concrete-simulator Haskell-div/mod (floor) semantics.
- Convert IntMod n to Int + Int.fmod, Rational to Lean's Rat,
Float/Double to Int x Int (faithful since SAW has no operations).
- Convert zip from axiom to Vector.ofFn with Nat.min bound proofs.
- Convert coerce from axiom to a def via Lean's cast (real
type-equality transport, sound).
- Add Inhabited instances for Stream, UnitType, EmptyType, PairType,
RecordType (data inductives with Inhabited-arg constructors).
- Fix bvsmin/bvsmax: previous defs assumed LSB-first but vecToBitVec
is MSB-first, making boundary axioms vacuously violable. Now route
through BitVec.intMin/intMax.
Add 2 SAW<->BitVec round-trip coherence axioms
(vecToBitVec_bitVecToVec, bitVecToVec_vecToBitVec); decidable per
width via 'by decide'.
Proof library (SAWCoreBitvectors_proofs.lean):
- Convert all ~30 axioms to theorems proven from BitVec lemmas plus
the 2 coherence axioms.
- Includes signed comparison + successor/predecessor + sign-bridge
lemmas (isBvslt_to_isBvsle_suc, isBvslt_pred_l, isBvsle_pred_l,
isBvsle_suc_r, isBvslt_suc_r, isBvult_to_isBvslt_pos,
isBvule_to_isBvsle_pos, bvule_to_bvslt_zero, bvule_to_zero_bvsle).
- Add toInt_eq_toNat_of_nonneg / _sub_of_neg helpers and
vecToBitVec_bvAdd / _bvSub / _intToBv routing helpers.
- Add Std.Tactic.BVDecide import (bv_decide proves these for any
fixed width; auditors can spot-check).
error.{u} investigation: tested tightening to
'def error (α : Sort (u+1)) [Inhabited α] (_ : String) : α := default'
matching SAW's isort 1, but Cryptol typeclass elaboration emits
'error <T> "invalid instance"' at potentially-uninhabited types
(e.g., Eq over Stream a) inside dead dictionary branches. SAW's
isort is advisory in practice. Reverted; documented in residual-trust
catalog.
Final axiom count in SAWCorePrimitives.lean: 4 (down from ~80).
- 2 Vec<->BitVec coherence (decidable per width)
- unsafeAssert (SAW-faithful intentional unsoundness, L-2 pinned)
- error.{u} (SAW-faithful intentional unsoundness, L-original pinned)
Verification: lake build passes, 44/44 smoketests, 24/24 integration
tests in otherTests/saw-core-lean (all .diff empty, no
.elaboration.fail), L-2/L-8/L-original soundness tests pass,
discharge proofs at intTests/test_lean_offline_proof_t1/3/4,
test_lean_recursion_stream_corec_proof, test_lean_walkthrough_proof
all close.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Phase 9 (axiom -> def conversions) substantially changed the proof-side experience: bv arithmetic now reduces, the BV theorem library is complete, and bv_decide is wired (via Std.Tactic.BVDecide import). The user-facing docs reflected the pre-Phase-9 state. - getting-started.md: refresh 'What works today, what doesn't' to reflect Phase 9. Document that bv arithmetic is now defined (concrete-input goals close by 'decide'), the theorem library in SAWCoreBitvectorsProofs covers symbolic identities, and Integer/Rat ops are reducible aliases over Lean natives. - doc/proof-cookbook.md (new): worked-examples companion with 8 patterns matching common Cryptol-emitted goal shapes, each with a tested discharge tactic. Tables of theorem names for bv arithmetic and signed predicates. - intTests/test_lean_proof_cookbook/ (new): pins the cookbook examples. If a future support-library change breaks any documented pattern, this test fails loud. Phase 7's first slice. Remaining: tactics for SAW-translated goals, more end-to-end discharge examples for symbolic-width bv properties, possibly a saw_simp meta-tactic. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Three macros packaged as CryptolToLean.Tactics, auto-imported via the root CryptolToLean module: - saw_bv: simp with every bv-op unfolded plus round-trip rewrites. Closes concrete-input goals, reduces symbolic goals to pure BitVec form. Replacement pattern for 'by decide' when decide stalls but simp can make progress. - saw_unfold: unfold the SAW-named bv primitives without closing. For inspection-before-manual-work. - saw_to_bitvec: saw_unfold + round-trip rewrites. Lifts a SAW- typed goal to a pure BitVec n goal so bv_decide / BitVec lemmas apply. Extended test_lean_proof_cookbook with saw_bv examples. Updated proof-cookbook.md with a 'convenience tactics' section + the saw_bv alternate in Pattern 1. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Stress-test plan (doc/2026-05-03_stress-test-plan.md) baseline example. Cryptol property \(x y : [8]) -> x + y == y + x; offline_lean emits the goal, intTests discharge closes it in 3 lines via bvAdd_comm + bvEq_refl. Pinned: - otherTests/saw-core-lean/test_offline_lean_stress.saw (driver) - otherTests/saw-core-lean/test_offline_lean_stress.log.good - otherTests/saw-core-lean/test_offline_lean_stress.E1_prove0.lean.good - intTests/test_lean_E1_bvAdd_comm_proof/ (discharge) Baseline is clean: standard import + open, three tactic lines. Ready for E2. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Cryptol property \(b : Bit) (x y : [8]) -> (if b then x else y) == (if b then x else y). Both sides syntactically identical in the emitted goal, so bvEq_refl closes it without touching the iteDep wrapper. Two tactic lines. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Cryptol property \(p1 p2 : Point) -> point_add p1 p2 == point_add p2 p1
where Point = { x : [32], y : [32] } and point_add adds fieldwise.
Exercises RecordType.rec reduction on two-field records. The
emitted goal has ~80 lines of RecordType.rec projections; after
`obtain \<x, y\> := p` these reduce to .1 / .2 accesses.
Discharge: 5 tactic lines total (intro + 2 obtains + 2 rws +
simp [bvEq_refl]). Clean — no support-library changes needed.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Cryptol property \(xs : [4][32]) -> map (\x -> x + 0) xs == xs. Discharge (8 lines): - simp only [bvAdd_id_r] — remove the +0 - rw [gen_atWithDefault] — gen-of-at-id-index round-trip - construct hgen for pointwise bvEq_refl (simp can't do this automatically because bvEq_refl's RHS has a metavariable) - simp only [hgen]; decide — fold of all-trues at size 4 BUG FOUND: all intTests/test_lean_*_proof/test.sh scripts accepted proofs that elaborated with `sorry`. The grep was for 'error' only, not for 'declaration uses sorry' warnings. This silently masked incomplete proofs. Fix: added an additional grep for 'declaration uses `sorry`' in test.sh; propagated to all 9 lean-proof test dirs. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Previously every intTests/test_lean_*/test.sh directory carried
its own copy of a 52-line / 75-line bash harness with subtle
per-dir variations. Duplication invited drift; in particular the
sorry-detection fix (E4 commit) had to be propagated across 10
identical files by hand. Soundness-affecting infrastructure must
be centralized, not scattered.
Two shared helpers in intTests/support/:
lean-proof-test.sh — for test_lean_*_proof/ directories. Runs
proof.lean through 'lake env lean' and
fails if elaboration errors OR if the
result uses 'sorry'.
lean-shape-test.sh — for test_lean_soundness_*_{shape,prop}/
directories. Runs every *.shouldfail.lean
(must fail elaboration) and every
*.shouldpass.lean (must succeed without
sorry) probe.
Probe file naming is the full contract for shape tests — no env
variables, no test.sh variance. Renamed:
attack.lean -> attack.shouldfail.lean
positive.lean -> positive.shouldpass.lean (coerce)
non_prop.lean -> non_prop.shouldpass.lean (error, unsafe_assert)
Each affected test.sh is now a one-liner:
exec ${TEST_SHELL:-bash} ../support/lean-{proof,shape}-test.sh "$@"
Adding a new proof or shape test is now: create the directory,
drop in proof.lean (or *.should{fail,pass}.lean probes), copy
the one-liner test.sh. Zero plumbing per directory.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Previously each intTests/test_lean_*_proof/proof.lean copy-pasted
the SAW-emitted goal verbatim from its .lean.good file and added
a tactic proof. This is unsafe: if SAW's emission drifts, the
pasted goal and the real emission silently diverge. The discharge
proves a copy, not the actual output — soundness gap.
New pattern: emitted file is untouched ground truth, discharge
imports it.
source.txt — one line: relative path (from saw-script/)
to the SAW-emitted .lean file.
proof.lean — does `import Emitted` and proves
`theorem goal_closed : goal := by …`.
The definition of `goal` comes from the
imported emitted file.
lean-proof-test.sh:
1. Read source.txt.
2. Copy the emitted file to Emitted.lean in the probe dir.
3. Compile Emitted.lean -> Emitted.olean.
4. Elaborate proof.lean with LEAN_PATH pointing at the probe
dir so `import Emitted` resolves.
5. Fail if the emission doesn't compile OR the tactic proof
doesn't close OR proof.lean's own declarations use sorry.
source.txt is optional: tests that are self-contained (like
test_lean_proof_cookbook, which exercises library patterns
without an emitted goal) omit it, and the Emitted step is
skipped.
Emission drift now surfaces loudly: a change in SAW's output
that the hand-written tactics don't handle fails elaboration,
rather than silently running a stale copied goal.
Converted all 9 existing import-style discharges:
- E1, E2, E3, E4 (stress tests)
- offline_proof_t1, t3, t4
- walkthrough_proof
- recursion_stream_corec_proof
Left the cookbook untouched (no emitted goal; source.txt absent).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Setting up E5 (littleendian round-trip discharge) surfaced a real
soundness bug: the translator emits
'CryptolToLean.SAWCorePrelude.divNat' (and modNat) into .lean
files, but those identifiers don't exist in our library. The
emitted .lean fails to compile with 'unknown identifier divNat'.
Root cause:
- divNat, modNat, divModNat are defined in SAW Prelude.sawcore
via Nat#rec. They're marked in 'leanOpaqueBuiltins' to keep
their bodies opaque during normalization (sound — we don't
want to expose Nat#rec).
- But they had NO SpecialTreatment entry routing them to a
Lean-side function. So the translator fell back to emitting
'CryptolToLean.SAWCorePrelude.<name>', which Lean can't
resolve.
- L-14 (existing check) only audits 'primitive' decls (no
body). These defs have Nat#rec bodies, so L-14 missed them.
Fixes:
1. Add divNat/modNat/divModNat to SpecialTreatment map,
routing to sawCorePrimitivesModule.
2. Add reducible Lean defs in SAWCorePrimitives.lean backed
by Nat.div / Nat.mod (matching SAW's div-by-zero = 0
convention that it inherits from the Prelude impl).
New audit (catches the bug class going forward):
'auditOpaqueBuiltinsCoveredBySpecialTreatment' in Exporter.hs
flags every leanOpaqueBuiltins entry that names a Prelude def
but lacks a SpecialTreatment mapping. The new smoketest
'every leanOpaqueBuiltins entry has SpecialTreatment
(L-14 companion)' runs this at CI time.
The audit immediately found 19 more entries lacking mappings.
All 19 are in 'leanOpaqueBuiltinsIntentionallyUnmapped'
(new list in Exporter.hs) with reasons: Pos/Z arithmetic that
Cryptol doesn't expose, Nat#rec wrappers already rejected by
L-3. Any new addition to leanOpaqueBuiltins now forces either a
real mapping OR a conscious entry in the exception list.
E5 setup: otherTests driver updated with the Cryptol property;
discharge dir exists with source.txt pointing at the emitted
file. The proof itself is still a sorry placeholder — the
import-based test.sh now correctly fails on sorry, so this is a
visible WIP rather than a false pass.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Cryptol property \(xs : [4][8]) -> reverse (reverse xs) == xs.
Initial attempt parked because the support library was missing
a structural lemma about the gen-of-(at-of-gen-of-at) shape that
emerges from double reverse. Added:
gen_atWithDefault_double_reverse :
gen n α (fun i => at (gen n α (fun j => at xs (subNat (subNat n 1) j)))
(subNat (subNat n 1) i)) = xs
(Stated in subNat form so simp only can match the translator's
emitted shape — subNat is a reducible alias but simp only doesn't
unfold reducibles by default.)
With that lemma, the discharge is a one-liner: simp only with
the new lemma collapses the inner double-reverse to xs; then
each fold element is bvEq xs[i] xs[i] = true via a
hand-quantified bvEq_refl; decide closes the all-trues fold of
size 4.
E5 originally targeted the full Salsa20 littleendian round-trip
(reverse-split-join-reverse). That remains parked as a future
tier-4 exercise since closing it needs a structural lemma for
split/join interaction we haven't added.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The point of E7 is that SMT bit-blasting at 256 bits is painful (cubic-ish in width), while Lean closes the goal in one line via `bvAdd_assoc`. The discharge is structurally identical to the width-16 t3 proof — `bvAdd_assoc` is generic in the width, so the same `rw ; bvEq_refl` recipe scales. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Width-4 discharge by case-decomposing bits : Vec 4 Bool into four booleans and finishing by `decide`. Both the foldl-spec form and the genFix-lowered self-referential comprehension reduce to a concrete 3-bit popcount per case (16 cases), so decide closes them. This is a stopgap. As the user pointed out, the principled discharge is a polymorphic-over-width inductive lemma in the support library — matching the E1/E5/E7 pattern where each per-width discharge is a one-line instantiation. The blocker is a `genFix_snoc` characterization for the Cryptol comprehension shape, which hasn't been built yet. Filed as a Phase 7 follow-up task. The proof file's docstring documents this gap explicitly so the test holds the slot until the inductive form lands. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
CRITICAL SOUNDNESS FIX. The previous error.{u} signature
`(α : Sort (u+1)) → String → α` was unsound:
example : False :=
Empty.elim (error Empty "boom") -- elaborated cleanly\!
`Empty : Type 0 = Sort 1` fits `Sort (u+1)` at u := 0, so
`error Empty "" : Empty` typechecked, and Empty.elim then gave
False. The Sort restriction excluding Prop was insufficient — it
blocked the False-attack but missed the Empty-attack.
Confirmed by direct check (lean_run_code):
'fake_false_via_empty' depends on axioms: [error]
Fix: tighten to `(α : Type u) → [Inhabited α] → String → α`.
`Inhabited Empty` does not exist, so the call no longer
synthesizes. Type u still excludes Prop. All legitimate
translator-emitted shapes carry generic Inhabited instances
(Vec / PairType / RecordType / Either / Stream / Stream-endo /
Bool / Nat) — confirmed by re-emitting all stress-test goals
(E1-E7 .good files identical) and re-running every Lean-side
intTest (16/16 pass).
New regression: attack_empty.shouldfail.lean pins the Empty hole
closed. soundness-boundaries.md updated to reflect the L-17
restriction.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…sion writeLeanProp / translateGoalAsDeclImports now emits two extra opens at the top of every `*_prove0.lean` file: open CryptolToLean.SAWCoreBitvectorsProofs open CryptolToLean.SAWCorePreludeProofs This makes the emitted goal file self-contained: a user who discharges in-place by replacing the `sorry` in `goal_holds` can reference `bvAdd_comm`, `gen_atWithDefault_double_reverse`, etc. without restating opens. Limitation (documented in the preamble's docstring): Lean opens are file-local. A separate discharge file using `import Emitted` still needs its own `open` statements. So the originally-claimed boilerplate reduction in proof.lean files is NOT delivered by this change. Reducing that boilerplate would require an `export`-aggregator module or `#export ... from ...` (no Lean equivalent). Left for a follow-up. writeLeanTerm / translateTermAsDeclImports keeps the False flag (no proof opens) — generated module files don't need them. Refresh of all 11 pinned .good files in otherTests/saw-core-lean/ verified line-by-line: each diff is exactly +2 `open` lines and zero changes elsewhere. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Contributor
|
It seems to have dumped a lot of lean-only stuff in |
Soundness probes that silently passed when their preconditions were
missing — that's how the L-17 Empty hole survived for so long, and
how the (Pi) drift in test_lean_soundness_polymorphic{,_nested} sat
for weeks without anyone noticing. Phase A patches the four
silent-skip patterns:
1. lean-shape-test.sh: `lake` missing → was `exit 0`, now `exit 1`
with a clear error message + remediation. Soundness-shape probes
have NO .good fallback; if the harness can't elaborate them, the
test must fail, not silently succeed.
2. lean-proof-test.sh: same. Proof discharges only validate via Lean
elaboration; lake missing must surface as a real failure.
3. Both harnesses: `lake build` failure → was `exit 0` (treated as
environment skip), now `exit 1`. A failing support-library build
is a real defect, not an environment issue.
4. lean-elaborate.sh (used for the OPTIONAL elaboration step in
driver tests): `lake` missing still exits 77 (correctly skipped
— driver tests have authoritative .good diff coverage), but
`lake build` failure now exits 1 (loud; library bugs aren't
environment skips).
5. test-lean.sh: run-tests now also clears `*.lean.elaboration.fail`
from previous runs (was missing from the cleanup glob; could
leak stale failures into check-diffs).
CI workflow comment updated to reflect that the elan install step
is no longer optional — Linux/macOS integration-tests now require
lake. Windows is already `continue-on-error: true` (issue GaloisInc#2648),
so this patch makes Windows test_lean_* failures visible-but-
non-gating rather than invisible. Filed as task GaloisInc#134 follow-up:
either install elan on Windows or filter test_lean_* off Windows
deliberately.
Verified: all 19 Lean-side intTests still pass with lake available;
both modified harnesses fail loudly when run with lake stripped from
PATH (env -i PATH=/usr/bin:/bin bash test.sh → exit 1 with the
remediation message).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
intTests/test_lean_soundness_polymorphic{,_nested}/poly{,_nested}.log.good
have been stale since commit 92f0020 (L-discipline-5: Lambda-side
polymorphismResidual check). That commit added the (Pi) / (Lambda)
disambiguator to the diagnostic — the translator's behavior is
correct, only the pinned reference output was forgotten.
Diff per file is exactly one line:
-Problematic binders: ["t : sort 1"]
+Problematic binders: ["t : sort 1 (Pi)"]
Sweep verified: every other .good file in otherTests/saw-core-lean/
(217 total: 25 .log + 192 .lean) and intTests/test_lean_*/ (3 other
.log) is byte-identical to fresh emission. No other drift exists.
How this kind of drift gets caught next time:
- Phase A (committed earlier this session): silent-skip patterns
removed from lean-shape-test.sh / lean-proof-test.sh. Lake or
build failures now surface as test failures, not silent passes.
- These two tests already failed loudly via test-lean.sh's
check-diffs (non-empty .diff → exit 1). The reason they sat
unnoticed wasn't silent-skip in the harness; it was that the
cabal integration-tests target on Linux/macOS would have caught
them — implication is that someone has been ignoring CI failures
on this branch, or this branch hasn't been pushed to CI recently.
Filed as task GaloisInc#134 follow-up.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…lean/
Per SAW maintainer feedback ("lean-only stuff in intTests doesn't
belong; should be in otherTests/saw-core-lean") and the user's
explicit constraints:
1. Everything Lean-backend specific lives under
otherTests/saw-core-lean/. Nothing in intTests/.
2. NO per-example shell scripts. ONE orchestrator + 3 harnesses.
3. Clear category-based subdir structure.
4. NO hand-rolled Lean that mimics generator output.
5. ALL FAILURES NOISY. No silent skips, no dropped errors.
New layout:
otherTests/saw-core-lean/
├── test.sh # ONE orchestrator (verb dispatch)
├── Makefile # local-dev wrapper
├── support/ # 3 harness scripts + helper
│ ├── lean-driver-test.sh
│ ├── lean-proof-test.sh
│ ├── lean-shape-test.sh
│ └── lean-elaborate.sh
├── drivers/<25 tests>/ # SAW emission + diff + elaborate
├── proofs/<13 tests>/ # discharge generator-emitted goals
├── shape/<3 tests>/ # negative attack probes only
└── saw-boundary/<5 tests>/ # SAW-rejection / boundary diagnostics
Subdirs are PURE DATA. No test.sh, no Makefile, no README,
no lean-elaborate flags.
Migration:
- 21 directories moved from intTests/test_lean_*/ → categorized
subdirs of otherTests/saw-core-lean/. Renamed (test_lean_E1_
bvAdd_comm_proof → proofs/E1_bvAdd_comm, etc.) for clarity.
- 25 flat top-level driver tests moved into drivers/<short-name>/
so each is self-contained.
- 4 harness scripts moved from intTests/support/ → support/.
- .cry files moved alongside their tests.
- Deleted 113 per-subdir scaffolding files (46 test.sh,
21 Makefile, 18 README, 25 lean-elaborate flags,
3 *.shouldpass.lean).
- Deleted intTests/.elan/ artifacts (leftover when Test.hs
set HOME=intTests; should never have been committed).
Harness changes ("all failures noisy"):
- lean-elaborate.sh: removed exit 77 path on missing lake;
now exit 1 with remediation message. Build failures also
exit 1.
- lean-driver-test.sh: dropped `lean-elaborate` flag check —
Lean elaboration is now mandatory for all driver tests with
*.lean output.
- lean-shape-test.sh: only handles *.shouldfail.lean now
(positive coverage moved to drivers/). Verb dispatch added.
- lean-proof-test.sh: same loud-fail policy. Verb dispatch
added.
Orchestrator (otherTests/saw-core-lean/test.sh):
- Iterates each category, runs every test, accumulates
failures, prints summary, exits non-zero on any failure.
No fail-fast (so all problems visible per run), but no
silent passes either.
L-17 reverted (separate task GaloisInc#137):
- The `error.{u}` Inhabited-α tightening turned out to break
real translator emission (free type variables at error
positions). Reverted to Sort (u+1). The Empty soundness
residual is documented and tracked via task GaloisInc#137 (proper
fix requires translator changes to emit Inhabited evidence
at every type binder).
- attack_empty.shouldfail.lean removed (would no longer fail
elaboration).
- soundness-boundaries.md updated with the residual trust
statement.
Verified: `bash test.sh test` from otherTests/saw-core-lean/
prints ALL TESTS PASSED. Every category exercised, every test
produces a clear pass/fail signal.
Final intTests/ diff vs master:
- 2 files modified: test1646/test15.log.good and
test_search/search03.log.good. Both refresh the SAW :list
and search enumerations to include the new Lean-backend
SAW commands (offline_lean, write_lean_cryptol_module,
write_lean_term, dump_lean_residual_primitives). These are
SAW command-set fixtures, not Lean-specific tests.
- Everything else: zero.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…mbo probe
L-17 incident lesson: example-driven attack tests ("error False")
miss structurally-different routes to the same goal (Empty.elim ∘
error Empty). Building a cross-cutting audit so every known route
to False is either pinned by a probe or documented as a residual.
Deliverables:
1. doc/2026-05-04_attack-surface.md — single inventory listing
every known attack route, classified as:
- Blocked (pinned by *.shouldfail.lean): 6 routes
- Residual (currently passes by design): 6+ routes
split into L-17 family (closes via GaloisInc#137) and unsafeAssert
family (cannot close without changing SAW semantics)
- Not applicable (symbol not user-reachable): 2 routes
2. shape/coerce_unsafeassert_combo/attack.shouldfail.lean — new
probe for the most direct combinational attack:
unsafeAssert _ : Eq Type Bool Empty
|> coerce Bool Empty _ true : Empty
|> Empty.elim : False
Currently blocked by the universe-level mismatch between
unsafeAssert's Eq.{1} output and coerce's expected Eq.{2}. If
either signature's universe pins shift, this probe trips —
making the combinational attack a regression alarm rather than
silent unsoundness.
3. soundness-boundaries.md updated to point at the new attack-
surface inventory.
Verified: bash test.sh test from otherTests/saw-core-lean/ passes,
including the new probe.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Phase 9 (2026-05-03) had attempted to close the L-17 "Empty
attack" residual by tightening `error.{u}` to require
`[Inhabited α]`. That broke real Cryptol module emission:
SAW emits `error <T> "invalid instance"` placeholders in dead
typeclass-dictionary branches even when `T` may be uninhabited
(e.g., `Eq` over `Stream a` for a free type variable `a`),
and Lean cannot synthesize `Inhabited a` for an abstract type.
Phase 9 reverted to the unrestricted `Sort (u+1)` axiom,
documenting the user-side Empty attack as residual trust.
Two-tier design (this commit) sidesteps the conflict by splitting
the surface:
* `error_unrestricted.{u} : (α : Sort (u+1)) → String → α` —
the unsafe SAW-faithful axiom. SpecialTreatment routes SAW's
`Prelude.error` here. Translator emission target only.
Long, scary name signals "don't use this in user code."
* `error.{u} (α : Type u) [Inhabited α] (msg : String) : α` —
user-facing constrained def. Unqualified `error` resolves
here in user discharges. Empty attack
`Empty.elim (error Empty "boom")` fails at Inhabited
synthesis. Same blocker for PEmpty, Fin 0, Inhabited Empty,
etc.
Translator emission is unaffected: `SpecialTreatment.hs` routes
`error` to `error_unrestricted`, which has no Inhabited
constraint, so free type variables in dead-branch typeclass
elaborations still emit cleanly.
Residual: a user who explicitly writes `error_unrestricted
Empty "..."` can still extract `Empty`. This is an opt-out
(same semantic class as deliberate `unsafeAssert` misuse), not
silent unsoundness, and is documented.
Changes:
- SAWCorePrimitives.lean: split error into two-tier definitions.
- SpecialTreatment.hs: route SAW's error → error_unrestricted.
- shape/error_prop/attack_empty.shouldfail.lean: re-add the
L-17 attack probe; user-facing error blocks it.
- proofs/E4_map_id, E5_littleendian: update proof.lean to
reference `error_unrestricted` (matching emission shape).
- 22 driver .good files refreshed: emission `error` →
`error_unrestricted`.
- soundness-boundaries.md, residual-trust.md, attack-surface.md
updated: L-17 family is now "blocked" status; only
`error_unrestricted` explicit-opt-out remains as residual.
Verified: all tests pass (drivers, proofs, shape, saw-boundary).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
First end-to-end test of the canonical SAW workflow with Lean as
the prover for one obligation. Adapted from
exercises/functional-correctness/point/ — point.c (LLVM impl) is
verified against Point.cry; the equivalence obligation is dispatched
to offline_lean instead of SMT, and proofs/llvm_point_eq/proof.lean
discharges it via a 6-line tactic.
The canonical workflow exercised:
exercises/functional-correctness/point/point.c (LLVM impl)
│
│ llvm_verify against Point.cry
▼
drivers/llvm_point_verify/test_llvm_point_verify.saw
│ (offline_lean) emits the equivalence obligation
▼
drivers/llvm_point_verify/*.point_eq_return_value_matching0.lean
│ imports Emitted, discharges via tactics
▼
proofs/llvm_point_eq/proof.lean
Three real translator/SAW bugs surfaced and were fixed:
1. `writeLeanProp` did not abstract free symbolic variables.
llvm_verify-emitted goals carry SAWCore Variables introduced
by llvm_fresh_var (e.g., "p1.x", "p2.y"). The Lean translator
hit LocalVarOutOfBounds because nothing Pi-bound them. Fix:
use SC.getAllVars + scPiList in writeLeanProp to abstract them
into outer Pi binders before translation. No-op for closed
prove_print goals (zero free vars).
2. `proveWithPropExporter` put spaces in filenames. crucible-LLVM
goalType strings ("return value matching") leaked into output
filenames as `*.point_eq_return value matching0.lean`. Fix:
sanitize spaces and shell-awkward chars to '_' in the
constructed path. Affects all offline_* exporters.
3. `escapeIdent` was not applied to local SAWCore var names.
SAW's "p1.x" (record-field-projection naming from
llvm_fresh_var) emitted as a Lean binder `(p1.x : ...)` —
invalid because Lean uses '.' as namespace separator. Fix:
route translateLocalIdent through escapeIdent so dot-containing
names get Z-encoded ("p1.x" → "Op_p1zix").
Discharge proof (6 tactic lines):
intro x1 y1 x2 y2
by_cases hx : bvEq 32 x1 x2 = true
all_goals (by_cases hy : bvEq 32 y1 y2 = true)
all_goals
(simp_all [CryptolToLean.SAWCorePreludeExtra.ite, bvEq_sym]
<;> rfl)
Soundness audit via #print axioms:
goal_closed depends on axioms: [propext]
Only Lean's standard propositional extensionality. NOT in the
dependency list: sorryAx, Classical.choice, error,
error_unrestricted, unsafeAssert, the Vec↔BitVec coherence
axioms. The C↔Cryptol equivalence is genuinely proved, grounded
in Lean stdlib + provably-correct SAWCoreBitvectors_proofs
theorems.
Files:
- drivers/llvm_point_verify/{test_llvm_point_verify.saw,point.bc,
*.log.good,*.lean.good}: new driver. point.bc rebuilds via
clang from exercises/.../point.c (referenced, not duplicated).
- proofs/llvm_point_eq/{source.txt,proof.lean}: new discharge.
- saw-central/src/SAWCentral/{Builtins,Prover/Exporter}.hs: SAW
fixes (filename sanitization, free-var abstraction).
- saw-core-lean/src/SAWCoreLean/Term.hs: translator fix
(escapeIdent on local var names).
Verified: bash test.sh test → ALL TESTS PASSED.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds
saw-core-lean, a SAW backend that translates SAWCore terms to Lean 4 source. Generated.leanfiles import a small handwritten support library (saw-core-lean/lean/CryptolToLean/) and elaborate underlake build.The translator runs
scNormalizeon each input term to a fixed point, then walks the result. After normalisation the only constructs left are SAWCore primitives, inductives, and recursors, which are mapped 1:1 onto declarations in the handwritten Lean support library. User-defined definitions are inlined rather than emitted as separate Leandefs. This sidesteps the Lean cumulativity gap that blocked a direct mirror of the Rocq backend — rationale and alternatives indoc/2026-04-23_specialization-approach.md.New SAW commands:
write_lean_term,write_lean_cryptol_module,offline_lean.Current coverage
Handles: monomorphic instances, Cryptol modules with
{a}-polymorphism overType 0, thesaw-lean-example/demo end-to-end.Not yet handled:
Prelude.fix, universe-polymorphic terms (parked alternative onsaw-core-lean-p4-wip), nativeLean.BitVecbinding. Seedoc/2026-05-01_status-and-next-steps.md.Soundness
No skip lists, no
sorryin the translator, no close-but-not-equal mappings. Audits indoc/2026-04-24_audit-*.md, consolidated indoc/2026-04-24_soundness-boundaries.md.