1# 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 Max2✔ [2/9] Built Wp34.Group (315ms)3✔ [3/9] Built Wp34.Sha256Words (2.5s)4✔ [4/9] Built Wp34.Schedule (1.5s)5✔ [5/9] Built Wp34.Sha256Step (27s)6✔ [6/9] Built Wp34.LocalCollision (1.7s)7ℹ [7/9] Built Wp34.Audit (201ms)8info: Wp34/Audit.lean:15:0: 'Wp34.Ch_opt' depends on axioms: [propext, Classical.choice, Quot.sound, Ch_opt._native.bv_decide.ax_1_5]9info: 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]10info: 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]11info: Wp34/Audit.lean:18:0: 'Wp34.Sigma0_xor' depends on axioms: [propext, Classical.choice, Quot.sound, Sigma0_xor._native.bv_decide.ax_1_5]12info: Wp34/Audit.lean:19:0: 'Wp34.Sigma0_injective' depends on axioms: [propext,13 Classical.choice,14 Quot.sound,15 Sigma0_injective._native.bv_decide.ax_1_5]16info: Wp34/Audit.lean:20:0: 'Wp34.sigma0_injective' depends on axioms: [propext,17 Classical.choice,18 Quot.sound,19 sigma0_injective._native.bv_decide.ax_1_5]20info: Wp34/Audit.lean:21:0: 'Wp34.sigma1_injective' depends on axioms: [propext,21 Classical.choice,22 Quot.sound,23 sigma1_injective._native.bv_decide.ax_1_5]24info: Wp34/Audit.lean:22:0: 'Wp34.rotr_xor' depends on axioms: [propext, Quot.sound]25info: Wp34/Audit.lean:23:0: 'Wp34.Sigma0Inv_xor' depends on axioms: [propext, Quot.sound]26info: Wp34/Audit.lean:24:0: 'Wp34.Sigma0Inv_Sigma0' depends on axioms: [propext,27 Classical.choice,28 Quot.sound,29 Sigma0Inv_Sigma0_b0._native.bv_decide.ax_1_5,30 Sigma0Inv_Sigma0_b1._native.bv_decide.ax_1_5,31 Sigma0Inv_Sigma0_b2._native.bv_decide.ax_1_5,32 Sigma0Inv_Sigma0_b3._native.bv_decide.ax_1_5,33 Sigma0_xor._native.bv_decide.ax_1_5,34 inv_of_quarters._native.bv_decide.ax_1_5]35info: Wp34/Audit.lean:25:0: 'Wp34.sigma0_bijective' depends on axioms: [propext,36 Classical.choice,37 Quot.sound,38 inv_of_quarters._native.bv_decide.ax_1_5,39 sigma0_injective._native.bv_decide.ax_1_5,40 sigma0_sigma0Inv_b0._native.bv_decide.ax_1_5,41 sigma0_sigma0Inv_b1._native.bv_decide.ax_1_5,42 sigma0_sigma0Inv_b2._native.bv_decide.ax_1_5,43 sigma0_sigma0Inv_b3._native.bv_decide.ax_1_5,44 sigma0_xor._native.bv_decide.ax_1_5,45 xor_and_right._native.bv_decide.ax_1_5]46info: Wp34/Audit.lean:26:0: 'Wp34.sigma1_bijective' depends on axioms: [propext,47 Classical.choice,48 Quot.sound,49 inv_of_quarters._native.bv_decide.ax_1_5,50 sigma1_injective._native.bv_decide.ax_1_5,51 sigma1_sigma1Inv_b0._native.bv_decide.ax_1_5,52 sigma1_sigma1Inv_b1._native.bv_decide.ax_1_5,53 sigma1_sigma1Inv_b2._native.bv_decide.ax_1_5,54 sigma1_sigma1Inv_b3._native.bv_decide.ax_1_5,55 sigma1_xor._native.bv_decide.ax_1_5,56 xor_and_right._native.bv_decide.ax_1_5]57info: Wp34/Audit.lean:27:0: 'Wp34.shr3_not_injective' depends on axioms: [propext]58info: Wp34/Audit.lean:28:0: 'Wp34.stepInv_step' depends on axioms: [propext, Classical.choice, Quot.sound, add4_sub4._native.bv_decide.ax_1_5]59info: Wp34/Audit.lean:29:0: 'Wp34.step_stepInv' depends on axioms: [propext, Classical.choice, Quot.sound, sub4_add4._native.bv_decide.ax_1_5]60info: Wp34/Audit.lean:30:0: 'Wp34.step_bijective' depends on axioms: [propext,61 Classical.choice,62 Quot.sound,63 add4_sub4._native.bv_decide.ax_1_5,64 sub4_add4._native.bv_decide.ax_1_5]65info: Wp34/Audit.lean:31:0: 'Wp34.steps_bijective' depends on axioms: [propext,66 Classical.choice,67 Quot.sound,68 add4_sub4._native.bv_decide.ax_1_5,69 sub4_add4._native.bv_decide.ax_1_5]70info: Wp34/Audit.lean:32:0: 'Wp34.add4_sub4' depends on axioms: [propext, Classical.choice, Quot.sound, add4_sub4._native.bv_decide.ax_1_5]71info: Wp34/Audit.lean:33:0: 'Wp34.sub4_add4' depends on axioms: [propext, Classical.choice, Quot.sound, sub4_add4._native.bv_decide.ax_1_5]72info: Wp34/Audit.lean:34:0: 'Wp34.scheduleStep_inv' depends on axioms: [propext,73 Classical.choice,74 Quot.sound,75 scheduleStep_inv._native.bv_decide.ax_1_5]76info: Wp34/Audit.lean:35:0: 'Wp34.schedule_backward' depends on axioms: [propext,77 Classical.choice,78 Quot.sound,79 scheduleStep_inv._native.bv_decide.ax_1_5]80info: Wp34/Audit.lean:36:0: 'Wp34.localCollision_absorb' depends on axioms: [propext,81 Classical.choice,82 Quot.sound,83 Sigma0_xor._native.bv_decide.ax_1_5,84 Sigma1_xor._native.bv_decide.ax_1_5,85 byte_split._native.bv_decide.ax_1_5,86 diff_absorb_b0._native.bv_decide.ax_1_13,87 diff_absorb_b1._native.bv_decide.ax_1_13,88 diff_absorb_b2._native.bv_decide.ax_1_13,89 diff_absorb_b3._native.bv_decide.ax_1_13,90 linStep_xor_absorb._native.bv_decide.ax_1_10,91 State.xor_zero._native.bv_decide.ax_1_7,92 Words9.xor_zero._native.bv_decide.ax_1_7]93info: Wp34/Audit.lean:37:0: 'Wp34.localCollision_xor3' depends on axioms: [propext,94 Classical.choice,95 Quot.sound,96 Sigma0_xor._native.bv_decide.ax_1_5,97 Sigma1_xor._native.bv_decide.ax_1_5,98 byte_split._native.bv_decide.ax_1_5,99 diff_xor3_b0._native.bv_decide.ax_1_13,100 diff_xor3_b1._native.bv_decide.ax_1_13,101 diff_xor3_b2._native.bv_decide.ax_1_13,102 diff_xor3_b3._native.bv_decide.ax_1_13,103 linStep_xor_xor3._native.bv_decide.ax_1_10,104 State.xor_zero._native.bv_decide.ax_1_7,105 Words9.xor_zero._native.bv_decide.ax_1_7]106info: Wp34/Audit.lean:38:0: 'Wp34.localCollision_absorb_diff' depends on axioms: [propext,107 Classical.choice,108 Quot.sound,109 Sigma0_xor._native.bv_decide.ax_1_5,110 Sigma1_xor._native.bv_decide.ax_1_5,111 byte_split._native.bv_decide.ax_1_5,112 diff_absorb_b0._native.bv_decide.ax_1_13,113 diff_absorb_b1._native.bv_decide.ax_1_13,114 diff_absorb_b2._native.bv_decide.ax_1_13,115 diff_absorb_b3._native.bv_decide.ax_1_13,116 linStep_xor_absorb._native.bv_decide.ax_1_10,117 State.xor_zero._native.bv_decide.ax_1_7,118 Words9.xor_zero._native.bv_decide.ax_1_7]119info: Wp34/Audit.lean:39:0: 'Wp34.lin9_xor_absorb' depends on axioms: [propext,120 Classical.choice,121 Quot.sound,122 linStep_xor_absorb._native.bv_decide.ax_1_10]123info: Wp34/Audit.lean:40:0: 'Wp34.linStep_xor_absorb' depends on axioms: [propext,124 Classical.choice,125 Quot.sound,126 linStep_xor_absorb._native.bv_decide.ax_1_10]127info: Wp34/Audit.lean:41:0: 'Wp34.absorb_corrections_not_real_collision' depends on axioms: [propext, Quot.sound]128info: Wp34/Audit.lean:42:0: 'Wp34.CyclicGroup.schnorr_correct' depends on axioms: [propext]129info: Wp34/Audit.lean:43:0: 'Wp34.CyclicGroup.ecdsa_malleable' depends on axioms: [propext, Quot.sound]130info: Wp34/Audit.lean:44:0: 'Wp34.CyclicGroup.ecdsa_correct' depends on axioms: [propext, Quot.sound]131✔ [8/9] Built Wp34 (193ms)132Build completed successfully (9 jobs).133# exit code 0 — wall time 32 s134