~/jendhub

proofs/crypto/blake/blake3/loop.bend

bend-collections-laws-crypto@1.0.0.0 · 147 lines · 17 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/blake3.bend as K
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
5import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as S
7import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/array.bend as A
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend as LS
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/chunk.bend as CH
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend as TR
11
12# The implementation's chunk loop (read a chunk, push its chaining value)
13# equals running the stack over the specification's list of chunk outputs,
14# which in turn is the specification's tree over that list.
15
16# The stack run over a list of outputs: every output but the last is pushed
17# as a chaining value, the last one is pending.
18def run2(rest: List<&2,T.Out>, s: K.Stack, x: T.Out) -> T.Out:
19  match rest:
20    case Nil{}: K.finish(s,x)
21    case Con{y,r}: run2(r,K.push(s,K.out_cv(x)),y)
22
23def run(s: K.Stack, xs: List<&2,T.Out>) -> T.Out:
24  match xs:
25    case Nil{}: S.first(Nil{})
26    case Con{x,r}: run2(r,s,x)
27
28def init2(rest: List<&2,T.Out>, +x: T.Out) -> List<&2,T.Out>:
29  match rest:
30    case Nil{}: Nil{}
31    case Con{y,r}: Con{x,init2(r,y)}
32
33def last2(rest: List<&2,T.Out>, +x: T.Out) -> T.Out:
34  match rest:
35    case Nil{}: x
36    case Con{y,r}: last2(r,y)
37
38def run2_split(+r: List<&2,T.Out>, +s: K.Stack, +x: T.Out) -> {run2(r,s,x) == K.finish(TR.push_all(s,TR.cvs(init2(r,x))),last2(r,x)) : T.Out}:
39  match r:
40    case Nil{}: {==}
41    case Con{+y,+q}: run2_split(q,K.push(s,K.out_cv(x)),y)
42
43def snoc2(+r: List<&2,T.Out>, +x: T.Out) -> {SC.append(T.Out,init2(r,x),Con{last2(r,x),Nil{}}) == Con{x,r} : List<&2,T.Out>}:
44  match r:
45    case Nil{}: {==}
46    case Con{+y,+q}: LS.cons_cong(T.Out,x,SC.append(T.Out,init2(q,y),Con{last2(q,y),Nil{}}),Con{y,q},snoc2(q,y))
47
48def len_init2(+r: List<&2,T.Out>, +x: T.Out) -> {SC.length(T.Out,init2(r,x)) == SC.length(T.Out,r) : Nat}:
49  match r:
50    case Nil{}: {==}
51    case Con{+y,+q}: N.succ_cong(SC.length(T.Out,init2(q,y)),SC.length(T.Out,q),len_init2(q,y))
52
53def run_tree_go(+x: T.Out, +r: List<&2,T.Out>) -> {K.finish(TR.push_all(K.StkNil{},TR.cvs(init2(r,x))),last2(r,x)) == S.tree(1n+SC.length(T.Out,r),Con{x,r}) : T.Out}:
54  %snoc2(r,x) : {K.finish(TR.push_all(K.StkNil{},TR.cvs(init2(r,x))),last2(r,x)) == S.tree(1n+SC.length(T.Out,r),_) : T.Out}
55  %len_init2(r,x) : {K.finish(TR.push_all(K.StkNil{},TR.cvs(init2(r,x))),last2(r,x)) == S.tree(1n+_,SC.append(T.Out,init2(r,x),Con{last2(r,x),Nil{}})) : T.Out}
56  TR.tree_stack(init2(r,x),last2(r,x))
57
58# A nonempty list of outputs: the stack run is the tree of height |list|.
59def run_tree(+x: T.Out, +r: List<&2,T.Out>) -> {run(K.StkNil{},Con{x,r}) == S.tree(SC.length(T.Out,Con{x,r}),Con{x,r}) : T.Out}:
60  Equal.trans(T.Out,run2(r,K.StkNil{},x),K.finish(TR.push_all(K.StkNil{},TR.cvs(init2(r,x))),last2(r,x)),S.tree(1n+SC.length(T.Out,r),Con{x,r}),
61    run2_split(r,K.StkNil{},x),
62    run_tree_go(x,r))
63
64# The specification's chunk list is never empty.
65def run_chunks(+n: Nat, +t: U32, +index: U32, +len: Nat, q: Array<U32> & T.Out) -> {run(K.StkNil{},S.chunks(n,t,index,len,q)) == S.tree(SC.length(T.Out,S.chunks(n,t,index,len,q)),S.chunks(n,t,index,len,q)) : T.Out}:
66  match n q:
67    case 0n Tuple{a,o}: run_tree(o,Nil{})
68    case 1n+p Tuple{a,o}: run_tree(o,S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,a)))
69
70def base_run(+t: U32, +index: U32, +len: Nat, q: Array<U32> & T.Out, +s: K.Stack) -> {run(s,S.chunks(0n,t,index,len,q)) == K.finish(s,Pair.snd(Array<U32>,T.Out,q)) : T.Out}:
71  (a,o) = q
72  {==}
73
74def run2_run(+p: Nat, +t: U32, +index: U32, +len: Nat, q: Array<U32> & T.Out, +s: K.Stack, +o: T.Out) -> {run2(S.chunks(p,t,index,len,q),s,o) == run(K.push(s,K.out_cv(o)),S.chunks(p,t,index,len,q)) : T.Out}:
75  match p q:
76    case 0n Tuple{a,y}: {==}
77    case 1n+g Tuple{a,y}: {==}
78
79# ---- the loop ----
80
81def fuse_zero(+t: U32, +index: U32, +len: Nat, -a: Array<U32>, +s: K.Stack, view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array<U32>}>) -> {K.chunks(0n,t,index,len,(a,s)) == run(s,S.chunks(0n,t,index,len,S.chunk_at(0n,t,index,len,a))) : T.Out}:
82  match view:
83    case Tuple{+tree,pf}:
84      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {K.chunks(0n,t,index,len,(_,s)) == run(s,S.chunks(0n,t,index,len,S.chunk_at(0n,t,index,len,_))) : T.Out}
85      Equal.trans(T.Out,
86        K.finish(s,Pair.snd(Array<U32>,T.Out,K.last_chunk(A.thaw(tree),t,index,len))),
87        K.finish(s,Pair.snd(Array<U32>,T.Out,S.chunk(A.thaw(tree),t,index,len))),
88        run(s,S.chunks(0n,t,index,len,S.chunk(A.thaw(tree),t,index,len))),
89        Equal.cong(Array<U32> & T.Out,T.Out,q => K.finish(s,Pair.snd(Array<U32>,T.Out,q)),K.last_chunk(A.thaw(tree),t,index,len),S.chunk(A.thaw(tree),t,index,len),CH.last_chunk_correct(A.thaw(tree),t,index,len)),
90        Equal.sym(T.Out,run(s,S.chunks(0n,t,index,len,S.chunk(A.thaw(tree),t,index,len))),K.finish(s,Pair.snd(Array<U32>,T.Out,S.chunk(A.thaw(tree),t,index,len))),base_run(t,index,len,S.chunk(A.thaw(tree),t,index,len),s)))
91
92def fuse_step2(+p: Nat, +t: U32, +index: U32, +len: Nat, +s: K.Stack, -a: Array<U32>, +o: T.Out,
93    view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array<U32>}>,
94    rec: @a2: Array<U32> -> @s2: K.Stack -> {K.chunks(p,U32.inc(t),U32.add(index,256),len,(a2,s2)) == run(s2,S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,a2))) : T.Out}
95  ) -> {K.chunks(p,U32.inc(t),U32.add(index,256),len,K.pushed(s,CH.outcv((a,o)))) == run(s,S.chunks(1n+p,t,index,len,(a,o))) : T.Out}:
96  match view:
97    case Tuple{+tree,pf}:
98      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {K.chunks(p,U32.inc(t),U32.add(index,256),len,K.pushed(s,CH.outcv((_,o)))) == run(s,S.chunks(1n+p,t,index,len,(_,o))) : T.Out}
99      Equal.trans(T.Out,
100        K.chunks(p,U32.inc(t),U32.add(index,256),len,(A.thaw(tree),K.push(s,S.cv(o)))),
101        run(K.push(s,S.cv(o)),S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree)))),
102        run2(S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree))),s,o),
103        rec(A.thaw(tree),K.push(s,S.cv(o))),
104        Equal.trans(T.Out,
105          run(K.push(s,S.cv(o)),S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree)))),
106          run(K.push(s,K.out_cv(o)),S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree)))),
107          run2(S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree))),s,o),
108          Equal.cong(T.CV,T.Out,c => run(K.push(s,c),S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree)))),
109            S.cv(o),K.out_cv(o),Equal.sym(T.CV,K.out_cv(o),S.cv(o),TR.out_cv_correct(o))),
110          Equal.sym(T.Out,run2(S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree))),s,o),
111            run(K.push(s,K.out_cv(o)),S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree)))),
112            run2_run(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,A.thaw(tree)),s,o))))
113
114def fuse_step(+p: Nat, +t: U32, +index: U32, +len: Nat, +s: K.Stack, q: Array<U32> & T.Out,
115    rec: @a2: Array<U32> -> @s2: K.Stack -> {K.chunks(p,U32.inc(t),U32.add(index,256),len,(a2,s2)) == run(s2,S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,a2))) : T.Out}
116  ) -> {K.chunks(p,U32.inc(t),U32.add(index,256),len,K.pushed(s,CH.outcv(q))) == run(s,S.chunks(1n+p,t,index,len,q)) : T.Out}:
117  (a,o) = q
118  fuse_step2(p,t,index,len,s,a,o,A.reify(a),rec)
119
120def fuse_one(+p: Nat, +t: U32, +index: U32, +len: Nat, -a: Array<U32>, +s: K.Stack,
121    view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array<U32>}>,
122    rec: @a2: Array<U32> -> @s2: K.Stack -> {K.chunks(p,U32.inc(t),U32.add(index,256),len,(a2,s2)) == run(s2,S.chunks(p,U32.inc(t),U32.add(index,256),len,S.chunk_at(p,U32.inc(t),U32.add(index,256),len,a2))) : T.Out}
123  ) -> {K.chunks(1n+p,t,index,len,(a,s)) == run(s,S.chunks(1n+p,t,index,len,S.chunk_at(1n+p,t,index,len,a))) : T.Out}:
124  match view:
125    case Tuple{+tree,pf}:
126      %Equal.sym(Array<U32>,a,A.thaw(tree),pf) : {K.chunks(1n+p,t,index,len,(_,s)) == run(s,S.chunks(1n+p,t,index,len,S.chunk_at(1n+p,t,index,len,_))) : T.Out}
127      Equal.trans(T.Out,
128        K.chunks(p,U32.inc(t),U32.add(index,256),len,K.pushed(s,K.full_chunk(A.thaw(tree),t,index))),
129        K.chunks(p,U32.inc(t),U32.add(index,256),len,K.pushed(s,CH.outcv(S.chunk(A.thaw(tree),t,index,1024n)))),
130        run(s,S.chunks(1n+p,t,index,len,S.chunk(A.thaw(tree),t,index,1024n))),
131        Equal.cong(Array<U32> & T.CV,T.Out,q => K.chunks(p,U32.inc(t),U32.add(index,256),len,K.pushed(s,q)),
132          K.full_chunk(A.thaw(tree),t,index),CH.outcv(S.chunk(A.thaw(tree),t,index,1024n)),CH.full_chunk_correct(A.thaw(tree),t,index)),
133        fuse_step(p,t,index,len,s,S.chunk(A.thaw(tree),t,index,1024n),rec))
134
135law fuse:
136  for +n: Nat
137  for +t: U32
138  for +index: U32
139  for +len: Nat
140  for a: Array<U32>
141  for +s: K.Stack
142  {K.chunks(n,t,index,len,(a,s)) == run(s,S.chunks(n,t,index,len,S.chunk_at(n,t,index,len,a))) : T.Out}
143
144def fuse(n,t,index,len,a,s):
145  match n:
146    case 0n: fuse_zero(t,index,len,a,s,A.reify(a))
147    case 1n+p: fuse_one(p,t,index,len,a,s,A.reify(a),a2 => s2 => fuse(p,U32.inc(t),U32.add(index,256),len,a2,s2))