proofs/crypto/blake/blake3/chunk.bend

bend-collections-laws-crypto@1.0.0.0 · 211 lines · 12 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/compress.bend as C
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend as K
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as S
6import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/compress.bend as P
7import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/read.bend as R
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/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
14def outcv(q: Array<U32> & T.Out) -> Array<U32> & 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.
20law 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
27def 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
33law 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<U32>
41  for +b: T.Block
42  for view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array<U32>}>
43  for recurse: @c: T.CV -> @q: (Array<U32> & 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<U32> & 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<U32> & T.Out}
45
46def last_step(p,t,index,flags,len,cv,a,b,view,recurse):
47  match view:
48    case Tuple{+tree,pf}:
49      %Equal.sym(Array<U32>,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<U32> & T.Out}
50      Equal.trans(Array<U32> & 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<U32> & 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<U32> & T.Block,Array<U32> & 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<U32> & 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
64law 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<U32>
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<U32> & T.Out}
73
74def 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<U32> & T.Out}
76  {==}
77
78law 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<U32> & T.Block
86  {K.last_go(n,t,index,flags,len,cv,pair) == S.chunk_blocks(n,t,index,flags,len,cv,pair) : Array<U32> & T.Out}
87
88def 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
96law 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<U32>
103  for +b: T.Block
104  for view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array<U32>}>
105  for recurse: @c: T.CV -> @q: (Array<U32> & 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<U32> & 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<U32> & T.CV}
107
108def full_step(p,t,index,flags,cv,a,b,view,recurse):
109  match view:
110    case Tuple{+tree,pf}:
111      %Equal.sym(Array<U32>,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<U32> & T.CV}
112      Equal.trans(Array<U32> & 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<U32> & 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<U32> & T.Block,Array<U32> & 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<U32> & 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
126law full_base:
127  for +t: U32
128  for +index: U32
129  for +flags: U32
130  for +cv: T.CV
131  for -a: Array<U32>
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<U32> & T.CV}
134
135def full_base(t,index,flags,cv,a,b):
136  Equal.cong(T.CV,Array<U32> & 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
138law 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<U32> & T.Block
145  {K.full_go(n,t,index,flags,cv,pair) == outcv(S.chunk_blocks(n,t,index,flags,64n,cv,pair)) : Array<U32> & T.CV}
146
147def 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
155law full_chunk_view:
156  for -a: Array<U32>
157  for +t: U32
158  for +index: U32
159  for view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array<U32>}>
160  {K.full_chunk(a,t,index) == outcv(S.chunk(a,t,index,1024n)) : Array<U32> & T.CV}
161
162def full_chunk_view(a,t,index,view):
163  match view:
164    case Tuple{+tree,pf}:
165      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {K.full_chunk(_,t,index) == outcv(S.chunk(_,t,index,1024n)) : Array<U32> & T.CV}
166      Equal.trans(Array<U32> & 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<U32> & T.Block,Array<U32> & 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
174law full_chunk_correct:
175  for a: Array<U32>
176  for +t: U32
177  for +index: U32
178  {K.full_chunk(a,t,index) == outcv(S.chunk(a,t,index,1024n)) : Array<U32> & T.CV}
179
180def full_chunk_correct(a,t,index):
181  full_chunk_view(a,t,index,A.reify(a))
182
183law last_chunk_view:
184  for -a: Array<U32>
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<U32>}>
189  {K.last_chunk(a,t,index,len) == S.chunk(a,t,index,len) : Array<U32> & T.Out}
190
191def last_chunk_view(a,t,index,len,view):
192  match view:
193    case Tuple{+tree,pf}:
194      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {K.last_chunk(_,t,index,len) == S.chunk(_,t,index,len) : Array<U32> & T.Out}
195      Equal.trans(Array<U32> & 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<U32> & T.Block,Array<U32> & 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
203law last_chunk_correct:
204  for a: Array<U32>
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<U32> & T.Out}
209
210def last_chunk_correct(a,t,index,len):
211  last_chunk_view(a,t,index,len,A.reify(a))