proofs/containers/bitset/trace.bend
bend-collections-laws-containers@1.0.0.0 · 132 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/proofs/lib/array.bend as A
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/src/containers/bitset.bend as B
7import bend-collections-laws-containers@1.0.0.0/spec/containers/bitset.bend as S
8import bend-collections-laws-containers@1.0.0.0/src/containers/types/bitset.bend as E
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/state.bend as ST
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/steps.bend as BS
11
12# Arbitrary finite operation traces: the real runner refines the spec runner.
13#
14# Base.Array is linear, so the statement is the same shadow form the per-step
15# laws use: running any finite list of operations on the array of a good
16# shadow lands on the array of another good shadow, emits exactly the spec
17# runner's observations, and the model of the final shadow is the spec
18# runner's final model.
19
20def srun_obs(ops: List<&2, E.Op>, m: List<&2, Bool>) -> List<&2, E.Obs>:
21 Pair.snd(List<&2, Bool>, List<&2, E.Obs>, S.run(ops, m))
22
23def srun_state(ops: List<&2, E.Op>, m: List<&2, Bool>) -> List<&2, Bool>:
24 Pair.fst(List<&2, Bool>, List<&2, E.Obs>, S.run(ops, m))
25
26def so_sh(-sh: ST.Sh, -op: E.Op, so: BS.StepOK(sh, op)) -> ST.Sh:
27 match so:
28 case Tuple{sh2, r}:
29 sh2
30
31def so_obs(-sh: ST.Sh, -op: E.Op, so: BS.StepOK(sh, op)) -> E.Obs:
32 match so:
33 case Tuple{sh2, Tuple{o, r}}:
34 o
35
36def so_step(-sh: ST.Sh, -op: E.Op, so: BS.StepOK(sh, op)) -> {B.step(ST.real(sh), op) == (ST.real(so_sh(sh, op, so)), so_obs(sh, op, so)) : B.Bitset & E.Obs}:
37 match so:
38 case Tuple{sh2, Tuple{o, Tuple{e, r}}}:
39 e
40
41def so_good(-sh: ST.Sh, -op: E.Op, so: BS.StepOK(sh, op)) -> {ST.good(so_sh(sh, op, so)) == True{} : Bool}:
42 match so:
43 case Tuple{sh2, Tuple{o, Tuple{e, Tuple{g, s}}}}:
44 g
45
46def so_spec(-sh: ST.Sh, -op: E.Op, so: BS.StepOK(sh, op)) -> {(ST.model(so_sh(sh, op, so)), so_obs(sh, op, so)) == S.step(ST.model(sh), op) : List<&2, Bool> & E.Obs}:
47 match so:
48 case Tuple{sh2, Tuple{o, Tuple{e, Tuple{g, s}}}}:
49 s
50
51def spec_run_cons(+op: E.Op, +rest: List<&2, E.Op>, +m: List<&2, Bool>, +m1: List<&2, Bool>, +o: E.Obs, +e: {(m1, o) == S.step(m, op) : List<&2, Bool> & E.Obs}) -> {S.run(Con{op, rest}, m) == (srun_state(rest, m1), Con{o, srun_obs(rest, m1)}) : List<&2, Bool> & List<&2, E.Obs>}:
52 %e : {S.cons_obs(Pair.snd(List<&2, Bool>, E.Obs, _), S.run(rest, Pair.fst(List<&2, Bool>, E.Obs, _))) == (srun_state(rest, m1), Con{o, srun_obs(rest, m1)}) : List<&2, Bool> & List<&2, E.Obs>}
53 %Equal.sym(List<&2, Bool> & List<&2, E.Obs>, S.run(rest, m1), (srun_state(rest, m1), srun_obs(rest, m1)), L.pair_eta(List<&2, Bool>, List<&2, E.Obs>, S.run(rest, m1))) : {S.cons_obs(o, _) == (srun_state(rest, m1), Con{o, srun_obs(rest, m1)}) : List<&2, Bool> & List<&2, E.Obs>}
54 {==}
55
56def RunOK(ops: List<&2, E.Op>, sh: ST.Sh, acc: List<&2, E.Obs>) -> Type:
57 Sigma<&1, &1, ST.Sh, sh2 => {B.run_acc(ops, (ST.real(sh), acc)) == (ST.real(sh2), List.reverse.go(&2, E.Obs, srun_obs(ops, ST.model(sh)), acc)) : B.Bitset & List<&2, E.Obs>} & ({ST.good(sh2) == True{} : Bool} & {ST.model(sh2) == srun_state(ops, ST.model(sh)) : List<&2, Bool>})>
58
59def ro_sh(-ops: List<&2, E.Op>, -sh: ST.Sh, -acc: List<&2, E.Obs>, r: RunOK(ops, sh, acc)) -> ST.Sh:
60 match r:
61 case Tuple{sh2, x}:
62 sh2
63
64def ro_run(-ops: List<&2, E.Op>, -sh: ST.Sh, -acc: List<&2, E.Obs>, r: RunOK(ops, sh, acc)) -> {B.run_acc(ops, (ST.real(sh), acc)) == (ST.real(ro_sh(ops, sh, acc, r)), List.reverse.go(&2, E.Obs, srun_obs(ops, ST.model(sh)), acc)) : B.Bitset & List<&2, E.Obs>}:
65 match r:
66 case Tuple{sh2, Tuple{e, x}}:
67 e
68
69def ro_good(-ops: List<&2, E.Op>, -sh: ST.Sh, -acc: List<&2, E.Obs>, r: RunOK(ops, sh, acc)) -> {ST.good(ro_sh(ops, sh, acc, r)) == True{} : Bool}:
70 match r:
71 case Tuple{sh2, Tuple{e, Tuple{g, m}}}:
72 g
73
74def ro_model(-ops: List<&2, E.Op>, -sh: ST.Sh, -acc: List<&2, E.Obs>, r: RunOK(ops, sh, acc)) -> {ST.model(ro_sh(ops, sh, acc, r)) == srun_state(ops, ST.model(sh)) : List<&2, Bool>}:
75 match r:
76 case Tuple{sh2, Tuple{e, Tuple{g, m}}}:
77 m
78
79def run_ok(+ops: List<&2, E.Op>, +sh: ST.Sh, +acc: List<&2, E.Obs>, +g: {ST.good(sh) == True{} : Bool}) -> RunOK(ops, sh, acc):
80 match ops:
81 case Nil{}:
82 (sh, ({==}, (g, {==})))
83 case Con{+op, +rest}:
84 +m = ST.model(sh)
85 +sh1 = so_sh(sh, op, BS.step_ok(sh, op, g))
86 +o = so_obs(sh, op, BS.step_ok(sh, op, g))
87 +g1 = so_good(sh, op, BS.step_ok(sh, op, g))
88 +m1 = ST.model(sh1)
89 +acc1 = {Con{o, acc} : List<&2, E.Obs>}
90 +sh2 = ro_sh(rest, sh1, acc1, run_ok(rest, sh1, acc1, g1))
91 +es = spec_run_cons(op, rest, m, m1, o, so_spec(sh, op, BS.step_ok(sh, op, g)))
92 -R = S.run(rest, m1)
93 (sh2, (
94 %Equal.sym(B.Bitset & E.Obs, B.step(ST.real(sh), op), (ST.real(sh1), o), so_step(sh, op, BS.step_ok(sh, op, g))) : {B.run_acc(rest, B.record(acc, _)) == (ST.real(sh2), List.reverse.go(&2, E.Obs, srun_obs(Con{op, rest}, m), acc)) : B.Bitset & List<&2, E.Obs>}
95 %Equal.sym(B.Bitset & List<&2, E.Obs>, B.run_acc(rest, (ST.real(sh1), acc1)), (ST.real(sh2), List.reverse.go(&2, E.Obs, srun_obs(rest, m1), acc1)), ro_run(rest, sh1, acc1, run_ok(rest, sh1, acc1, g1))) : {_ == (ST.real(sh2), List.reverse.go(&2, E.Obs, srun_obs(Con{op, rest}, m), acc)) : B.Bitset & List<&2, E.Obs>}
96 %Equal.sym(List<&2, Bool> & List<&2, E.Obs>, S.run(Con{op, rest}, m), (Pair.fst(List<&2, Bool>, List<&2, E.Obs>, R), Con{o, Pair.snd(List<&2, Bool>, List<&2, E.Obs>, R)}), es) : {(ST.real(sh2), List.reverse.go(&2, E.Obs, srun_obs(rest, m1), acc1)) == (ST.real(sh2), List.reverse.go(&2, E.Obs, Pair.snd(List<&2, Bool>, List<&2, E.Obs>, _), acc)) : B.Bitset & List<&2, E.Obs>}
97 {==},
98 (ro_good(rest, sh1, acc1, run_ok(rest, sh1, acc1, g1)),
99 %Equal.sym(List<&2, Bool> & List<&2, E.Obs>, S.run(Con{op, rest}, m), (Pair.fst(List<&2, Bool>, List<&2, E.Obs>, R), Con{o, Pair.snd(List<&2, Bool>, List<&2, E.Obs>, R)}), es) : {ST.model(sh2) == Pair.fst(List<&2, Bool>, List<&2, E.Obs>, _) : List<&2, Bool>}
100 ro_model(rest, sh1, acc1, run_ok(rest, sh1, acc1, g1)))))
101
102# The finished run: B.run reverses the accumulator, which is the spec's own
103# observation list.
104def run_from(+ops: List<&2, E.Op>, +sh0: ST.Sh, +g0: {ST.good(sh0) == True{} : Bool}) -> {B.run(ops, ST.real(sh0)) == (ST.real(ro_sh(ops, sh0, Nil{}, run_ok(ops, sh0, Nil{}, g0))), srun_obs(ops, ST.model(sh0))) : B.Bitset & List<&2, E.Obs>}:
105 +sh2 = ro_sh(ops, sh0, Nil{}, run_ok(ops, sh0, Nil{}, g0))
106 +os = srun_obs(ops, ST.model(sh0))
107 %Equal.sym(B.Bitset & List<&2, E.Obs>, B.run_acc(ops, (ST.real(sh0), Nil{})), (ST.real(sh2), List.reverse.go(&2, E.Obs, os, Nil{})), ro_run(ops, sh0, Nil{}, run_ok(ops, sh0, Nil{}, g0))) : {B.finish(_) == (ST.real(sh2), os) : B.Bitset & List<&2, E.Obs>}
108 %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(sh2), _) == (ST.real(sh2), os) : B.Bitset & List<&2, E.Obs>}
109 {==}
110
111def TraceOK(ops: List<&2, E.Op>, sh0: ST.Sh) -> Type:
112 Sigma<&1, &1, ST.Sh, sh2 => {B.run(ops, ST.real(sh0)) == (ST.real(sh2), srun_obs(ops, ST.model(sh0))) : B.Bitset & List<&2, E.Obs>} & ({ST.good(sh2) == True{} : Bool} & {ST.model(sh2) == srun_state(ops, ST.model(sh0)) : List<&2, Bool>})>
113
114def trace_from(+ops: List<&2, E.Op>, +sh0: ST.Sh, +g0: {ST.good(sh0) == True{} : Bool}) -> TraceOK(ops, sh0):
115 (ro_sh(ops, sh0, Nil{}, run_ok(ops, sh0, Nil{}, g0)),
116 (run_from(ops, sh0, g0),
117 (ro_good(ops, sh0, Nil{}, run_ok(ops, sh0, Nil{}, g0)),
118 ro_model(ops, sh0, Nil{}, run_ok(ops, sh0, Nil{}, g0)))))
119
120# ---- from the constructor ----
121
122def initial(+n: Nat) -> ST.Sh:
123 {ST.Sh{n, B.depth_for(n), A.trep(B.Wd, B.depth_for(n), B.W{0})} : ST.Sh}
124
125def new_real(+n: Nat) -> {B.new(n) == ST.real(initial(n)) : B.Bitset}:
126 ST.new_form(n)
127
128def new_good(+n: Nat, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> {ST.good(initial(n)) == True{} : Bool}:
129 ST.new_rep(n, h)
130
131def new_model(+n: Nat, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> {ST.model(initial(n)) == S.new(n) : List<&2, Bool>}:
132 ST.new_abs(n, h)