1 import Base 2 import ../../../../src/crypto/blake/blake3/types.bend as T 3 import ../../../../src/crypto/blake/blake3/compress.bend as C 4 import ../../../../src/crypto/blake/blake3/blake3.bend as K 5 import ../../../../spec/crypto/blake/blake3.bend as S 6 import ./compress.bend as P 7 import ./read.bend as R 8 import ./array.bend as A 9 10 # The implementation's chunk loops equal the specification's chunk: a full 11 # chunk's chaining value is the chaining value of the specification's chunk 12 # output, and the last chunk's pending output is the specification's. 13 14 def outcv(q: Array & T.Out) -> Array & T.CV: 15 (a,o) = q 16 (a,S.cv(o)) 17 18 # A full (64-byte) block: the implementation compresses the raw block, the 19 # specification the block truncated to 64 bytes. 20 law compress_full: 21 for +cv: T.CV 22 for +b: T.Block 23 for +t: U32 24 for +flags: U32 25 {C.compress(cv,b,t,64,flags) == S.compress(cv,S.zero_tail(b,64n),t,64,flags) : T.CV} 26 27 def compress_full(cv,b,t,flags): 28 %Equal.sym(T.Block,S.zero_tail(b,64n),b,R.zero_tail_full(b)) : {C.compress(cv,b,t,64,flags) == S.compress(cv,_,t,64,flags) : T.CV} 29 P.compress_correct(cv,b,t,64,flags) 30 31 # ---- the last chunk ---- 32 33 law last_step: 34 for +p: Nat 35 for +t: U32 36 for +index: U32 37 for +flags: U32 38 for +len: Nat 39 for +cv: T.CV 40 for -a: Array 41 for +b: T.Block 42 for view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array}> 43 for recurse: @c: T.CV -> @q: (Array & T.Block) -> {K.last_go(p,t,U32.add(index,16),0,len,c,q) == S.chunk_blocks(p,t,U32.add(index,16),0,len,c,q) : Array & T.Out} 44 {K.last_go(1n+p,t,index,flags,len,cv,(a,b)) == S.chunk_blocks(1n+p,t,index,flags,len,cv,(a,b)) : Array & T.Out} 45 46 def last_step(p,t,index,flags,len,cv,a,b,view,recurse): 47 match view: 48 case Tuple{+tree,pf}: 49 %Equal.sym(Array,a,A.thaw(tree),pf) : {K.last_go(1n+p,t,index,flags,len,cv,(_,b)) == S.chunk_blocks(1n+p,t,index,flags,len,cv,(_,b)) : Array & T.Out} 50 Equal.trans(Array & T.Out, 51 K.last_go(p,t,U32.add(index,16),0,len,C.compress(cv,b,t,64,flags),K.read_block(A.thaw(tree),U32.add(index,16))), 52 S.chunk_blocks(p,t,U32.add(index,16),0,len,C.compress(cv,b,t,64,flags),K.read_block(A.thaw(tree),U32.add(index,16))), 53 S.chunk_blocks(p,t,U32.add(index,16),0,len,S.compress(cv,S.zero_tail(b,64n),t,64,flags),S.read_block(A.thaw(tree),U32.add(index,16))), 54 recurse(C.compress(cv,b,t,64,flags),K.read_block(A.thaw(tree),U32.add(index,16))), 55 Equal.trans(Array & T.Out, 56 S.chunk_blocks(p,t,U32.add(index,16),0,len,C.compress(cv,b,t,64,flags),K.read_block(A.thaw(tree),U32.add(index,16))), 57 S.chunk_blocks(p,t,U32.add(index,16),0,len,C.compress(cv,b,t,64,flags),S.read_block(A.thaw(tree),U32.add(index,16))), 58 S.chunk_blocks(p,t,U32.add(index,16),0,len,S.compress(cv,S.zero_tail(b,64n),t,64,flags),S.read_block(A.thaw(tree),U32.add(index,16))), 59 Equal.cong(Array & T.Block,Array & T.Out,q => S.chunk_blocks(p,t,U32.add(index,16),0,len,C.compress(cv,b,t,64,flags),q), 60 K.read_block(A.thaw(tree),U32.add(index,16)),S.read_block(A.thaw(tree),U32.add(index,16)),R.read_block_correct(A.thaw(tree),U32.add(index,16))), 61 Equal.cong(T.CV,Array & T.Out,c => S.chunk_blocks(p,t,U32.add(index,16),0,len,c,S.read_block(A.thaw(tree),U32.add(index,16))), 62 C.compress(cv,b,t,64,flags),S.compress(cv,S.zero_tail(b,64n),t,64,flags),compress_full(cv,b,t,flags)))) 63 64 law last_base: 65 for +t: U32 66 for +index: U32 67 for +flags: U32 68 for +len: Nat 69 for +cv: T.CV 70 for -a: Array 71 for +b: T.Block 72 {K.last_go(0n,t,index,flags,len,cv,(a,b)) == S.chunk_blocks(0n,t,index,flags,len,cv,(a,b)) : Array & T.Out} 73 74 def last_base(t,index,flags,len,cv,a,b): 75 %R.mask_block_correct(b,len) : {(a,T.Out{cv,K.mask_block(b,len),t,U32.from_nat(len),U32.or(flags,2)}) == (a,T.Out{cv,_,t,U32.from_nat(len),U32.or(flags,2)}) : Array & T.Out} 76 {==} 77 78 law last_go_correct: 79 for +n: Nat 80 for +t: U32 81 for +index: U32 82 for +flags: U32 83 for +len: Nat 84 for +cv: T.CV 85 for pair: Array & T.Block 86 {K.last_go(n,t,index,flags,len,cv,pair) == S.chunk_blocks(n,t,index,flags,len,cv,pair) : Array & T.Out} 87 88 def last_go_correct(n,t,index,flags,len,cv,pair): 89 match n pair: 90 case 0n Tuple{a,b}: last_base(t,index,flags,len,cv,a,b) 91 case 1n+p Tuple{a,b}: 92 last_step(p,t,index,flags,len,cv,a,b,A.reify(a),c => q => last_go_correct(p,t,U32.add(index,16),0,len,c,q)) 93 94 # ---- full chunks ---- 95 96 law full_step: 97 for +p: Nat 98 for +t: U32 99 for +index: U32 100 for +flags: U32 101 for +cv: T.CV 102 for -a: Array 103 for +b: T.Block 104 for view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array}> 105 for recurse: @c: T.CV -> @q: (Array & T.Block) -> {K.full_go(p,t,U32.add(index,16),0,c,q) == outcv(S.chunk_blocks(p,t,U32.add(index,16),0,64n,c,q)) : Array & T.CV} 106 {K.full_go(1n+p,t,index,flags,cv,(a,b)) == outcv(S.chunk_blocks(1n+p,t,index,flags,64n,cv,(a,b))) : Array & T.CV} 107 108 def full_step(p,t,index,flags,cv,a,b,view,recurse): 109 match view: 110 case Tuple{+tree,pf}: 111 %Equal.sym(Array,a,A.thaw(tree),pf) : {K.full_go(1n+p,t,index,flags,cv,(_,b)) == outcv(S.chunk_blocks(1n+p,t,index,flags,64n,cv,(_,b))) : Array & T.CV} 112 Equal.trans(Array & T.CV, 113 K.full_go(p,t,U32.add(index,16),0,C.compress(cv,b,t,64,flags),K.read_block(A.thaw(tree),U32.add(index,16))), 114 outcv(S.chunk_blocks(p,t,U32.add(index,16),0,64n,C.compress(cv,b,t,64,flags),K.read_block(A.thaw(tree),U32.add(index,16)))), 115 outcv(S.chunk_blocks(p,t,U32.add(index,16),0,64n,S.compress(cv,S.zero_tail(b,64n),t,64,flags),S.read_block(A.thaw(tree),U32.add(index,16)))), 116 recurse(C.compress(cv,b,t,64,flags),K.read_block(A.thaw(tree),U32.add(index,16))), 117 Equal.trans(Array & T.CV, 118 outcv(S.chunk_blocks(p,t,U32.add(index,16),0,64n,C.compress(cv,b,t,64,flags),K.read_block(A.thaw(tree),U32.add(index,16)))), 119 outcv(S.chunk_blocks(p,t,U32.add(index,16),0,64n,C.compress(cv,b,t,64,flags),S.read_block(A.thaw(tree),U32.add(index,16)))), 120 outcv(S.chunk_blocks(p,t,U32.add(index,16),0,64n,S.compress(cv,S.zero_tail(b,64n),t,64,flags),S.read_block(A.thaw(tree),U32.add(index,16)))), 121 Equal.cong(Array & T.Block,Array & T.CV,q => outcv(S.chunk_blocks(p,t,U32.add(index,16),0,64n,C.compress(cv,b,t,64,flags),q)), 122 K.read_block(A.thaw(tree),U32.add(index,16)),S.read_block(A.thaw(tree),U32.add(index,16)),R.read_block_correct(A.thaw(tree),U32.add(index,16))), 123 Equal.cong(T.CV,Array & T.CV,c => outcv(S.chunk_blocks(p,t,U32.add(index,16),0,64n,c,S.read_block(A.thaw(tree),U32.add(index,16)))), 124 C.compress(cv,b,t,64,flags),S.compress(cv,S.zero_tail(b,64n),t,64,flags),compress_full(cv,b,t,flags)))) 125 126 law full_base: 127 for +t: U32 128 for +index: U32 129 for +flags: U32 130 for +cv: T.CV 131 for -a: Array 132 for +b: T.Block 133 {K.full_go(0n,t,index,flags,cv,(a,b)) == outcv(S.chunk_blocks(0n,t,index,flags,64n,cv,(a,b))) : Array & T.CV} 134 135 def full_base(t,index,flags,cv,a,b): 136 Equal.cong(T.CV,Array & T.CV,c => (a,c),C.compress(cv,b,t,64,U32.or(flags,2)),S.compress(cv,S.zero_tail(b,64n),t,64,U32.or(flags,2)),compress_full(cv,b,t,U32.or(flags,2))) 137 138 law full_go_correct: 139 for +n: Nat 140 for +t: U32 141 for +index: U32 142 for +flags: U32 143 for +cv: T.CV 144 for pair: Array & T.Block 145 {K.full_go(n,t,index,flags,cv,pair) == outcv(S.chunk_blocks(n,t,index,flags,64n,cv,pair)) : Array & T.CV} 146 147 def full_go_correct(n,t,index,flags,cv,pair): 148 match n pair: 149 case 0n Tuple{a,b}: full_base(t,index,flags,cv,a,b) 150 case 1n+p Tuple{a,b}: 151 full_step(p,t,index,flags,cv,a,b,A.reify(a),c => q => full_go_correct(p,t,U32.add(index,16),0,c,q)) 152 153 # ---- whole chunks ---- 154 155 law full_chunk_view: 156 for -a: Array 157 for +t: U32 158 for +index: U32 159 for view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array}> 160 {K.full_chunk(a,t,index) == outcv(S.chunk(a,t,index,1024n)) : Array & T.CV} 161 162 def full_chunk_view(a,t,index,view): 163 match view: 164 case Tuple{+tree,pf}: 165 %Equal.sym(Array,a,A.thaw(tree),pf) : {K.full_chunk(_,t,index) == outcv(S.chunk(_,t,index,1024n)) : Array & T.CV} 166 Equal.trans(Array & T.CV, 167 K.full_go(15n,t,index,1,K.iv(),K.read_block(A.thaw(tree),index)), 168 outcv(S.chunk_blocks(15n,t,index,1,64n,K.iv(),K.read_block(A.thaw(tree),index))), 169 outcv(S.chunk_blocks(15n,t,index,1,64n,K.iv(),S.read_block(A.thaw(tree),index))), 170 full_go_correct(15n,t,index,1,K.iv(),K.read_block(A.thaw(tree),index)), 171 Equal.cong(Array & T.Block,Array & T.CV,q => outcv(S.chunk_blocks(15n,t,index,1,64n,K.iv(),q)), 172 K.read_block(A.thaw(tree),index),S.read_block(A.thaw(tree),index),R.read_block_correct(A.thaw(tree),index))) 173 174 law full_chunk_correct: 175 for a: Array 176 for +t: U32 177 for +index: U32 178 {K.full_chunk(a,t,index) == outcv(S.chunk(a,t,index,1024n)) : Array & T.CV} 179 180 def full_chunk_correct(a,t,index): 181 full_chunk_view(a,t,index,A.reify(a)) 182 183 law last_chunk_view: 184 for -a: Array 185 for +t: U32 186 for +index: U32 187 for +len: Nat 188 for view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array}> 189 {K.last_chunk(a,t,index,len) == S.chunk(a,t,index,len) : Array & T.Out} 190 191 def last_chunk_view(a,t,index,len,view): 192 match view: 193 case Tuple{+tree,pf}: 194 %Equal.sym(Array,a,A.thaw(tree),pf) : {K.last_chunk(_,t,index,len) == S.chunk(_,t,index,len) : Array & T.Out} 195 Equal.trans(Array & T.Out, 196 K.last_go(Nat.div(Nat.sub(len,1n),64n),t,index,1,Nat.sub(len,Nat.mul(Nat.div(Nat.sub(len,1n),64n),64n)),K.iv(),K.read_block(A.thaw(tree),index)), 197 S.chunk_blocks(Nat.div(Nat.sub(len,1n),64n),t,index,1,Nat.sub(len,Nat.mul(Nat.div(Nat.sub(len,1n),64n),64n)),K.iv(),K.read_block(A.thaw(tree),index)), 198 S.chunk_blocks(Nat.div(Nat.sub(len,1n),64n),t,index,1,Nat.sub(len,Nat.mul(Nat.div(Nat.sub(len,1n),64n),64n)),K.iv(),S.read_block(A.thaw(tree),index)), 199 last_go_correct(Nat.div(Nat.sub(len,1n),64n),t,index,1,Nat.sub(len,Nat.mul(Nat.div(Nat.sub(len,1n),64n),64n)),K.iv(),K.read_block(A.thaw(tree),index)), 200 Equal.cong(Array & T.Block,Array & T.Out,q => S.chunk_blocks(Nat.div(Nat.sub(len,1n),64n),t,index,1,Nat.sub(len,Nat.mul(Nat.div(Nat.sub(len,1n),64n),64n)),K.iv(),q), 201 K.read_block(A.thaw(tree),index),S.read_block(A.thaw(tree),index),R.read_block_correct(A.thaw(tree),index))) 202 203 law last_chunk_correct: 204 for a: Array 205 for +t: U32 206 for +index: U32 207 for +len: Nat 208 {K.last_chunk(a,t,index,len) == S.chunk(a,t,index,len) : Array & T.Out} 209 210 def last_chunk_correct(a,t,index,len): 211 last_chunk_view(a,t,index,len,A.reify(a))