/-
  WP34 — axiom audit. `#print axioms` lists every axiom a theorem ultimately depends on; the
  output is part of `lake build`'s log (`formal/build.log`). Expected: only Lean-core axioms
  (`propext`, `Classical.choice`, `Quot.sound`) and, for `bv_decide` proofs,
  `Lean.ofReduceBool` (the kernel trusts the compiled LRAT certificate checker).
-/
import Wp34.Sha256Words
import Wp34.Sha256Step
import Wp34.Schedule
import Wp34.LocalCollision
import Wp34.Group

namespace Wp34

#print axioms Ch_opt
#print axioms Maj_opt_or
#print axioms Maj_opt_xor
#print axioms Sigma0_xor
#print axioms Sigma0_injective
#print axioms sigma0_injective
#print axioms sigma1_injective
#print axioms rotr_xor
#print axioms Sigma0Inv_xor
#print axioms Sigma0Inv_Sigma0
#print axioms sigma0_bijective
#print axioms sigma1_bijective
#print axioms shr3_not_injective
#print axioms stepInv_step
#print axioms step_stepInv
#print axioms step_bijective
#print axioms steps_bijective
#print axioms add4_sub4
#print axioms sub4_add4
#print axioms scheduleStep_inv
#print axioms schedule_backward
#print axioms localCollision_absorb
#print axioms localCollision_xor3
#print axioms localCollision_absorb_diff
#print axioms lin9_xor_absorb
#print axioms linStep_xor_absorb
#print axioms absorb_corrections_not_real_collision
#print axioms CyclicGroup.schnorr_correct
#print axioms CyclicGroup.ecdsa_malleable
#print axioms CyclicGroup.ecdsa_correct

end Wp34