def complete_zero

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

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

210def complete_zero(+xs: List<&2,T.Out>, +t: K.Stack, +hl: {SC.length(T.Out,xs) == 1n : Nat}) -> {push_all(E(0n,t),cvs(xs)) == E(0n,K.push(t,S.cv(S.tree(0n,xs)))) : K.Stack}:
211  match xs:
212    case Nil{}: Empty.absurd({push_all(E(0n,t),cvs(Nil{})) == E(0n,K.push(t,S.cv(S.tree(0n,Nil{})))) : K.Stack},N.zero_succ(0n,hl))
213    case Con{+x,Nil{}}:
214      %Equal.sym(K.Stack,E(0n,t),t,E_zero(t)) : {push_all(_,cvs(Con{x,Nil{}})) == E(0n,K.push(t,S.cv(S.tree(0n,Con{x,Nil{}})))) : K.Stack}
215      %Equal.sym(K.Stack,E(0n,K.push(t,S.cv(x))),K.push(t,S.cv(x)),E_zero(K.push(t,S.cv(x)))) : {push_all(t,cvs(Con{x,Nil{}})) == _ : K.Stack}
216      %out_cv_correct(x) : {push_all(t,cvs(Con{x,Nil{}})) == K.push(t,_) : K.Stack}
217      {==}
218    case Con{+x,Con{+y,+r}}: Empty.absurd({push_all(E(0n,t),cvs(Con{x,Con{y,r}})) == E(0n,K.push(t,S.cv(S.tree(0n,Con{x,Con{y,r}})))) : K.Stack},N.succ_zero(SC.length(T.Out,r),N.succ_inj(1n+SC.length(T.Out,r),0n,hl)))