num_integer: opt-level 3 build + proved opt0/opt3 gcd equivalence - #142
Merged
Conversation
`num_integer_opt3` is a byte-for-byte copy of `num_integer` compiled at opt-level 3 (a per-package `[profile.release.package]` override; the workspace default stays 0). At opt-level 3 the binary-GCD is inlined into a single, memory-free function; the opt-level 0 build instead runs Stein's algorithm through the shadow stack in linear memory (three functions, spills operands + scratch to memory, mutates then restores `global 0`). `Project/NumIntegerOpt3/Equivalence.lean` states (statement only, proofs left as `sorry`) that the two exported `gcd_u64` functions are observationally equivalent from the canonical initial store: they agree on the returned value / trap and on the host state, deliberately excluding linear memory — the opt0 build's shadow-stack scratch writes differ and are unobservable to the caller. The `initial = mod0.initialStore` precondition is load-bearing: on a pathological store the opt0 build can trap where the memory-free opt3 build still returns. Neither module is wired into `Project.lean` while the proofs are pending, so the `sorry`s stay out of the default build / CI. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Contributor
|
Verifier report preview: https://talos-verifier-report-pr-142.vercel.app (This URL is stable for this PR — it always points to the latest build of c9572fc.) |
Drop the positive "happy-path" form (`GcdOptEquiv'`). Under the canonical-store precondition both builds are total, so it was logically equivalent to the biconditional; the biconditional `GcdOptEquiv` is the intended statement — if one build fails to return, the other must too (success *or* trap agree). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
mfornet
reviewed
Jul 14, 2026
…icate Lift the opt0-vs-opt3 gcd equivalence into a parametrized, reusable notion in `CodeLib/Equivalence.lean`: `Wasm.ObservationallyEquiv env m₁ id₁ m₂ id₂ initial args` says two entry points, run from the same store on the same args, reach exactly the same observable outcomes — returned values + host state, with success/trap symmetric — deliberately not observing linear memory. Ships the discharge rule `ObservationallyEquiv.of_common_outcome` (reduce an equivalence to "both `TerminatesWith` the same `(result, host)` outcome", via `TerminatesWith.outcome_unique`) plus `refl`/`symm`/`trans`. All proven, no `sorry`, so the addition is clean for CI. `NumIntegerOpt3/Equivalence.lean`'s `GcdOptEquiv` now just instantiates the predicate at the two builds and `mod0.initialStore`; the statement is unchanged. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…onflicts-9483db # Conflicts: # programs/rust/Cargo.toml
`gcd_opt_equiv` is now proved, no `sorry`. The proof reduces the observational equivalence to a common outcome both builds reach (`ObservationallyEquiv.of_common_outcome`): each exported `gcd_u64` terminates with the same value (the gcd) and the same host state. - opt0 side reuses the existing `Project.NumInteger.Spec.gcd_u64_correct`. - opt3 side is the new `NumIntegerOpt3/Spec.lean`: `mod3_gcd` proves the register-only build computes the gcd and leaves the store untouched. Its core is `inner_wp`, a `wp_loop_cons` invariant for Stein's subtract-and-halve loop that reuses the CodeLib `UInt64` Stein lemmas (`stein_step_x/y`, `shr_ctz_*`, `recombine_loop`); the surrounding `func0` structure (odd-part reduction, zero-checks, recombine) is driven by two small local macros (`drive`/`pick`). Both modules are wired into `Project.lean`, so CI verifies them. `#print axioms gcd_opt_equiv` is clean (no `sorryAx`). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
El3ssar
changed the title
…e/pr-142-merge-conflicts-9483db
mfornet
marked this pull request as ready for review
July 15, 2026 09:21
mfornet
self-requested a review
July 15, 2026 09:21
mfornet
approved these changes
Jul 15, 2026
mfornet
added a commit
that referenced
this pull request
Jul 17, 2026
…ements opt0/opt3 (#151) * programs: add swap_elements opt-level 3 build Byte-for-byte the same source as `swap_elements`, compiled at opt-level 3 via a per-package profile override (workspace default stays 0), mirroring the `num_integer_opt3` pattern from #142. The two builds differ structurally: opt0 exports `func4` and spreads the swap across a five-function call chain, while opt3 inlines the whole thing into `func0` (bounds checks, two load64/store64, return). Unlike the `gcd` pair, this function's result lives in linear memory, so relating the builds needs a memory-aware observational equivalence. Spec.lean is the `verifier emit` scaffold for now; the equivalence proof lands in a follow-up. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * codelib+programs: memory-aware program equivalence, proved on swap_elements opt0/opt3 `ObservationallyEquiv` (#142) observes the returned values and `Store.host`, and deliberately omits linear memory — its docstring noted that "programs whose result lives in memory need a stronger observation than this one; add it when such a proof arrives". `swap_elements` is exactly that program: it returns `[]` and communicates only by mutating the caller's array, so the existing notion degenerates to bare co-termination and says nothing about the swap. This adds the stronger observation, and the proof that motivates it. codelib: * `Wasm.ObservationallyEquivOn … (obs : Store α → β)` — the observation is now a parameter, with `outcome_unique_on` / `of_common_outcome` / refl / symm / trans stated once against it. `ObservationallyEquiv` becomes the instance at `Store.host`: every statement is unchanged and its proofs are now one-liners, so a new observation costs an instance rather than a copy of the proofs (following the `write_write_comm_of_footprints` precedent in #147). * `Mem.words64_swap` — the view-level counterpart of a per-element swap postcondition: `m'`'s array view is `m`'s with positions `i` and `j` exchanged. Stated at the slot addresses, so it needs no no-wrap hypothesis, and `i = j` is allowed. programs: * `SwapElementsOpt3.Spec.func0_swap` — total correctness of the opt3 export. The optimiser inlined the four-deep call chain into a single function, so this build needs strictly fewer preconditions than opt0: no shadow-stack pin and no `1048576 ≤ ptr`. * `SwapElementsOpt3.Equivalence.swap_opt_equiv` — the two builds are `ObservationallyEquivOn` at `fun st => (st.host, st.mem.words64 ptr len.toNat)`. The opt0 side reuses the merged `swap_elements_correct`; both are routed through one shared bridge so they land on the same observation. The observation is a region rather than all of memory, and must be: opt0 also writes the scratch slot at [1048552, 1048560), which opt3 never touches. That is precisely the caller-invisible traffic a memory-aware equivalence has to ignore. `#print axioms swap_opt_equiv` is clean (no `sorryAx`); `Project.NumIntegerOpt3` builds unchanged. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * codelib+programs: address review findings on the swap equivalence - Hoist the UInt32-indexed bridge from per-element swap postconditions to the words64 view into CodeLib as Mem.words64_swap' — it was program- agnostic plumbing living as a private lemma in the program's equivalence file; the next memory-result equivalence would have re-derived it. - Share the opt0 spec's elemAddr vocabulary (elemAddr / elemAddr_of_shl / elemAddr_toNat) in the opt3 spec instead of duplicating it, deleting the opt3_elemAddr_eq normalisation bridge from the equivalence proof. - Drop the direct Interpreter.Wasm.Wp.* imports from the opt3 spec: they arrive transitively via CodeLib, and programs/ should not import the interpreter directly (CLAUDE.md dependency direction). - Fix the "inlines everything into a single function" docstring: the swap path is one function, but the module still carries panic/formatting machinery, unreachable under the in-bounds preconditions. - Mention words64_swap / words64_swap' in MemArray.lean's lemma inventory. No statement changes; #print axioms swap_opt_equiv unchanged. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Co-authored-by: Marcelo Fornet <mfornet94@gmail.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.
What
Adds a second build of the existing
num_integer::gcd_u64at opt-level 3,a reusable program-equivalence predicate in CodeLib, and a proved
equivalence between the two builds.
gcd_opt_equivis proved — nosorry(
#print axiomsis clean). CI builds all of it.The two builds
num_integer_opt3is a byte-for-byte copy of thenum_integersource,compiled at opt-level 3 via a per-package profile override
(
[profile.release.package.num_integer_opt3]); the workspace default stays 0.num_integer)num_integer_opt3)func0/func1/func2)global 0(stack pointer)gcd_u64exportBoth modules declare the same mutable state (16-page memory, globals
[1048576×3], one 1×1 funcref table), somod0.initialStore = mod3.initialStore.Empirically cross-checked with node over 1225
u64pairs (incl.(0,0),powers of two,
u64::MAX): opt0 ≡ opt3 ≡ reference gcd, 0 mismatches.Reusable predicate —
CodeLib/Equivalence.leanWasm.ObservationallyEquiv env m₁ id₁ m₂ id₂ initial args: two entry points,run from the same initial store on the same args, reach exactly the same
observable outcomes — returned values + host state (
Store.host), successand trap symmetric — linear memory deliberately not observed.
Ships fully-proven (no
sorry):ObservationallyEquiv.of_common_outcome(thedischarge rule, via
TerminatesWith.outcome_unique) plusrefl/symm/trans.The equivalence —
Project/NumIntegerOpt3/Equivalence.leanGcdOptEquivinstantiates the predicate at the two builds from the canonicalstore;
gcd_opt_equivproves it by reducing to a common outcome both buildsreach — each
gcd_u64terminates with the same value (the gcd) and the samehost state.
Project.NumInteger.Spec.gcd_u64_correct.NumIntegerOpt3/Spec.lean:mod3_gcdproves theregister-only build computes the gcd and leaves the store untouched. Its core
is
inner_wp, awp_loop_consinvariant for Stein's subtract-and-halveloop reusing the CodeLib
UInt64Stein lemmas (stein_step_x/y,shr_ctz_*,recombine_loop); the surrounding structure (odd-partreduction, zero-checks, recombine) is driven by two small local macros.
The
mod0.initialStorestarting point is load-bearing: on a pathologicalstore the opt0 build can trap (shadow-stack pointer / pages) where the
memory-free opt3 build still returns, so the two are not equivalent for an
arbitrary initial state.
Notes for review
sorryanywhere;#print axioms gcd_opt_equiv= the standard axioms plusthe interpreter's two
bv_decideaxioms (inherited from the opt0 memorylemmas). CodeLib addition is
sorry-free.Spec,Equivalence, and the CodeLib predicate) are wiredinto the build, so CI checks them.
Spec.leanplaceholder was replaced by the realmod3_gcd; the equivalence lives inEquivalence.lean.