proofs/crypto/blake/blake3/tree.bend

bend-collections-laws-crypto@1.0.0.0 · 307 lines · 40 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/compress.bend as C
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend as K
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
7import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
8import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as S
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/compress.bend as P
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend as LS
11
12# The implementation's subtree stack computes the specification's tree.
13#
14# For a list F of chunk outputs pushed onto the stack (as chaining values) and
15# a pending last output o, folding the stack into o gives the root of the
16# specification's tree over F ++ [o] (tree_stack below), for every F and o.
17# The invariant: a stack whose h lowest slots are empty (E(h, t)) absorbs
18# 2^h chaining values as one complete subtree carried into slot h (complete),
19# and fewer than 2^h values plus the pending output fold into the
20# specification's tree of height h (partial).
21
22# ---- node-level agreement ----
23
24def out_cv_correct(+o: T.Out) -> {K.out_cv(o) == S.cv(o) : T.CV}:
25  match o:
26    case T.Out{+c,+b,+t,+len,+flags}: P.compress_correct(c,b,t,len,flags)
27
28def parent_block_correct(+l: T.CV, +r: T.CV) -> {K.parent_block(l,r) == S.block_of(SC.append(U32,S.cv_words(l),S.cv_words(r))) : T.Block}:
29  match l r:
30    case T.CV{l0,l1,l2,l3,l4,l5,l6,l7} T.CV{r0,r1,r2,r3,r4,r5,r6,r7}: {==}
31
32def iv_correct() -> {K.iv() == S.cv_of(S.iv()) : T.CV}:
33  {==}
34
35def parent_out_correct(+l: T.CV, +r: T.CV) -> {K.parent_out(l,r) == S.parent(l,r) : T.Out}:
36  %parent_block_correct(l,r) : {K.parent_out(l,r) == T.Out{S.cv_of(S.iv()),_,0,64,S.parent_flag()} : T.Out}
37  {==}
38
39def parent_cv_correct(+l: T.CV, +r: T.CV) -> {K.parent_cv(l,r) == S.cv(S.parent(l,r)) : T.CV}:
40  Equal.trans(T.CV,
41    C.compress(K.iv(),K.parent_block(l,r),0,64,4),
42    S.compress(K.iv(),K.parent_block(l,r),0,64,4),
43    S.compress(S.cv_of(S.iv()),S.block_of(SC.append(U32,S.cv_words(l),S.cv_words(r))),0,64,S.parent_flag()),
44    P.compress_correct(K.iv(),K.parent_block(l,r),0,64,4),
45    Equal.trans(T.CV,
46      S.compress(K.iv(),K.parent_block(l,r),0,64,4),
47      S.compress(S.cv_of(S.iv()),K.parent_block(l,r),0,64,4),
48      S.compress(S.cv_of(S.iv()),S.block_of(SC.append(U32,S.cv_words(l),S.cv_words(r))),0,64,S.parent_flag()),
49      Equal.cong(T.CV,T.CV,c => S.compress(c,K.parent_block(l,r),0,64,4),K.iv(),S.cv_of(S.iv()),iv_correct()),
50      Equal.cong(T.Block,T.CV,b => S.compress(S.cv_of(S.iv()),b,0,64,S.parent_flag()),K.parent_block(l,r),S.block_of(SC.append(U32,S.cv_words(l),S.cv_words(r))),parent_block_correct(l,r))))
51
52# ---- stacks ----
53
54# h empty slots below y.
55def emps(h: Nat, y: K.Stack) -> K.Stack:
56  match h:
57    case 0n: y
58    case 1n+g: emps(g,K.SEmpty{y})
59
60# The stack t with h empty slots below it (the empty stack stays empty).
61def E(+h: Nat, t: K.Stack) -> K.Stack:
62  match t:
63    case K.StkNil{}: K.StkNil{}
64    case K.SEmpty{r}: emps(h,K.SEmpty{r})
65    case K.SFull{c,r}: emps(h,K.SFull{c,r})
66
67def lift(t: K.Stack) -> K.Stack:
68  match t:
69    case K.StkNil{}: K.StkNil{}
70    case K.SEmpty{r}: K.SEmpty{K.SEmpty{r}}
71    case K.SFull{c,r}: K.SEmpty{K.SFull{c,r}}
72
73def pushes(cs: List<&2,T.CV>, s: K.Stack) -> K.Stack:
74  match cs:
75    case Nil{}: s
76    case Con{c,r}: pushes(r,K.push(s,c))
77
78# Pushes the chaining values cs in order.
79def push_all(s: K.Stack, cs: List<&2,T.CV>) -> K.Stack:
80  pushes(cs,s)
81
82def cvs(xs: List<&2,T.Out>) -> List<&2,T.CV>:
83  match xs:
84    case Nil{}: Nil{}
85    case Con{x,r}: Con{K.out_cv(x),cvs(r)}
86
87def E_succ(+g: Nat, +t: K.Stack) -> {E(1n+g,t) == E(g,lift(t)) : K.Stack}:
88  match t:
89    case K.StkNil{}: {==}
90    case K.SEmpty{+r}: {==}
91    case K.SFull{+c,+r}: {==}
92
93def E_zero(+t: K.Stack) -> {E(0n,t) == t : K.Stack}:
94  match t:
95    case K.StkNil{}: {==}
96    case K.SEmpty{+r}: {==}
97    case K.SFull{+c,+r}: {==}
98
99def push_lift(+t: K.Stack, +c: T.CV) -> {K.push(lift(t),c) == K.SFull{c,t} : K.Stack}:
100  match t:
101    case K.StkNil{}: {==}
102    case K.SEmpty{+r}: {==}
103    case K.SFull{+d,+r}: {==}
104
105def lift_push(+t: K.Stack, +c: T.CV) -> {lift(K.push(t,c)) == K.SEmpty{K.push(t,c)} : K.Stack}:
106  match t:
107    case K.StkNil{}: {==}
108    case K.SEmpty{+r}: {==}
109    case K.SFull{+d,+r}: {==}
110
111def finish_lift(+t: K.Stack, +o: T.Out) -> {K.finish(lift(t),o) == K.finish(t,o) : T.Out}:
112  match t:
113    case K.StkNil{}: {==}
114    case K.SEmpty{+r}: {==}
115    case K.SFull{+d,+r}: {==}
116
117def pushes_append(+xs: List<&2,T.CV>, +s: K.Stack, +ys: List<&2,T.CV>) -> {push_all(s,SC.append(T.CV,xs,ys)) == push_all(push_all(s,xs),ys) : K.Stack}:
118  match xs:
119    case Nil{}: {==}
120    case Con{+c,+r}: pushes_append(r,K.push(s,c),ys)
121
122def push_all_append(+s: K.Stack, +xs: List<&2,T.CV>, +ys: List<&2,T.CV>) -> {push_all(s,SC.append(T.CV,xs,ys)) == push_all(push_all(s,xs),ys) : K.Stack}:
123  pushes_append(xs,s,ys)
124
125def cvs_append(+xs: List<&2,T.Out>, +ys: List<&2,T.Out>) -> {cvs(SC.append(T.Out,xs,ys)) == SC.append(T.CV,cvs(xs),cvs(ys)) : List<&2,T.CV>}:
126  match xs:
127    case Nil{}: {==}
128    case Con{+x,+r}: LS.cons_cong(T.CV,K.out_cv(x),cvs(SC.append(T.Out,r,ys)),SC.append(T.CV,cvs(r),cvs(ys)),cvs_append(r,ys))
129
130# Pushing the chaining values of xs ++ ys.
131def push_split(+s: K.Stack, +xs: List<&2,T.Out>, +ys: List<&2,T.Out>) -> {push_all(s,cvs(SC.append(T.Out,xs,ys))) == push_all(push_all(s,cvs(xs)),cvs(ys)) : K.Stack}:
132  %Equal.sym(List<&2,T.CV>,cvs(SC.append(T.Out,xs,ys)),SC.append(T.CV,cvs(xs),cvs(ys)),cvs_append(xs,ys)) : {push_all(s,_) == push_all(push_all(s,cvs(xs)),cvs(ys)) : K.Stack}
133  push_all_append(s,cvs(xs),cvs(ys))
134
135# ---- the specification's tree ----
136
137def tree_con(+g: Nat, +xs: List<&2,T.Out>, +ne: {S.is_nil(xs) == False{} : Bool}) -> {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)))) : T.Out}:
138  match xs:
139    case Nil{}: Empty.absurd({S.tree(1n+g,Nil{}) == S.join(S.tree(g,SC.take(T.Out,Nil{},SC.pow2(g))),S.tree(g,SC.drop(T.Out,Nil{},SC.pow2(g))),S.is_nil(SC.drop(T.Out,Nil{},SC.pow2(g)))) : T.Out},L.true_false(ne))
140    case Con{+x,+r}: {==}
141
142def nil_is_empty(+xs: List<&2,T.Out>) -> {S.is_nil(xs) == LS.is_empty(T.Out,xs) : Bool}:
143  match xs:
144    case Nil{}: {==}
145    case Con{+x,+r}: {==}
146
147def snoc_ne(+xs: List<&2,T.Out>, +o: T.Out) -> {S.is_nil(SC.append(T.Out,xs,Con{o,Nil{}})) == False{} : Bool}:
148  match xs:
149    case Nil{}: {==}
150    case Con{+x,+r}: {==}
151
152def len_ne(+xs: List<&2,T.Out>, +n: Nat, +h: {SC.length(T.Out,xs) == 1n+n : Nat}) -> {S.is_nil(xs) == False{} : Bool}:
153  match xs:
154    case Nil{}: Empty.absurd({S.is_nil(Nil{}) == False{} : Bool},N.zero_succ(n,h))
155    case Con{+x,+r}: {==}
156
157# The drop is empty exactly when the list fits.
158def drop_nil(+xs: List<&2,T.Out>, +k: Nat) -> {S.is_nil(SC.drop(T.Out,xs,k)) == Nat.is_le(SC.length(T.Out,xs),k) : Bool}:
159  %Equal.sym(Bool,S.is_nil(SC.drop(T.Out,xs,k)),LS.is_empty(T.Out,SC.drop(T.Out,xs,k)),nil_is_empty(SC.drop(T.Out,xs,k))) : {_ == Nat.is_le(SC.length(T.Out,xs),k) : Bool}
160  LS.empty_drop(T.Out,xs,k)
161
162def join_false(+l: T.Out, +r: T.Out) -> {S.join(l,r,False{}) == S.parent(S.cv(l),S.cv(r)) : T.Out}:
163  {==}
164
165def zero_pow(+p: Nat, +hl: {0n == SC.pow2(p) : Nat}) -> {Nat.is_le(1n,0n) == True{} : Bool}:
166  %Equal.sym(Nat,0n,SC.pow2(p),hl) : {Nat.is_le(1n,_) == True{} : Bool}
167  N.pow2_pos(p)
168
169def pow_ne(+xs: List<&2,T.Out>, +p: Nat, +hl: {SC.length(T.Out,xs) == SC.pow2(p) : Nat}) -> {S.is_nil(xs) == False{} : Bool}:
170  match xs:
171    case Nil{}: Empty.absurd({S.is_nil(Nil{}) == False{} : Bool},L.false_true(zero_pow(p,hl)))
172    case Con{+x,+r}: {==}
173
174# ---- complete subtrees ----
175
176# The two halves of a list of 2^(g+1) outputs.
177def half_len_take(+xs: List<&2,T.Out>, +g: Nat, +hl: {SC.length(T.Out,xs) == SC.pow2(1n+g) : Nat}) -> {SC.length(T.Out,SC.take(T.Out,xs,SC.pow2(g))) == SC.pow2(g) : Nat}:
178  LS.length_take(T.Out,xs,SC.pow2(g),Equal.trans(Bool,Nat.is_le(SC.pow2(g),SC.length(T.Out,xs)),Nat.is_le(SC.pow2(g),Nat.double(SC.pow2(g))),True{},
179    Equal.cong(Nat,Bool,n => Nat.is_le(SC.pow2(g),n),SC.length(T.Out,xs),Nat.double(SC.pow2(g)),hl),N.double_self_le(SC.pow2(g))))
180
181def half_len_drop(+xs: List<&2,T.Out>, +g: Nat, +hl: {SC.length(T.Out,xs) == SC.pow2(1n+g) : Nat}) -> {SC.length(T.Out,SC.drop(T.Out,xs,SC.pow2(g))) == SC.pow2(g) : Nat}:
182  %Equal.sym(Nat,SC.length(T.Out,SC.drop(T.Out,xs,SC.pow2(g))),Nat.sub(SC.length(T.Out,xs),SC.pow2(g)),LS.length_drop(T.Out,xs,SC.pow2(g))) : {_ == SC.pow2(g) : Nat}
183  %Equal.sym(Nat,SC.length(T.Out,xs),SC.pow2(1n+g),hl) : {Nat.sub(_,SC.pow2(g)) == SC.pow2(g) : Nat}
184  LS.sub_double(SC.pow2(g))
185
186def half_not_nil(+xs: List<&2,T.Out>, +g: Nat, +hl: {SC.length(T.Out,xs) == SC.pow2(1n+g) : Nat}) -> {S.is_nil(SC.drop(T.Out,xs,SC.pow2(g))) == False{} : Bool}:
187  %Equal.sym(Bool,S.is_nil(SC.drop(T.Out,xs,SC.pow2(g))),Nat.is_le(SC.length(T.Out,xs),SC.pow2(g)),drop_nil(xs,SC.pow2(g))) : {_ == False{} : Bool}
188  %Equal.sym(Nat,SC.length(T.Out,xs),SC.pow2(1n+g),hl) : {Nat.is_le(_,SC.pow2(g)) == False{} : Bool}
189  N.lt_not_le(SC.pow2(g),Nat.double(SC.pow2(g)),N.pow2_lt_succ(g))
190
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
209
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)))
219
220# A stack with g empty low slots absorbs the chaining values of 2^g outputs
221# as one complete subtree pushed at slot g.
222def complete(+g: Nat, +xs: List<&2,T.Out>, +t: K.Stack, +hl: {SC.length(T.Out,xs) == SC.pow2(g) : Nat}) -> {push_all(E(g,t),cvs(xs)) == E(g,K.push(t,S.cv(S.tree(g,xs)))) : K.Stack}:
223  match g:
224    case 0n: complete_zero(xs,t,hl)
225    case 1n+p:
226      complete_step(p,xs,t,pow_ne(xs,1n+p,hl),half_not_nil(xs,p,hl),
227        complete(p,SC.take(T.Out,xs,SC.pow2(p)),lift(t),half_len_take(xs,p,hl)),
228        complete(p,SC.drop(T.Out,xs,SC.pow2(p)),K.SFull{S.cv(S.tree(p,SC.take(T.Out,xs,SC.pow2(p)))),t},half_len_drop(xs,p,hl)))
229
230# ---- the pending output ----
231
232def partial_zero(+fs: List<&2,T.Out>, +o: T.Out, +t: K.Stack, +hl: {Nat.is_lt(SC.length(T.Out,fs),1n) == True{} : Bool}) -> {K.finish(push_all(E(0n,t),cvs(fs)),o) == K.finish(t,S.tree(0n,SC.append(T.Out,fs,Con{o,Nil{}}))) : T.Out}:
233  match fs:
234    case Nil{}:
235      %Equal.sym(K.Stack,E(0n,t),t,E_zero(t)) : {K.finish(_,o) == K.finish(t,S.tree(0n,Con{o,Nil{}})) : T.Out}
236      {==}
237    case Con{+f,+r}: Empty.absurd({K.finish(push_all(E(0n,t),cvs(Con{f,r})),o) == K.finish(t,S.tree(0n,SC.append(T.Out,Con{f,r},Con{o,Nil{}}))) : T.Out},N.lt_zero_absurd(SC.length(T.Out,r),hl))
238
239# Fewer than 2^p outputs before o: the whole tree fits in height p.
240def partial_fit(+p: Nat, +fs: List<&2,T.Out>, +o: T.Out, +t: K.Stack,
241    +hb: {Nat.is_lt(SC.length(T.Out,fs),SC.pow2(p)) == True{} : Bool},
242    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}
243  ) -> {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}:
244  +xs = SC.append(T.Out,fs,Con{o,Nil{}})
245  +k = SC.pow2(p)
246  +hx = {%Equal.sym(Nat,SC.length(T.Out,xs),1n+SC.length(T.Out,fs),LS.length_snoc(T.Out,fs,o)) : {Nat.is_le(_,k) == True{} : Bool}
247    N.lt_succ_le_succ(SC.length(T.Out,fs),k,hb) : {Nat.is_le(SC.length(T.Out,xs),k) == True{} : Bool}}
248  %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}
249  %Equal.sym(List<&2,T.Out>,SC.take(T.Out,xs,k),xs,LS.take_all(T.Out,xs,k,hx)) : {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}
250  %Equal.sym(List<&2,T.Out>,SC.drop(T.Out,xs,k),Nil{},LS.drop_all(T.Out,xs,k,hx)) : {K.finish(push_all(E(1n+p,t),cvs(fs)),o) == K.finish(t,S.join(S.tree(p,xs),S.tree(p,_),S.is_nil(_))) : T.Out}
251  %Equal.sym(K.Stack,E(1n+p,t),E(p,lift(t)),E_succ(p,t)) : {K.finish(push_all(_,cvs(fs)),o) == K.finish(t,S.join(S.tree(p,xs),S.tree(p,Nil{}),S.is_nil(Nil{}))) : T.Out}
252  Equal.trans(T.Out,K.finish(push_all(E(p,lift(t)),cvs(fs)),o),K.finish(lift(t),S.tree(p,xs)),K.finish(t,S.tree(p,xs)),
253    rec(fs,lift(t),hb),finish_lift(t,S.tree(p,xs)))
254
255# At least 2^p outputs before o: a complete left subtree of 2^p chunks, then
256# the rest with o.
257def partial_big(+p: Nat, +fs: List<&2,T.Out>, +o: T.Out, +t: K.Stack,
258    +hl: {Nat.is_lt(SC.length(T.Out,fs),SC.pow2(1n+p)) == True{} : Bool},
259    +hb: {Nat.is_lt(SC.length(T.Out,fs),SC.pow2(p)) == False{} : Bool},
260    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}
261  ) -> {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}:
262  +xs = SC.append(T.Out,fs,Con{o,Nil{}})
263  +k = SC.pow2(p)
264  +f1 = SC.take(T.Out,fs,k)
265  +f2 = SC.drop(T.Out,fs,k)
266  +c1 = S.cv(S.tree(p,f1))
267  +t2 = S.tree(p,SC.append(T.Out,f2,Con{o,Nil{}}))
268  +kl = N.not_lt_le(SC.length(T.Out,fs),k,hb)
269  +h1 = LS.length_take(T.Out,fs,k,kl)
270  +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}
271    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}
272      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}}
273  %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}
274  %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}
275  %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}
276  %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}
277  %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}
278  %out_cv_correct(t2) : {K.finish(push_all(E(1n+p,t),cvs(fs)),o) == K.finish(t,S.parent(c1,_)) : T.Out}
279  %parent_out_correct(c1,K.out_cv(t2)) : {K.finish(push_all(E(1n+p,t),cvs(fs)),o) == K.finish(t,_) : T.Out}
280  %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}
281  %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}
282  %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}
283  %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}
284  %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}
285  rec(f2,K.SFull{c1,t},h2)
286
287def partial_split(+p: Nat, +fs: List<&2,T.Out>, +o: T.Out, +t: K.Stack,
288    +hl: {Nat.is_lt(SC.length(T.Out,fs),SC.pow2(1n+p)) == True{} : Bool},
289    +b: Bool, +hb: {Nat.is_lt(SC.length(T.Out,fs),SC.pow2(p)) == b : Bool},
290    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}
291  ) -> {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}:
292  match b:
293    case True{}: partial_fit(p,fs,o,t,hb,rec)
294    case False{}: partial_big(p,fs,o,t,hl,hb,rec)
295
296# Fewer than 2^g chaining values pushed on a stack with g empty low slots,
297# then folded into the pending output o: the specification's tree of height
298# g over the outputs and o, folded into the rest of the stack.
299def partial(+g: Nat, +fs: List<&2,T.Out>, +o: T.Out, +t: K.Stack, +hl: {Nat.is_lt(SC.length(T.Out,fs),SC.pow2(g)) == True{} : Bool}) -> {K.finish(push_all(E(g,t),cvs(fs)),o) == K.finish(t,S.tree(g,SC.append(T.Out,fs,Con{o,Nil{}}))) : T.Out}:
300  match g:
301    case 0n: partial_zero(fs,o,t,hl)
302    case 1n+p:
303      partial_split(p,fs,o,t,hl,Nat.is_lt(SC.length(T.Out,fs),SC.pow2(p)),{==},f2 => t2 => h2 => partial(p,f2,o,t2,h2))
304
305# The whole message: the stack starts empty and the height is the chunk count.
306def tree_stack(+fs: List<&2,T.Out>, +o: T.Out) -> {K.finish(push_all(K.StkNil{},cvs(fs)),o) == S.tree(1n+SC.length(T.Out,fs),SC.append(T.Out,fs,Con{o,Nil{}})) : T.Out}:
307  partial(1n+SC.length(T.Out,fs),fs,o,K.StkNil{},LS.lt_pow2_succ(SC.length(T.Out,fs)))