1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/list.bend as LL 5 import ../../lib/order.bend as O 6 import ../../../spec/lib/common.bend as SC 7 import ../../../spec/containers/binary_heap.bend as S 8 import ../../../src/containers/binary_heap.bend as H 9 import ../../../src/containers/types/binary_heap.bend as E 10 import ./state.bend as ST 11 import ./steps.bend as SP 12 import ./root.bend as RT 13 import ./budget.bend as BG 14 15 def add_le_a(+a: Nat, +x: Nat, +y: Nat, +h: {Nat.is_le(x, y) == True{} : Bool}) -> {Nat.is_le(Nat.add(a, x), Nat.add(a, y)) == True{} : Bool}: 16 N.le_add_left(x, y, a, h) 17 18 # Arbitrary finite operation traces: the real runner refines the spec runner. 19 # 20 # The slot array is linear, so the statement is the shadow form the per-step 21 # laws use: running any finite list of operations on the array of a good 22 # shadow lands on the array of another good shadow, emits exactly the spec 23 # runner's observations, and the model of the final shadow is the spec 24 # runner's final model. 25 # 26 # `pushes(ops)` is the number of elements the list can add (one per push, 27 # |ys| per from_list). No operation grows the heap by more than its push 28 # count, so ONE premise -- size + pushes(ops) < 2^q with q <= 31 -- keeps the 29 # size below 2^q at every step and discharges each step's capacity 30 # condition. It is the representation's capacity condition (Base arrays 31 # have at most 2^31 slots), with no bound on the length of the trace. 32 33 def pushes(~A: Data, ops: List<&2, E.Op>) -> Nat: 34 match ops: 35 case Nil{}: 36 0n 37 case Con{op, rest}: 38 Nat.add(SP.pushcost(~A, op), pushes(~A, rest)) 39 40 def add_le_l(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}: 41 %Equal.sym(Nat, Nat.add(a, c), Nat.add(c, a), N.add_comm(a, c)) : {Nat.is_le(_, Nat.add(b, c)) == True{} : Bool} 42 %Equal.sym(Nat, Nat.add(b, c), Nat.add(c, b), N.add_comm(b, c)) : {Nat.is_le(Nat.add(c, a), _) == True{} : Bool} 43 add_le_a(c, a, b, h) 44 45 def budget_head(~A: Data, +d: Nat, +op: E.Op, +rest: List<&2, E.Op>, +q: Nat, +h: {Nat.is_lt(Nat.add(d, pushes(~A, Con{op, rest})), SC.pow2(q)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(d, SP.pushcost(~A, op)), SC.pow2(q)) == True{} : Bool}: 46 N.le_lt_trans(Nat.add(d, SP.pushcost(~A, op)), Nat.add(d, Nat.add(SP.pushcost(~A, op), pushes(~A, rest))), SC.pow2(q), 47 add_le_a(d, SP.pushcost(~A, op), Nat.add(SP.pushcost(~A, op), pushes(~A, rest)), N.le_add_right(SP.pushcost(~A, op), pushes(~A, rest))), h) 48 49 def budget_tail(~A: Data, +d: Nat, +d2: Nat, +op: E.Op, +rest: List<&2, E.Op>, +q: Nat, +hd2: {Nat.is_le(d2, Nat.add(d, SP.pushcost(~A, op))) == True{} : Bool}, +h: {Nat.is_lt(Nat.add(d, pushes(~A, Con{op, rest})), SC.pow2(q)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(d2, pushes(~A, rest)), SC.pow2(q)) == True{} : Bool}: 50 N.le_lt_trans(Nat.add(d2, pushes(~A, rest)), Nat.add(Nat.add(d, SP.pushcost(~A, op)), pushes(~A, rest)), SC.pow2(q), 51 add_le_l(d2, Nat.add(d, SP.pushcost(~A, op)), pushes(~A, rest), hd2), 52 L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(q)) == True{} : Bool}, Nat.add(d, Nat.add(SP.pushcost(~A, op), pushes(~A, rest))), Nat.add(Nat.add(d, SP.pushcost(~A, op)), pushes(~A, rest)), Equal.sym(Nat, Nat.add(Nat.add(d, SP.pushcost(~A, op)), pushes(~A, rest)), Nat.add(d, Nat.add(SP.pushcost(~A, op), pushes(~A, rest))), N.add_assoc(d, SP.pushcost(~A, op), pushes(~A, rest))), h)) 53 54 # ---- the spec step adds at most pushcost(op) elements ---- 55 56 def slen_pop(-A: Data, xs: List<&2, A>) -> {Nat.is_le(SC.length(A, Pair.fst(List<&2, A>, E.Obs, S.pop(A, xs))), Nat.add(SC.length(A, xs), 0n)) == True{} : Bool}: 57 match xs: 58 case Nil{}: 59 {==} 60 case Con{+h, +t}: 61 N.le_trans(SC.length(A, t), 1n+SC.length(A, t), Nat.add(1n+SC.length(A, t), 0n), N.le_succ(SC.length(A, t)), SP.le_same(1n+SC.length(A, t))) 62 63 def slen_step(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, op: E.Op) -> {Nat.is_le(SC.length(A, Pair.fst(List<&2, A>, E.Obs, S.step(~A, ~cmp, xs, op))), Nat.add(SC.length(A, xs), SP.pushcost(~A, op))) == True{} : Bool}: 64 match op: 65 case E.Length{}: 66 SP.le_same(SC.length(A, xs)) 67 case E.Push{+x}: 68 L.subst(Nat, z => {Nat.is_le(z, Nat.add(SC.length(A, xs), 1n)) == True{} : Bool}, 1n+SC.length(A, xs), SC.length(A, S.ins(~A, ~cmp, x, xs)), Equal.sym(Nat, SC.length(A, S.ins(~A, ~cmp, x, xs)), 1n+SC.length(A, xs), RT.length_ins(~A, ~cmp, x, xs)), SP.le_succ_add(SC.length(A, xs))) 69 case E.Peek{}: 70 SP.le_same(SC.length(A, xs)) 71 case E.Pop{}: 72 slen_pop(A, xs) 73 case E.FromList{+ys}: 74 L.subst(Nat, z => {Nat.is_le(z, Nat.add(SC.length(A, xs), SC.length(A, ys))) == True{} : Bool}, Nat.add(0n, SC.length(A, ys)), SC.length(A, S.from_list(~A, ~cmp, ys, Nil{})), 75 Equal.sym(Nat, SC.length(A, S.from_list(~A, ~cmp, ys, Nil{})), SC.length(A, ys), Equal.trans(Nat, SC.length(A, S.from_list(~A, ~cmp, ys, Nil{})), Nat.add(SC.length(A, ys), 0n), SC.length(A, ys), BG.len_from_list(~A, ~cmp, ys, Nil{}), N.add_zero(SC.length(A, ys)))), 76 SP.le_add_zero(SC.length(A, ys), SC.length(A, xs))) 77 case E.ToSortedList{}: 78 SP.le_same(SC.length(A, xs)) 79 80 # ---- projections of a step ---- 81 82 def so_sh(~A: Data, ~cmp: A -> A -> Cmp, -sh: ST.Shadow, -op: E.Op, so: SP.StepOK(~A, ~cmp, sh, op)) -> ST.Shadow: 83 match so: 84 case Tuple{sh2, r}: 85 sh2 86 87 def so_obs(~A: Data, ~cmp: A -> A -> Cmp, -sh: ST.Shadow, -op: E.Op, so: SP.StepOK(~A, ~cmp, sh, op)) -> E.Obs: 88 match so: 89 case Tuple{sh2, Tuple{o, r}}: 90 o 91 92 def so_step(~A: Data, ~cmp: A -> A -> Cmp, -sh: ST.Shadow, -op: E.Op, so: SP.StepOK(~A, ~cmp, sh, op)) -> {H.step(~A, ~cmp, ST.real(~A, sh), op) == (ST.real(~A, so_sh(~A, ~cmp, sh, op, so)), so_obs(~A, ~cmp, sh, op, so)) : H.Heap & E.Obs}: 93 match so: 94 case Tuple{sh2, Tuple{o, Tuple{e, r}}}: 95 e 96 97 def so_good(~A: Data, ~cmp: A -> A -> Cmp, -sh: ST.Shadow, -op: E.Op, so: SP.StepOK(~A, ~cmp, sh, op)) -> {ST.good(~A, ~cmp, so_sh(~A, ~cmp, sh, op, so)) == True{} : Bool}: 98 match so: 99 case Tuple{sh2, Tuple{o, Tuple{e, Tuple{g, s}}}}: 100 g 101 102 def so_spec(~A: Data, ~cmp: A -> A -> Cmp, -sh: ST.Shadow, -op: E.Op, so: SP.StepOK(~A, ~cmp, sh, op)) -> {(ST.model(~A, ~cmp, so_sh(~A, ~cmp, sh, op, so)), so_obs(~A, ~cmp, sh, op, so)) == S.step(~A, ~cmp, ST.model(~A, ~cmp, sh), op) : List<&2, A> & E.Obs}: 103 match so: 104 case Tuple{sh2, Tuple{o, Tuple{e, Tuple{g, Tuple{s, dd}}}}}: 105 s 106 107 def so_depth(~A: Data, ~cmp: A -> A -> Cmp, -sh: ST.Shadow, -op: E.Op, so: SP.StepOK(~A, ~cmp, sh, op)) -> {Nat.is_le(ST.sh_depth(~A, so_sh(~A, ~cmp, sh, op, so)), Nat.add(ST.sh_depth(~A, sh), SP.pushcost(~A, op))) == True{} : Bool}: 108 match so: 109 case Tuple{sh2, Tuple{o, Tuple{e, Tuple{g, Tuple{s, dd}}}}}: 110 dd 111 112 # the size grows by at most the step's push count 113 def so_size(~A: Data, ~cmp: A -> A -> Cmp, +sh: ST.Shadow, +op: E.Op, +g: {ST.good(~A, ~cmp, sh) == True{} : Bool}, so: SP.StepOK(~A, ~cmp, sh, op)) -> {Nat.is_le(ST.sh_size(~A, so_sh(~A, ~cmp, sh, op, so)), Nat.add(ST.sh_size(~A, sh), SP.pushcost(~A, op))) == True{} : Bool}: 114 match so: 115 case Tuple{sh2, Tuple{o, Tuple{e, Tuple{g2, Tuple{sp, dd}}}}}: 116 +m1 = Pair.fst(List<&2, A>, E.Obs, S.step(~A, ~cmp, ST.model(~A, ~cmp, sh), op)) 117 +el = Equal.trans(Nat, ST.sh_size(~A, sh2), SC.length(A, ST.model(~A, ~cmp, sh2)), SC.length(A, m1), 118 BG.sz_len(~A, ~cmp, sh2, g2), 119 Equal.cong(List<&2, A> & E.Obs, Nat, pr => SC.length(A, Pair.fst(List<&2, A>, E.Obs, pr)), (ST.model(~A, ~cmp, sh2), o), S.step(~A, ~cmp, ST.model(~A, ~cmp, sh), op), sp)) 120 L.subst(Nat, z => {Nat.is_le(z, Nat.add(ST.sh_size(~A, sh), SP.pushcost(~A, op))) == True{} : Bool}, SC.length(A, m1), ST.sh_size(~A, sh2), Equal.sym(Nat, ST.sh_size(~A, sh2), SC.length(A, m1), el), 121 L.subst(Nat, z => {Nat.is_le(SC.length(A, m1), Nat.add(z, SP.pushcost(~A, op))) == True{} : Bool}, SC.length(A, ST.model(~A, ~cmp, sh)), ST.sh_size(~A, sh), Equal.sym(Nat, ST.sh_size(~A, sh), SC.length(A, ST.model(~A, ~cmp, sh)), BG.sz_len(~A, ~cmp, sh, g)), 122 slen_step(~A, ~cmp, ST.model(~A, ~cmp, sh), op))) 123 124 # ---- the run ---- 125 126 def srun_obs(~A: Data, ~cmp: A -> A -> Cmp, ops: List<&2, E.Op>, m: List<&2, A>) -> List<&2, E.Obs>: 127 Pair.snd(List<&2, A>, List<&2, E.Obs>, S.run(~A, ~cmp, ops, m)) 128 129 def srun_state(~A: Data, ~cmp: A -> A -> Cmp, ops: List<&2, E.Op>, m: List<&2, A>) -> List<&2, A>: 130 Pair.fst(List<&2, A>, List<&2, E.Obs>, S.run(~A, ~cmp, ops, m)) 131 132 def spec_run_cons(~A: Data, ~cmp: A -> A -> Cmp, +op: E.Op, +rest: List<&2, E.Op>, +m: List<&2, A>, +m1: List<&2, A>, +o: E.Obs, +e: {(m1, o) == S.step(~A, ~cmp, m, op) : List<&2, A> & E.Obs}) -> {S.run(~A, ~cmp, Con{op, rest}, m) == (srun_state(~A, ~cmp, rest, m1), Con{o, srun_obs(~A, ~cmp, rest, m1)}) : List<&2, A> & List<&2, E.Obs>}: 133 %e : {S.cons_obs(A, Pair.snd(List<&2, A>, E.Obs, _), S.run(~A, ~cmp, rest, Pair.fst(List<&2, A>, E.Obs, _))) == (srun_state(~A, ~cmp, rest, m1), Con{o, srun_obs(~A, ~cmp, rest, m1)}) : List<&2, A> & List<&2, E.Obs>} 134 %Equal.sym(List<&2, A> & List<&2, E.Obs>, S.run(~A, ~cmp, rest, m1), (srun_state(~A, ~cmp, rest, m1), srun_obs(~A, ~cmp, rest, m1)), L.pair_eta(List<&2, A>, List<&2, E.Obs>, S.run(~A, ~cmp, rest, m1))) : {S.cons_obs(A, o, _) == (srun_state(~A, ~cmp, rest, m1), Con{o, srun_obs(~A, ~cmp, rest, m1)}) : List<&2, A> & List<&2, E.Obs>} 135 {==} 136 137 def RunOK(~A: Data, ~cmp: A -> A -> Cmp, ops: List<&2, E.Op>, sh: ST.Shadow, acc: List<&2, E.Obs>) -> Type: 138 Sigma<&1, &1, ST.Shadow, sh2 => {H.run_acc(~A, ~cmp, ops, (ST.real(~A, sh), acc)) == (ST.real(~A, sh2), List.reverse.go(&2, E.Obs, srun_obs(~A, ~cmp, ops, ST.model(~A, ~cmp, sh)), acc)) : H.Heap & List<&2, E.Obs>} & ({ST.good(~A, ~cmp, sh2) == True{} : Bool} & {ST.model(~A, ~cmp, sh2) == srun_state(~A, ~cmp, ops, ST.model(~A, ~cmp, sh)) : List<&2, A>})> 139 140 def ro_sh(~A: Data, ~cmp: A -> A -> Cmp, -ops: List<&2, E.Op>, -sh: ST.Shadow, -acc: List<&2, E.Obs>, r: RunOK(~A, ~cmp, ops, sh, acc)) -> ST.Shadow: 141 match r: 142 case Tuple{sh2, x}: 143 sh2 144 145 def ro_run(~A: Data, ~cmp: A -> A -> Cmp, -ops: List<&2, E.Op>, -sh: ST.Shadow, -acc: List<&2, E.Obs>, r: RunOK(~A, ~cmp, ops, sh, acc)) -> {H.run_acc(~A, ~cmp, ops, (ST.real(~A, sh), acc)) == (ST.real(~A, ro_sh(~A, ~cmp, ops, sh, acc, r)), List.reverse.go(&2, E.Obs, srun_obs(~A, ~cmp, ops, ST.model(~A, ~cmp, sh)), acc)) : H.Heap & List<&2, E.Obs>}: 146 match r: 147 case Tuple{sh2, Tuple{e, x}}: 148 e 149 150 def ro_good(~A: Data, ~cmp: A -> A -> Cmp, -ops: List<&2, E.Op>, -sh: ST.Shadow, -acc: List<&2, E.Obs>, r: RunOK(~A, ~cmp, ops, sh, acc)) -> {ST.good(~A, ~cmp, ro_sh(~A, ~cmp, ops, sh, acc, r)) == True{} : Bool}: 151 match r: 152 case Tuple{sh2, Tuple{e, Tuple{g, m}}}: 153 g 154 155 def ro_model(~A: Data, ~cmp: A -> A -> Cmp, -ops: List<&2, E.Op>, -sh: ST.Shadow, -acc: List<&2, E.Obs>, r: RunOK(~A, ~cmp, ops, sh, acc)) -> {ST.model(~A, ~cmp, ro_sh(~A, ~cmp, ops, sh, acc, r)) == srun_state(~A, ~cmp, ops, ST.model(~A, ~cmp, sh)) : List<&2, A>}: 156 match r: 157 case Tuple{sh2, Tuple{e, Tuple{g, m}}}: 158 m 159 160 def run_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ops: List<&2, E.Op>, +sh: ST.Shadow, +acc: List<&2, E.Obs>, +g: {ST.good(~A, ~cmp, sh) == True{} : Bool}, +q: Nat, +hq: {Nat.is_le(q, 31n) == True{} : Bool}, +room: {Nat.is_lt(Nat.add(ST.sh_size(~A, sh), pushes(~A, ops)), SC.pow2(q)) == True{} : Bool}) -> RunOK(~A, ~cmp, ops, sh, acc): 161 match ops: 162 case Nil{}: 163 (sh, ({==}, (g, {==}))) 164 case Con{+op, +rest}: 165 +m = ST.model(~A, ~cmp, sh) 166 +hh = budget_head(~A, ST.sh_size(~A, sh), op, rest, q, room) 167 +sh1 = so_sh(~A, ~cmp, sh, op, SP.step_ok(~A, ~cmp, ~o, sh, op, g, q, hq, hh)) 168 +ob = so_obs(~A, ~cmp, sh, op, SP.step_ok(~A, ~cmp, ~o, sh, op, g, q, hq, hh)) 169 +g1 = so_good(~A, ~cmp, sh, op, SP.step_ok(~A, ~cmp, ~o, sh, op, g, q, hq, hh)) 170 +r1 = budget_tail(~A, ST.sh_size(~A, sh), ST.sh_size(~A, sh1), op, rest, q, so_size(~A, ~cmp, sh, op, g, SP.step_ok(~A, ~cmp, ~o, sh, op, g, q, hq, hh)), room) 171 +m1 = ST.model(~A, ~cmp, sh1) 172 +acc1 = {Con{ob, acc} : List<&2, E.Obs>} 173 +sh2 = ro_sh(~A, ~cmp, rest, sh1, acc1, run_ok(~A, ~cmp, ~o, rest, sh1, acc1, g1, q, hq, r1)) 174 +es = spec_run_cons(~A, ~cmp, op, rest, m, m1, ob, so_spec(~A, ~cmp, sh, op, SP.step_ok(~A, ~cmp, ~o, sh, op, g, q, hq, hh))) 175 -R = S.run(~A, ~cmp, rest, m1) 176 (sh2, ( 177 %Equal.sym(H.Heap & E.Obs, H.step(~A, ~cmp, ST.real(~A, sh), op), (ST.real(~A, sh1), ob), so_step(~A, ~cmp, sh, op, SP.step_ok(~A, ~cmp, ~o, sh, op, g, q, hq, hh))) : {H.run_acc(~A, ~cmp, rest, H.record(~A, acc, _)) == (ST.real(~A, sh2), List.reverse.go(&2, E.Obs, srun_obs(~A, ~cmp, Con{op, rest}, m), acc)) : H.Heap & List<&2, E.Obs>} 178 %Equal.sym(H.Heap & List<&2, E.Obs>, H.run_acc(~A, ~cmp, rest, (ST.real(~A, sh1), acc1)), (ST.real(~A, sh2), List.reverse.go(&2, E.Obs, srun_obs(~A, ~cmp, rest, m1), acc1)), ro_run(~A, ~cmp, rest, sh1, acc1, run_ok(~A, ~cmp, ~o, rest, sh1, acc1, g1, q, hq, r1))) : {_ == (ST.real(~A, sh2), List.reverse.go(&2, E.Obs, srun_obs(~A, ~cmp, Con{op, rest}, m), acc)) : H.Heap & List<&2, E.Obs>} 179 %Equal.sym(List<&2, A> & List<&2, E.Obs>, S.run(~A, ~cmp, Con{op, rest}, m), (Pair.fst(List<&2, A>, List<&2, E.Obs>, R), Con{ob, Pair.snd(List<&2, A>, List<&2, E.Obs>, R)}), es) : {(ST.real(~A, sh2), List.reverse.go(&2, E.Obs, srun_obs(~A, ~cmp, rest, m1), acc1)) == (ST.real(~A, sh2), List.reverse.go(&2, E.Obs, Pair.snd(List<&2, A>, List<&2, E.Obs>, _), acc)) : H.Heap & List<&2, E.Obs>} 180 {==}, 181 (ro_good(~A, ~cmp, rest, sh1, acc1, run_ok(~A, ~cmp, ~o, rest, sh1, acc1, g1, q, hq, r1)), 182 %Equal.sym(List<&2, A> & List<&2, E.Obs>, S.run(~A, ~cmp, Con{op, rest}, m), (Pair.fst(List<&2, A>, List<&2, E.Obs>, R), Con{ob, Pair.snd(List<&2, A>, List<&2, E.Obs>, R)}), es) : {ST.model(~A, ~cmp, sh2) == Pair.fst(List<&2, A>, List<&2, E.Obs>, _) : List<&2, A>} 183 ro_model(~A, ~cmp, rest, sh1, acc1, run_ok(~A, ~cmp, ~o, rest, sh1, acc1, g1, q, hq, r1))))) 184 185 def run_from(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ops: List<&2, E.Op>, +sh0: ST.Shadow, +g0: {ST.good(~A, ~cmp, sh0) == True{} : Bool}, +q: Nat, +hq: {Nat.is_le(q, 31n) == True{} : Bool}, +room: {Nat.is_lt(Nat.add(ST.sh_size(~A, sh0), pushes(~A, ops)), SC.pow2(q)) == True{} : Bool}) -> {H.run(~A, ~cmp, ops, ST.real(~A, sh0)) == (ST.real(~A, ro_sh(~A, ~cmp, ops, sh0, Nil{}, run_ok(~A, ~cmp, ~o, ops, sh0, Nil{}, g0, q, hq, room))), srun_obs(~A, ~cmp, ops, ST.model(~A, ~cmp, sh0))) : H.Heap & List<&2, E.Obs>}: 186 +sh2 = ro_sh(~A, ~cmp, ops, sh0, Nil{}, run_ok(~A, ~cmp, ~o, ops, sh0, Nil{}, g0, q, hq, room)) 187 +os = srun_obs(~A, ~cmp, ops, ST.model(~A, ~cmp, sh0)) 188 %Equal.sym(H.Heap & List<&2, E.Obs>, H.run_acc(~A, ~cmp, ops, (ST.real(~A, sh0), Nil{})), (ST.real(~A, sh2), List.reverse.go(&2, E.Obs, os, Nil{})), ro_run(~A, ~cmp, ops, sh0, Nil{}, run_ok(~A, ~cmp, ~o, ops, sh0, Nil{}, g0, q, hq, room))) : {H.finish(~A, _) == (ST.real(~A, sh2), os) : H.Heap & List<&2, E.Obs>} 189 %Equal.sym(List<&2, E.Obs>, List.reverse(&2, E.Obs, List.reverse.go(&2, E.Obs, os, Nil{})), os, LL.rev_rev(E.Obs, os)) : {(ST.real(~A, sh2), _) == (ST.real(~A, sh2), os) : H.Heap & List<&2, E.Obs>} 190 {==} 191 192 def TraceOK(~A: Data, ~cmp: A -> A -> Cmp, ops: List<&2, E.Op>, sh0: ST.Shadow) -> Type: 193 Sigma<&1, &1, ST.Shadow, sh2 => {H.run(~A, ~cmp, ops, ST.real(~A, sh0)) == (ST.real(~A, sh2), srun_obs(~A, ~cmp, ops, ST.model(~A, ~cmp, sh0))) : H.Heap & List<&2, E.Obs>} & ({ST.good(~A, ~cmp, sh2) == True{} : Bool} & {ST.model(~A, ~cmp, sh2) == srun_state(~A, ~cmp, ops, ST.model(~A, ~cmp, sh0)) : List<&2, A>})> 194 195 def trace_from(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ops: List<&2, E.Op>, +sh0: ST.Shadow, +g0: {ST.good(~A, ~cmp, sh0) == True{} : Bool}, +q: Nat, +hq: {Nat.is_le(q, 31n) == True{} : Bool}, +room: {Nat.is_lt(Nat.add(ST.sh_size(~A, sh0), pushes(~A, ops)), SC.pow2(q)) == True{} : Bool}) -> TraceOK(~A, ~cmp, ops, sh0): 196 (ro_sh(~A, ~cmp, ops, sh0, Nil{}, run_ok(~A, ~cmp, ~o, ops, sh0, Nil{}, g0, q, hq, room)), 197 (run_from(~A, ~cmp, ~o, ops, sh0, g0, q, hq, room), 198 (ro_good(~A, ~cmp, ops, sh0, Nil{}, run_ok(~A, ~cmp, ~o, ops, sh0, Nil{}, g0, q, hq, room)), 199 ro_model(~A, ~cmp, ops, sh0, Nil{}, run_ok(~A, ~cmp, ~o, ops, sh0, Nil{}, g0, q, hq, room)))))