Memory.tree_ext: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as Memory Lines 132-158 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&start_line=132&end_line=158 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 # A perfect tree is the tree of its words. def tree_ext(+d: Nat, +t: AR.Tree, +pf: {AR.perfect(U32, d, t) == True{} : Bool}) -> {t == tree(d, AR.slots(U32, t)) : AR.Tree}: match d t: case 0n AR.TLeaf{x}: {==} case 0n AR.TNode{l, r}: Empty.absurd({AR.TNode{l, r} == tree(0n, AR.slots(U32, AR.TNode{l, r})) : AR.Tree}, L.false_true(pf)) case 1n+p AR.TLeaf{x}: Empty.absurd({AR.TLeaf{x} == tree(1n+p, AR.slots(U32, AR.TLeaf{x})) : AR.Tree}, L.false_true(pf)) case 1n+ +p AR.TNode{+l, +r}: +pl = AR.pf_left(U32, p, l, r, pf) +pr = AR.pf_right(U32, p, l, r, pf) +sl = AR.slots(U32, l) +sr = AR.slots(U32, r) +hl = AR.slots_length(U32, p, l, pl) +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, 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))), take_all(sl, SC.pow2(p), hl)) +ed = drop_all(sl, sr, SC.pow2(p), hl) Equal.trans(AR.Tree, 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)))}, Equal.trans(AR.Tree, AR.TNode{l, r}, AR.TNode{tree(p, sl), r}, AR.TNode{tree(p, sl), tree(p, sr)}, Equal.cong(AR.Tree, AR.Tree, z => AR.TNode{z, r}, l, tree(p, sl), tree_ext(p, l, pl)), Equal.cong(AR.Tree, AR.Tree, z => AR.TNode{tree(p, sl), z}, r, tree(p, sr), tree_ext(p, r, pr))), Equal.sym(AR.Tree, 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)}, Equal.trans(AR.Tree, 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)}, Equal.cong(List<&2, U32>, AR.Tree, 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), Equal.cong(List<&2, U32>, AR.Tree, z => AR.TNode{tree(p, sl), tree(p, z)}, SC.drop(U32, SC.append(U32, sl, sr), SC.pow2(p)), sr, ed)))) Uses (25): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans 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=U32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=drop_all https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=take_all https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=tree https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend&name=Tree https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend&name=perfect https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend&name=pf_left https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend&name=pf_right https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend&name=slots https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend&name=slots_length https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend&name=sc_take_append_left https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=false_true https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=eq_le 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