quad-voter-proof local reproduce 2026-09-24 (b2cdeeb, clean tree)
Verbatim raw log, mechanically split into the commands actually run and
their real stdout+stderr; the one declared omission is the aeneas
progress-bar span noted inline below (see gen_cast.py's OMIT_NOTE).

$ sha256sum -c reports/PROOF.sha256
rust/src/lib.rs: OK
rust/Cargo.toml: OK
rust/Cargo.lock: OK
lean/lakefile.lean: OK
llbc/quad_voter_proof.llbc: OK
lean/QuadVoterProof.lean: OK
lean/VoterProof.lean: OK
lean/VoterStatements.lean: OK
scripts/check-extraction.sh: OK
scripts/normalize-llbc-diff.py: OK
scripts/check-no-sorry.py: OK
scripts/check-no-sorry.sh: OK

$ cd rust && cargo test
    Finished `test` profile [unoptimized + debuginfo] target(s) in 0.07s
     Running unittests src/lib.rs (target/debug/deps/quad_voter_proof-5c2e1630d1e9aef7)

running 12 tests
test tests::no_active_channels_is_its_own_variant ... ok
test tests::all_four_agree ... ok
test tests::one_of_four_disagrees_each_position ... ok
test tests::pair_disagreeing_is_undetermined ... ok
test tests::all_four_different_is_outside_hypothesis ... ok
test tests::pair_agreeing_is_agreed ... ok
test tests::single_active_channel_is_agreed ... ok
test tests::three_active_all_different_is_outside_hypothesis ... ok
test tests::three_active_majority_disables_the_odd_one ... ok
test tests::two_one_one_split_is_outside_hypothesis ... ok
test tests::two_two_split_is_outside_hypothesis ... ok
test tests::step_matches_oracle_exhaustively ... ok

test result: ok. 12 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s

   Doc-tests quad_voter_proof

running 1 test
test src/lib.rs - step (line 298) ... ok

test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 1.07s


$ cd .. && export PATH="$HOME/charon/bin:$PATH"

$ scripts/check-extraction.sh
== charon: 0.1.220
== aeneas: aeneas c2015b86
== cargo test (rust/)

running 12 tests
............
test result: ok. 12 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s


running 1 test
.
test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.20s

== charon cargo --preset=aeneas
   Compiling quad_voter_proof v0.1.0 (/Users/dzatona/Sites/MacExchange/quad-voter-proof/rust)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.92s
== aeneas -backend lean
[aeneas progress-bar frames (\r-animated) and their two temp-path Info lines omitted here -- see the provenance line on the page]
[Info ] Total execution time: 0.340699 seconds
== diff: llbc/quad_voter_proof.llbc (semantic: ignores dest_file path and debug name-table order)
fresh (matches committed)
== diff: lean/QuadVoterProof.lean
fresh (matches committed)

$ scripts/check-no-sorry.sh
== self-test ==
[ok] case 0: expect_flagged=True got=True
[ok] case 1: expect_flagged=True got=True
[ok] case 2: expect_flagged=True got=True
[ok] case 3: expect_flagged=True got=True
[ok] case 4: expect_flagged=True got=True
[ok] case 5: expect_flagged=False got=False
[ok] case 6: expect_flagged=False got=False
[ok] case 7: expect_flagged=False got=False
[ok] case 8: expect_flagged=False got=False
[ok] case 9: expect_flagged=False got=False
[ok] case 10: expect_flagged=True got=True
self-test: all 11 cases passed
== project files (every lean/*.lean) ==
clean: no sorry/admit/axiom in 4 file(s)

$ cd lean && lake build
⚠ [1546/1700] Replayed Aeneas.Std.Slice
warning: Aeneas/Std/Slice.lean:363:4: declaration uses `sorry`
warning: Aeneas/Std/Slice.lean:586:8: declaration uses `sorry`
⚠ [1592/1700] Replayed Aeneas.Std.StringIter
warning: Aeneas/Std/StringIter.lean:13:4: declaration uses `sorry`
⚠ [1699/1700] Replayed VoterStatements
warning: VoterStatements.lean:466:5: Variable name `hD1` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: VoterStatements.lean:623:40: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: VoterStatements.lean:623:59: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: VoterStatements.lean:623:69: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
Build completed successfully (1700 jobs).

$ out=$(lake env lean --stdin <<'LEAN'
import VoterStatements
open VoterStatements
#print axioms VoterStatements.T1
#print axioms VoterStatements.T2
#print axioms VoterStatements.T3a
#print axioms VoterStatements.T3a_correct_never_disabled
#print axioms VoterStatements.T3a_nonempty
#print axioms VoterStatements.T3b
#print axioms VoterStatements.T4
LEAN
)
echo "$out"
'VoterStatements.T1' depends on axioms: [propext, Classical.choice, Quot.sound]
'VoterStatements.T2' depends on axioms: [propext, Classical.choice, Quot.sound]
'VoterStatements.T3a' depends on axioms: [propext, Classical.choice, Quot.sound]
'VoterStatements.T3a_correct_never_disabled' depends on axioms: [propext, Classical.choice, Quot.sound]
'VoterStatements.T3a_nonempty' depends on axioms: [propext, Classical.choice, Quot.sound]
'VoterStatements.T3b' depends on axioms: [propext, Classical.choice, Quot.sound]
'VoterStatements.T4' depends on axioms: [propext, Classical.choice, Quot.sound]

$ extra=$(echo "$out" | grep "depends on axioms:" | sed 's/.*\[//;s/\].*//' | tr ',' '\n' | sed 's/^ *//;s/ *$//' | grep -v '^$' | grep -vx 'propext' | grep -vx 'Classical.choice' | grep -vx 'Quot.sound')
if [ -z "$extra" ]; then
  echo "extra axioms outside propext / Classical.choice / Quot.sound: (none)"
  echo "PASS"
else
  echo "extra axioms outside propext / Classical.choice / Quot.sound: $extra"
  echo "FAIL"
fi
extra axioms outside propext / Classical.choice / Quot.sound: (none)
PASS