1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/array.bend as AR 5 import ../../../spec/lib/common.bend as SC 6 import ../../../spec/containers/dynamic_array.bend as S 7 import ../../../src/containers/dynamic_array.bend as DA 8 import ./layout.bend as LY 9 import ./state.bend as ST 10 import ../../lib/list.bend as LL 11 12 # The reserve loop DA.grow_until, described on shadows, and the least 13 # capacity exponent it reaches (S.fit, fuel-independent). 14 15 # The grown shadow (depth + 1, old tree as left half) is good when d < l. 16 def grow_good(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hdl: {Nat.is_lt(d, l) == True{} : Bool}) -> {ST.good(T, ST.Sh{l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}}) == True{} : Bool}: 17 ST.good_intro(T, l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}, ST.g_limit(T, l, d, n, t, g), N.lt_succ_le_succ(d, l, hdl), 18 L.and_intro(AR.perfect(Maybe<&2, T>, d, t), AR.perfect(Maybe<&2, T>, d, AR.trep(Maybe<&2, T>, d, None{})), ST.g_perfect(T, l, d, n, t, g), AR.trep_perfect(Maybe<&2, T>, d, None{})), 19 L.subst(List<&2, Maybe<&2, T>>, ys => {LY.lay(T, ys, n) == True{} : Bool}, SC.append(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{})), AR.slots(Maybe<&2, T>, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}), SC.append(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{})), ST.slots_grown(T, d, t)), LY.lay_grow(T, AR.slots(Maybe<&2, T>, t), n, SC.pow2(d), ST.g_lay(T, l, d, n, t, g)))) 20 21 def grow_model(-T: Data, +d: Nat, +t: AR.Tree>) -> {LY.somes(T, AR.slots(Maybe<&2, T>, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})})) == LY.somes(T, AR.slots(Maybe<&2, T>, t)) : List<&2, T>}: 22 %Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}), SC.append(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{})), ST.slots_grown(T, d, t)) : {LY.somes(T, _) == LY.somes(T, AR.slots(Maybe<&2, T>, t)) : List<&2, T>} 23 LY.somes_grow(T, AR.slots(Maybe<&2, T>, t), SC.pow2(d)) 24 25 def sgstep(-T: Data, +k: Nat, sh: ST.Shadow) -> ST.Shadow: 26 match sh: 27 case ST.Sh{+l, +d, +n, +t}: 28 Bool.pick(ST.Shadow, Nat.is_le(k, SC.pow2(d)), ST.Sh{l, d, n, t}, ST.Sh{l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}}) 29 30 def sgrow(-T: Data, f: Nat, +k: Nat, sh: ST.Shadow) -> ST.Shadow: 31 match f: 32 case 0n: 33 sh 34 case 1n+g: 35 sgrow(T, g, k, sgstep(T, k, sh)) 36 37 # The source's own pow2 (still used for the 2^limit feasibility test, which 38 # is not cached) is the spec's. 39 def fits_nat(+k: Nat, +d: Nat, +b: Bool, +e: {Nat.is_le(k, DA.pow2(d)) == b : Bool}) -> {Nat.is_le(k, SC.pow2(d)) == b : Bool}: 40 L.subst(Nat, x => {Nat.is_le(k, x) == b : Bool}, DA.pow2(d), SC.pow2(d), ST.pow2_src(d), e) 41 42 def gstep_case(-T: Data, +k: Nat, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree>, +b: Bool, +eb: {Nat.is_le(k, SC.pow2(d)) == b : Bool}) -> {DA.grow_step(T, k, ST.real(T, ST.Sh{l, d, n, t})) == ST.real(T, sgstep(T, k, ST.Sh{l, d, n, t})) : DA.DynArray<&2, T>}: 43 match b: 44 case True{}: 45 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), True{}, eb) : {DA.grow_if(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), _) == ST.real(T, Bool.pick(ST.Shadow, Nat.is_le(k, SC.pow2(d)), ST.Sh{l, d, n, t}, ST.Sh{l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}})) : DA.DynArray<&2, T>} 46 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), True{}, eb) : {DA.DA{l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t)} == ST.real(T, Bool.pick(ST.Shadow, _, ST.Sh{l, d, n, t}, ST.Sh{l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}})) : DA.DynArray<&2, T>} 47 {==} 48 case False{}: 49 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), False{}, eb) : {DA.grow_if(T, l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t), _) == ST.real(T, Bool.pick(ST.Shadow, Nat.is_le(k, SC.pow2(d)), ST.Sh{l, d, n, t}, ST.Sh{l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}})) : DA.DynArray<&2, T>} 50 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), False{}, eb) : {DA.DA{l, 1n+d, Nat.double(SC.pow2(d)), n, DA.grown(T, d, AR.thaw(Maybe<&2, T>, t))} == ST.real(T, Bool.pick(ST.Shadow, _, ST.Sh{l, d, n, t}, ST.Sh{l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}})) : DA.DynArray<&2, T>} 51 %Equal.sym(Array>, DA.grown(T, d, AR.thaw(Maybe<&2, T>, t)), AR.thaw(Maybe<&2, T>, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}), ST.grown_eq(T, d, t)) : {DA.DA{l, 1n+d, Nat.double(SC.pow2(d)), n, _} == ST.real(T, ST.Sh{l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}}) : DA.DynArray<&2, T>} 52 {==} 53 54 def grow_until_real(-T: Data, +f: Nat, +k: Nat, +sh: ST.Shadow) -> {DA.grow_until(T, f, k, ST.real(T, sh)) == ST.real(T, sgrow(T, f, k, sh)) : DA.DynArray<&2, T>}: 55 match f sh: 56 case 0n _: 57 {==} 58 case 1n+g ST.Sh{+l, +d, +n, +t}: 59 %Equal.sym(DA.DynArray<&2, T>, DA.grow_step(T, k, ST.real(T, ST.Sh{l, d, n, t})), ST.real(T, sgstep(T, k, ST.Sh{l, d, n, t})), gstep_case(T, k, l, d, n, t, Nat.is_le(k, SC.pow2(d)), {==})) : {DA.grow_until(T, g, k, _) == ST.real(T, sgrow(T, g, k, sgstep(T, k, ST.Sh{l, d, n, t}))) : DA.DynArray<&2, T>} 60 grow_until_real(T, g, k, sgstep(T, k, ST.Sh{l, d, n, t})) 61 62 # ---- the least exponent ---- 63 64 def fit_fits(+f: Nat, +d: Nat, +k: Nat, +h: {Nat.is_le(k, SC.pow2(d)) == True{} : Bool}) -> {S.fit(f, d, k) == d : Nat}: 65 match f: 66 case 0n: 67 {==} 68 case 1n+g: 69 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), True{}, h) : {Bool.pick(Nat, _, d, S.fit(g, 1n+d, k)) == d : Nat} 70 {==} 71 72 def sgrow_fits(-T: Data, +f: Nat, +k: Nat, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree>, +h: {Nat.is_le(k, SC.pow2(d)) == True{} : Bool}) -> {sgrow(T, f, k, ST.Sh{l, d, n, t}) == ST.Sh{l, d, n, t} : ST.Shadow}: 73 match f: 74 case 0n: 75 {==} 76 case 1n+g: 77 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), True{}, h) : {sgrow(T, g, k, Bool.pick(ST.Shadow, _, ST.Sh{l, d, n, t}, ST.Sh{l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}})) == ST.Sh{l, d, n, t} : ST.Shadow} 78 sgrow_fits(T, g, k, l, d, n, t, h) 79 80 def room_left(+d: Nat, +g: Nat, +l: Nat, +h: {Nat.is_le(Nat.add(d, 1n+g), l) == True{} : Bool}) -> {Nat.is_lt(d, l) == True{} : Bool}: 81 N.succ_le_lt(d, l, N.le_trans(1n+d, Nat.add(d, 1n+g), l, L.subst(Nat, x => {Nat.is_le(1n+d, x) == True{} : Bool}, 1n+Nat.add(d, g), Nat.add(d, 1n+g), Equal.sym(Nat, Nat.add(d, 1n+g), 1n+Nat.add(d, g), N.add_succ(d, g)), N.le_add_right(d, g)), h)) 82 83 def fuel_shift(+d: Nat, +g: Nat, +l: Nat, +h: {Nat.is_le(Nat.add(d, 1n+g), l) == True{} : Bool}) -> {Nat.is_le(Nat.add(1n+d, g), l) == True{} : Bool}: 84 L.subst(Nat, x => {Nat.is_le(x, l) == True{} : Bool}, Nat.add(d, 1n+g), 1n+Nat.add(d, g), N.add_succ(d, g), h) 85 86 def sgrow_props(-T: Data, +f: Nat, +k: Nat, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree>, +g: {ST.good(T, ST.Sh{l, d, n, t}) == True{} : Bool}, +hf: {Nat.is_le(Nat.add(d, f), l) == True{} : Bool}, +b: Bool, +eb: {Nat.is_le(k, SC.pow2(d)) == b : Bool}) -> {ST.model(T, sgrow(T, f, k, ST.Sh{l, d, n, t})) == S.M{l, S.fit(f, d, k), LY.somes(T, AR.slots(Maybe<&2, T>, t))} : S.Model} & {ST.good(T, sgrow(T, f, k, ST.Sh{l, d, n, t})) == True{} : Bool}: 87 match f b: 88 case 0n _: 89 ({==}, g) 90 case 1n+h True{}: 91 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), True{}, eb) : {ST.model(T, sgrow(T, h, k, Bool.pick(ST.Shadow, _, ST.Sh{l, d, n, t}, ST.Sh{l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}}))) == S.M{l, Bool.pick(Nat, _, d, S.fit(h, 1n+d, k)), LY.somes(T, AR.slots(Maybe<&2, T>, t))} : S.Model} & {ST.good(T, sgrow(T, h, k, Bool.pick(ST.Shadow, _, ST.Sh{l, d, n, t}, ST.Sh{l, 1n+d, n, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}}))) == True{} : Bool} 92 %Equal.sym(ST.Shadow, sgrow(T, h, k, ST.Sh{l, d, n, t}), ST.Sh{l, d, n, t}, sgrow_fits(T, h, k, l, d, n, t, eb)) : {ST.model(T, _) == S.M{l, d, LY.somes(T, AR.slots(Maybe<&2, T>, t))} : S.Model} & {ST.good(T, _) == True{} : Bool} 93 ({==}, g) 94 case 1n+h False{}: 95 +t1 = {AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})} : AR.Tree>} 96 +g1 = grow_good(T, l, d, n, t, g, room_left(d, h, l, hf)) 97 r = sgrow_props(T, h, k, l, 1n+d, n, t1, g1, fuel_shift(d, h, l, hf), Nat.is_le(k, SC.pow2(1n+d)), {==}) 98 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), False{}, eb) : {ST.model(T, sgrow(T, h, k, Bool.pick(ST.Shadow, _, ST.Sh{l, d, n, t}, ST.Sh{l, 1n+d, n, t1}))) == S.M{l, Bool.pick(Nat, _, d, S.fit(h, 1n+d, k)), LY.somes(T, AR.slots(Maybe<&2, T>, t))} : S.Model} & {ST.good(T, sgrow(T, h, k, Bool.pick(ST.Shadow, _, ST.Sh{l, d, n, t}, ST.Sh{l, 1n+d, n, t1}))) == True{} : Bool} 99 %grow_model(T, d, t) : {ST.model(T, sgrow(T, h, k, ST.Sh{l, 1n+d, n, t1})) == S.M{l, S.fit(h, 1n+d, k), _} : S.Model} & {ST.good(T, sgrow(T, h, k, ST.Sh{l, 1n+d, n, t1})) == True{} : Bool} 100 r 101 102 def fe_case(+f1: Nat, +f2: Nat, +d: Nat, +k: Nat, +h1: {Nat.is_le(k, SC.pow2(Nat.add(d, f1))) == True{} : Bool}, +h2: {Nat.is_le(k, SC.pow2(Nat.add(d, f2))) == True{} : Bool}, +b: Bool, +eb: {Nat.is_le(k, SC.pow2(d)) == b : Bool}) -> {S.fit(f1, d, k) == S.fit(f2, d, k) : Nat}: 103 match f1 f2 b: 104 case _ _ True{}: 105 Equal.trans(Nat, S.fit(f1, d, k), d, S.fit(f2, d, k), fit_fits(f1, d, k, eb), Equal.sym(Nat, S.fit(f2, d, k), d, fit_fits(f2, d, k, eb))) 106 case 0n _ False{}: 107 Empty.absurd({d == S.fit(f2, d, k) : Nat}, L.true_not_false(Nat.is_le(k, SC.pow2(d)), L.subst(Nat, x => {Nat.is_le(k, SC.pow2(x)) == True{} : Bool}, Nat.add(d, 0n), d, N.add_zero(d), h1), eb)) 108 case 1n+g1 0n False{}: 109 Empty.absurd({S.fit(1n+g1, d, k) == d : Nat}, L.true_not_false(Nat.is_le(k, SC.pow2(d)), L.subst(Nat, x => {Nat.is_le(k, SC.pow2(x)) == True{} : Bool}, Nat.add(d, 0n), d, N.add_zero(d), h2), eb)) 110 case 1n+g1 1n+g2 False{}: 111 %Equal.sym(Bool, Nat.is_le(k, SC.pow2(d)), False{}, eb) : {Bool.pick(Nat, _, d, S.fit(g1, 1n+d, k)) == Bool.pick(Nat, _, d, S.fit(g2, 1n+d, k)) : Nat} 112 fe_case(g1, g2, 1n+d, k, L.subst(Nat, x => {Nat.is_le(k, SC.pow2(x)) == True{} : Bool}, Nat.add(d, 1n+g1), 1n+Nat.add(d, g1), N.add_succ(d, g1), h1), L.subst(Nat, x => {Nat.is_le(k, SC.pow2(x)) == True{} : Bool}, Nat.add(d, 1n+g2), 1n+Nat.add(d, g2), N.add_succ(d, g2), h2), Nat.is_le(k, SC.pow2(1n+d)), {==}) 113 114 def pow2_gt(+k: Nat) -> {Nat.is_lt(k, SC.pow2(k)) == True{} : Bool}: 115 match k: 116 case 0n: 117 {==} 118 case 1n+p: 119 N.le_lt_trans(1n+p, SC.pow2(p), Nat.double(SC.pow2(p)), N.lt_succ_le_succ(p, SC.pow2(p), pow2_gt(p)), N.pow2_lt_succ(p))