1 import Base 2 import ../../../../src/crypto/blake/blake3/types.bend as T 3 import ../../../../src/crypto/blake/blake3/blake3.bend as K 4 import ../../../lib/nat.bend as N 5 import ../../../../spec/lib/common.bend as SC 6 import ../../../../spec/crypto/blake/blake3.bend as S 7 import ./array.bend as A 8 import ./lists.bend as LS 9 import ./chunk.bend as CH 10 import ./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. 18 def 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 23 def 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 28 def 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 33 def 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 38 def 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 43 def 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 48 def 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 53 def 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|. 59 def 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. 65 def run_chunks(+n: Nat, +t: U32, +index: U32, +len: Nat, q: Array & 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 70 def base_run(+t: U32, +index: U32, +len: Nat, q: Array & T.Out, +s: K.Stack) -> {run(s,S.chunks(0n,t,index,len,q)) == K.finish(s,Pair.snd(Array,T.Out,q)) : T.Out}: 71 (a,o) = q 72 {==} 73 74 def run2_run(+p: Nat, +t: U32, +index: U32, +len: Nat, q: Array & 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 81 def fuse_zero(+t: U32, +index: U32, +len: Nat, -a: Array, +s: K.Stack, view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array}>) -> {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,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,T.Out,K.last_chunk(A.thaw(tree),t,index,len))), 87 K.finish(s,Pair.snd(Array,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 & T.Out,T.Out,q => K.finish(s,Pair.snd(Array,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,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 92 def fuse_step2(+p: Nat, +t: U32, +index: U32, +len: Nat, +s: K.Stack, -a: Array, +o: T.Out, 93 view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array}>, 94 rec: @a2: Array -> @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,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 114 def fuse_step(+p: Nat, +t: U32, +index: U32, +len: Nat, +s: K.Stack, q: Array & T.Out, 115 rec: @a2: Array -> @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 120 def fuse_one(+p: Nat, +t: U32, +index: U32, +len: Nat, -a: Array, +s: K.Stack, 121 view: Sigma<&2,&1,A.Tree,x => {a == A.thaw(x) : Array}>, 122 rec: @a2: Array -> @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,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 & 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 135 law fuse: 136 for +n: Nat 137 for +t: U32 138 for +index: U32 139 for +len: Nat 140 for a: Array 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 144 def 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))