proofs/containers/bitlist/trace.bend
bend-collections-laws-containers@1.0.0.0 · 166 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/list.bend as LL
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/src/containers/bitlist.bend as BLI
6import bend-collections-laws-containers@1.0.0.0/src/containers/types/bitlist.bend as E
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/trace.bend as DTR
8import bend-collections-laws-containers@1.0.0.0/spec/containers/bitlist.bend as S
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/state.bend as SS
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/steps.bend as BS
11
12# Arbitrary finite operation traces: the real runner refines the spec runner
13# (the same shadow form as the per-step laws), from the constructors new and
14# with_limit, and from_bools builds exactly the list its bits spell.
15# (source: proofs/containers/bitlist/trace.src)
16
17
18def srun_obs(ops: List<&2, E.Op>, m: S.Model) -> List<&2, E.Obs>:
19 Pair.snd(S.Model, List<&2, E.Obs>, S.run(ops, m))
20
21def srun_state(ops: List<&2, E.Op>, m: S.Model) -> S.Model:
22 Pair.fst(S.Model, List<&2, E.Obs>, S.run(ops, m))
23
24def so_sh(-sh: SS.Sh, -op: E.Op, so: BS.StepOK(sh, op)) -> SS.Sh:
25 match so:
26 case Tuple{sh2, r}:
27 sh2
28
29def so_obs(-sh: SS.Sh, -op: E.Op, so: BS.StepOK(sh, op)) -> E.Obs:
30 match so:
31 case Tuple{sh2, Tuple{o, r}}:
32 o
33
34def so_step(-sh: SS.Sh, -op: E.Op, so: BS.StepOK(sh, op)) -> {BLI.step(SS.real(sh), op) == (SS.real(so_sh(sh, op, so)), so_obs(sh, op, so)) : BLI.Bitlist & E.Obs}:
35 match so:
36 case Tuple{sh2, Tuple{o, Tuple{e, r}}}:
37 e
38
39def so_good(-sh: SS.Sh, -op: E.Op, so: BS.StepOK(sh, op)) -> {SS.good(so_sh(sh, op, so)) == True{} : Bool}:
40 match so:
41 case Tuple{sh2, Tuple{o, Tuple{e, Tuple{g, s}}}}:
42 g
43
44def so_spec(-sh: SS.Sh, -op: E.Op, so: BS.StepOK(sh, op)) -> {(SS.model(so_sh(sh, op, so)), so_obs(sh, op, so)) == S.step(SS.model(sh), op) : S.Model & E.Obs}:
45 match so:
46 case Tuple{sh2, Tuple{o, Tuple{e, Tuple{g, s}}}}:
47 s
48
49def spec_run_cons(+op: E.Op, +rest: List<&2, E.Op>, +m: S.Model, +m1: S.Model, +o: E.Obs, +e: {(m1, o) == S.step(m, op) : S.Model & E.Obs}) -> {S.run(Con{op, rest}, m) == (srun_state(rest, m1), Con{o, srun_obs(rest, m1)}) : S.Model & List<&2, E.Obs>}:
50 %e : {S.cons_obs(Pair.snd(S.Model, E.Obs, _), S.run(rest, Pair.fst(S.Model, E.Obs, _))) == (srun_state(rest, m1), Con{o, srun_obs(rest, m1)}) : S.Model & List<&2, E.Obs>}
51 %Equal.sym(S.Model & List<&2, E.Obs>, S.run(rest, m1), (srun_state(rest, m1), srun_obs(rest, m1)), L.pair_eta(S.Model, List<&2, E.Obs>, S.run(rest, m1))) : {S.cons_obs(o, _) == (srun_state(rest, m1), Con{o, srun_obs(rest, m1)}) : S.Model & List<&2, E.Obs>}
52 {==}
53
54def RunOK(ops: List<&2, E.Op>, sh: SS.Sh, acc: List<&2, E.Obs>) -> Type:
55 Sigma<&1, &1, SS.Sh, sh_2 => {BLI.run_acc(ops, (SS.real(sh), acc)) == (SS.real(sh_2), List.reverse.go(&2, E.Obs, srun_obs(ops, SS.model(sh)), acc)) : BLI.Bitlist & List<&2, E.Obs>} & ({SS.good(sh_2) == True{} : Bool} & {SS.model(sh_2) == srun_state(ops, SS.model(sh)) : S.Model})>
56
57def ro_sh(-ops: List<&2, E.Op>, -sh: SS.Sh, -acc: List<&2, E.Obs>, r: RunOK(ops, sh, acc)) -> SS.Sh:
58 match r:
59 case Tuple{sh2, x}:
60 sh2
61
62def ro_run(-ops: List<&2, E.Op>, -sh: SS.Sh, -acc: List<&2, E.Obs>, r: RunOK(ops, sh, acc)) -> {BLI.run_acc(ops, (SS.real(sh), acc)) == (SS.real(ro_sh(ops, sh, acc, r)), List.reverse.go(&2, E.Obs, srun_obs(ops, SS.model(sh)), acc)) : BLI.Bitlist & List<&2, E.Obs>}:
63 match r:
64 case Tuple{sh2, Tuple{e, x}}:
65 e
66
67def ro_good(-ops: List<&2, E.Op>, -sh: SS.Sh, -acc: List<&2, E.Obs>, r: RunOK(ops, sh, acc)) -> {SS.good(ro_sh(ops, sh, acc, r)) == True{} : Bool}:
68 match r:
69 case Tuple{sh2, Tuple{e, Tuple{g, m}}}:
70 g
71
72def ro_model(-ops: List<&2, E.Op>, -sh: SS.Sh, -acc: List<&2, E.Obs>, r: RunOK(ops, sh, acc)) -> {SS.model(ro_sh(ops, sh, acc, r)) == srun_state(ops, SS.model(sh)) : S.Model}:
73 match r:
74 case Tuple{sh2, Tuple{e, Tuple{g, m}}}:
75 m
76
77def run_ok(+ops: List<&2, E.Op>, +sh: SS.Sh, +acc: List<&2, E.Obs>, +g: {SS.good(sh) == True{} : Bool}) -> RunOK(ops, sh, acc):
78 match ops:
79 case Nil{}:
80 (sh, ({==}, (g, {==})))
81 case Con{+op, +rest}:
82 +m = SS.model(sh)
83 +sh1 = so_sh(sh, op, BS.step_ok(sh, op, g))
84 +o = so_obs(sh, op, BS.step_ok(sh, op, g))
85 +g1 = so_good(sh, op, BS.step_ok(sh, op, g))
86 +m1 = SS.model(sh1)
87 +acc1 = {Con{o, acc} : List<&2, E.Obs>}
88 +sh2 = ro_sh(rest, sh1, acc1, run_ok(rest, sh1, acc1, g1))
89 +es = spec_run_cons(op, rest, m, m1, o, so_spec(sh, op, BS.step_ok(sh, op, g)))
90 -R = S.run(rest, m1)
91 (sh2, (
92 %Equal.sym(BLI.Bitlist & E.Obs, BLI.step(SS.real(sh), op), (SS.real(sh1), o), so_step(sh, op, BS.step_ok(sh, op, g))) : {BLI.run_acc(rest, BLI.record(acc, _)) == (SS.real(sh2), List.reverse.go(&2, E.Obs, srun_obs(Con{op, rest}, m), acc)) : BLI.Bitlist & List<&2, E.Obs>}
93 %Equal.sym(BLI.Bitlist & List<&2, E.Obs>, BLI.run_acc(rest, (SS.real(sh1), acc1)), (SS.real(sh2), List.reverse.go(&2, E.Obs, srun_obs(rest, m1), acc1)), ro_run(rest, sh1, acc1, run_ok(rest, sh1, acc1, g1))) : {_ == (SS.real(sh2), List.reverse.go(&2, E.Obs, srun_obs(Con{op, rest}, m), acc)) : BLI.Bitlist & List<&2, E.Obs>}
94 %Equal.sym(S.Model & List<&2, E.Obs>, S.run(Con{op, rest}, m), (Pair.fst(S.Model, List<&2, E.Obs>, R), Con{o, Pair.snd(S.Model, List<&2, E.Obs>, R)}), es) : {(SS.real(sh2), List.reverse.go(&2, E.Obs, srun_obs(rest, m1), acc1)) == (SS.real(sh2), List.reverse.go(&2, E.Obs, Pair.snd(S.Model, List<&2, E.Obs>, _), acc)) : BLI.Bitlist & List<&2, E.Obs>}
95 {==},
96 (ro_good(rest, sh1, acc1, run_ok(rest, sh1, acc1, g1)),
97 %Equal.sym(S.Model & List<&2, E.Obs>, S.run(Con{op, rest}, m), (Pair.fst(S.Model, List<&2, E.Obs>, R), Con{o, Pair.snd(S.Model, List<&2, E.Obs>, R)}), es) : {SS.model(sh2) == Pair.fst(S.Model, List<&2, E.Obs>, _) : S.Model}
98 ro_model(rest, sh1, acc1, run_ok(rest, sh1, acc1, g1)))))
99
100def run_from(+ops: List<&2, E.Op>, +sh0: SS.Sh, +g0: {SS.good(sh0) == True{} : Bool}) -> {BLI.run(ops, SS.real(sh0)) == (SS.real(ro_sh(ops, sh0, Nil{}, run_ok(ops, sh0, Nil{}, g0))), srun_obs(ops, SS.model(sh0))) : BLI.Bitlist & List<&2, E.Obs>}:
101 +sh2 = ro_sh(ops, sh0, Nil{}, run_ok(ops, sh0, Nil{}, g0))
102 +os = srun_obs(ops, SS.model(sh0))
103 %Equal.sym(BLI.Bitlist & List<&2, E.Obs>, BLI.run_acc(ops, (SS.real(sh0), Nil{})), (SS.real(sh2), List.reverse.go(&2, E.Obs, os, Nil{})), ro_run(ops, sh0, Nil{}, run_ok(ops, sh0, Nil{}, g0))) : {BLI.finish(_) == (SS.real(sh2), os) : BLI.Bitlist & List<&2, E.Obs>}
104 %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)) : {(SS.real(sh2), _) == (SS.real(sh2), os) : BLI.Bitlist & List<&2, E.Obs>}
105 {==}
106
107def TraceOK(ops: List<&2, E.Op>, sh0: SS.Sh) -> Type:
108 Sigma<&1, &1, SS.Sh, sh_2 => {BLI.run(ops, SS.real(sh0)) == (SS.real(sh_2), srun_obs(ops, SS.model(sh0))) : BLI.Bitlist & List<&2, E.Obs>} & ({SS.good(sh_2) == True{} : Bool} & {SS.model(sh_2) == srun_state(ops, SS.model(sh0)) : S.Model})>
109
110def trace_from(+ops: List<&2, E.Op>, +sh0: SS.Sh, +g0: {SS.good(sh0) == True{} : Bool}) -> TraceOK(ops, sh0):
111 (ro_sh(ops, sh0, Nil{}, run_ok(ops, sh0, Nil{}, g0)),
112 (run_from(ops, sh0, g0),
113 (ro_good(ops, sh0, Nil{}, run_ok(ops, sh0, Nil{}, g0)),
114 ro_model(ops, sh0, Nil{}, run_ok(ops, sh0, Nil{}, g0)))))
115
116# ---- the constructors ----
117
118def initial(+l: Maybe<&2, Nat>) -> SS.Sh:
119 {SS.BSh{l, 0n, DTR.initial(U32)} : SS.Sh}
120
121def new_real() -> {BLI.new() == SS.real(initial(None{})) : BLI.Bitlist}:
122 {==}
123
124def with_limit_real(+n: Nat) -> {BLI.with_limit(n) == SS.real(initial(Some{n})) : BLI.Bitlist}:
125 {==}
126
127def initial_good(+l: Maybe<&2, Nat>) -> {SS.good(initial(l)) == True{} : Bool}:
128 {==}
129
130def new_model() -> {SS.model(initial(None{})) == S.new() : S.Model}:
131 {==}
132
133def with_limit_model(+n: Nat) -> {SS.model(initial(Some{n})) == S.with_limit(n) : S.Model}:
134 {==}
135
136# ---- from_bools ----
137
138def fpush(p: BLI.Bitlist & Result<&2, &2, E.Error, Unit>) -> {BLI.from_push(p) == Pair.fst(BLI.Bitlist, E.Obs, BLI.obs_unit(p)) : BLI.Bitlist}:
139 match p:
140 case Tuple{s, r}:
141 {==}
142
143def FromOK(bs: List<&2, Bool>, sh: SS.Sh) -> Type:
144 Sigma<&1, &1, SS.Sh, sh_2 => {BLI.from_go(bs, SS.real(sh)) == SS.real(sh_2) : BLI.Bitlist} & ({SS.good(sh_2) == True{} : Bool} & {SS.model(sh_2) == S.push_all(bs, SS.model(sh)) : S.Model})>
145
146def from_lift(+b: Bool, +t: List<&2, Bool>, sh: SS.Sh, +sh1: SS.Sh, +e1: {BLI.from_push(BLI.push(SS.real(sh), b)) == SS.real(sh1) : BLI.Bitlist}, +m1: {SS.model(sh1) == Pair.fst(S.Model, E.Obs, S.step(SS.model(sh), E.Push{b})) : S.Model}, ih: FromOK(t, sh1)) -> FromOK(Con{b, t}, sh):
147 match ih:
148 case Tuple{sh2, Tuple{e2, Tuple{g2, mm}}}:
149 (sh2, (%Equal.sym(BLI.Bitlist, BLI.from_push(BLI.push(SS.real(sh), b)), SS.real(sh1), e1) : {BLI.from_go(t, _) == SS.real(sh2) : BLI.Bitlist}
150 e2,
151 (g2, %Equal.sym(S.Model, Pair.fst(S.Model, E.Obs, S.step(SS.model(sh), E.Push{b})), SS.model(sh1), Equal.sym(S.Model, SS.model(sh1), Pair.fst(S.Model, E.Obs, S.step(SS.model(sh), E.Push{b})), m1)) : {SS.model(sh2) == S.push_all(t, _) : S.Model}
152 mm)))
153
154def from_ok(+bs: List<&2, Bool>, +sh: SS.Sh, +g: {SS.good(sh) == True{} : Bool}) -> FromOK(bs, sh):
155 match bs:
156 case Nil{}:
157 (sh, ({==}, (g, {==})))
158 case Con{+b, +t}:
159 +sh1 = so_sh(sh, E.Push{b}, BS.step_ok(sh, E.Push{b}, g))
160 +e1 = Equal.trans(BLI.Bitlist, BLI.from_push(BLI.push(SS.real(sh), b)), Pair.fst(BLI.Bitlist, E.Obs, BLI.step(SS.real(sh), E.Push{b})), SS.real(sh1), fpush(BLI.push(SS.real(sh), b)),
161 Equal.cong(BLI.Bitlist & E.Obs, BLI.Bitlist, p => Pair.fst(BLI.Bitlist, E.Obs, p), BLI.step(SS.real(sh), E.Push{b}), (SS.real(sh1), so_obs(sh, E.Push{b}, BS.step_ok(sh, E.Push{b}, g))), so_step(sh, E.Push{b}, BS.step_ok(sh, E.Push{b}, g))))
162 +m1 = Equal.cong(S.Model & E.Obs, S.Model, p => Pair.fst(S.Model, E.Obs, p), (SS.model(sh1), so_obs(sh, E.Push{b}, BS.step_ok(sh, E.Push{b}, g))), S.step(SS.model(sh), E.Push{b}), so_spec(sh, E.Push{b}, BS.step_ok(sh, E.Push{b}, g)))
163 from_lift(b, t, sh, sh1, e1, m1, from_ok(t, sh1, so_good(sh, E.Push{b}, BS.step_ok(sh, E.Push{b}, g))))
164
165def from_bools_ok(+bs: List<&2, Bool>) -> FromOK(bs, initial(None{})):
166 from_ok(bs, initial(None{}), initial_good(None{}))