def tree_ext

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/memory.bend:132

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend as AR
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend as LL
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

132# A perfect tree is the tree of its words.
133def tree_ext(+d: Nat, +t: AR.Tree<U32>, +pf: {AR.perfect(U32, d, t) == True{} : Bool}) -> {t == tree(d, AR.slots(U32, t)) : AR.Tree<U32>}:
134  match d t:
135    case 0n AR.TLeaf{x}:
136      {==}
137    case 0n AR.TNode{l, r}:
138      Empty.absurd({AR.TNode{l, r} == tree(0n, AR.slots(U32, AR.TNode{l, r})) : AR.Tree<U32>}, L.false_true(pf))
139    case 1n+p AR.TLeaf{x}:
140      Empty.absurd({AR.TLeaf{x} == tree(1n+p, AR.slots(U32, AR.TLeaf{x})) : AR.Tree<U32>}, L.false_true(pf))
141    case 1n+ +p AR.TNode{+l, +r}:
142      +pl = AR.pf_left(U32, p, l, r, pf)
143      +pr = AR.pf_right(U32, p, l, r, pf)
144      +sl = AR.slots(U32, l)
145      +sr = AR.slots(U32, r)
146      +hl = AR.slots_length(U32, p, l, pl)
147      +et = Equal.trans(List<&2, U32>, SC.take(U32, SC.append(U32, sl, sr), SC.pow2(p)), SC.take(U32, sl, SC.pow2(p)), sl,
148        LL.sc_take_append_left(U32, sl, sr, SC.pow2(p), N.eq_le(SC.pow2(p), SC.length(U32, sl), Equal.sym(Nat, SC.length(U32, sl), SC.pow2(p), hl))),
149        take_all(sl, SC.pow2(p), hl))
150      +ed = drop_all(sl, sr, SC.pow2(p), hl)
151      Equal.trans(AR.Tree<U32>, AR.TNode{l, r}, AR.TNode{tree(p, sl), tree(p, sr)}, AR.TNode{tree(p, SC.take(U32, SC.append(U32, sl, sr), SC.pow2(p))), tree(p, SC.drop(U32, SC.append(U32, sl, sr), SC.pow2(p)))},
152        Equal.trans(AR.Tree<U32>, AR.TNode{l, r}, AR.TNode{tree(p, sl), r}, AR.TNode{tree(p, sl), tree(p, sr)},
153          Equal.cong(AR.Tree<U32>, AR.Tree<U32>, z => AR.TNode{z, r}, l, tree(p, sl), tree_ext(p, l, pl)),
154          Equal.cong(AR.Tree<U32>, AR.Tree<U32>, z => AR.TNode{tree(p, sl), z}, r, tree(p, sr), tree_ext(p, r, pr))),
155        Equal.sym(AR.Tree<U32>, AR.TNode{tree(p, SC.take(U32, SC.append(U32, sl, sr), SC.pow2(p))), tree(p, SC.drop(U32, SC.append(U32, sl, sr), SC.pow2(p)))}, AR.TNode{tree(p, sl), tree(p, sr)},
156          Equal.trans(AR.Tree<U32>, AR.TNode{tree(p, SC.take(U32, SC.append(U32, sl, sr), SC.pow2(p))), tree(p, SC.drop(U32, SC.append(U32, sl, sr), SC.pow2(p)))}, AR.TNode{tree(p, sl), tree(p, SC.drop(U32, SC.append(U32, sl, sr), SC.pow2(p)))}, AR.TNode{tree(p, sl), tree(p, sr)},
157            Equal.cong(List<&2, U32>, AR.Tree<U32>, z => AR.TNode{tree(p, z), tree(p, SC.drop(U32, SC.append(U32, sl, sr), SC.pow2(p)))}, SC.take(U32, SC.append(U32, sl, sr), SC.pow2(p)), sl, et),
158            Equal.cong(List<&2, U32>, AR.Tree<U32>, z => AR.TNode{tree(p, sl), tree(p, z)}, SC.drop(U32, SC.append(U32, sl, sr), SC.pow2(p)), sr, ed))))