1/-2 WP34 — Stage 5 formal verification.3 SHA-256 (FIPS 180-4) word functions on `BitVec 32`, transcribed from `src/wp34/sha256.py`.45 Everything in this file is machine-checked by Lean 4 core only (no Mathlib).6 The `bv_decide` tactic bit-blasts the goal, calls the bundled CaDiCaL SAT solver and7 re-checks the LRAT certificate it returns inside Lean's kernel.8-/9import Std.Tactic.BVDecide1011namespace Wp341213/-- A SHA-256 word. -/14abbrev Word := BitVec 321516/-- Right rotation (`rotr` in `sha256.py`). -/17def rotr (x : Word) (k : Nat) : Word := x.rotateRight k1819-- The four sigma functions and the two Boolean functions, exactly as in `sha256.py`.20def Sigma0 (x : Word) : Word := rotr x 2 ^^^ rotr x 13 ^^^ rotr x 2221def Sigma1 (x : Word) : Word := rotr x 6 ^^^ rotr x 11 ^^^ rotr x 2522def sigma0 (x : Word) : Word := rotr x 7 ^^^ rotr x 18 ^^^ (x >>> 3)23def sigma1 (x : Word) : Word := rotr x 17 ^^^ rotr x 19 ^^^ (x >>> 10)24def Ch (x y z : Word) : Word := (x &&& y) ^^^ (~~~x &&& z)25def Maj (x y z : Word) : Word := (x &&& y) ^^^ (x &&& z) ^^^ (y &&& z)2627/-! ### 1(a)–(b) Optimised forms of `Ch` and `Maj` (used by most implementations) -/2829/-- `Ch x y z = ((y ^ z) & x) ^ z` — one fewer operation and no complement. -/30theorem Ch_opt (x y z : Word) : Ch x y z = ((y ^^^ z) &&& x) ^^^ z := by31 unfold Ch; bv_decide3233/-- `Maj x y z = (x & (y | z)) | (y & z)`. -/34theorem Maj_opt_or (x y z : Word) : Maj x y z = (x &&& (y ||| z)) ||| (y &&& z) := by35 unfold Maj; bv_decide3637/-- `Maj x y z = ((x ^ y) & (y ^ z)) ^ y`. -/38theorem Maj_opt_xor (x y z : Word) : Maj x y z = ((x ^^^ y) &&& (y ^^^ z)) ^^^ y := by39 unfold Maj; bv_decide4041/-- `Maj` is symmetric in its arguments (used implicitly by the local-collision analysis). -/42theorem Maj_comm (x y z : Word) : Maj x y z = Maj y x z ∧ Maj x y z = Maj x z y := by43 unfold Maj; bv_decide4445/-! ### 1(c) GF(2)-linearity of Σ0, Σ1, σ0, σ1 -/4647theorem Sigma0_xor (x y : Word) : Sigma0 (x ^^^ y) = Sigma0 x ^^^ Sigma0 y := by48 unfold Sigma0 rotr; bv_decide49theorem Sigma1_xor (x y : Word) : Sigma1 (x ^^^ y) = Sigma1 x ^^^ Sigma1 y := by50 unfold Sigma1 rotr; bv_decide51theorem sigma0_xor (x y : Word) : sigma0 (x ^^^ y) = sigma0 x ^^^ sigma0 y := by52 unfold sigma0 rotr; bv_decide53theorem sigma1_xor (x y : Word) : sigma1 (x ^^^ y) = sigma1 x ^^^ sigma1 y := by54 unfold sigma1 rotr; bv_decide5556theorem Sigma0_zero : Sigma0 0 = 0 := by unfold Sigma0 rotr; bv_decide57theorem Sigma1_zero : Sigma1 0 = 0 := by unfold Sigma1 rotr; bv_decide58theorem sigma0_zero : sigma0 0 = 0 := by unfold sigma0 rotr; bv_decide59theorem sigma1_zero : sigma1 0 = 0 := by unfold sigma1 rotr; bv_decide6061/-! ### 1(d)–(e) Injectivity and explicit inverses6263`Function.Injective` is Lean-core. Core has no `Function.Bijective`/`Surjective`, so we state64bijectivity as "injective and has an explicit right inverse" through the definition below. -/6566/-- Bijectivity without Mathlib: injective and surjective. -/67def Bijective {α β : Type} (f : α → β) : Prop := Function.Injective f ∧ ∀ y, ∃ x, f x = y6869theorem Sigma0_injective : Function.Injective Sigma0 := fun x y h => by70 unfold Sigma0 rotr at h; bv_decide71theorem Sigma1_injective : Function.Injective Sigma1 := fun x y h => by72 unfold Sigma1 rotr at h; bv_decide73/-- σ0 contains a logical shift, yet it IS injective on 32 bits (GF(2) rank 32, see74`scripts/gf2_rank.py`); `bv_decide` finds no counter-example (UNSAT, certificate checked). -/75theorem sigma0_injective : Function.Injective sigma0 := fun x y h => by76 unfold sigma0 rotr at h; bv_decide77/-- Same for σ1. -/78theorem sigma1_injective : Function.Injective sigma1 := fun x y h => by79 unfold sigma1 rotr at h; bv_decide8081/-- Control: the shift term alone is NOT injective (`0 >>> 3 = 1 >>> 3`). -/82theorem shr3_not_injective : ¬ Function.Injective (fun x : Word => x >>> 3) := fun h =>83 absurd (h (a₁ := 0) (a₂ := 1) (by decide)) (by decide)8485/-- Control: the rotation part of σ0 alone is NOT injective either:86`rotr x 7 ^ rotr x 18 = x ^ rotr x 11` up to rotation, whose kernel is `{0, 0xFFFFFFFF}`. -/87theorem sigma0_rotations_not_injective :88 ¬ Function.Injective (fun x : Word => rotr x 7 ^^^ rotr x 18) := fun h =>89 absurd (h (a₁ := 0) (a₂ := 0xFFFFFFFF) (by decide)) (by decide)9091/-- Control: the rotation part of σ1 alone is NOT injective (`x ^ rotr x 2` kills `0xFFFFFFFF`). -/92theorem sigma1_rotations_not_injective :93 ¬ Function.Injective (fun x : Word => rotr x 17 ^^^ rotr x 19) := fun h =>94 absurd (h (a₁ := 0) (a₂ := 0xFFFFFFFF) (by decide)) (by decide)9596/-- All-ones mask when bit `i` of `x` is set, zero otherwise (row selector for a GF(2) matrix). -/97def bitMask (x : Word) (i : Nat) : Word := if x.getLsbD i then BitVec.allOnes 32 else 09899-- Explicit inverses, computed over GF(2) by `scripts/gf2_rank.py --lean` and verified below.100-- Σ0⁻¹ and Σ1⁻¹ are themselves XORs of 17 rotations (the inverse of a unit of101-- GF(2)[ρ]/(ρ³²−1) is a polynomial in ρ); σ0⁻¹ and σ1⁻¹ are general 32×32 GF(2) matrices,102-- written column by column (`bitMask x i &&& cᵢ` = column `i` if bit `i` of `x` is set).103104def Sigma0Inv (x : Word) : Word :=105 rotr x 0 ^^^ rotr x 1 ^^^ rotr x 2 ^^^ rotr x 5 ^^^ rotr x 7 ^^^ rotr x 8 ^^^ rotr x 9 ^^^106 rotr x 10 ^^^ rotr x 12 ^^^ rotr x 16 ^^^ rotr x 17 ^^^ rotr x 19 ^^^ rotr x 22 ^^^107 rotr x 23 ^^^ rotr x 25 ^^^ rotr x 29 ^^^ rotr x 30108109def Sigma1Inv (x : Word) : Word :=110 rotr x 2 ^^^ rotr x 3 ^^^ rotr x 5 ^^^ rotr x 7 ^^^ rotr x 9 ^^^ rotr x 11 ^^^ rotr x 12 ^^^111 rotr x 13 ^^^ rotr x 18 ^^^ rotr x 21 ^^^ rotr x 22 ^^^ rotr x 23 ^^^ rotr x 24 ^^^112 rotr x 26 ^^^ rotr x 27 ^^^ rotr x 29 ^^^ rotr x 30113114def sigma0Inv (x : Word) : Word :=115 bitMask x 0 &&& 0x185744e9#32 ^^^116 bitMask x 1 &&& 0x30ae89d2#32 ^^^117 bitMask x 2 &&& 0x615d13a4#32 ^^^118 bitMask x 3 &&& 0xdaed63a1#32 ^^^119 bitMask x 4 &&& 0x9cd03a8e#32 ^^^120 bitMask x 5 &&& 0x08fdcc39#32 ^^^121 bitMask x 6 &&& 0x11fb9872#32 ^^^122 bitMask x 7 &&& 0x23f730e4#32 ^^^123 bitMask x 8 &&& 0x5fb92521#32 ^^^124 bitMask x 9 &&& 0xbf724a42#32 ^^^125 bitMask x 10 &&& 0x57ee6948#32 ^^^126 bitMask x 11 &&& 0xafdcd290#32 ^^^127 bitMask x 12 &&& 0x76b358ec#32 ^^^128 bitMask x 13 &&& 0xf531f531#32 ^^^129 bitMask x 14 &&& 0xc36917ae#32 ^^^130 bitMask x 15 &&& 0xb78f9679#32 ^^^131 bitMask x 16 &&& 0x4615d13e#32 ^^^132 bitMask x 17 &&& 0x947ce695#32 ^^^133 bitMask x 18 &&& 0x19a4740f#32 ^^^134 bitMask x 19 &&& 0x2b1facf7#32 ^^^135 bitMask x 20 &&& 0x4e681d07#32 ^^^136 bitMask x 21 &&& 0x84877ee7#32 ^^^137 bitMask x 22 &&& 0x385344eb#32 ^^^138 bitMask x 23 &&& 0x70a689d6#32 ^^^139 bitMask x 24 &&& 0xf91a5745#32 ^^^140 bitMask x 25 &&& 0xc36917af#32 ^^^141 bitMask x 26 &&& 0xb78f967b#32 ^^^142 bitMask x 27 &&& 0x4615d13a#32 ^^^143 bitMask x 28 &&& 0x8c2ba274#32 ^^^144 bitMask x 29 &&& 0x290afdcd#32 ^^^145 bitMask x 30 &&& 0x4a42bf73#32 ^^^146 bitMask x 31 &&& 0x94857ee6#32147148def sigma1Inv (x : Word) : Word :=149 bitMask x 0 &&& 0x2ccfffed#32 ^^^150 bitMask x 1 &&& 0x75500037#32 ^^^151 bitMask x 2 &&& 0xeaa0006e#32 ^^^152 bitMask x 3 &&& 0x589d5570#32 ^^^153 bitMask x 4 &&& 0xb13aaae0#32 ^^^154 bitMask x 5 &&& 0xc367ff81#32 ^^^155 bitMask x 6 &&& 0x27dd5543#32 ^^^156 bitMask x 7 &&& 0x4fbaaa86#32 ^^^157 bitMask x 8 &&& 0xb3baaae1#32 ^^^158 bitMask x 9 &&& 0xc667ff83#32 ^^^159 bitMask x 10 &&& 0x2ddd5547#32 ^^^160 bitMask x 11 &&& 0x5bbaaa8e#32 ^^^161 bitMask x 12 &&& 0x9bbaaaf1#32 ^^^162 bitMask x 13 &&& 0x9667ffa3#32 ^^^163 bitMask x 14 &&& 0x8ddd5507#32 ^^^164 bitMask x 15 &&& 0x9667ffa2#32 ^^^165 bitMask x 16 &&& 0x8ddd5505#32 ^^^166 bitMask x 17 &&& 0x9667ffa6#32 ^^^167 bitMask x 18 &&& 0x8ddd550d#32 ^^^168 bitMask x 19 &&& 0x9667ffb6#32 ^^^169 bitMask x 20 &&& 0x8ddd552d#32 ^^^170 bitMask x 21 &&& 0x9667fff6#32 ^^^171 bitMask x 22 &&& 0x8ddd55ad#32 ^^^172 bitMask x 23 &&& 0x9667fef6#32 ^^^173 bitMask x 24 &&& 0x8ddd57ad#32 ^^^174 bitMask x 25 &&& 0xbaa8051b#32 ^^^175 bitMask x 26 &&& 0xf88d5f9a#32 ^^^176 bitMask x 27 &&& 0x50081575#32 ^^^177 bitMask x 28 &&& 0xa0102aea#32 ^^^178 bitMask x 29 &&& 0xe132ff95#32 ^^^179 bitMask x 30 &&& 0x6377556b#32 ^^^180 bitMask x 31 &&& 0xc6eeaad6#32181182/-! #### Proof strategy for the inverse identities183184`Sigma0Inv (Sigma0 x) = x` is a pure parity (XOR) identity in 32 variables: each output bit is the185XOR of 51 input-bit occurrences that cancel pairwise. CDCL SAT solvers handle such parity186instances badly (the direct `bv_decide` call exceeds a 10 s timeout, see README). We therefore187(i) prove GF(2)-linearity of the inverses by the general lemmas `rotr_xor` / `bitMask_xor`188(bit-level, no SAT) and `ac_rfl`; (ii) check the identity on the two 16-bit halves of `x` with189`bv_decide` (16 free variables: trivial for SAT); (iii) glue with `inv_of_halves`. -/190191/-- Rotation distributes over XOR (bit-level proof from core's `getLsbD_rotateRight`). -/192theorem rotr_xor (x y : Word) (k : Nat) : rotr (x ^^^ y) k = rotr x k ^^^ rotr y k := by193 apply BitVec.eq_of_getLsbD_eq194 intro i195 simp only [rotr, BitVec.getLsbD_rotateRight, BitVec.getLsbD_xor]196 by_cases h : i < 32 - k % 32 <;> by_cases h' : i < 32 <;> simp [h, h']197198theorem bitMask_xor (x y : Word) (i : Nat) :199 bitMask (x ^^^ y) i = bitMask x i ^^^ bitMask y i := by200 unfold bitMask201 simp only [BitVec.getLsbD_xor]202 cases x.getLsbD i <;> cases y.getLsbD i <;> simp203204theorem xor_and_right (a b c : Word) : (a ^^^ b) &&& c = (a &&& c) ^^^ (b &&& c) := by205 bv_decide206207theorem Sigma0Inv_xor (x y : Word) : Sigma0Inv (x ^^^ y) = Sigma0Inv x ^^^ Sigma0Inv y := by208 simp only [Sigma0Inv, rotr_xor]; ac_rfl209theorem Sigma1Inv_xor (x y : Word) : Sigma1Inv (x ^^^ y) = Sigma1Inv x ^^^ Sigma1Inv y := by210 simp only [Sigma1Inv, rotr_xor]; ac_rfl211theorem sigma0Inv_xor (x y : Word) : sigma0Inv (x ^^^ y) = sigma0Inv x ^^^ sigma0Inv y := by212 simp only [sigma0Inv, bitMask_xor, xor_and_right]; ac_rfl213theorem sigma1Inv_xor (x y : Word) : sigma1Inv (x ^^^ y) = sigma1Inv x ^^^ sigma1Inv y := by214 simp only [sigma1Inv, bitMask_xor, xor_and_right]; ac_rfl215216/-- Two GF(2)-linear maps whose composite fixes each of the four bytes of `x` compose to the217identity. (Bytes rather than 16-bit halves: an 8-variable SAT instance yields a ~0.6 MB LRAT218certificate, a 16-variable one ~100 MB, and the certificates are stored in the `.olean`.) -/219theorem inv_of_quarters (f g : Word → Word)220 (hf : ∀ x y, f (x ^^^ y) = f x ^^^ f y) (hg : ∀ x y, g (x ^^^ y) = g x ^^^ g y)221 (h0 : ∀ x, g (f (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32)222 (h1 : ∀ x, g (f (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32)223 (h2 : ∀ x, g (f (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32)224 (h3 : ∀ x, g (f (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32) :225 ∀ x, g (f x) = x := by226 intro x227 have hsplit : x = (x &&& 0x000000FF#32) ^^^ (x &&& 0x0000FF00#32) ^^^ (x &&& 0x00FF0000#32)228 ^^^ (x &&& 0xFF000000#32) := by bv_decide229 calc g (f x) = g (f ((x &&& 0x000000FF#32) ^^^ (x &&& 0x0000FF00#32) ^^^ (x &&& 0x00FF0000#32)230 ^^^ (x &&& 0xFF000000#32))) := by rw [← hsplit]231 _ = g (f (x &&& 0x000000FF#32)) ^^^ g (f (x &&& 0x0000FF00#32)) ^^^ g (f (x &&& 0x00FF0000#32))232 ^^^ g (f (x &&& 0xFF000000#32)) := by rw [hf, hf, hf, hg, hg, hg]233 _ = x := by rw [h0, h1, h2, h3, ← hsplit]234235-- Byte instances (each a small SAT problem with 8 free variables).236theorem Sigma0Inv_Sigma0_b0 (x : Word) :237 Sigma0Inv (Sigma0 (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32 := by238 unfold Sigma0Inv Sigma0 rotr; bv_decide239theorem Sigma0Inv_Sigma0_b1 (x : Word) :240 Sigma0Inv (Sigma0 (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32 := by241 unfold Sigma0Inv Sigma0 rotr; bv_decide242theorem Sigma0Inv_Sigma0_b2 (x : Word) :243 Sigma0Inv (Sigma0 (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32 := by244 unfold Sigma0Inv Sigma0 rotr; bv_decide245theorem Sigma0Inv_Sigma0_b3 (x : Word) :246 Sigma0Inv (Sigma0 (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32 := by247 unfold Sigma0Inv Sigma0 rotr; bv_decide248theorem Sigma0_Sigma0Inv_b0 (x : Word) :249 Sigma0 (Sigma0Inv (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32 := by250 unfold Sigma0Inv Sigma0 rotr; bv_decide251theorem Sigma0_Sigma0Inv_b1 (x : Word) :252 Sigma0 (Sigma0Inv (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32 := by253 unfold Sigma0Inv Sigma0 rotr; bv_decide254theorem Sigma0_Sigma0Inv_b2 (x : Word) :255 Sigma0 (Sigma0Inv (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32 := by256 unfold Sigma0Inv Sigma0 rotr; bv_decide257theorem Sigma0_Sigma0Inv_b3 (x : Word) :258 Sigma0 (Sigma0Inv (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32 := by259 unfold Sigma0Inv Sigma0 rotr; bv_decide260theorem Sigma1Inv_Sigma1_b0 (x : Word) :261 Sigma1Inv (Sigma1 (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32 := by262 unfold Sigma1Inv Sigma1 rotr; bv_decide263theorem Sigma1Inv_Sigma1_b1 (x : Word) :264 Sigma1Inv (Sigma1 (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32 := by265 unfold Sigma1Inv Sigma1 rotr; bv_decide266theorem Sigma1Inv_Sigma1_b2 (x : Word) :267 Sigma1Inv (Sigma1 (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32 := by268 unfold Sigma1Inv Sigma1 rotr; bv_decide269theorem Sigma1Inv_Sigma1_b3 (x : Word) :270 Sigma1Inv (Sigma1 (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32 := by271 unfold Sigma1Inv Sigma1 rotr; bv_decide272theorem Sigma1_Sigma1Inv_b0 (x : Word) :273 Sigma1 (Sigma1Inv (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32 := by274 unfold Sigma1Inv Sigma1 rotr; bv_decide275theorem Sigma1_Sigma1Inv_b1 (x : Word) :276 Sigma1 (Sigma1Inv (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32 := by277 unfold Sigma1Inv Sigma1 rotr; bv_decide278theorem Sigma1_Sigma1Inv_b2 (x : Word) :279 Sigma1 (Sigma1Inv (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32 := by280 unfold Sigma1Inv Sigma1 rotr; bv_decide281theorem Sigma1_Sigma1Inv_b3 (x : Word) :282 Sigma1 (Sigma1Inv (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32 := by283 unfold Sigma1Inv Sigma1 rotr; bv_decide284theorem sigma0Inv_sigma0_b0 (x : Word) :285 sigma0Inv (sigma0 (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32 := by286 unfold sigma0Inv sigma0 bitMask rotr; bv_decide287theorem sigma0Inv_sigma0_b1 (x : Word) :288 sigma0Inv (sigma0 (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32 := by289 unfold sigma0Inv sigma0 bitMask rotr; bv_decide290theorem sigma0Inv_sigma0_b2 (x : Word) :291 sigma0Inv (sigma0 (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32 := by292 unfold sigma0Inv sigma0 bitMask rotr; bv_decide293theorem sigma0Inv_sigma0_b3 (x : Word) :294 sigma0Inv (sigma0 (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32 := by295 unfold sigma0Inv sigma0 bitMask rotr; bv_decide296theorem sigma0_sigma0Inv_b0 (x : Word) :297 sigma0 (sigma0Inv (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32 := by298 unfold sigma0Inv sigma0 bitMask rotr; bv_decide299theorem sigma0_sigma0Inv_b1 (x : Word) :300 sigma0 (sigma0Inv (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32 := by301 unfold sigma0Inv sigma0 bitMask rotr; bv_decide302theorem sigma0_sigma0Inv_b2 (x : Word) :303 sigma0 (sigma0Inv (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32 := by304 unfold sigma0Inv sigma0 bitMask rotr; bv_decide305theorem sigma0_sigma0Inv_b3 (x : Word) :306 sigma0 (sigma0Inv (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32 := by307 unfold sigma0Inv sigma0 bitMask rotr; bv_decide308theorem sigma1Inv_sigma1_b0 (x : Word) :309 sigma1Inv (sigma1 (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32 := by310 unfold sigma1Inv sigma1 bitMask rotr; bv_decide311theorem sigma1Inv_sigma1_b1 (x : Word) :312 sigma1Inv (sigma1 (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32 := by313 unfold sigma1Inv sigma1 bitMask rotr; bv_decide314theorem sigma1Inv_sigma1_b2 (x : Word) :315 sigma1Inv (sigma1 (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32 := by316 unfold sigma1Inv sigma1 bitMask rotr; bv_decide317theorem sigma1Inv_sigma1_b3 (x : Word) :318 sigma1Inv (sigma1 (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32 := by319 unfold sigma1Inv sigma1 bitMask rotr; bv_decide320theorem sigma1_sigma1Inv_b0 (x : Word) :321 sigma1 (sigma1Inv (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32 := by322 unfold sigma1Inv sigma1 bitMask rotr; bv_decide323theorem sigma1_sigma1Inv_b1 (x : Word) :324 sigma1 (sigma1Inv (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32 := by325 unfold sigma1Inv sigma1 bitMask rotr; bv_decide326theorem sigma1_sigma1Inv_b2 (x : Word) :327 sigma1 (sigma1Inv (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32 := by328 unfold sigma1Inv sigma1 bitMask rotr; bv_decide329theorem sigma1_sigma1Inv_b3 (x : Word) :330 sigma1 (sigma1Inv (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32 := by331 unfold sigma1Inv sigma1 bitMask rotr; bv_decide332333/-- `Sigma0Inv ∘ Sigma0 = id`. -/334theorem Sigma0Inv_Sigma0 : ∀ x, Sigma0Inv (Sigma0 x) = x :=335 inv_of_quarters Sigma0 Sigma0Inv Sigma0_xor Sigma0Inv_xor Sigma0Inv_Sigma0_b0 Sigma0Inv_Sigma0_b1 Sigma0Inv_Sigma0_b2 Sigma0Inv_Sigma0_b3336/-- `Sigma0 ∘ Sigma0Inv = id`. -/337theorem Sigma0_Sigma0Inv : ∀ x, Sigma0 (Sigma0Inv x) = x :=338 inv_of_quarters Sigma0Inv Sigma0 Sigma0Inv_xor Sigma0_xor Sigma0_Sigma0Inv_b0 Sigma0_Sigma0Inv_b1 Sigma0_Sigma0Inv_b2 Sigma0_Sigma0Inv_b3339/-- `Sigma1Inv ∘ Sigma1 = id`. -/340theorem Sigma1Inv_Sigma1 : ∀ x, Sigma1Inv (Sigma1 x) = x :=341 inv_of_quarters Sigma1 Sigma1Inv Sigma1_xor Sigma1Inv_xor Sigma1Inv_Sigma1_b0 Sigma1Inv_Sigma1_b1 Sigma1Inv_Sigma1_b2 Sigma1Inv_Sigma1_b3342/-- `Sigma1 ∘ Sigma1Inv = id`. -/343theorem Sigma1_Sigma1Inv : ∀ x, Sigma1 (Sigma1Inv x) = x :=344 inv_of_quarters Sigma1Inv Sigma1 Sigma1Inv_xor Sigma1_xor Sigma1_Sigma1Inv_b0 Sigma1_Sigma1Inv_b1 Sigma1_Sigma1Inv_b2 Sigma1_Sigma1Inv_b3345/-- `sigma0Inv ∘ sigma0 = id`. -/346theorem sigma0Inv_sigma0 : ∀ x, sigma0Inv (sigma0 x) = x :=347 inv_of_quarters sigma0 sigma0Inv sigma0_xor sigma0Inv_xor sigma0Inv_sigma0_b0 sigma0Inv_sigma0_b1 sigma0Inv_sigma0_b2 sigma0Inv_sigma0_b3348/-- `sigma0 ∘ sigma0Inv = id`. -/349theorem sigma0_sigma0Inv : ∀ x, sigma0 (sigma0Inv x) = x :=350 inv_of_quarters sigma0Inv sigma0 sigma0Inv_xor sigma0_xor sigma0_sigma0Inv_b0 sigma0_sigma0Inv_b1 sigma0_sigma0Inv_b2 sigma0_sigma0Inv_b3351/-- `sigma1Inv ∘ sigma1 = id`. -/352theorem sigma1Inv_sigma1 : ∀ x, sigma1Inv (sigma1 x) = x :=353 inv_of_quarters sigma1 sigma1Inv sigma1_xor sigma1Inv_xor sigma1Inv_sigma1_b0 sigma1Inv_sigma1_b1 sigma1Inv_sigma1_b2 sigma1Inv_sigma1_b3354/-- `sigma1 ∘ sigma1Inv = id`. -/355theorem sigma1_sigma1Inv : ∀ x, sigma1 (sigma1Inv x) = x :=356 inv_of_quarters sigma1Inv sigma1 sigma1Inv_xor sigma1_xor sigma1_sigma1Inv_b0 sigma1_sigma1Inv_b1 sigma1_sigma1Inv_b2 sigma1_sigma1Inv_b3357358/-- Σ0 is a bijection of `BitVec 32` (explicit inverse `Sigma0Inv`). -/359theorem Sigma0_bijective : Bijective Sigma0 :=360 ⟨Sigma0_injective, fun y => ⟨Sigma0Inv y, Sigma0_Sigma0Inv y⟩⟩361theorem Sigma1_bijective : Bijective Sigma1 :=362 ⟨Sigma1_injective, fun y => ⟨Sigma1Inv y, Sigma1_Sigma1Inv y⟩⟩363/-- σ0 is a bijection of `BitVec 32` (explicit inverse `sigma0Inv`): the shift does not364destroy invertibility; the kernel of the GF(2) map is trivial. -/365theorem sigma0_bijective : Bijective sigma0 :=366 ⟨sigma0_injective, fun y => ⟨sigma0Inv y, sigma0_sigma0Inv y⟩⟩367theorem sigma1_bijective : Bijective sigma1 :=368 ⟨sigma1_injective, fun y => ⟨sigma1Inv y, sigma1_sigma1Inv y⟩⟩369370end Wp34371