1 import Base 2 import ../../../../src/crypto/blake/blake3/types.bend as T 3 import ../../../../src/crypto/blake/blake3/compress.bend as C 4 import ../../../../src/crypto/blake/blake3/blake3.bend as K 5 import ../../../lib/logic.bend as L 6 import ../../../lib/nat.bend as N 7 import ../../../../spec/lib/common.bend as SC 8 import ../../../../spec/crypto/blake/blake3.bend as S 9 import ./compress.bend as P 10 import ./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 24 def 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 28 def 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 32 def iv_correct() -> {K.iv() == S.cv_of(S.iv()) : T.CV}: 33 {==} 34 35 def 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 39 def 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. 55 def 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). 61 def 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 67 def 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 73 def 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. 79 def push_all(s: K.Stack, cs: List<&2,T.CV>) -> K.Stack: 80 pushes(cs,s) 81 82 def 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 87 def 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 93 def 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 99 def 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 105 def 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 111 def 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 117 def 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 122 def 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 125 def 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. 131 def 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 137 def 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 142 def 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 147 def 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 152 def 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. 158 def 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 162 def 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 165 def 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 169 def 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. 177 def 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 181 def 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 186 def 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 191 def 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 210 def 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. 222 def 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 232 def 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. 240 def 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. 257 def 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 287 def 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. 299 def 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. 306 def 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)))