1 # Proofs of mode-core's laws. block_octets_round_trip is the block's own 2 # law; the others are the lemmas the modes share, proved here once (each 3 # def Laws.x at the end of the file is the lemma above it). 4 import Base 5 import bend-osdev-bytes@0.1.1.0/bytes.bend as B 6 import bend-osdev-bytes@0.1.1.0/LAWS.bend as BL 7 import bend-osdev-bytes@0.1.1.0/PROOF.bend as BP 8 import ./mode_core.bend as M 9 import bend-osdev-u32@0.1.0.0/LAWS.bend as UL 10 import bend-osdev-u32@0.1.0.0/PROOF.bend as UP 11 import ./LAWS.bend as Laws 12 13 # How the proofs go. The modes work on blocks; the byte layer splits a byte 14 # string into blocks and joins blocks back. The lemmas below show: 15 # * XOR with the same block twice is the identity (bit by bit); 16 # * a word split into bytes and joined back is the word, and the bytes of a 17 # joined word are the (masked) bytes (bit slicing, every bit symbolic); 18 # * splitting joined blocks gives the blocks back, and joining a split 19 # byte string gives it back (induction, 16 bytes at a time); 20 # * every to_list of an Octets is masked (the bytes interface laws 21 # octets_of_to and octets_to_of), so the bytes a mode reads back are the 22 # bytes it wrote. 23 # Nothing here looks inside Octets: only the bytes laws and its list layer. 24 25 # Bits: each lemma splits its words into their 32 bits, so the slicing 26 # computes 27 28 def bits.word_bytes(w: U32) -> {M.cm.word(M.cm.b0(w), M.cm.b1(w), M.cm.b2(w), M.cm.b3(w)) == w : U32}: 29 match w: 30 case U32{WCon{w0, WCon{w1, WCon{w2, WCon{w3, WCon{w4, WCon{w5, WCon{w6, WCon{w7, WCon{w8, WCon{w9, WCon{w10, WCon{w11, WCon{w12, WCon{w13, WCon{w14, WCon{w15, WCon{w16, WCon{w17, WCon{w18, WCon{w19, WCon{w20, WCon{w21, WCon{w22, WCon{w23, WCon{w24, WCon{w25, WCon{w26, WCon{w27, WCon{w28, WCon{w29, WCon{w30, WCon{w31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 31 {==} 32 33 def bits.byte0_word(a: U32, b: U32, c: U32, d: U32) -> {M.cm.b0(M.cm.word(a, b, c, d)) == B.byte(a) : U32}: 34 match a b c d: 35 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{d0, WCon{d1, WCon{d2, WCon{d3, WCon{d4, WCon{d5, WCon{d6, WCon{d7, WCon{d8, WCon{d9, WCon{d10, WCon{d11, WCon{d12, WCon{d13, WCon{d14, WCon{d15, WCon{d16, WCon{d17, WCon{d18, WCon{d19, WCon{d20, WCon{d21, WCon{d22, WCon{d23, WCon{d24, WCon{d25, WCon{d26, WCon{d27, WCon{d28, WCon{d29, WCon{d30, WCon{d31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 36 {==} 37 38 def bits.byte1_word(a: U32, b: U32, c: U32, d: U32) -> {M.cm.b1(M.cm.word(a, b, c, d)) == B.byte(b) : U32}: 39 match a b c d: 40 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{d0, WCon{d1, WCon{d2, WCon{d3, WCon{d4, WCon{d5, WCon{d6, WCon{d7, WCon{d8, WCon{d9, WCon{d10, WCon{d11, WCon{d12, WCon{d13, WCon{d14, WCon{d15, WCon{d16, WCon{d17, WCon{d18, WCon{d19, WCon{d20, WCon{d21, WCon{d22, WCon{d23, WCon{d24, WCon{d25, WCon{d26, WCon{d27, WCon{d28, WCon{d29, WCon{d30, WCon{d31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 41 {==} 42 43 def bits.byte2_word(a: U32, b: U32, c: U32, d: U32) -> {M.cm.b2(M.cm.word(a, b, c, d)) == B.byte(c) : U32}: 44 match a b c d: 45 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{d0, WCon{d1, WCon{d2, WCon{d3, WCon{d4, WCon{d5, WCon{d6, WCon{d7, WCon{d8, WCon{d9, WCon{d10, WCon{d11, WCon{d12, WCon{d13, WCon{d14, WCon{d15, WCon{d16, WCon{d17, WCon{d18, WCon{d19, WCon{d20, WCon{d21, WCon{d22, WCon{d23, WCon{d24, WCon{d25, WCon{d26, WCon{d27, WCon{d28, WCon{d29, WCon{d30, WCon{d31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 46 {==} 47 48 def bits.byte3_word(a: U32, b: U32, c: U32, d: U32) -> {M.cm.b3(M.cm.word(a, b, c, d)) == B.byte(d) : U32}: 49 match a b c d: 50 case U32{WCon{a0, WCon{a1, WCon{a2, WCon{a3, WCon{a4, WCon{a5, WCon{a6, WCon{a7, WCon{a8, WCon{a9, WCon{a10, WCon{a11, WCon{a12, WCon{a13, WCon{a14, WCon{a15, WCon{a16, WCon{a17, WCon{a18, WCon{a19, WCon{a20, WCon{a21, WCon{a22, WCon{a23, WCon{a24, WCon{a25, WCon{a26, WCon{a27, WCon{a28, WCon{a29, WCon{a30, WCon{a31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{d0, WCon{d1, WCon{d2, WCon{d3, WCon{d4, WCon{d5, WCon{d6, WCon{d7, WCon{d8, WCon{d9, WCon{d10, WCon{d11, WCon{d12, WCon{d13, WCon{d14, WCon{d15, WCon{d16, WCon{d17, WCon{d18, WCon{d19, WCon{d20, WCon{d21, WCon{d22, WCon{d23, WCon{d24, WCon{d25, WCon{d26, WCon{d27, WCon{d28, WCon{d29, WCon{d30, WCon{d31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 51 {==} 52 53 def bits.byte_b0(w: U32) -> {B.byte(M.cm.b0(w)) == M.cm.b0(w) : U32}: 54 match w: 55 case U32{WCon{w0, WCon{w1, WCon{w2, WCon{w3, WCon{w4, WCon{w5, WCon{w6, WCon{w7, WCon{w8, WCon{w9, WCon{w10, WCon{w11, WCon{w12, WCon{w13, WCon{w14, WCon{w15, WCon{w16, WCon{w17, WCon{w18, WCon{w19, WCon{w20, WCon{w21, WCon{w22, WCon{w23, WCon{w24, WCon{w25, WCon{w26, WCon{w27, WCon{w28, WCon{w29, WCon{w30, WCon{w31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 56 {==} 57 58 def bits.byte_b1(w: U32) -> {B.byte(M.cm.b1(w)) == M.cm.b1(w) : U32}: 59 match w: 60 case U32{WCon{w0, WCon{w1, WCon{w2, WCon{w3, WCon{w4, WCon{w5, WCon{w6, WCon{w7, WCon{w8, WCon{w9, WCon{w10, WCon{w11, WCon{w12, WCon{w13, WCon{w14, WCon{w15, WCon{w16, WCon{w17, WCon{w18, WCon{w19, WCon{w20, WCon{w21, WCon{w22, WCon{w23, WCon{w24, WCon{w25, WCon{w26, WCon{w27, WCon{w28, WCon{w29, WCon{w30, WCon{w31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 61 {==} 62 63 def bits.byte_b2(w: U32) -> {B.byte(M.cm.b2(w)) == M.cm.b2(w) : U32}: 64 match w: 65 case U32{WCon{w0, WCon{w1, WCon{w2, WCon{w3, WCon{w4, WCon{w5, WCon{w6, WCon{w7, WCon{w8, WCon{w9, WCon{w10, WCon{w11, WCon{w12, WCon{w13, WCon{w14, WCon{w15, WCon{w16, WCon{w17, WCon{w18, WCon{w19, WCon{w20, WCon{w21, WCon{w22, WCon{w23, WCon{w24, WCon{w25, WCon{w26, WCon{w27, WCon{w28, WCon{w29, WCon{w30, WCon{w31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 66 {==} 67 68 def bits.byte_b3(w: U32) -> {B.byte(M.cm.b3(w)) == M.cm.b3(w) : U32}: 69 match w: 70 case U32{WCon{w0, WCon{w1, WCon{w2, WCon{w3, WCon{w4, WCon{w5, WCon{w6, WCon{w7, WCon{w8, WCon{w9, WCon{w10, WCon{w11, WCon{w12, WCon{w13, WCon{w14, WCon{w15, WCon{w16, WCon{w17, WCon{w18, WCon{w19, WCon{w20, WCon{w21, WCon{w22, WCon{w23, WCon{w24, WCon{w25, WCon{w26, WCon{w27, WCon{w28, WCon{w29, WCon{w30, WCon{w31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 71 {==} 72 73 def bits.byte_byte(y: U32) -> {B.byte(B.byte(y)) == B.byte(y) : U32}: 74 match y: 75 case U32{WCon{y0, WCon{y1, WCon{y2, WCon{y3, WCon{y4, WCon{y5, WCon{y6, WCon{y7, WCon{y8, WCon{y9, WCon{y10, WCon{y11, WCon{y12, WCon{y13, WCon{y14, WCon{y15, WCon{y16, WCon{y17, WCon{y18, WCon{y19, WCon{y20, WCon{y21, WCon{y22, WCon{y23, WCon{y24, WCon{y25, WCon{y26, WCon{y27, WCon{y28, WCon{y29, WCon{y30, WCon{y31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 76 {==} 77 78 # Splits 79 80 def sp.cons_blocks(b: M.CmBlock, s: M.CmSplit) -> {M.cm.split.blocks(M.cm.split.cons(b, s)) == Con{b, M.cm.split.blocks(s)} : List<&2, M.CmBlock>}: 81 match s: 82 case M.CmSplit{bs, t}: 83 {==} 84 85 def sp.cons_tail(b: M.CmBlock, s: M.CmSplit) -> {M.cm.split.tail(M.cm.split.cons(b, s)) == M.cm.split.tail(s) : List<&2, U32>}: 86 match s: 87 case M.CmSplit{bs, t}: 88 {==} 89 90 def sp.eta(s: M.CmSplit) -> {M.CmSplit{M.cm.split.blocks(s), M.cm.split.tail(s)} == s : M.CmSplit}: 91 match s: 92 case M.CmSplit{bs, t}: 93 {==} 94 95 # Booleans: False is not True 96 97 def bo.disc(b: Bool) -> Type: 98 match b: 99 case False{}: 100 Unit 101 case True{}: 102 Empty 103 104 def bo.empty(h: {False{} == True{} : Bool}) -> Empty: 105 %h : bo.disc(_) 106 Unit{} 107 108 def bo.absurd(-A: Type, h: {False{} == True{} : Bool}) -> A: 109 Empty.absurd(A, bo.empty(h)) 110 111 # Lists of bytes (the bytes list layer) 112 113 def li.mask_mask(zs: List<&2, U32>) -> {B.mask(B.mask(zs)) == B.mask(zs) : List<&2, U32>}: 114 match zs: 115 case Nil{}: 116 {==} 117 case Con{+z, +t}: 118 %bits.byte_byte(z) : {Con{B.byte(B.byte(z)), B.mask(B.mask(t))} == Con{_, B.mask(t)} : List<&2, U32>} 119 %li.mask_mask(t) : {Con{B.byte(B.byte(z)), B.mask(B.mask(t))} == Con{B.byte(B.byte(z)), _} : List<&2, U32>} 120 {==} 121 122 def li.take_append(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.take(B.len(a), B.append(a, b)) == a : List<&2, U32>}: 123 match a: 124 case Nil{}: 125 {==} 126 case Con{+h, +t}: 127 %Equal.sym(List<&2, U32>, B.take(B.len(t), B.append(t, b)), t, li.take_append(t, b)) : {Con{h, _} == Con{h, t} : List<&2, U32>} 128 {==} 129 130 def li.drop_append(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.drop(B.len(a), B.append(a, b)) == b : List<&2, U32>}: 131 match a: 132 case Nil{}: 133 {==} 134 case Con{+h, +t}: 135 li.drop_append(t, b) 136 137 def li.mask_append(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.mask(B.append(a, b)) == B.append(B.mask(a), B.mask(b)) : List<&2, U32>}: 138 match a: 139 case Nil{}: 140 {==} 141 case Con{+h, +t}: 142 %li.mask_append(t, b) : {Con{B.byte(h), B.mask(B.append(t, b))} == Con{B.byte(h), _} : List<&2, U32>} 143 {==} 144 145 def li.mask_take(+n: Nat, +xs: List<&2, U32>) -> {B.mask(B.take(n, xs)) == B.take(n, B.mask(xs)) : List<&2, U32>}: 146 match n: 147 case 0n: 148 {==} 149 case 1n+p: 150 match xs: 151 case Nil{}: 152 {==} 153 case Con{+h, +t}: 154 %li.mask_take(p, t) : {Con{B.byte(h), B.mask(B.take(p, t))} == Con{B.byte(h), _} : List<&2, U32>} 155 {==} 156 157 def li.len_append(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.len(B.append(a, b)) == Nat.add(B.len(a), B.len(b)) : Nat}: 158 match a: 159 case Nil{}: 160 {==} 161 case Con{+h, +t}: 162 %li.len_append(t, b) : {1n+B.len(B.append(t, b)) == 1n+_ : Nat} 163 {==} 164 165 def li.len_take(+n: Nat, +xs: List<&2, U32>) -> {Nat.is_le(n, B.len(xs)) == True{} : Bool} -> {B.len(B.take(n, xs)) == n : Nat}: 166 match n: 167 case 0n: 168 h => {==} 169 case 1n+p: 170 match xs: 171 case Nil{}: 172 h => bo.absurd({B.len(B.take(1n+p, Nil{})) == 1n+p : Nat}, h) 173 case Con{+x, +t}: 174 h => %li.len_take(p, t)(h) : {1n+B.len(B.take(p, t)) == 1n+_ : Nat} 175 {==} 176 177 def na.lt_le(+a: Nat, +b: Nat) -> {Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_le(a, b) == True{} : Bool}: 178 match a b: 179 case 0n 0n: 180 h => bo.absurd({Nat.is_le(0n, 0n) == True{} : Bool}, h) 181 case 0n 1n+bp: 182 h => {==} 183 case 1n+ap 0n: 184 h => bo.absurd({Nat.is_le(1n+ap, 0n) == True{} : Bool}, h) 185 case 1n+ap 1n+bp: 186 h => na.lt_le(ap, bp)(h) 187 188 # splitting the bytes of a block gives the block back 189 def sp.blk(b: M.CmBlock, rest: List<&2, U32>) -> {M.cm.split(M.cm.bytes_onto(b, rest)) == M.cm.split.cons(b, M.cm.split(rest)) : M.CmSplit}: 190 match b: 191 case M.CmBlock{U32{WCon{p0, WCon{p1, WCon{p2, WCon{p3, WCon{p4, WCon{p5, WCon{p6, WCon{p7, WCon{p8, WCon{p9, WCon{p10, WCon{p11, WCon{p12, WCon{p13, WCon{p14, WCon{p15, WCon{p16, WCon{p17, WCon{p18, WCon{p19, WCon{p20, WCon{p21, WCon{p22, WCon{p23, WCon{p24, WCon{p25, WCon{p26, WCon{p27, WCon{p28, WCon{p29, WCon{p30, WCon{p31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{q0, WCon{q1, WCon{q2, WCon{q3, WCon{q4, WCon{q5, WCon{q6, WCon{q7, WCon{q8, WCon{q9, WCon{q10, WCon{q11, WCon{q12, WCon{q13, WCon{q14, WCon{q15, WCon{q16, WCon{q17, WCon{q18, WCon{q19, WCon{q20, WCon{q21, WCon{q22, WCon{q23, WCon{q24, WCon{q25, WCon{q26, WCon{q27, WCon{q28, WCon{q29, WCon{q30, WCon{q31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{r0, WCon{r1, WCon{r2, WCon{r3, WCon{r4, WCon{r5, WCon{r6, WCon{r7, WCon{r8, WCon{r9, WCon{r10, WCon{r11, WCon{r12, WCon{r13, WCon{r14, WCon{r15, WCon{r16, WCon{r17, WCon{r18, WCon{r19, WCon{r20, WCon{r21, WCon{r22, WCon{r23, WCon{r24, WCon{r25, WCon{r26, WCon{r27, WCon{r28, WCon{r29, WCon{r30, WCon{r31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{s0, WCon{s1, WCon{s2, WCon{s3, WCon{s4, WCon{s5, WCon{s6, WCon{s7, WCon{s8, WCon{s9, WCon{s10, WCon{s11, WCon{s12, WCon{s13, WCon{s14, WCon{s15, WCon{s16, WCon{s17, WCon{s18, WCon{s19, WCon{s20, WCon{s21, WCon{s22, WCon{s23, WCon{s24, WCon{s25, WCon{s26, WCon{s27, WCon{s28, WCon{s29, WCon{s30, WCon{s31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 192 {==} 193 194 # the bytes of a block are bytes: masking changes nothing 195 def sp.mask_blk(b: M.CmBlock, rest: List<&2, U32>) -> {B.mask(M.cm.bytes_onto(b, rest)) == M.cm.bytes_onto(b, B.mask(rest)) : List<&2, U32>}: 196 match b: 197 case M.CmBlock{U32{WCon{p0, WCon{p1, WCon{p2, WCon{p3, WCon{p4, WCon{p5, WCon{p6, WCon{p7, WCon{p8, WCon{p9, WCon{p10, WCon{p11, WCon{p12, WCon{p13, WCon{p14, WCon{p15, WCon{p16, WCon{p17, WCon{p18, WCon{p19, WCon{p20, WCon{p21, WCon{p22, WCon{p23, WCon{p24, WCon{p25, WCon{p26, WCon{p27, WCon{p28, WCon{p29, WCon{p30, WCon{p31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{q0, WCon{q1, WCon{q2, WCon{q3, WCon{q4, WCon{q5, WCon{q6, WCon{q7, WCon{q8, WCon{q9, WCon{q10, WCon{q11, WCon{q12, WCon{q13, WCon{q14, WCon{q15, WCon{q16, WCon{q17, WCon{q18, WCon{q19, WCon{q20, WCon{q21, WCon{q22, WCon{q23, WCon{q24, WCon{q25, WCon{q26, WCon{q27, WCon{q28, WCon{q29, WCon{q30, WCon{q31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{r0, WCon{r1, WCon{r2, WCon{r3, WCon{r4, WCon{r5, WCon{r6, WCon{r7, WCon{r8, WCon{r9, WCon{r10, WCon{r11, WCon{r12, WCon{r13, WCon{r14, WCon{r15, WCon{r16, WCon{r17, WCon{r18, WCon{r19, WCon{r20, WCon{r21, WCon{r22, WCon{r23, WCon{r24, WCon{r25, WCon{r26, WCon{r27, WCon{r28, WCon{r29, WCon{r30, WCon{r31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{s0, WCon{s1, WCon{s2, WCon{s3, WCon{s4, WCon{s5, WCon{s6, WCon{s7, WCon{s8, WCon{s9, WCon{s10, WCon{s11, WCon{s12, WCon{s13, WCon{s14, WCon{s15, WCon{s16, WCon{s17, WCon{s18, WCon{s19, WCon{s20, WCon{s21, WCon{s22, WCon{s23, WCon{s24, WCon{s25, WCon{s26, WCon{s27, WCon{s28, WCon{s29, WCon{s30, WCon{s31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 198 {==} 199 200 # the block of 16 bytes, as bytes again 201 def sp.blk16(y0: U32, y1: U32, y2: U32, y3: U32, y4: U32, y5: U32, y6: U32, y7: U32, y8: U32, y9: U32, y10: U32, y11: U32, y12: U32, y13: U32, y14: U32, y15: U32, rest: List<&2, U32>) -> {M.cm.bytes_onto(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), rest) == Con{B.byte(y0), Con{B.byte(y1), Con{B.byte(y2), Con{B.byte(y3), Con{B.byte(y4), Con{B.byte(y5), Con{B.byte(y6), Con{B.byte(y7), Con{B.byte(y8), Con{B.byte(y9), Con{B.byte(y10), Con{B.byte(y11), Con{B.byte(y12), Con{B.byte(y13), Con{B.byte(y14), Con{B.byte(y15), rest}}}}}}}}}}}}}}}} : List<&2, U32>}: 202 match y0 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15: 203 case U32{WCon{y00, WCon{y01, WCon{y02, WCon{y03, WCon{y04, WCon{y05, WCon{y06, WCon{y07, WCon{y08, WCon{y09, WCon{y010, WCon{y011, WCon{y012, WCon{y013, WCon{y014, WCon{y015, WCon{y016, WCon{y017, WCon{y018, WCon{y019, WCon{y020, WCon{y021, WCon{y022, WCon{y023, WCon{y024, WCon{y025, WCon{y026, WCon{y027, WCon{y028, WCon{y029, WCon{y030, WCon{y031, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y10, WCon{y11, WCon{y12, WCon{y13, WCon{y14, WCon{y15, WCon{y16, WCon{y17, WCon{y18, WCon{y19, WCon{y110, WCon{y111, WCon{y112, WCon{y113, WCon{y114, WCon{y115, WCon{y116, WCon{y117, WCon{y118, WCon{y119, WCon{y120, WCon{y121, WCon{y122, WCon{y123, WCon{y124, WCon{y125, WCon{y126, WCon{y127, WCon{y128, WCon{y129, WCon{y130, WCon{y131, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y20, WCon{y21, WCon{y22, WCon{y23, WCon{y24, WCon{y25, WCon{y26, WCon{y27, WCon{y28, WCon{y29, WCon{y210, WCon{y211, WCon{y212, WCon{y213, WCon{y214, WCon{y215, WCon{y216, WCon{y217, WCon{y218, WCon{y219, WCon{y220, WCon{y221, WCon{y222, WCon{y223, WCon{y224, WCon{y225, WCon{y226, WCon{y227, WCon{y228, WCon{y229, WCon{y230, WCon{y231, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y30, WCon{y31, WCon{y32, WCon{y33, WCon{y34, WCon{y35, WCon{y36, WCon{y37, WCon{y38, WCon{y39, WCon{y310, WCon{y311, WCon{y312, WCon{y313, WCon{y314, WCon{y315, WCon{y316, WCon{y317, WCon{y318, WCon{y319, WCon{y320, WCon{y321, WCon{y322, WCon{y323, WCon{y324, WCon{y325, WCon{y326, WCon{y327, WCon{y328, WCon{y329, WCon{y330, WCon{y331, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y40, WCon{y41, WCon{y42, WCon{y43, WCon{y44, WCon{y45, WCon{y46, WCon{y47, WCon{y48, WCon{y49, WCon{y410, WCon{y411, WCon{y412, WCon{y413, WCon{y414, WCon{y415, WCon{y416, WCon{y417, WCon{y418, WCon{y419, WCon{y420, WCon{y421, WCon{y422, WCon{y423, WCon{y424, WCon{y425, WCon{y426, WCon{y427, WCon{y428, WCon{y429, WCon{y430, WCon{y431, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y50, WCon{y51, WCon{y52, WCon{y53, WCon{y54, WCon{y5 204 {==} 205 206 # a masked list is its blocks and its tail joined back 207 def sp.join_split(ys: List<&2, U32>) -> {M.cm.join_onto(M.cm.split.blocks(M.cm.split(B.mask(ys))), M.cm.split.tail(M.cm.split(B.mask(ys)))) == B.mask(ys) : List<&2, U32>}: 208 match ys: 209 case Nil{}: 210 {==} 211 case Con{+y0, +r0}: 212 match r0: 213 case Nil{}: 214 {==} 215 case Con{+y1, +r1}: 216 match r1: 217 case Nil{}: 218 {==} 219 case Con{+y2, +r2}: 220 match r2: 221 case Nil{}: 222 {==} 223 case Con{+y3, +r3}: 224 match r3: 225 case Nil{}: 226 {==} 227 case Con{+y4, +r4}: 228 match r4: 229 case Nil{}: 230 {==} 231 case Con{+y5, +r5}: 232 match r5: 233 case Nil{}: 234 {==} 235 case Con{+y6, +r6}: 236 match r6: 237 case Nil{}: 238 {==} 239 case Con{+y7, +r7}: 240 match r7: 241 case Nil{}: 242 {==} 243 case Con{+y8, +r8}: 244 match r8: 245 case Nil{}: 246 {==} 247 case Con{+y9, +r9}: 248 match r9: 249 case Nil{}: 250 {==} 251 case Con{+y10, +r10}: 252 match r10: 253 case Nil{}: 254 {==} 255 case Con{+y11, +r11}: 256 match r11: 257 case Nil{}: 258 {==} 259 case Con{+y12, +r12}: 260 match r12: 261 case Nil{}: 262 {==} 263 case Con{+y13, +r13}: 264 match r13: 265 case Nil{}: 266 {==} 267 case Con{+y14, +r14}: 268 match r14: 269 case Nil{}: 270 {==} 271 case Con{+y15, +t}: 272 %Equal.sym(List<&2, M.CmBlock>, M.cm.split.blocks(M.cm.split.cons(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))), Con{M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split.blocks(M.cm.split(B.mask(t)))}, sp.cons_blocks(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))) : {M.cm.join_onto(_, M.cm.split.tail(M.cm.split.cons(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t))))) == Con{B.byte(y0), Con{B.byte(y1), Con{B.byte(y2), Con{B.byte(y3), Con{B.byte(y4), Con{B.byte(y5), Con{B.byte(y6), Con{B.byte(y7), Con{B.byte(y8), Con{B.byte(y9), Con{B.byte(y10), Con{B.byte(y11), Con{B.byte(y12), Con{B.byte(y13), Con{B.byte(y14), Con{B.byte(y15), B.mask(t)}}}}}}}}}}}}}}}} : List<&2, U32>} 273 %Equal.sym(List<&2, U32>, M.cm.split.tail(M.cm.split.cons(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))), M.cm.split.tail(M.cm.split(B.mask(t))), sp.cons_tail(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))) : {M.cm.join_onto(Con{M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split.blocks(M.cm.split(B.mask(t)))}, _) == Con{B.byte(y0), Con{B.byte(y1), Con{B.byte(y2), Con{B.byte(y3), Con{B.byte(y4), Con{B.byte(y5), Con{B.byte(y6), Con{B.byte(y7), Con{B.byte(y8), Con{B.byte(y9), Con{B.byte(y10), Con{B.byte(y11), Con{B.byte(y12), Con{B.byte(y13), Con{B.byte(y14), Con{B.byte(y15), B.mask(t)}}}}}}}}}}}}}}}} : List<&2, U32>} 274 %Equal.sym(List<&2, U32>, M.cm.join_onto(M.cm.split.blocks(M.cm.split(B.mask(t))), M.cm.split.tail(M.cm.split(B.mask(t)))), B.mask(t), sp.join_split(t)) : {M.cm.bytes_onto(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), _) == Con{B.byte(y0), Con{B.byte(y1), Con{B.byte(y2), Con{B.byte(y3), Con{B.byte(y4), Con{B.byte(y5), Con{B.byte(y6), Con{B.byte(y7), Con{B.byte(y8), Con{B.byte(y9), Con{B.byte(y10), Con{B.byte(y11), Con{B.byte(y12), Con{B.byte(y13), Con{B.byte(y14), Con{B.byte(y15), B.mask(t)}}}}}}}}}}}}}}}} : List<&2, U32>} 275 sp.blk16(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15, B.mask(t)) 276 277 # the bytes of the block of any 16 values are those values, masked 278 def sp.blk16g(z0: U32, z1: U32, z2: U32, z3: U32, z4: U32, z5: U32, z6: U32, z7: U32, z8: U32, z9: U32, z10: U32, z11: U32, z12: U32, z13: U32, z14: U32, z15: U32, rest: List<&2, U32>) -> {M.cm.bytes_onto(M.cm.block16(z0, z1, z2, z3, z4, z5, z6, z7, z8, z9, z10, z11, z12, z13, z14, z15), rest) == Con{B.byte(z0), Con{B.byte(z1), Con{B.byte(z2), Con{B.byte(z3), Con{B.byte(z4), Con{B.byte(z5), Con{B.byte(z6), Con{B.byte(z7), Con{B.byte(z8), Con{B.byte(z9), Con{B.byte(z10), Con{B.byte(z11), Con{B.byte(z12), Con{B.byte(z13), Con{B.byte(z14), Con{B.byte(z15), rest}}}}}}}}}}}}}}}} : List<&2, U32>}: 279 match z0 z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11 z12 z13 z14 z15: 280 case U32{WCon{z00, WCon{z01, WCon{z02, WCon{z03, WCon{z04, WCon{z05, WCon{z06, WCon{z07, WCon{z08, WCon{z09, WCon{z010, WCon{z011, WCon{z012, WCon{z013, WCon{z014, WCon{z015, WCon{z016, WCon{z017, WCon{z018, WCon{z019, WCon{z020, WCon{z021, WCon{z022, WCon{z023, WCon{z024, WCon{z025, WCon{z026, WCon{z027, WCon{z028, WCon{z029, WCon{z030, WCon{z031, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z10, WCon{z11, WCon{z12, WCon{z13, WCon{z14, WCon{z15, WCon{z16, WCon{z17, WCon{z18, WCon{z19, WCon{z110, WCon{z111, WCon{z112, WCon{z113, WCon{z114, WCon{z115, WCon{z116, WCon{z117, WCon{z118, WCon{z119, WCon{z120, WCon{z121, WCon{z122, WCon{z123, WCon{z124, WCon{z125, WCon{z126, WCon{z127, WCon{z128, WCon{z129, WCon{z130, WCon{z131, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z20, WCon{z21, WCon{z22, WCon{z23, WCon{z24, WCon{z25, WCon{z26, WCon{z27, WCon{z28, WCon{z29, WCon{z210, WCon{z211, WCon{z212, WCon{z213, WCon{z214, WCon{z215, WCon{z216, WCon{z217, WCon{z218, WCon{z219, WCon{z220, WCon{z221, WCon{z222, WCon{z223, WCon{z224, WCon{z225, WCon{z226, WCon{z227, WCon{z228, WCon{z229, WCon{z230, WCon{z231, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z30, WCon{z31, WCon{z32, WCon{z33, WCon{z34, WCon{z35, WCon{z36, WCon{z37, WCon{z38, WCon{z39, WCon{z310, WCon{z311, WCon{z312, WCon{z313, WCon{z314, WCon{z315, WCon{z316, WCon{z317, WCon{z318, WCon{z319, WCon{z320, WCon{z321, WCon{z322, WCon{z323, WCon{z324, WCon{z325, WCon{z326, WCon{z327, WCon{z328, WCon{z329, WCon{z330, WCon{z331, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z40, WCon{z41, WCon{z42, WCon{z43, WCon{z44, WCon{z45, WCon{z46, WCon{z47, WCon{z48, WCon{z49, WCon{z410, WCon{z411, WCon{z412, WCon{z413, WCon{z414, WCon{z415, WCon{z416, WCon{z417, WCon{z418, WCon{z419, WCon{z420, WCon{z421, WCon{z422, WCon{z423, WCon{z424, WCon{z425, WCon{z426, WCon{z427, WCon{z428, WCon{z429, WCon{z430, WCon{z431, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{z50, WCon{z51, WCon{z52, WCon{z53, WCon{z54, WCon{z5 281 {==} 282 283 # the tail of a split has fewer than 16 bytes 284 def sp.tail_short(ys: List<&2, U32>) -> {Nat.is_lt(B.len(M.cm.split.tail(M.cm.split(B.mask(ys)))), 16n) == True{} : Bool}: 285 match ys: 286 case Nil{}: 287 {==} 288 case Con{+y0, +r0}: 289 match r0: 290 case Nil{}: 291 {==} 292 case Con{+y1, +r1}: 293 match r1: 294 case Nil{}: 295 {==} 296 case Con{+y2, +r2}: 297 match r2: 298 case Nil{}: 299 {==} 300 case Con{+y3, +r3}: 301 match r3: 302 case Nil{}: 303 {==} 304 case Con{+y4, +r4}: 305 match r4: 306 case Nil{}: 307 {==} 308 case Con{+y5, +r5}: 309 match r5: 310 case Nil{}: 311 {==} 312 case Con{+y6, +r6}: 313 match r6: 314 case Nil{}: 315 {==} 316 case Con{+y7, +r7}: 317 match r7: 318 case Nil{}: 319 {==} 320 case Con{+y8, +r8}: 321 match r8: 322 case Nil{}: 323 {==} 324 case Con{+y9, +r9}: 325 match r9: 326 case Nil{}: 327 {==} 328 case Con{+y10, +r10}: 329 match r10: 330 case Nil{}: 331 {==} 332 case Con{+y11, +r11}: 333 match r11: 334 case Nil{}: 335 {==} 336 case Con{+y12, +r12}: 337 match r12: 338 case Nil{}: 339 {==} 340 case Con{+y13, +r13}: 341 match r13: 342 case Nil{}: 343 {==} 344 case Con{+y14, +r14}: 345 match r14: 346 case Nil{}: 347 {==} 348 case Con{+y15, +t}: 349 %Equal.sym(List<&2, U32>, M.cm.split.tail(M.cm.split.cons(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))), M.cm.split.tail(M.cm.split(B.mask(t))), sp.cons_tail(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))) : {Nat.is_lt(B.len(_), 16n) == True{} : Bool} 350 sp.tail_short(t) 351 352 # the tail of a masked split is masked 353 def sp.tail_masked(ys: List<&2, U32>) -> {B.mask(M.cm.split.tail(M.cm.split(B.mask(ys)))) == M.cm.split.tail(M.cm.split(B.mask(ys))) : List<&2, U32>}: 354 match ys: 355 case Nil{}: 356 li.mask_mask(Nil{}) 357 case Con{+y0, +r0}: 358 match r0: 359 case Nil{}: 360 li.mask_mask(Con{y0, Nil{}}) 361 case Con{+y1, +r1}: 362 match r1: 363 case Nil{}: 364 li.mask_mask(Con{y0, Con{y1, Nil{}}}) 365 case Con{+y2, +r2}: 366 match r2: 367 case Nil{}: 368 li.mask_mask(Con{y0, Con{y1, Con{y2, Nil{}}}}) 369 case Con{+y3, +r3}: 370 match r3: 371 case Nil{}: 372 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Nil{}}}}}) 373 case Con{+y4, +r4}: 374 match r4: 375 case Nil{}: 376 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Nil{}}}}}}) 377 case Con{+y5, +r5}: 378 match r5: 379 case Nil{}: 380 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Nil{}}}}}}}) 381 case Con{+y6, +r6}: 382 match r6: 383 case Nil{}: 384 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Nil{}}}}}}}}) 385 case Con{+y7, +r7}: 386 match r7: 387 case Nil{}: 388 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Nil{}}}}}}}}}) 389 case Con{+y8, +r8}: 390 match r8: 391 case Nil{}: 392 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Nil{}}}}}}}}}}) 393 case Con{+y9, +r9}: 394 match r9: 395 case Nil{}: 396 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Nil{}}}}}}}}}}}) 397 case Con{+y10, +r10}: 398 match r10: 399 case Nil{}: 400 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Nil{}}}}}}}}}}}}) 401 case Con{+y11, +r11}: 402 match r11: 403 case Nil{}: 404 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Nil{}}}}}}}}}}}}}) 405 case Con{+y12, +r12}: 406 match r12: 407 case Nil{}: 408 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Nil{}}}}}}}}}}}}}}) 409 case Con{+y13, +r13}: 410 match r13: 411 case Nil{}: 412 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Con{y13, Nil{}}}}}}}}}}}}}}}) 413 case Con{+y14, +r14}: 414 match r14: 415 case Nil{}: 416 li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Con{y13, Con{y14, Nil{}}}}}}}}}}}}}}}}) 417 case Con{+y15, +t}: 418 %Equal.sym(List<&2, U32>, M.cm.split.tail(M.cm.split.cons(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))), M.cm.split.tail(M.cm.split(B.mask(t))), sp.cons_tail(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))) : {B.mask(_) == _ : List<&2, U32>} 419 sp.tail_masked(t) 420 421 # fewer than 16 bytes are all tail 422 def sp.short_split(ys: List<&2, U32>) -> {Nat.is_lt(B.len(ys), 16n) == True{} : Bool} -> {M.cm.split(ys) == M.CmSplit{Nil{}, ys} : M.CmSplit}: 423 match ys: 424 case Nil{}: 425 h => {==} 426 case Con{+y0, +r0}: 427 match r0: 428 case Nil{}: 429 h => {==} 430 case Con{+y1, +r1}: 431 match r1: 432 case Nil{}: 433 h => {==} 434 case Con{+y2, +r2}: 435 match r2: 436 case Nil{}: 437 h => {==} 438 case Con{+y3, +r3}: 439 match r3: 440 case Nil{}: 441 h => {==} 442 case Con{+y4, +r4}: 443 match r4: 444 case Nil{}: 445 h => {==} 446 case Con{+y5, +r5}: 447 match r5: 448 case Nil{}: 449 h => {==} 450 case Con{+y6, +r6}: 451 match r6: 452 case Nil{}: 453 h => {==} 454 case Con{+y7, +r7}: 455 match r7: 456 case Nil{}: 457 h => {==} 458 case Con{+y8, +r8}: 459 match r8: 460 case Nil{}: 461 h => {==} 462 case Con{+y9, +r9}: 463 match r9: 464 case Nil{}: 465 h => {==} 466 case Con{+y10, +r10}: 467 match r10: 468 case Nil{}: 469 h => {==} 470 case Con{+y11, +r11}: 471 match r11: 472 case Nil{}: 473 h => {==} 474 case Con{+y12, +r12}: 475 match r12: 476 case Nil{}: 477 h => {==} 478 case Con{+y13, +r13}: 479 match r13: 480 case Nil{}: 481 h => {==} 482 case Con{+y14, +r14}: 483 match r14: 484 case Nil{}: 485 h => {==} 486 case Con{+y15, +t}: 487 match t: 488 case Nil{}: 489 h => bo.absurd({M.cm.split(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Con{y13, Con{y14, Con{y15, Nil{}}}}}}}}}}}}}}}}}) == M.CmSplit{Nil{}, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Con{y13, Con{y14, Con{y15, Nil{}}}}}}}}}}}}}}}}}} : M.CmSplit}, h) 490 case Con{+z, +zs}: 491 h => bo.absurd({M.cm.split(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Con{y13, Con{y14, Con{y15, Con{z, zs}}}}}}}}}}}}}}}}}) == M.CmSplit{Nil{}, Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Con{y13, Con{y14, Con{y15, Con{z, zs}}}}}}}}}}}}}}}}}} : M.CmSplit}, h) 492 493 # the block of a block's bytes is the block 494 def sp.block_bytes(b: M.CmBlock) -> {M.cm.block_of(M.cm.bytes_of(b)) == b : M.CmBlock}: 495 match b: 496 case M.CmBlock{U32{WCon{p0, WCon{p1, WCon{p2, WCon{p3, WCon{p4, WCon{p5, WCon{p6, WCon{p7, WCon{p8, WCon{p9, WCon{p10, WCon{p11, WCon{p12, WCon{p13, WCon{p14, WCon{p15, WCon{p16, WCon{p17, WCon{p18, WCon{p19, WCon{p20, WCon{p21, WCon{p22, WCon{p23, WCon{p24, WCon{p25, WCon{p26, WCon{p27, WCon{p28, WCon{p29, WCon{p30, WCon{p31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{q0, WCon{q1, WCon{q2, WCon{q3, WCon{q4, WCon{q5, WCon{q6, WCon{q7, WCon{q8, WCon{q9, WCon{q10, WCon{q11, WCon{q12, WCon{q13, WCon{q14, WCon{q15, WCon{q16, WCon{q17, WCon{q18, WCon{q19, WCon{q20, WCon{q21, WCon{q22, WCon{q23, WCon{q24, WCon{q25, WCon{q26, WCon{q27, WCon{q28, WCon{q29, WCon{q30, WCon{q31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{r0, WCon{r1, WCon{r2, WCon{r3, WCon{r4, WCon{r5, WCon{r6, WCon{r7, WCon{r8, WCon{r9, WCon{r10, WCon{r11, WCon{r12, WCon{r13, WCon{r14, WCon{r15, WCon{r16, WCon{r17, WCon{r18, WCon{r19, WCon{r20, WCon{r21, WCon{r22, WCon{r23, WCon{r24, WCon{r25, WCon{r26, WCon{r27, WCon{r28, WCon{r29, WCon{r30, WCon{r31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{s0, WCon{s1, WCon{s2, WCon{s3, WCon{s4, WCon{s5, WCon{s6, WCon{s7, WCon{s8, WCon{s9, WCon{s10, WCon{s11, WCon{s12, WCon{s13, WCon{s14, WCon{s15, WCon{s16, WCon{s17, WCon{s18, WCon{s19, WCon{s20, WCon{s21, WCon{s22, WCon{s23, WCon{s24, WCon{s25, WCon{s26, WCon{s27, WCon{s28, WCon{s29, WCon{s30, WCon{s31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}: 497 {==} 498 499 # Every Octets is masked: to_list(o) = to_list(of_list(to_list(o))) = mask(to_list(o)) 500 def oc.masked(+o: B.Octets) -> {B.mask(B.Octets.to_list(o)) == B.Octets.to_list(o) : List<&2, U32>}: 501 Equal.trans(List<&2, U32>, B.mask(B.Octets.to_list(o)), B.Octets.to_list(B.Octets.of_list(B.Octets.to_list(o))), B.Octets.to_list(o), Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(B.Octets.to_list(o))), B.mask(B.Octets.to_list(o)), BL.octets_to_of(B.Octets.to_list(o))), Equal.cong(B.Octets, List<&2, U32>, x => B.Octets.to_list(x), B.Octets.of_list(B.Octets.to_list(o)), o, BL.octets_of_to(o))) 502 503 def oc.len(+o: B.Octets, +n: Nat, h: {B.Octets.len(o) == n : Nat}) -> {B.len(B.Octets.to_list(o)) == n : Nat}: 504 Equal.trans(Nat, B.len(B.Octets.to_list(o)), B.Octets.len(o), n, Equal.sym(Nat, B.Octets.len(o), B.len(B.Octets.to_list(o)), BL.octets_len_list(o)), h) 505 506 def tr.len_go(+bs: List<&2, M.CmBlock>, +n: Nat) -> {M.cm.blocks.len.go(bs, n) == Nat.add(List.length(&2, M.CmBlock, bs), n) : Nat}: 507 match bs: 508 case Nil{}: 509 {==} 510 case Con{h, t}: 511 Equal.trans(Nat, M.cm.blocks.len.go(t, 1n+n), Nat.add(List.length(&2, M.CmBlock, t), 1n+n), 1n+Nat.add(List.length(&2, M.CmBlock, t), n), tr.len_go(t, 1n+n), UL.nat_add_succ(List.length(&2, M.CmBlock, t), n)) 512 513 def tr.len_eq(+bs: List<&2, M.CmBlock>) -> {List.length(&2, M.CmBlock, bs) == M.cm.blocks.len(bs) : Nat}: 514 Equal.sym(Nat, M.cm.blocks.len(bs), List.length(&2, M.CmBlock, bs), Equal.trans(Nat, M.cm.blocks.len.go(bs, 0n), Nat.add(List.length(&2, M.CmBlock, bs), 0n), List.length(&2, M.CmBlock, bs), tr.len_go(bs, 0n), UL.nat_add_zero(List.length(&2, M.CmBlock, bs)))) 515 516 # Splitting: the blocks so far, reversed in acc, go in front of the 517 # structural split's blocks 518 519 def tr.split_fin(acc: List<&2, M.CmBlock>, s: M.CmSplit) -> M.CmSplit: 520 match s: 521 case M.CmSplit{bs, t}: 522 M.CmSplit{M.cm.blocks.rev_onto(acc, bs), t} 523 524 def tr.split_fin_cons(+b: M.CmBlock, +acc: List<&2, M.CmBlock>, +s: M.CmSplit) -> {tr.split_fin(Con{b, acc}, s) == tr.split_fin(acc, M.cm.split.cons(b, s)) : M.CmSplit}: 525 match s: 526 case M.CmSplit{bs, t}: 527 {==} 528 529 def tr.split_fin_nil(+s: M.CmSplit) -> {tr.split_fin(Nil{}, s) == s : M.CmSplit}: 530 match s: 531 case M.CmSplit{bs, t}: 532 {==} 533 534 def tr.split_go(+xs: List<&2, U32>, +acc: List<&2, M.CmBlock>) -> {M.cm.split.go(xs, acc) == tr.split_fin(acc, M.cm.split(xs)) : M.CmSplit}: 535 match xs: 536 case Nil{}: 537 {==} 538 case Con{+y0, +r0}: 539 match r0: 540 case Nil{}: 541 {==} 542 case Con{+y1, +r1}: 543 match r1: 544 case Nil{}: 545 {==} 546 case Con{+y2, +r2}: 547 match r2: 548 case Nil{}: 549 {==} 550 case Con{+y3, +r3}: 551 match r3: 552 case Nil{}: 553 {==} 554 case Con{+y4, +r4}: 555 match r4: 556 case Nil{}: 557 {==} 558 case Con{+y5, +r5}: 559 match r5: 560 case Nil{}: 561 {==} 562 case Con{+y6, +r6}: 563 match r6: 564 case Nil{}: 565 {==} 566 case Con{+y7, +r7}: 567 match r7: 568 case Nil{}: 569 {==} 570 case Con{+y8, +r8}: 571 match r8: 572 case Nil{}: 573 {==} 574 case Con{+y9, +r9}: 575 match r9: 576 case Nil{}: 577 {==} 578 case Con{+y10, +r10}: 579 match r10: 580 case Nil{}: 581 {==} 582 case Con{+y11, +r11}: 583 match r11: 584 case Nil{}: 585 {==} 586 case Con{+y12, +r12}: 587 match r12: 588 case Nil{}: 589 {==} 590 case Con{+y13, +r13}: 591 match r13: 592 case Nil{}: 593 {==} 594 case Con{+y14, +r14}: 595 match r14: 596 case Nil{}: 597 {==} 598 case Con{+y15, +t}: 599 Equal.trans(M.CmSplit, M.cm.split.go(t, Con{M.cm.block16(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15), acc}), tr.split_fin(Con{M.cm.block16(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15), acc}, M.cm.split(t)), tr.split_fin(acc, M.cm.split.cons(M.cm.block16(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15), M.cm.split(t))), tr.split_go(t, Con{M.cm.block16(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15), acc}), tr.split_fin_cons(M.cm.block16(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15), acc, M.cm.split(t))) 600 601 def tr.split_eq(+xs: List<&2, U32>) -> {M.cm.split(xs) == M.cm.split.fast(xs) : M.CmSplit}: 602 Equal.sym(M.CmSplit, M.cm.split.fast(xs), M.cm.split(xs), Equal.trans(M.CmSplit, M.cm.split.go(xs, Nil{}), tr.split_fin(Nil{}, M.cm.split(xs)), M.cm.split(xs), tr.split_go(xs, Nil{}), tr.split_fin_nil(M.cm.split(xs)))) 603 604 # Joining 605 606 def tr.join_go(xs: List<&2, M.CmBlock>, rs: List<&2, M.CmBlock>, +rest: List<&2, U32>) -> {M.cm.join.go(M.cm.blocks.rev_onto(xs, rs), rest) == M.cm.join.go(rs, M.cm.join_onto(xs, rest)) : List<&2, U32>}: 607 match xs: 608 case Nil{}: 609 {==} 610 case Con{x, t}: 611 tr.join_go(t, Con{x, rs}, rest) 612 613 def tr.join_eq(+bs: List<&2, M.CmBlock>, +rest: List<&2, U32>) -> {M.cm.join_onto(bs, rest) == M.cm.join_onto.fast(bs, rest) : List<&2, U32>}: 614 Equal.sym(List<&2, U32>, M.cm.join_onto.fast(bs, rest), M.cm.join_onto(bs, rest), tr.join_go(bs, Nil{}, rest)) 615 616 # a bind whose continuations agree on every value agrees 617 def tr.bind_cong(r: Result<&2, &2, M.CmError, B.Octets>, f: B.Octets -> Result<&2, &2, M.CmError, B.Octets>, g: B.Octets -> Result<&2, &2, M.CmError, B.Octets>, h: @c: B.Octets -> {f(c) == g(c) : Result<&2, &2, M.CmError, B.Octets>}) -> {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, r, f) == Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, r, g) : Result<&2, &2, M.CmError, B.Octets>}: 618 match r: 619 case Fail{e}: 620 {==} 621 case Done{c}: 622 h(c) 623 624 # The round trips' hypothesis: the law's inv at the list of blocks the mode 625 # gives the cipher, an equation (so copyable) that the inductions below take 626 # apart a block at a time 627 628 def cmp.head(d: M.CmBlock, xs: List<&2, M.CmBlock>) -> M.CmBlock: 629 match xs: 630 case Nil{}: 631 d 632 case Con{h, t}: 633 h 634 635 def cmp.tail(xs: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>: 636 match xs: 637 case Nil{}: 638 Nil{} 639 case Con{h, t}: 640 t 641 642 def li.con_hd(+a: M.CmBlock, +s: List<&2, M.CmBlock>, +b: M.CmBlock, +t: List<&2, M.CmBlock>, +e: {Con{a, s} == Con{b, t} : List<&2, M.CmBlock>}) -> {a == b : M.CmBlock}: 643 %e : {a == cmp.head(b, _) : M.CmBlock} 644 {==} 645 646 def li.con_tl(+a: M.CmBlock, +s: List<&2, M.CmBlock>, +b: M.CmBlock, +t: List<&2, M.CmBlock>, +e: {Con{a, s} == Con{b, t} : List<&2, M.CmBlock>}) -> {s == t : List<&2, M.CmBlock>}: 647 %e : {s == cmp.tail(_) : List<&2, M.CmBlock>} 648 {==} 649 650 # the first block's round trip, and the rest's 651 def cmp.hd(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +x: M.CmBlock, +xs: List<&2, M.CmBlock>, +h: {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, Con{x, xs}) == Con{x, xs} : List<&2, M.CmBlock>}) -> {dec(k, enc(k, x)) == x : M.CmBlock}: 652 li.con_hd(dec(k, enc(k, x)), M.CmBlock.dec_enc(~K, ~enc, ~dec, k, xs), x, xs, h) 653 654 def cmp.tl(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +x: M.CmBlock, +xs: List<&2, M.CmBlock>, +h: {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, Con{x, xs}) == Con{x, xs} : List<&2, M.CmBlock>}) -> {M.CmBlock.dec_enc(~K, ~enc, ~dec, k, xs) == xs : List<&2, M.CmBlock>}: 655 li.con_tl(dec(k, enc(k, x)), M.CmBlock.dec_enc(~K, ~enc, ~dec, k, xs), x, xs, h) 656 657 # XOR, cancelling on the right: xor(xor(a, b), b) == a 658 659 def bx.rbool(a: Bool, b: Bool) -> {Bool.xor(Bool.xor(a, b), b) == a : Bool}: 660 match a b: 661 case False{} False{}: 662 {==} 663 case False{} True{}: 664 {==} 665 case True{} False{}: 666 {==} 667 case True{} True{}: 668 {==} 669 670 def bx.rword(n: Nat, a: Word(n), b: Word(n)) -> {Word.xor(n, Word.xor(n, a, b), b) == a : Word(n)}: 671 match n: 672 case 0n: 673 match a: 674 case WNil{}: 675 {==} 676 case 1n+p: 677 match a b: 678 case WCon{ah, at} WCon{bh, bt}: 679 %bx.rbool(ah, bh) : {WCon{Bool.xor(Bool.xor(ah, bh), bh), Word.xor(p, Word.xor(p, at, bt), bt)} == WCon{_, at} : Word(1n+p)} 680 %bx.rword(p, at, bt) : {WCon{Bool.xor(Bool.xor(ah, bh), bh), Word.xor(p, Word.xor(p, at, bt), bt)} == WCon{Bool.xor(Bool.xor(ah, bh), bh), _} : Word(1n+p)} 681 {==} 682 683 def bx.ru32(a: U32, b: U32) -> {U32.xor(U32.xor(a, b), b) == a : U32}: 684 match a b: 685 case U32{x} U32{y}: 686 %bx.rword(32n, x, y) : {U32{Word.xor(32n, Word.xor(32n, x, y), y)} == U32{_} : U32} 687 {==} 688 689 def bx.rblock(+a: M.CmBlock, +b: M.CmBlock) -> {M.CmBlock.xor(M.CmBlock.xor(a, b), b) == a : M.CmBlock}: 690 match a b: 691 case M.CmBlock{a0, a1, a2, a3} M.CmBlock{b0, b1, b2, b3}: 692 %bx.ru32(a0, b0) : {M.CmBlock.xor(M.CmBlock.xor(M.CmBlock{a0, a1, a2, a3}, M.CmBlock{b0, b1, b2, b3}), M.CmBlock{b0, b1, b2, b3}) == M.CmBlock{_, a1, a2, a3} : M.CmBlock} 693 %bx.ru32(a1, b1) : {M.CmBlock.xor(M.CmBlock.xor(M.CmBlock{a0, a1, a2, a3}, M.CmBlock{b0, b1, b2, b3}), M.CmBlock{b0, b1, b2, b3}) == M.CmBlock{U32.xor(U32.xor(a0, b0), b0), _, a2, a3} : M.CmBlock} 694 %bx.ru32(a2, b2) : {M.CmBlock.xor(M.CmBlock.xor(M.CmBlock{a0, a1, a2, a3}, M.CmBlock{b0, b1, b2, b3}), M.CmBlock{b0, b1, b2, b3}) == M.CmBlock{U32.xor(U32.xor(a0, b0), b0), U32.xor(U32.xor(a1, b1), b1), _, a3} : M.CmBlock} 695 %bx.ru32(a3, b3) : {M.CmBlock.xor(M.CmBlock.xor(M.CmBlock{a0, a1, a2, a3}, M.CmBlock{b0, b1, b2, b3}), M.CmBlock{b0, b1, b2, b3}) == M.CmBlock{U32.xor(U32.xor(a0, b0), b0), U32.xor(U32.xor(a1, b1), b1), U32.xor(U32.xor(a2, b2), b2), _} : M.CmBlock} 696 {==} 697 698 # More on joining and splitting 699 700 def sp.mask_join_onto(bs: List<&2, M.CmBlock>, +rest: List<&2, U32>) -> {B.mask(M.cm.join_onto(bs, rest)) == M.cm.join_onto(bs, B.mask(rest)) : List<&2, U32>}: 701 match bs: 702 case Nil{}: 703 {==} 704 case Con{+b, +t}: 705 %Equal.sym(List<&2, U32>, B.mask(M.cm.bytes_onto(b, M.cm.join_onto(t, rest))), M.cm.bytes_onto(b, B.mask(M.cm.join_onto(t, rest))), sp.mask_blk(b, M.cm.join_onto(t, rest))) : {_ == M.cm.bytes_onto(b, M.cm.join_onto(t, B.mask(rest))) : List<&2, U32>} 706 %sp.mask_join_onto(t, rest) : {M.cm.bytes_onto(b, B.mask(M.cm.join_onto(t, rest))) == M.cm.bytes_onto(b, _) : List<&2, U32>} 707 {==} 708 709 # blocks joined in front of a short tail split back into those blocks and tail 710 def sp.split_join_short(bs: List<&2, M.CmBlock>, +rest: List<&2, U32>) -> {M.cm.split(rest) == M.CmSplit{Nil{}, rest} : M.CmSplit} -> {M.cm.split(M.cm.join_onto(bs, rest)) == M.CmSplit{bs, rest} : M.CmSplit}: 711 match bs: 712 case Nil{}: 713 h => h 714 case Con{+b, +t}: 715 h => %Equal.sym(M.CmSplit, M.cm.split(M.cm.bytes_onto(b, M.cm.join_onto(t, rest))), M.cm.split.cons(b, M.cm.split(M.cm.join_onto(t, rest))), sp.blk(b, M.cm.join_onto(t, rest))) : {_ == M.CmSplit{Con{b, t}, rest} : M.CmSplit} 716 %Equal.sym(M.CmSplit, M.cm.split(M.cm.join_onto(t, rest)), M.CmSplit{t, rest}, sp.split_join_short(t, rest)(h)) : {M.cm.split.cons(b, _) == M.CmSplit{Con{b, t}, rest} : M.CmSplit} 717 {==} 718 719 def li.len_bytes(+b: M.CmBlock, +rest: List<&2, U32>) -> {B.len(M.cm.bytes_onto(b, rest)) == Nat.add(16n, B.len(rest)) : Nat}: 720 {==} 721 722 # A block through Octets and back 723 724 def Laws.block_octets_round_trip(b): 725 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(M.cm.bytes_of(b))), B.mask(M.cm.bytes_of(b)), BL.octets_to_of(M.cm.bytes_of(b))) : {M.CmBlock.of_octets.pick(Nat.is_eq(B.len(_), 16n), _) == Some{b} : Maybe<&2, M.CmBlock>} 726 %Equal.sym(List<&2, U32>, B.mask(M.cm.bytes_onto(b, Nil{})), M.cm.bytes_onto(b, B.mask(Nil{})), sp.mask_blk(b, Nil{})) : {M.CmBlock.of_octets.pick(Nat.is_eq(B.len(_), 16n), _) == Some{b} : Maybe<&2, M.CmBlock>} 727 %Equal.sym(M.CmBlock, M.cm.block_of(M.cm.bytes_of(b)), b, sp.block_bytes(b)) : {Some{_} == Some{b} : Maybe<&2, M.CmBlock>} 728 {==} 729 730 # The laws of the lemmas the modes share: each is the lemma above 731 732 def Laws.byte_byte(y): 733 bits.byte_byte(y) 734 735 def Laws.split_cons_blocks(b, s): 736 sp.cons_blocks(b, s) 737 738 def Laws.split_cons_tail(b, s): 739 sp.cons_tail(b, s) 740 741 def Laws.split_eta(s): 742 sp.eta(s) 743 744 def Laws.list_take_append(a, b): 745 li.take_append(a, b) 746 747 def Laws.list_drop_append(a, b): 748 li.drop_append(a, b) 749 750 def Laws.list_mask_append(a, b): 751 li.mask_append(a, b) 752 753 def Laws.list_mask_take(n, xs): 754 li.mask_take(n, xs) 755 756 def Laws.list_len_append(a, b): 757 li.len_append(a, b) 758 759 def Laws.list_len_take(n, xs, h1): 760 li.len_take(n, xs)(h1) 761 762 def Laws.nat_lt_le(a, b, h1): 763 na.lt_le(a, b)(h1) 764 765 def Laws.split_bytes_onto(b, rest): 766 sp.blk(b, rest) 767 768 def Laws.mask_bytes_onto(b, rest): 769 sp.mask_blk(b, rest) 770 771 def Laws.join_split(ys): 772 sp.join_split(ys) 773 774 def Laws.bytes_onto_block16(z0, z1, z2, z3, z4, z5, z6, z7, z8, z9, z10, z11, z12, z13, z14, z15, rest): 775 sp.blk16g(z0, z1, z2, z3, z4, z5, z6, z7, z8, z9, z10, z11, z12, z13, z14, z15, rest) 776 777 def Laws.split_tail_short(ys): 778 sp.tail_short(ys) 779 780 def Laws.split_tail_masked(ys): 781 sp.tail_masked(ys) 782 783 def Laws.split_short(ys, h1): 784 sp.short_split(ys)(h1) 785 786 def Laws.block_of_bytes_of(b): 787 sp.block_bytes(b) 788 789 def Laws.octets_masked(o): 790 oc.masked(o) 791 792 def Laws.octets_len(o, n, h): 793 oc.len(o, n, h) 794 795 def Laws.blocks_len_fast(bs): 796 tr.len_eq(bs) 797 798 def Laws.split_fast(xs): 799 tr.split_eq(xs) 800 801 def Laws.join_onto_fast(bs, rest): 802 tr.join_eq(bs, rest) 803 804 def Laws.bind_cong(r, f, g, h): 805 tr.bind_cong(r, f, g, h) 806 807 def Laws.dec_enc_head(K, enc, dec, k, x, xs, h): 808 cmp.hd(~K, ~enc, ~dec, k, x, xs, h) 809 810 def Laws.dec_enc_tail(K, enc, dec, k, x, xs, h): 811 cmp.tl(~K, ~enc, ~dec, k, x, xs, h) 812 813 def Laws.word_xor_xor(n, a, b): 814 bx.rword(n, a, b) 815 816 def Laws.u32_xor_xor(a, b): 817 bx.ru32(a, b) 818 819 def Laws.block_xor_xor(a, b): 820 bx.rblock(a, b) 821 822 def Laws.mask_join_onto(bs, rest): 823 sp.mask_join_onto(bs, rest) 824 825 def Laws.split_join_short(bs, rest, h1): 826 sp.split_join_short(bs, rest)(h1)