Tree.partial_big: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend as Tree Lines 255-285 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&start_line=255&end_line=285 import Base import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend as K import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as S import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend as LS # At least 2^p outputs before o: a complete left subtree of 2^p chunks, then # the rest with o. def partial_big(+p: Nat, +fs: List<&2,T.Out>, +o: T.Out, +t: K.Stack, +hl: {Nat.is_lt(SC.length(T.Out,fs),SC.pow2(1n+p)) == True{} : Bool}, +hb: {Nat.is_lt(SC.length(T.Out,fs),SC.pow2(p)) == False{} : Bool}, rec: @f2: List<&2,T.Out> -> @t2: K.Stack -> @h2: {Nat.is_lt(SC.length(T.Out,f2),SC.pow2(p)) == True{} : Bool} -> {K.finish(push_all(E(p,t2),cvs(f2)),o) == K.finish(t2,S.tree(p,SC.append(T.Out,f2,Con{o,Nil{}}))) : T.Out} ) -> {K.finish(push_all(E(1n+p,t),cvs(fs)),o) == K.finish(t,S.tree(1n+p,SC.append(T.Out,fs,Con{o,Nil{}}))) : T.Out}: +xs = SC.append(T.Out,fs,Con{o,Nil{}}) +k = SC.pow2(p) +f1 = SC.take(T.Out,fs,k) +f2 = SC.drop(T.Out,fs,k) +c1 = S.cv(S.tree(p,f1)) +t2 = S.tree(p,SC.append(T.Out,f2,Con{o,Nil{}})) +kl = N.not_lt_le(SC.length(T.Out,fs),k,hb) +h1 = LS.length_take(T.Out,fs,k,kl) +h2 = {%Equal.sym(Nat,SC.length(T.Out,f2),Nat.sub(SC.length(T.Out,fs),k),LS.length_drop(T.Out,fs,k)) : {Nat.is_lt(_,k) == True{} : Bool} N.sub_lt(SC.length(T.Out,fs),k,k,kl,{%LS.double_add(k) : {Nat.is_lt(SC.length(T.Out,fs),_) == True{} : Bool} hl : {Nat.is_lt(SC.length(T.Out,fs),Nat.add(k,k)) == True{} : Bool}}) : {Nat.is_lt(SC.length(T.Out,f2),k) == True{} : Bool}} %Equal.sym(T.Out,S.tree(1n+p,xs),S.join(S.tree(p,SC.take(T.Out,xs,k)),S.tree(p,SC.drop(T.Out,xs,k)),S.is_nil(SC.drop(T.Out,xs,k))),tree_con(p,xs,snoc_ne(fs,o))) : {K.finish(push_all(E(1n+p,t),cvs(fs)),o) == K.finish(t,_) : T.Out} %Equal.sym(List<&2,T.Out>,SC.take(T.Out,xs,k),f1,LS.take_append_left(T.Out,fs,Con{o,Nil{}},k,kl)) : {K.finish(push_all(E(1n+p,t),cvs(fs)),o) == K.finish(t,S.join(S.tree(p,_),S.tree(p,SC.drop(T.Out,xs,k)),S.is_nil(SC.drop(T.Out,xs,k)))) : T.Out} %Equal.sym(List<&2,T.Out>,SC.drop(T.Out,xs,k),SC.append(T.Out,f2,Con{o,Nil{}}),LS.drop_append_left(T.Out,fs,Con{o,Nil{}},k,kl)) : {K.finish(push_all(E(1n+p,t),cvs(fs)),o) == K.finish(t,S.join(S.tree(p,f1),S.tree(p,_),S.is_nil(_))) : T.Out} %Equal.sym(Bool,S.is_nil(SC.append(T.Out,f2,Con{o,Nil{}})),False{},snoc_ne(f2,o)) : {K.finish(push_all(E(1n+p,t),cvs(fs)),o) == K.finish(t,S.join(S.tree(p,f1),t2,_)) : T.Out} %Equal.sym(T.Out,S.join(S.tree(p,f1),t2,False{}),S.parent(c1,S.cv(t2)),join_false(S.tree(p,f1),t2)) : {K.finish(push_all(E(1n+p,t),cvs(fs)),o) == K.finish(t,_) : T.Out} %out_cv_correct(t2) : {K.finish(push_all(E(1n+p,t),cvs(fs)),o) == K.finish(t,S.parent(c1,_)) : T.Out} %parent_out_correct(c1,K.out_cv(t2)) : {K.finish(push_all(E(1n+p,t),cvs(fs)),o) == K.finish(t,_) : T.Out} %LS.take_drop(T.Out,fs,k) : {K.finish(push_all(E(1n+p,t),cvs(_)),o) == K.finish(t,K.parent_out(c1,K.out_cv(t2))) : T.Out} %Equal.sym(K.Stack,E(1n+p,t),E(p,lift(t)),E_succ(p,t)) : {K.finish(push_all(_,cvs(SC.append(T.Out,f1,f2))),o) == K.finish(t,K.parent_out(c1,K.out_cv(t2))) : T.Out} %Equal.sym(K.Stack,push_all(E(p,lift(t)),cvs(SC.append(T.Out,f1,f2))),push_all(push_all(E(p,lift(t)),cvs(f1)),cvs(f2)),push_split(E(p,lift(t)),f1,f2)) : {K.finish(_,o) == K.finish(t,K.parent_out(c1,K.out_cv(t2))) : T.Out} %Equal.sym(K.Stack,push_all(E(p,lift(t)),cvs(f1)),E(p,K.push(lift(t),c1)),complete(p,f1,lift(t),h1)) : {K.finish(push_all(_,cvs(f2)),o) == K.finish(t,K.parent_out(c1,K.out_cv(t2))) : T.Out} %Equal.sym(K.Stack,K.push(lift(t),c1),K.SFull{c1,t},push_lift(t,c1)) : {K.finish(push_all(E(p,_),cvs(f2)),o) == K.finish(t,K.parent_out(c1,K.out_cv(t2))) : T.Out} rec(f2,K.SFull{c1,t},h2) Uses (44): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend&name=double_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend&name=drop_append_left https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend&name=length_drop https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend&name=length_take https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend&name=take_append_left https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend&name=take_drop https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=E https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=E_succ https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=complete https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=cvs https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=join_false https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=lift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=out_cv_correct https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=parent_out_correct https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=push_all https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=push_lift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=push_split https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=snoc_ne https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=tree_con https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=not_lt_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=sub_lt https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=cv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=is_nil https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=join https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=parent https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=tree https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=append https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=drop https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=length https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=pow2 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=take https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=Stack https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=finish https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=out_cv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=parent_out https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=push https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend&name=Out