proofs/containers/deque/trace.bend
bend-collections-laws-containers@1.0.0.0 · 104 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/containers/deque.bend as S
5import bend-collections-laws-containers@1.0.0.0/src/containers/deque.bend as DQ
6import bend-collections-laws-containers@1.0.0.0/src/containers/types/deque.bend as E
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/state.bend as ST
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/stepok.bend as K
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/deque/steps.bend as PS
10
11# Arbitrary finite operation traces: the real runner refines the spec
12# runner. Running any list of operations on the deque of a shadow lands on
13# the deque of another shadow, emits exactly the spec runner's observations,
14# and the final shadow's model is the spec runner's final state. There is no
15# size or length premise.
16
17# ---- projections of a step ----
18
19def so_sh(~T: Data, -sh: ST.Shadow<T>, -op: E.Op<T>, so: K.StepOK(~T, sh, op)) -> ST.Shadow<T>:
20 match so:
21 case Tuple{sh2, r}:
22 sh2
23
24def so_obs(~T: Data, -sh: ST.Shadow<T>, -op: E.Op<T>, so: K.StepOK(~T, sh, op)) -> E.Obs<T>:
25 match so:
26 case Tuple{sh2, Tuple{o, r}}:
27 o
28
29def so_step(~T: Data, -sh: ST.Shadow<T>, -op: E.Op<T>, so: K.StepOK(~T, sh, op)) -> {DQ.step(~T, ST.real(T, sh), op) == (ST.real(T, so_sh(~T, sh, op, so)), so_obs(~T, sh, op, so)) : DQ.Deque<T> & E.Obs<T>}:
30 match so:
31 case Tuple{sh2, Tuple{o, Tuple{e, s}}}:
32 e
33
34def so_spec(~T: Data, -sh: ST.Shadow<T>, -op: E.Op<T>, so: K.StepOK(~T, sh, op)) -> {(ST.model(T, so_sh(~T, sh, op, so)), so_obs(~T, sh, op, so)) == S.step(T, ST.model(T, sh), op) : List<&2, T> & E.Obs<T>}:
35 match so:
36 case Tuple{sh2, Tuple{o, Tuple{e, s}}}:
37 s
38
39# ---- the run ----
40
41def srun_obs(-T: Data, ops: List<&2, E.Op<T>>, m: List<&2, T>) -> List<&2, E.Obs<T>>:
42 Pair.snd(List<&2, T>, List<&2, E.Obs<T>>, S.run(T, ops, m))
43
44def srun_state(-T: Data, ops: List<&2, E.Op<T>>, m: List<&2, T>) -> List<&2, T>:
45 Pair.fst(List<&2, T>, List<&2, E.Obs<T>>, S.run(T, ops, m))
46
47def spec_run_cons(-T: Data, +op: E.Op<T>, +rest: List<&2, E.Op<T>>, +m: List<&2, T>, +m1: List<&2, T>, +o: E.Obs<T>, +e: {(m1, o) == S.step(T, m, op) : List<&2, T> & E.Obs<T>}) -> {S.run(T, Con{op, rest}, m) == (srun_state(T, rest, m1), Con{o, srun_obs(T, rest, m1)}) : List<&2, T> & List<&2, E.Obs<T>>}:
48 %e : {S.cons_obs(T, Pair.snd(List<&2, T>, E.Obs<T>, _), S.run(T, rest, Pair.fst(List<&2, T>, E.Obs<T>, _))) == (srun_state(T, rest, m1), Con{o, srun_obs(T, rest, m1)}) : List<&2, T> & List<&2, E.Obs<T>>}
49 %Equal.sym(List<&2, T> & List<&2, E.Obs<T>>, S.run(T, rest, m1), (srun_state(T, rest, m1), srun_obs(T, rest, m1)), L.pair_eta(List<&2, T>, List<&2, E.Obs<T>>, S.run(T, rest, m1))) : {S.cons_obs(T, o, _) == (srun_state(T, rest, m1), Con{o, srun_obs(T, rest, m1)}) : List<&2, T> & List<&2, E.Obs<T>>}
50 {==}
51
52def RunOK(~T: Data, ops: List<&2, E.Op<T>>, sh: ST.Shadow<T>, acc: List<&2, E.Obs<T>>) -> Type:
53 Sigma<&1, &1, ST.Shadow<T>, sh2 => {DQ.run_acc(~T, ops, (ST.real(T, sh), acc)) == (ST.real(T, sh2), List.reverse.go(&2, E.Obs<T>, srun_obs(T, ops, ST.model(T, sh)), acc)) : DQ.Deque<T> & List<&2, E.Obs<T>>} & {ST.model(T, sh2) == srun_state(T, ops, ST.model(T, sh)) : List<&2, T>}>
54
55def ro_sh(~T: Data, -ops: List<&2, E.Op<T>>, -sh: ST.Shadow<T>, -acc: List<&2, E.Obs<T>>, r: RunOK(~T, ops, sh, acc)) -> ST.Shadow<T>:
56 match r:
57 case Tuple{sh2, x}:
58 sh2
59
60def ro_run(~T: Data, -ops: List<&2, E.Op<T>>, -sh: ST.Shadow<T>, -acc: List<&2, E.Obs<T>>, r: RunOK(~T, ops, sh, acc)) -> {DQ.run_acc(~T, ops, (ST.real(T, sh), acc)) == (ST.real(T, ro_sh(~T, ops, sh, acc, r)), List.reverse.go(&2, E.Obs<T>, srun_obs(T, ops, ST.model(T, sh)), acc)) : DQ.Deque<T> & List<&2, E.Obs<T>>}:
61 match r:
62 case Tuple{sh2, Tuple{e, m}}:
63 e
64
65def ro_model(~T: Data, -ops: List<&2, E.Op<T>>, -sh: ST.Shadow<T>, -acc: List<&2, E.Obs<T>>, r: RunOK(~T, ops, sh, acc)) -> {ST.model(T, ro_sh(~T, ops, sh, acc, r)) == srun_state(T, ops, ST.model(T, sh)) : List<&2, T>}:
66 match r:
67 case Tuple{sh2, Tuple{e, m}}:
68 m
69
70def run_ok(~T: Data, +ops: List<&2, E.Op<T>>, +sh: ST.Shadow<T>, +acc: List<&2, E.Obs<T>>) -> RunOK(~T, ops, sh, acc):
71 match ops:
72 case Nil{}:
73 (sh, ({==}, {==}))
74 case Con{+op, +rest}:
75 +m = ST.model(T, sh)
76 +sh1 = so_sh(~T, sh, op, PS.step_ok(~T, sh, op))
77 +o = so_obs(~T, sh, op, PS.step_ok(~T, sh, op))
78 +m1 = ST.model(T, sh1)
79 +acc1 = {Con{o, acc} : List<&2, E.Obs<T>>}
80 +sh2 = ro_sh(~T, rest, sh1, acc1, run_ok(~T, rest, sh1, acc1))
81 +es = spec_run_cons(T, op, rest, m, m1, o, so_spec(~T, sh, op, PS.step_ok(~T, sh, op)))
82 -R = S.run(T, rest, m1)
83 (sh2, (
84 %Equal.sym(DQ.Deque<T> & E.Obs<T>, DQ.step(~T, ST.real(T, sh), op), (ST.real(T, sh1), o), so_step(~T, sh, op, PS.step_ok(~T, sh, op))) : {DQ.run_acc(~T, rest, DQ.record(~T, acc, _)) == (ST.real(T, sh2), List.reverse.go(&2, E.Obs<T>, srun_obs(T, Con{op, rest}, m), acc)) : DQ.Deque<T> & List<&2, E.Obs<T>>}
85 %Equal.sym(DQ.Deque<T> & List<&2, E.Obs<T>>, DQ.run_acc(~T, rest, (ST.real(T, sh1), acc1)), (ST.real(T, sh2), List.reverse.go(&2, E.Obs<T>, srun_obs(T, rest, m1), acc1)), ro_run(~T, rest, sh1, acc1, run_ok(~T, rest, sh1, acc1))) : {_ == (ST.real(T, sh2), List.reverse.go(&2, E.Obs<T>, srun_obs(T, Con{op, rest}, m), acc)) : DQ.Deque<T> & List<&2, E.Obs<T>>}
86 %Equal.sym(List<&2, T> & List<&2, E.Obs<T>>, S.run(T, Con{op, rest}, m), (Pair.fst(List<&2, T>, List<&2, E.Obs<T>>, R), Con{o, Pair.snd(List<&2, T>, List<&2, E.Obs<T>>, R)}), es) : {(ST.real(T, sh2), List.reverse.go(&2, E.Obs<T>, srun_obs(T, rest, m1), acc1)) == (ST.real(T, sh2), List.reverse.go(&2, E.Obs<T>, Pair.snd(List<&2, T>, List<&2, E.Obs<T>>, _), acc)) : DQ.Deque<T> & List<&2, E.Obs<T>>}
87 {==},
88 %Equal.sym(List<&2, T> & List<&2, E.Obs<T>>, S.run(T, Con{op, rest}, m), (Pair.fst(List<&2, T>, List<&2, E.Obs<T>>, R), Con{o, Pair.snd(List<&2, T>, List<&2, E.Obs<T>>, R)}), es) : {ST.model(T, sh2) == Pair.fst(List<&2, T>, List<&2, E.Obs<T>>, _) : List<&2, T>}
89 ro_model(~T, rest, sh1, acc1, run_ok(~T, rest, sh1, acc1))))
90
91def run_from(~T: Data, +ops: List<&2, E.Op<T>>, +sh0: ST.Shadow<T>) -> {DQ.run(~T, ops, ST.real(T, sh0)) == (ST.real(T, ro_sh(~T, ops, sh0, Nil{}, run_ok(~T, ops, sh0, Nil{}))), srun_obs(T, ops, ST.model(T, sh0))) : DQ.Deque<T> & List<&2, E.Obs<T>>}:
92 +sh2 = ro_sh(~T, ops, sh0, Nil{}, run_ok(~T, ops, sh0, Nil{}))
93 +os = srun_obs(T, ops, ST.model(T, sh0))
94 %Equal.sym(DQ.Deque<T> & List<&2, E.Obs<T>>, DQ.run_acc(~T, ops, (ST.real(T, sh0), Nil{})), (ST.real(T, sh2), List.reverse.go(&2, E.Obs<T>, os, Nil{})), ro_run(~T, ops, sh0, Nil{}, run_ok(~T, ops, sh0, Nil{}))) : {DQ.finish(~T, _) == (ST.real(T, sh2), os) : DQ.Deque<T> & List<&2, E.Obs<T>>}
95 %Equal.sym(List<&2, E.Obs<T>>, List.reverse(&2, E.Obs<T>, List.reverse.go(&2, E.Obs<T>, os, Nil{})), os, LL.rev_rev(E.Obs<T>, os)) : {(ST.real(T, sh2), _) == (ST.real(T, sh2), os) : DQ.Deque<T> & List<&2, E.Obs<T>>}
96 {==}
97
98def TraceOK(~T: Data, ops: List<&2, E.Op<T>>, sh0: ST.Shadow<T>) -> Type:
99 Sigma<&1, &1, ST.Shadow<T>, sh2 => {DQ.run(~T, ops, ST.real(T, sh0)) == (ST.real(T, sh2), srun_obs(T, ops, ST.model(T, sh0))) : DQ.Deque<T> & List<&2, E.Obs<T>>} & {ST.model(T, sh2) == srun_state(T, ops, ST.model(T, sh0)) : List<&2, T>}>
100
101def trace_from(~T: Data, +ops: List<&2, E.Op<T>>, +sh0: ST.Shadow<T>) -> TraceOK(~T, ops, sh0):
102 (ro_sh(~T, ops, sh0, Nil{}, run_ok(~T, ops, sh0, Nil{})),
103 (run_from(~T, ops, sh0),
104 ro_model(~T, ops, sh0, Nil{}, run_ok(~T, ops, sh0, Nil{}))))