def complete_step

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/tree.bend:191

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/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

191def complete_step(+g: Nat, +xs: List<&2,T.Out>, +t: K.Stack,
192    ne: {S.is_nil(xs) == False{} : Bool},
193    nd: {S.is_nil(SC.drop(T.Out,xs,SC.pow2(g))) == False{} : Bool},
194    ih1: {push_all(E(g,lift(t)),cvs(SC.take(T.Out,xs,SC.pow2(g)))) == E(g,K.push(lift(t),S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))))) : K.Stack},
195    ih2: {push_all(E(g,K.SFull{S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),t}),cvs(SC.drop(T.Out,xs,SC.pow2(g)))) == E(g,K.push(K.SFull{S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),t},S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g)))))) : K.Stack}
196  ) -> {push_all(E(1n+g,t),cvs(xs)) == E(1n+g,K.push(t,S.cv(S.tree(1n+g,xs)))) : K.Stack}:
197  %Equal.sym(T.Out,S.tree(1n+g,xs),S.join(S.tree(g,SC.take(T.Out,xs,SC.pow2(g))),S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))),S.is_nil(SC.drop(T.Out,xs,SC.pow2(g)))),tree_con(g,xs,ne)) : {push_all(E(1n+g,t),cvs(xs)) == E(1n+g,K.push(t,S.cv(_))) : K.Stack}
198  %Equal.sym(Bool,S.is_nil(SC.drop(T.Out,xs,SC.pow2(g))),False{},nd) : {push_all(E(1n+g,t),cvs(xs)) == E(1n+g,K.push(t,S.cv(S.join(S.tree(g,SC.take(T.Out,xs,SC.pow2(g))),S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))),_)))) : K.Stack}
199  %Equal.sym(T.Out,S.join(S.tree(g,SC.take(T.Out,xs,SC.pow2(g))),S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))),False{}),S.parent(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))),join_false(S.tree(g,SC.take(T.Out,xs,SC.pow2(g))),S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))) : {push_all(E(1n+g,t),cvs(xs)) == E(1n+g,K.push(t,S.cv(_))) : K.Stack}
200  %parent_cv_correct(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))) : {push_all(E(1n+g,t),cvs(xs)) == E(1n+g,K.push(t,_)) : K.Stack}
201  %Equal.sym(K.Stack,E(1n+g,K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))),E(g,lift(K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g)))))))),E_succ(g,K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g)))))))) : {push_all(E(1n+g,t),cvs(xs)) == _ : K.Stack}
202  %Equal.sym(K.Stack,lift(K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))),K.SEmpty{K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))},lift_push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))) : {push_all(E(1n+g,t),cvs(xs)) == E(g,_) : K.Stack}
203  %LS.take_drop(T.Out,xs,SC.pow2(g)) : {push_all(E(1n+g,t),cvs(_)) == E(g,K.SEmpty{K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))}) : K.Stack}
204  %Equal.sym(K.Stack,E(1n+g,t),E(g,lift(t)),E_succ(g,t)) : {push_all(_,cvs(SC.append(T.Out,SC.take(T.Out,xs,SC.pow2(g)),SC.drop(T.Out,xs,SC.pow2(g))))) == E(g,K.SEmpty{K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))}) : K.Stack}
205  %Equal.sym(K.Stack,push_all(E(g,lift(t)),cvs(SC.append(T.Out,SC.take(T.Out,xs,SC.pow2(g)),SC.drop(T.Out,xs,SC.pow2(g))))),push_all(push_all(E(g,lift(t)),cvs(SC.take(T.Out,xs,SC.pow2(g)))),cvs(SC.drop(T.Out,xs,SC.pow2(g)))),push_split(E(g,lift(t)),SC.take(T.Out,xs,SC.pow2(g)),SC.drop(T.Out,xs,SC.pow2(g)))) : {_ == E(g,K.SEmpty{K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))}) : K.Stack}
206  %Equal.sym(K.Stack,push_all(E(g,lift(t)),cvs(SC.take(T.Out,xs,SC.pow2(g)))),E(g,K.push(lift(t),S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))))),ih1) : {push_all(_,cvs(SC.drop(T.Out,xs,SC.pow2(g)))) == E(g,K.SEmpty{K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))}) : K.Stack}
207  %Equal.sym(K.Stack,K.push(lift(t),S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g))))),K.SFull{S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),t},push_lift(t,S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))))) : {push_all(E(g,_),cvs(SC.drop(T.Out,xs,SC.pow2(g)))) == E(g,K.SEmpty{K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))}) : K.Stack}
208  ih2