1/-2 WP34 — axiom audit. `#print axioms` lists every axiom a theorem ultimately depends on; the3 output is part of `lake build`'s log (`formal/build.log`). Expected: only Lean-core axioms4 (`propext`, `Classical.choice`, `Quot.sound`) and, for `bv_decide` proofs,5 `Lean.ofReduceBool` (the kernel trusts the compiled LRAT certificate checker).6-/7import Wp34.Sha256Words8import Wp34.Sha256Step9import Wp34.Schedule10import Wp34.LocalCollision11import Wp34.Group1213namespace Wp341415#print axioms Ch_opt16#print axioms Maj_opt_or17#print axioms Maj_opt_xor18#print axioms Sigma0_xor19#print axioms Sigma0_injective20#print axioms sigma0_injective21#print axioms sigma1_injective22#print axioms rotr_xor23#print axioms Sigma0Inv_xor24#print axioms Sigma0Inv_Sigma025#print axioms sigma0_bijective26#print axioms sigma1_bijective27#print axioms shr3_not_injective28#print axioms stepInv_step29#print axioms step_stepInv30#print axioms step_bijective31#print axioms steps_bijective32#print axioms add4_sub433#print axioms sub4_add434#print axioms scheduleStep_inv35#print axioms schedule_backward36#print axioms localCollision_absorb37#print axioms localCollision_xor338#print axioms localCollision_absorb_diff39#print axioms lin9_xor_absorb40#print axioms linStep_xor_absorb41#print axioms absorb_corrections_not_real_collision42#print axioms CyclicGroup.schnorr_correct43#print axioms CyclicGroup.ecdsa_malleable44#print axioms CyclicGroup.ecdsa_correct4546end Wp3447