# lake clean && lake build — 2026-11-01 01:56:37 EST — Lean (version 4.35.0, arm64-apple-darwin24.6.0, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) — Apple M5 Max
✔ [2/9] Built Wp34.Group (315ms)
✔ [3/9] Built Wp34.Sha256Words (2.5s)
✔ [4/9] Built Wp34.Schedule (1.5s)
✔ [5/9] Built Wp34.Sha256Step (27s)
✔ [6/9] Built Wp34.LocalCollision (1.7s)
ℹ [7/9] Built Wp34.Audit (201ms)
info: Wp34/Audit.lean:15:0: 'Wp34.Ch_opt' depends on axioms: [propext, Classical.choice, Quot.sound, Ch_opt._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:16:0: 'Wp34.Maj_opt_or' depends on axioms: [propext, Classical.choice, Quot.sound, Maj_opt_or._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:17:0: 'Wp34.Maj_opt_xor' depends on axioms: [propext, Classical.choice, Quot.sound, Maj_opt_xor._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:18:0: 'Wp34.Sigma0_xor' depends on axioms: [propext, Classical.choice, Quot.sound, Sigma0_xor._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:19:0: 'Wp34.Sigma0_injective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 Sigma0_injective._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:20:0: 'Wp34.sigma0_injective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 sigma0_injective._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:21:0: 'Wp34.sigma1_injective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 sigma1_injective._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:22:0: 'Wp34.rotr_xor' depends on axioms: [propext, Quot.sound]
info: Wp34/Audit.lean:23:0: 'Wp34.Sigma0Inv_xor' depends on axioms: [propext, Quot.sound]
info: Wp34/Audit.lean:24:0: 'Wp34.Sigma0Inv_Sigma0' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 Sigma0Inv_Sigma0_b0._native.bv_decide.ax_1_5,
 Sigma0Inv_Sigma0_b1._native.bv_decide.ax_1_5,
 Sigma0Inv_Sigma0_b2._native.bv_decide.ax_1_5,
 Sigma0Inv_Sigma0_b3._native.bv_decide.ax_1_5,
 Sigma0_xor._native.bv_decide.ax_1_5,
 inv_of_quarters._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:25:0: 'Wp34.sigma0_bijective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 inv_of_quarters._native.bv_decide.ax_1_5,
 sigma0_injective._native.bv_decide.ax_1_5,
 sigma0_sigma0Inv_b0._native.bv_decide.ax_1_5,
 sigma0_sigma0Inv_b1._native.bv_decide.ax_1_5,
 sigma0_sigma0Inv_b2._native.bv_decide.ax_1_5,
 sigma0_sigma0Inv_b3._native.bv_decide.ax_1_5,
 sigma0_xor._native.bv_decide.ax_1_5,
 xor_and_right._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:26:0: 'Wp34.sigma1_bijective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 inv_of_quarters._native.bv_decide.ax_1_5,
 sigma1_injective._native.bv_decide.ax_1_5,
 sigma1_sigma1Inv_b0._native.bv_decide.ax_1_5,
 sigma1_sigma1Inv_b1._native.bv_decide.ax_1_5,
 sigma1_sigma1Inv_b2._native.bv_decide.ax_1_5,
 sigma1_sigma1Inv_b3._native.bv_decide.ax_1_5,
 sigma1_xor._native.bv_decide.ax_1_5,
 xor_and_right._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:27:0: 'Wp34.shr3_not_injective' depends on axioms: [propext]
info: Wp34/Audit.lean:28:0: 'Wp34.stepInv_step' depends on axioms: [propext, Classical.choice, Quot.sound, add4_sub4._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:29:0: 'Wp34.step_stepInv' depends on axioms: [propext, Classical.choice, Quot.sound, sub4_add4._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:30:0: 'Wp34.step_bijective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 add4_sub4._native.bv_decide.ax_1_5,
 sub4_add4._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:31:0: 'Wp34.steps_bijective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 add4_sub4._native.bv_decide.ax_1_5,
 sub4_add4._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:32:0: 'Wp34.add4_sub4' depends on axioms: [propext, Classical.choice, Quot.sound, add4_sub4._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:33:0: 'Wp34.sub4_add4' depends on axioms: [propext, Classical.choice, Quot.sound, sub4_add4._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:34:0: 'Wp34.scheduleStep_inv' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 scheduleStep_inv._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:35:0: 'Wp34.schedule_backward' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 scheduleStep_inv._native.bv_decide.ax_1_5]
info: Wp34/Audit.lean:36:0: 'Wp34.localCollision_absorb' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 Sigma0_xor._native.bv_decide.ax_1_5,
 Sigma1_xor._native.bv_decide.ax_1_5,
 byte_split._native.bv_decide.ax_1_5,
 diff_absorb_b0._native.bv_decide.ax_1_13,
 diff_absorb_b1._native.bv_decide.ax_1_13,
 diff_absorb_b2._native.bv_decide.ax_1_13,
 diff_absorb_b3._native.bv_decide.ax_1_13,
 linStep_xor_absorb._native.bv_decide.ax_1_10,
 State.xor_zero._native.bv_decide.ax_1_7,
 Words9.xor_zero._native.bv_decide.ax_1_7]
info: Wp34/Audit.lean:37:0: 'Wp34.localCollision_xor3' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 Sigma0_xor._native.bv_decide.ax_1_5,
 Sigma1_xor._native.bv_decide.ax_1_5,
 byte_split._native.bv_decide.ax_1_5,
 diff_xor3_b0._native.bv_decide.ax_1_13,
 diff_xor3_b1._native.bv_decide.ax_1_13,
 diff_xor3_b2._native.bv_decide.ax_1_13,
 diff_xor3_b3._native.bv_decide.ax_1_13,
 linStep_xor_xor3._native.bv_decide.ax_1_10,
 State.xor_zero._native.bv_decide.ax_1_7,
 Words9.xor_zero._native.bv_decide.ax_1_7]
info: Wp34/Audit.lean:38:0: 'Wp34.localCollision_absorb_diff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 Sigma0_xor._native.bv_decide.ax_1_5,
 Sigma1_xor._native.bv_decide.ax_1_5,
 byte_split._native.bv_decide.ax_1_5,
 diff_absorb_b0._native.bv_decide.ax_1_13,
 diff_absorb_b1._native.bv_decide.ax_1_13,
 diff_absorb_b2._native.bv_decide.ax_1_13,
 diff_absorb_b3._native.bv_decide.ax_1_13,
 linStep_xor_absorb._native.bv_decide.ax_1_10,
 State.xor_zero._native.bv_decide.ax_1_7,
 Words9.xor_zero._native.bv_decide.ax_1_7]
info: Wp34/Audit.lean:39:0: 'Wp34.lin9_xor_absorb' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 linStep_xor_absorb._native.bv_decide.ax_1_10]
info: Wp34/Audit.lean:40:0: 'Wp34.linStep_xor_absorb' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 linStep_xor_absorb._native.bv_decide.ax_1_10]
info: Wp34/Audit.lean:41:0: 'Wp34.absorb_corrections_not_real_collision' depends on axioms: [propext, Quot.sound]
info: Wp34/Audit.lean:42:0: 'Wp34.CyclicGroup.schnorr_correct' depends on axioms: [propext]
info: Wp34/Audit.lean:43:0: 'Wp34.CyclicGroup.ecdsa_malleable' depends on axioms: [propext, Quot.sound]
info: Wp34/Audit.lean:44:0: 'Wp34.CyclicGroup.ecdsa_correct' depends on axioms: [propext, Quot.sound]
✔ [8/9] Built Wp34 (193ms)
Build completed successfully (9 jobs).
# exit code 0 — wall time 32 s