proofs/containers/binary_heap/trace.bend
bend-collections-laws-containers@1.0.0.0 · 199 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/spec/containers/binary_heap.bend as S
8import bend-collections-laws-containers@1.0.0.0/src/containers/binary_heap.bend as H
9import bend-collections-laws-containers@1.0.0.0/src/containers/types/binary_heap.bend as E
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/state.bend as ST
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/steps.bend as SP
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/root.bend as RT
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/budget.bend as BG
14
15def 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
33def pushes(~A: Data, ops: List<&2, E.Op<A>>) -> 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
40def 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
45def budget_head(~A: Data, +d: Nat, +op: E.Op<A>, +rest: List<&2, E.Op<A>>, +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
49def budget_tail(~A: Data, +d: Nat, +d2: Nat, +op: E.Op<A>, +rest: List<&2, E.Op<A>>, +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
56def slen_pop(-A: Data, xs: List<&2, A>) -> {Nat.is_le(SC.length(A, Pair.fst(List<&2, A>, E.Obs<A>, 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
63def slen_step(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, op: E.Op<A>) -> {Nat.is_le(SC.length(A, Pair.fst(List<&2, A>, E.Obs<A>, 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
82def so_sh(~A: Data, ~cmp: A -> A -> Cmp, -sh: ST.Shadow<A>, -op: E.Op<A>, so: SP.StepOK(~A, ~cmp, sh, op)) -> ST.Shadow<A>:
83 match so:
84 case Tuple{sh2, r}:
85 sh2
86
87def so_obs(~A: Data, ~cmp: A -> A -> Cmp, -sh: ST.Shadow<A>, -op: E.Op<A>, so: SP.StepOK(~A, ~cmp, sh, op)) -> E.Obs<A>:
88 match so:
89 case Tuple{sh2, Tuple{o, r}}:
90 o
91
92def so_step(~A: Data, ~cmp: A -> A -> Cmp, -sh: ST.Shadow<A>, -op: E.Op<A>, 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<A> & E.Obs<A>}:
93 match so:
94 case Tuple{sh2, Tuple{o, Tuple{e, r}}}:
95 e
96
97def so_good(~A: Data, ~cmp: A -> A -> Cmp, -sh: ST.Shadow<A>, -op: E.Op<A>, 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
102def so_spec(~A: Data, ~cmp: A -> A -> Cmp, -sh: ST.Shadow<A>, -op: E.Op<A>, 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<A>}:
103 match so:
104 case Tuple{sh2, Tuple{o, Tuple{e, Tuple{g, Tuple{s, dd}}}}}:
105 s
106
107def so_depth(~A: Data, ~cmp: A -> A -> Cmp, -sh: ST.Shadow<A>, -op: E.Op<A>, 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
113def so_size(~A: Data, ~cmp: A -> A -> Cmp, +sh: ST.Shadow<A>, +op: E.Op<A>, +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<A>, 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<A>, Nat, pr => SC.length(A, Pair.fst(List<&2, A>, E.Obs<A>, 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
126def srun_obs(~A: Data, ~cmp: A -> A -> Cmp, ops: List<&2, E.Op<A>>, m: List<&2, A>) -> List<&2, E.Obs<A>>:
127 Pair.snd(List<&2, A>, List<&2, E.Obs<A>>, S.run(~A, ~cmp, ops, m))
128
129def srun_state(~A: Data, ~cmp: A -> A -> Cmp, ops: List<&2, E.Op<A>>, m: List<&2, A>) -> List<&2, A>:
130 Pair.fst(List<&2, A>, List<&2, E.Obs<A>>, S.run(~A, ~cmp, ops, m))
131
132def spec_run_cons(~A: Data, ~cmp: A -> A -> Cmp, +op: E.Op<A>, +rest: List<&2, E.Op<A>>, +m: List<&2, A>, +m1: List<&2, A>, +o: E.Obs<A>, +e: {(m1, o) == S.step(~A, ~cmp, m, op) : List<&2, A> & E.Obs<A>}) -> {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<A>>}:
133 %e : {S.cons_obs(A, Pair.snd(List<&2, A>, E.Obs<A>, _), S.run(~A, ~cmp, rest, Pair.fst(List<&2, A>, E.Obs<A>, _))) == (srun_state(~A, ~cmp, rest, m1), Con{o, srun_obs(~A, ~cmp, rest, m1)}) : List<&2, A> & List<&2, E.Obs<A>>}
134 %Equal.sym(List<&2, A> & List<&2, E.Obs<A>>, 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<A>>, 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<A>>}
135 {==}
136
137def RunOK(~A: Data, ~cmp: A -> A -> Cmp, ops: List<&2, E.Op<A>>, sh: ST.Shadow<A>, acc: List<&2, E.Obs<A>>) -> Type:
138 Sigma<&1, &1, ST.Shadow<A>, sh2 => {H.run_acc(~A, ~cmp, ops, (ST.real(~A, sh), acc)) == (ST.real(~A, sh2), List.reverse.go(&2, E.Obs<A>, srun_obs(~A, ~cmp, ops, ST.model(~A, ~cmp, sh)), acc)) : H.Heap<A> & List<&2, E.Obs<A>>} & ({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
140def ro_sh(~A: Data, ~cmp: A -> A -> Cmp, -ops: List<&2, E.Op<A>>, -sh: ST.Shadow<A>, -acc: List<&2, E.Obs<A>>, r: RunOK(~A, ~cmp, ops, sh, acc)) -> ST.Shadow<A>:
141 match r:
142 case Tuple{sh2, x}:
143 sh2
144
145def ro_run(~A: Data, ~cmp: A -> A -> Cmp, -ops: List<&2, E.Op<A>>, -sh: ST.Shadow<A>, -acc: List<&2, E.Obs<A>>, 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<A>, srun_obs(~A, ~cmp, ops, ST.model(~A, ~cmp, sh)), acc)) : H.Heap<A> & List<&2, E.Obs<A>>}:
146 match r:
147 case Tuple{sh2, Tuple{e, x}}:
148 e
149
150def ro_good(~A: Data, ~cmp: A -> A -> Cmp, -ops: List<&2, E.Op<A>>, -sh: ST.Shadow<A>, -acc: List<&2, E.Obs<A>>, 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
155def ro_model(~A: Data, ~cmp: A -> A -> Cmp, -ops: List<&2, E.Op<A>>, -sh: ST.Shadow<A>, -acc: List<&2, E.Obs<A>>, 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
160def run_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ops: List<&2, E.Op<A>>, +sh: ST.Shadow<A>, +acc: List<&2, E.Obs<A>>, +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<A>>}
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<A> & E.Obs<A>, 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<A>, srun_obs(~A, ~cmp, Con{op, rest}, m), acc)) : H.Heap<A> & List<&2, E.Obs<A>>}
178 %Equal.sym(H.Heap<A> & List<&2, E.Obs<A>>, H.run_acc(~A, ~cmp, rest, (ST.real(~A, sh1), acc1)), (ST.real(~A, sh2), List.reverse.go(&2, E.Obs<A>, 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<A>, srun_obs(~A, ~cmp, Con{op, rest}, m), acc)) : H.Heap<A> & List<&2, E.Obs<A>>}
179 %Equal.sym(List<&2, A> & List<&2, E.Obs<A>>, S.run(~A, ~cmp, Con{op, rest}, m), (Pair.fst(List<&2, A>, List<&2, E.Obs<A>>, R), Con{ob, Pair.snd(List<&2, A>, List<&2, E.Obs<A>>, R)}), es) : {(ST.real(~A, sh2), List.reverse.go(&2, E.Obs<A>, srun_obs(~A, ~cmp, rest, m1), acc1)) == (ST.real(~A, sh2), List.reverse.go(&2, E.Obs<A>, Pair.snd(List<&2, A>, List<&2, E.Obs<A>>, _), acc)) : H.Heap<A> & List<&2, E.Obs<A>>}
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<A>>, S.run(~A, ~cmp, Con{op, rest}, m), (Pair.fst(List<&2, A>, List<&2, E.Obs<A>>, R), Con{ob, Pair.snd(List<&2, A>, List<&2, E.Obs<A>>, R)}), es) : {ST.model(~A, ~cmp, sh2) == Pair.fst(List<&2, A>, List<&2, E.Obs<A>>, _) : List<&2, A>}
183 ro_model(~A, ~cmp, rest, sh1, acc1, run_ok(~A, ~cmp, ~o, rest, sh1, acc1, g1, q, hq, r1)))))
184
185def run_from(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ops: List<&2, E.Op<A>>, +sh0: ST.Shadow<A>, +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<A> & List<&2, E.Obs<A>>}:
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<A> & List<&2, E.Obs<A>>, H.run_acc(~A, ~cmp, ops, (ST.real(~A, sh0), Nil{})), (ST.real(~A, sh2), List.reverse.go(&2, E.Obs<A>, 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<A> & List<&2, E.Obs<A>>}
189 %Equal.sym(List<&2, E.Obs<A>>, List.reverse(&2, E.Obs<A>, List.reverse.go(&2, E.Obs<A>, os, Nil{})), os, LL.rev_rev(E.Obs<A>, os)) : {(ST.real(~A, sh2), _) == (ST.real(~A, sh2), os) : H.Heap<A> & List<&2, E.Obs<A>>}
190 {==}
191
192def TraceOK(~A: Data, ~cmp: A -> A -> Cmp, ops: List<&2, E.Op<A>>, sh0: ST.Shadow<A>) -> Type:
193 Sigma<&1, &1, ST.Shadow<A>, 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<A> & List<&2, E.Obs<A>>} & ({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
195def trace_from(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +ops: List<&2, E.Op<A>>, +sh0: ST.Shadow<A>, +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)))))