/- WP34 — Stage 5 formal verification. SHA-256 (FIPS 180-4) word functions on `BitVec 32`, transcribed from `src/wp34/sha256.py`. Everything in this file is machine-checked by Lean 4 core only (no Mathlib). The `bv_decide` tactic bit-blasts the goal, calls the bundled CaDiCaL SAT solver and re-checks the LRAT certificate it returns inside Lean's kernel. -/ import Std.Tactic.BVDecide namespace Wp34 /-- A SHA-256 word. -/ abbrev Word := BitVec 32 /-- Right rotation (`rotr` in `sha256.py`). -/ def rotr (x : Word) (k : Nat) : Word := x.rotateRight k -- The four sigma functions and the two Boolean functions, exactly as in `sha256.py`. def Sigma0 (x : Word) : Word := rotr x 2 ^^^ rotr x 13 ^^^ rotr x 22 def Sigma1 (x : Word) : Word := rotr x 6 ^^^ rotr x 11 ^^^ rotr x 25 def sigma0 (x : Word) : Word := rotr x 7 ^^^ rotr x 18 ^^^ (x >>> 3) def sigma1 (x : Word) : Word := rotr x 17 ^^^ rotr x 19 ^^^ (x >>> 10) def Ch (x y z : Word) : Word := (x &&& y) ^^^ (~~~x &&& z) def Maj (x y z : Word) : Word := (x &&& y) ^^^ (x &&& z) ^^^ (y &&& z) /-! ### 1(a)–(b) Optimised forms of `Ch` and `Maj` (used by most implementations) -/ /-- `Ch x y z = ((y ^ z) & x) ^ z` — one fewer operation and no complement. -/ theorem Ch_opt (x y z : Word) : Ch x y z = ((y ^^^ z) &&& x) ^^^ z := by unfold Ch; bv_decide /-- `Maj x y z = (x & (y | z)) | (y & z)`. -/ theorem Maj_opt_or (x y z : Word) : Maj x y z = (x &&& (y ||| z)) ||| (y &&& z) := by unfold Maj; bv_decide /-- `Maj x y z = ((x ^ y) & (y ^ z)) ^ y`. -/ theorem Maj_opt_xor (x y z : Word) : Maj x y z = ((x ^^^ y) &&& (y ^^^ z)) ^^^ y := by unfold Maj; bv_decide /-- `Maj` is symmetric in its arguments (used implicitly by the local-collision analysis). -/ theorem Maj_comm (x y z : Word) : Maj x y z = Maj y x z ∧ Maj x y z = Maj x z y := by unfold Maj; bv_decide /-! ### 1(c) GF(2)-linearity of Σ0, Σ1, σ0, σ1 -/ theorem Sigma0_xor (x y : Word) : Sigma0 (x ^^^ y) = Sigma0 x ^^^ Sigma0 y := by unfold Sigma0 rotr; bv_decide theorem Sigma1_xor (x y : Word) : Sigma1 (x ^^^ y) = Sigma1 x ^^^ Sigma1 y := by unfold Sigma1 rotr; bv_decide theorem sigma0_xor (x y : Word) : sigma0 (x ^^^ y) = sigma0 x ^^^ sigma0 y := by unfold sigma0 rotr; bv_decide theorem sigma1_xor (x y : Word) : sigma1 (x ^^^ y) = sigma1 x ^^^ sigma1 y := by unfold sigma1 rotr; bv_decide theorem Sigma0_zero : Sigma0 0 = 0 := by unfold Sigma0 rotr; bv_decide theorem Sigma1_zero : Sigma1 0 = 0 := by unfold Sigma1 rotr; bv_decide theorem sigma0_zero : sigma0 0 = 0 := by unfold sigma0 rotr; bv_decide theorem sigma1_zero : sigma1 0 = 0 := by unfold sigma1 rotr; bv_decide /-! ### 1(d)–(e) Injectivity and explicit inverses `Function.Injective` is Lean-core. Core has no `Function.Bijective`/`Surjective`, so we state bijectivity as "injective and has an explicit right inverse" through the definition below. -/ /-- Bijectivity without Mathlib: injective and surjective. -/ def Bijective {α β : Type} (f : α → β) : Prop := Function.Injective f ∧ ∀ y, ∃ x, f x = y theorem Sigma0_injective : Function.Injective Sigma0 := fun x y h => by unfold Sigma0 rotr at h; bv_decide theorem Sigma1_injective : Function.Injective Sigma1 := fun x y h => by unfold Sigma1 rotr at h; bv_decide /-- σ0 contains a logical shift, yet it IS injective on 32 bits (GF(2) rank 32, see `scripts/gf2_rank.py`); `bv_decide` finds no counter-example (UNSAT, certificate checked). -/ theorem sigma0_injective : Function.Injective sigma0 := fun x y h => by unfold sigma0 rotr at h; bv_decide /-- Same for σ1. -/ theorem sigma1_injective : Function.Injective sigma1 := fun x y h => by unfold sigma1 rotr at h; bv_decide /-- Control: the shift term alone is NOT injective (`0 >>> 3 = 1 >>> 3`). -/ theorem shr3_not_injective : ¬ Function.Injective (fun x : Word => x >>> 3) := fun h => absurd (h (a₁ := 0) (a₂ := 1) (by decide)) (by decide) /-- Control: the rotation part of σ0 alone is NOT injective either: `rotr x 7 ^ rotr x 18 = x ^ rotr x 11` up to rotation, whose kernel is `{0, 0xFFFFFFFF}`. -/ theorem sigma0_rotations_not_injective : ¬ Function.Injective (fun x : Word => rotr x 7 ^^^ rotr x 18) := fun h => absurd (h (a₁ := 0) (a₂ := 0xFFFFFFFF) (by decide)) (by decide) /-- Control: the rotation part of σ1 alone is NOT injective (`x ^ rotr x 2` kills `0xFFFFFFFF`). -/ theorem sigma1_rotations_not_injective : ¬ Function.Injective (fun x : Word => rotr x 17 ^^^ rotr x 19) := fun h => absurd (h (a₁ := 0) (a₂ := 0xFFFFFFFF) (by decide)) (by decide) /-- All-ones mask when bit `i` of `x` is set, zero otherwise (row selector for a GF(2) matrix). -/ def bitMask (x : Word) (i : Nat) : Word := if x.getLsbD i then BitVec.allOnes 32 else 0 -- Explicit inverses, computed over GF(2) by `scripts/gf2_rank.py --lean` and verified below. -- Σ0⁻¹ and Σ1⁻¹ are themselves XORs of 17 rotations (the inverse of a unit of -- GF(2)[ρ]/(ρ³²−1) is a polynomial in ρ); σ0⁻¹ and σ1⁻¹ are general 32×32 GF(2) matrices, -- written column by column (`bitMask x i &&& cᵢ` = column `i` if bit `i` of `x` is set). def Sigma0Inv (x : Word) : Word := rotr x 0 ^^^ rotr x 1 ^^^ rotr x 2 ^^^ rotr x 5 ^^^ rotr x 7 ^^^ rotr x 8 ^^^ rotr x 9 ^^^ rotr x 10 ^^^ rotr x 12 ^^^ rotr x 16 ^^^ rotr x 17 ^^^ rotr x 19 ^^^ rotr x 22 ^^^ rotr x 23 ^^^ rotr x 25 ^^^ rotr x 29 ^^^ rotr x 30 def Sigma1Inv (x : Word) : Word := rotr x 2 ^^^ rotr x 3 ^^^ rotr x 5 ^^^ rotr x 7 ^^^ rotr x 9 ^^^ rotr x 11 ^^^ rotr x 12 ^^^ rotr x 13 ^^^ rotr x 18 ^^^ rotr x 21 ^^^ rotr x 22 ^^^ rotr x 23 ^^^ rotr x 24 ^^^ rotr x 26 ^^^ rotr x 27 ^^^ rotr x 29 ^^^ rotr x 30 def sigma0Inv (x : Word) : Word := bitMask x 0 &&& 0x185744e9#32 ^^^ bitMask x 1 &&& 0x30ae89d2#32 ^^^ bitMask x 2 &&& 0x615d13a4#32 ^^^ bitMask x 3 &&& 0xdaed63a1#32 ^^^ bitMask x 4 &&& 0x9cd03a8e#32 ^^^ bitMask x 5 &&& 0x08fdcc39#32 ^^^ bitMask x 6 &&& 0x11fb9872#32 ^^^ bitMask x 7 &&& 0x23f730e4#32 ^^^ bitMask x 8 &&& 0x5fb92521#32 ^^^ bitMask x 9 &&& 0xbf724a42#32 ^^^ bitMask x 10 &&& 0x57ee6948#32 ^^^ bitMask x 11 &&& 0xafdcd290#32 ^^^ bitMask x 12 &&& 0x76b358ec#32 ^^^ bitMask x 13 &&& 0xf531f531#32 ^^^ bitMask x 14 &&& 0xc36917ae#32 ^^^ bitMask x 15 &&& 0xb78f9679#32 ^^^ bitMask x 16 &&& 0x4615d13e#32 ^^^ bitMask x 17 &&& 0x947ce695#32 ^^^ bitMask x 18 &&& 0x19a4740f#32 ^^^ bitMask x 19 &&& 0x2b1facf7#32 ^^^ bitMask x 20 &&& 0x4e681d07#32 ^^^ bitMask x 21 &&& 0x84877ee7#32 ^^^ bitMask x 22 &&& 0x385344eb#32 ^^^ bitMask x 23 &&& 0x70a689d6#32 ^^^ bitMask x 24 &&& 0xf91a5745#32 ^^^ bitMask x 25 &&& 0xc36917af#32 ^^^ bitMask x 26 &&& 0xb78f967b#32 ^^^ bitMask x 27 &&& 0x4615d13a#32 ^^^ bitMask x 28 &&& 0x8c2ba274#32 ^^^ bitMask x 29 &&& 0x290afdcd#32 ^^^ bitMask x 30 &&& 0x4a42bf73#32 ^^^ bitMask x 31 &&& 0x94857ee6#32 def sigma1Inv (x : Word) : Word := bitMask x 0 &&& 0x2ccfffed#32 ^^^ bitMask x 1 &&& 0x75500037#32 ^^^ bitMask x 2 &&& 0xeaa0006e#32 ^^^ bitMask x 3 &&& 0x589d5570#32 ^^^ bitMask x 4 &&& 0xb13aaae0#32 ^^^ bitMask x 5 &&& 0xc367ff81#32 ^^^ bitMask x 6 &&& 0x27dd5543#32 ^^^ bitMask x 7 &&& 0x4fbaaa86#32 ^^^ bitMask x 8 &&& 0xb3baaae1#32 ^^^ bitMask x 9 &&& 0xc667ff83#32 ^^^ bitMask x 10 &&& 0x2ddd5547#32 ^^^ bitMask x 11 &&& 0x5bbaaa8e#32 ^^^ bitMask x 12 &&& 0x9bbaaaf1#32 ^^^ bitMask x 13 &&& 0x9667ffa3#32 ^^^ bitMask x 14 &&& 0x8ddd5507#32 ^^^ bitMask x 15 &&& 0x9667ffa2#32 ^^^ bitMask x 16 &&& 0x8ddd5505#32 ^^^ bitMask x 17 &&& 0x9667ffa6#32 ^^^ bitMask x 18 &&& 0x8ddd550d#32 ^^^ bitMask x 19 &&& 0x9667ffb6#32 ^^^ bitMask x 20 &&& 0x8ddd552d#32 ^^^ bitMask x 21 &&& 0x9667fff6#32 ^^^ bitMask x 22 &&& 0x8ddd55ad#32 ^^^ bitMask x 23 &&& 0x9667fef6#32 ^^^ bitMask x 24 &&& 0x8ddd57ad#32 ^^^ bitMask x 25 &&& 0xbaa8051b#32 ^^^ bitMask x 26 &&& 0xf88d5f9a#32 ^^^ bitMask x 27 &&& 0x50081575#32 ^^^ bitMask x 28 &&& 0xa0102aea#32 ^^^ bitMask x 29 &&& 0xe132ff95#32 ^^^ bitMask x 30 &&& 0x6377556b#32 ^^^ bitMask x 31 &&& 0xc6eeaad6#32 /-! #### Proof strategy for the inverse identities `Sigma0Inv (Sigma0 x) = x` is a pure parity (XOR) identity in 32 variables: each output bit is the XOR of 51 input-bit occurrences that cancel pairwise. CDCL SAT solvers handle such parity instances badly (the direct `bv_decide` call exceeds a 10 s timeout, see README). We therefore (i) prove GF(2)-linearity of the inverses by the general lemmas `rotr_xor` / `bitMask_xor` (bit-level, no SAT) and `ac_rfl`; (ii) check the identity on the two 16-bit halves of `x` with `bv_decide` (16 free variables: trivial for SAT); (iii) glue with `inv_of_halves`. -/ /-- Rotation distributes over XOR (bit-level proof from core's `getLsbD_rotateRight`). -/ theorem rotr_xor (x y : Word) (k : Nat) : rotr (x ^^^ y) k = rotr x k ^^^ rotr y k := by apply BitVec.eq_of_getLsbD_eq intro i simp only [rotr, BitVec.getLsbD_rotateRight, BitVec.getLsbD_xor] by_cases h : i < 32 - k % 32 <;> by_cases h' : i < 32 <;> simp [h, h'] theorem bitMask_xor (x y : Word) (i : Nat) : bitMask (x ^^^ y) i = bitMask x i ^^^ bitMask y i := by unfold bitMask simp only [BitVec.getLsbD_xor] cases x.getLsbD i <;> cases y.getLsbD i <;> simp theorem xor_and_right (a b c : Word) : (a ^^^ b) &&& c = (a &&& c) ^^^ (b &&& c) := by bv_decide theorem Sigma0Inv_xor (x y : Word) : Sigma0Inv (x ^^^ y) = Sigma0Inv x ^^^ Sigma0Inv y := by simp only [Sigma0Inv, rotr_xor]; ac_rfl theorem Sigma1Inv_xor (x y : Word) : Sigma1Inv (x ^^^ y) = Sigma1Inv x ^^^ Sigma1Inv y := by simp only [Sigma1Inv, rotr_xor]; ac_rfl theorem sigma0Inv_xor (x y : Word) : sigma0Inv (x ^^^ y) = sigma0Inv x ^^^ sigma0Inv y := by simp only [sigma0Inv, bitMask_xor, xor_and_right]; ac_rfl theorem sigma1Inv_xor (x y : Word) : sigma1Inv (x ^^^ y) = sigma1Inv x ^^^ sigma1Inv y := by simp only [sigma1Inv, bitMask_xor, xor_and_right]; ac_rfl /-- Two GF(2)-linear maps whose composite fixes each of the four bytes of `x` compose to the identity. (Bytes rather than 16-bit halves: an 8-variable SAT instance yields a ~0.6 MB LRAT certificate, a 16-variable one ~100 MB, and the certificates are stored in the `.olean`.) -/ theorem inv_of_quarters (f g : Word → Word) (hf : ∀ x y, f (x ^^^ y) = f x ^^^ f y) (hg : ∀ x y, g (x ^^^ y) = g x ^^^ g y) (h0 : ∀ x, g (f (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32) (h1 : ∀ x, g (f (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32) (h2 : ∀ x, g (f (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32) (h3 : ∀ x, g (f (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32) : ∀ x, g (f x) = x := by intro x have hsplit : x = (x &&& 0x000000FF#32) ^^^ (x &&& 0x0000FF00#32) ^^^ (x &&& 0x00FF0000#32) ^^^ (x &&& 0xFF000000#32) := by bv_decide calc g (f x) = g (f ((x &&& 0x000000FF#32) ^^^ (x &&& 0x0000FF00#32) ^^^ (x &&& 0x00FF0000#32) ^^^ (x &&& 0xFF000000#32))) := by rw [← hsplit] _ = g (f (x &&& 0x000000FF#32)) ^^^ g (f (x &&& 0x0000FF00#32)) ^^^ g (f (x &&& 0x00FF0000#32)) ^^^ g (f (x &&& 0xFF000000#32)) := by rw [hf, hf, hf, hg, hg, hg] _ = x := by rw [h0, h1, h2, h3, ← hsplit] -- Byte instances (each a small SAT problem with 8 free variables). theorem Sigma0Inv_Sigma0_b0 (x : Word) : Sigma0Inv (Sigma0 (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32 := by unfold Sigma0Inv Sigma0 rotr; bv_decide theorem Sigma0Inv_Sigma0_b1 (x : Word) : Sigma0Inv (Sigma0 (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32 := by unfold Sigma0Inv Sigma0 rotr; bv_decide theorem Sigma0Inv_Sigma0_b2 (x : Word) : Sigma0Inv (Sigma0 (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32 := by unfold Sigma0Inv Sigma0 rotr; bv_decide theorem Sigma0Inv_Sigma0_b3 (x : Word) : Sigma0Inv (Sigma0 (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32 := by unfold Sigma0Inv Sigma0 rotr; bv_decide theorem Sigma0_Sigma0Inv_b0 (x : Word) : Sigma0 (Sigma0Inv (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32 := by unfold Sigma0Inv Sigma0 rotr; bv_decide theorem Sigma0_Sigma0Inv_b1 (x : Word) : Sigma0 (Sigma0Inv (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32 := by unfold Sigma0Inv Sigma0 rotr; bv_decide theorem Sigma0_Sigma0Inv_b2 (x : Word) : Sigma0 (Sigma0Inv (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32 := by unfold Sigma0Inv Sigma0 rotr; bv_decide theorem Sigma0_Sigma0Inv_b3 (x : Word) : Sigma0 (Sigma0Inv (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32 := by unfold Sigma0Inv Sigma0 rotr; bv_decide theorem Sigma1Inv_Sigma1_b0 (x : Word) : Sigma1Inv (Sigma1 (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32 := by unfold Sigma1Inv Sigma1 rotr; bv_decide theorem Sigma1Inv_Sigma1_b1 (x : Word) : Sigma1Inv (Sigma1 (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32 := by unfold Sigma1Inv Sigma1 rotr; bv_decide theorem Sigma1Inv_Sigma1_b2 (x : Word) : Sigma1Inv (Sigma1 (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32 := by unfold Sigma1Inv Sigma1 rotr; bv_decide theorem Sigma1Inv_Sigma1_b3 (x : Word) : Sigma1Inv (Sigma1 (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32 := by unfold Sigma1Inv Sigma1 rotr; bv_decide theorem Sigma1_Sigma1Inv_b0 (x : Word) : Sigma1 (Sigma1Inv (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32 := by unfold Sigma1Inv Sigma1 rotr; bv_decide theorem Sigma1_Sigma1Inv_b1 (x : Word) : Sigma1 (Sigma1Inv (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32 := by unfold Sigma1Inv Sigma1 rotr; bv_decide theorem Sigma1_Sigma1Inv_b2 (x : Word) : Sigma1 (Sigma1Inv (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32 := by unfold Sigma1Inv Sigma1 rotr; bv_decide theorem Sigma1_Sigma1Inv_b3 (x : Word) : Sigma1 (Sigma1Inv (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32 := by unfold Sigma1Inv Sigma1 rotr; bv_decide theorem sigma0Inv_sigma0_b0 (x : Word) : sigma0Inv (sigma0 (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32 := by unfold sigma0Inv sigma0 bitMask rotr; bv_decide theorem sigma0Inv_sigma0_b1 (x : Word) : sigma0Inv (sigma0 (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32 := by unfold sigma0Inv sigma0 bitMask rotr; bv_decide theorem sigma0Inv_sigma0_b2 (x : Word) : sigma0Inv (sigma0 (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32 := by unfold sigma0Inv sigma0 bitMask rotr; bv_decide theorem sigma0Inv_sigma0_b3 (x : Word) : sigma0Inv (sigma0 (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32 := by unfold sigma0Inv sigma0 bitMask rotr; bv_decide theorem sigma0_sigma0Inv_b0 (x : Word) : sigma0 (sigma0Inv (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32 := by unfold sigma0Inv sigma0 bitMask rotr; bv_decide theorem sigma0_sigma0Inv_b1 (x : Word) : sigma0 (sigma0Inv (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32 := by unfold sigma0Inv sigma0 bitMask rotr; bv_decide theorem sigma0_sigma0Inv_b2 (x : Word) : sigma0 (sigma0Inv (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32 := by unfold sigma0Inv sigma0 bitMask rotr; bv_decide theorem sigma0_sigma0Inv_b3 (x : Word) : sigma0 (sigma0Inv (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32 := by unfold sigma0Inv sigma0 bitMask rotr; bv_decide theorem sigma1Inv_sigma1_b0 (x : Word) : sigma1Inv (sigma1 (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32 := by unfold sigma1Inv sigma1 bitMask rotr; bv_decide theorem sigma1Inv_sigma1_b1 (x : Word) : sigma1Inv (sigma1 (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32 := by unfold sigma1Inv sigma1 bitMask rotr; bv_decide theorem sigma1Inv_sigma1_b2 (x : Word) : sigma1Inv (sigma1 (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32 := by unfold sigma1Inv sigma1 bitMask rotr; bv_decide theorem sigma1Inv_sigma1_b3 (x : Word) : sigma1Inv (sigma1 (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32 := by unfold sigma1Inv sigma1 bitMask rotr; bv_decide theorem sigma1_sigma1Inv_b0 (x : Word) : sigma1 (sigma1Inv (x &&& 0x000000FF#32)) = x &&& 0x000000FF#32 := by unfold sigma1Inv sigma1 bitMask rotr; bv_decide theorem sigma1_sigma1Inv_b1 (x : Word) : sigma1 (sigma1Inv (x &&& 0x0000FF00#32)) = x &&& 0x0000FF00#32 := by unfold sigma1Inv sigma1 bitMask rotr; bv_decide theorem sigma1_sigma1Inv_b2 (x : Word) : sigma1 (sigma1Inv (x &&& 0x00FF0000#32)) = x &&& 0x00FF0000#32 := by unfold sigma1Inv sigma1 bitMask rotr; bv_decide theorem sigma1_sigma1Inv_b3 (x : Word) : sigma1 (sigma1Inv (x &&& 0xFF000000#32)) = x &&& 0xFF000000#32 := by unfold sigma1Inv sigma1 bitMask rotr; bv_decide /-- `Sigma0Inv ∘ Sigma0 = id`. -/ theorem Sigma0Inv_Sigma0 : ∀ x, Sigma0Inv (Sigma0 x) = x := inv_of_quarters Sigma0 Sigma0Inv Sigma0_xor Sigma0Inv_xor Sigma0Inv_Sigma0_b0 Sigma0Inv_Sigma0_b1 Sigma0Inv_Sigma0_b2 Sigma0Inv_Sigma0_b3 /-- `Sigma0 ∘ Sigma0Inv = id`. -/ theorem Sigma0_Sigma0Inv : ∀ x, Sigma0 (Sigma0Inv x) = x := inv_of_quarters Sigma0Inv Sigma0 Sigma0Inv_xor Sigma0_xor Sigma0_Sigma0Inv_b0 Sigma0_Sigma0Inv_b1 Sigma0_Sigma0Inv_b2 Sigma0_Sigma0Inv_b3 /-- `Sigma1Inv ∘ Sigma1 = id`. -/ theorem Sigma1Inv_Sigma1 : ∀ x, Sigma1Inv (Sigma1 x) = x := inv_of_quarters Sigma1 Sigma1Inv Sigma1_xor Sigma1Inv_xor Sigma1Inv_Sigma1_b0 Sigma1Inv_Sigma1_b1 Sigma1Inv_Sigma1_b2 Sigma1Inv_Sigma1_b3 /-- `Sigma1 ∘ Sigma1Inv = id`. -/ theorem Sigma1_Sigma1Inv : ∀ x, Sigma1 (Sigma1Inv x) = x := inv_of_quarters Sigma1Inv Sigma1 Sigma1Inv_xor Sigma1_xor Sigma1_Sigma1Inv_b0 Sigma1_Sigma1Inv_b1 Sigma1_Sigma1Inv_b2 Sigma1_Sigma1Inv_b3 /-- `sigma0Inv ∘ sigma0 = id`. -/ theorem sigma0Inv_sigma0 : ∀ x, sigma0Inv (sigma0 x) = x := inv_of_quarters sigma0 sigma0Inv sigma0_xor sigma0Inv_xor sigma0Inv_sigma0_b0 sigma0Inv_sigma0_b1 sigma0Inv_sigma0_b2 sigma0Inv_sigma0_b3 /-- `sigma0 ∘ sigma0Inv = id`. -/ theorem sigma0_sigma0Inv : ∀ x, sigma0 (sigma0Inv x) = x := inv_of_quarters sigma0Inv sigma0 sigma0Inv_xor sigma0_xor sigma0_sigma0Inv_b0 sigma0_sigma0Inv_b1 sigma0_sigma0Inv_b2 sigma0_sigma0Inv_b3 /-- `sigma1Inv ∘ sigma1 = id`. -/ theorem sigma1Inv_sigma1 : ∀ x, sigma1Inv (sigma1 x) = x := inv_of_quarters sigma1 sigma1Inv sigma1_xor sigma1Inv_xor sigma1Inv_sigma1_b0 sigma1Inv_sigma1_b1 sigma1Inv_sigma1_b2 sigma1Inv_sigma1_b3 /-- `sigma1 ∘ sigma1Inv = id`. -/ theorem sigma1_sigma1Inv : ∀ x, sigma1 (sigma1Inv x) = x := inv_of_quarters sigma1Inv sigma1 sigma1Inv_xor sigma1_xor sigma1_sigma1Inv_b0 sigma1_sigma1Inv_b1 sigma1_sigma1Inv_b2 sigma1_sigma1Inv_b3 /-- Σ0 is a bijection of `BitVec 32` (explicit inverse `Sigma0Inv`). -/ theorem Sigma0_bijective : Bijective Sigma0 := ⟨Sigma0_injective, fun y => ⟨Sigma0Inv y, Sigma0_Sigma0Inv y⟩⟩ theorem Sigma1_bijective : Bijective Sigma1 := ⟨Sigma1_injective, fun y => ⟨Sigma1Inv y, Sigma1_Sigma1Inv y⟩⟩ /-- σ0 is a bijection of `BitVec 32` (explicit inverse `sigma0Inv`): the shift does not destroy invertibility; the kernel of the GF(2) map is trivial. -/ theorem sigma0_bijective : Bijective sigma0 := ⟨sigma0_injective, fun y => ⟨sigma0Inv y, sigma0_sigma0Inv y⟩⟩ theorem sigma1_bijective : Bijective sigma1 := ⟨sigma1_injective, fun y => ⟨sigma1Inv y, sigma1_sigma1Inv y⟩⟩ end Wp34