proofs/containers/dynamic_array/trace.bend
bend-collections-laws-containers@1.0.0.0 · 121 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/nat.bend as N
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
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/dynamic_array.bend as S
8import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as DA
9import bend-collections-laws-containers@1.0.0.0/src/containers/types/dynamic_array.bend as E
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/layout.bend as LY
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/state.bend as ST
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/steps.bend as SP
13
14# Arbitrary finite operation traces through DA.run.
15
16def so_sh(-T: Data, -sh: ST.Shadow<T>, -op: E.Op<T>, so: SP.StepOK(T, sh, op)) -> ST.Shadow<T>:
17 match so:
18 case Tuple{sh2, r}:
19 sh2
20
21def so_obs(-T: Data, -sh: ST.Shadow<T>, -op: E.Op<T>, so: SP.StepOK(T, sh, op)) -> E.Obs<T>:
22 match so:
23 case Tuple{sh2, Tuple{o, r}}:
24 o
25
26def so_step(-T: Data, -sh: ST.Shadow<T>, -op: E.Op<T>, so: SP.StepOK(T, sh, op)) -> {DA.step(T, ST.real(T, sh), op) == (ST.real(T, so_sh(T, sh, op, so)), so_obs(T, sh, op, so)) : DA.DynArray<&2, T> & E.Obs<T>}:
27 match so:
28 case Tuple{sh2, Tuple{o, Tuple{e, r}}}:
29 e
30
31def so_good(-T: Data, -sh: ST.Shadow<T>, -op: E.Op<T>, so: SP.StepOK(T, sh, op)) -> {ST.good(T, so_sh(T, sh, op, so)) == True{} : Bool}:
32 match so:
33 case Tuple{sh2, Tuple{o, Tuple{e, Tuple{g, s}}}}:
34 g
35
36def so_spec(-T: Data, -sh: ST.Shadow<T>, -op: E.Op<T>, so: SP.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) : S.Model<T> & E.Obs<T>}:
37 match so:
38 case Tuple{sh2, Tuple{o, Tuple{e, Tuple{g, s}}}}:
39 s
40
41def spec_run_cons(-T: Data, +op: E.Op<T>, +rest: List<&2, E.Op<T>>, +m: S.Model<T>, +m1: S.Model<T>, +o: E.Obs<T>, +e: {(m1, o) == S.step(T, m, op) : S.Model<T> & E.Obs<T>}) -> {S.run(T, Con{op, rest}, m) == (Pair.fst(S.Model<T>, List<&2, E.Obs<T>>, S.run(T, rest, m1)), Con{o, Pair.snd(S.Model<T>, List<&2, E.Obs<T>>, S.run(T, rest, m1))}) : S.Model<T> & List<&2, E.Obs<T>>}:
42 %e : {S.cons_obs(T, Pair.snd(S.Model<T>, E.Obs<T>, _), S.run(T, rest, Pair.fst(S.Model<T>, E.Obs<T>, _))) == (Pair.fst(S.Model<T>, List<&2, E.Obs<T>>, S.run(T, rest, m1)), Con{o, Pair.snd(S.Model<T>, List<&2, E.Obs<T>>, S.run(T, rest, m1))}) : S.Model<T> & List<&2, E.Obs<T>>}
43 %Equal.sym(S.Model<T> & List<&2, E.Obs<T>>, S.run(T, rest, m1), (Pair.fst(S.Model<T>, List<&2, E.Obs<T>>, S.run(T, rest, m1)), Pair.snd(S.Model<T>, List<&2, E.Obs<T>>, S.run(T, rest, m1))), L.pair_eta(S.Model<T>, List<&2, E.Obs<T>>, S.run(T, rest, m1))) : {S.cons_obs(T, o, _) == (Pair.fst(S.Model<T>, List<&2, E.Obs<T>>, S.run(T, rest, m1)), Con{o, Pair.snd(S.Model<T>, List<&2, E.Obs<T>>, S.run(T, rest, m1))}) : S.Model<T> & List<&2, E.Obs<T>>}
44 {==}
45
46def srun_obs(-T: Data, ops: List<&2, E.Op<T>>, m: S.Model<T>) -> List<&2, E.Obs<T>>:
47 Pair.snd(S.Model<T>, List<&2, E.Obs<T>>, S.run(T, ops, m))
48
49def srun_state(-T: Data, ops: List<&2, E.Op<T>>, m: S.Model<T>) -> S.Model<T>:
50 Pair.fst(S.Model<T>, List<&2, E.Obs<T>>, S.run(T, ops, m))
51
52# Running ops from the array of a good shadow, with any accumulator.
53def RunOK(-T: Data, ops: List<&2, E.Op<T>>, sh: ST.Shadow<T>, acc: List<&2, E.Obs<T>>) -> Type:
54 Sigma<&1, &1, ST.Shadow<T>, sh2 => {DA.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)) : DA.DynArray<&2, T> & List<&2, E.Obs<T>>} & ({ST.good(T, sh2) == True{} : Bool} & {ST.model(T, sh2) == srun_state(T, ops, ST.model(T, sh)) : S.Model<T>})>
55
56def 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>:
57 match r:
58 case Tuple{sh2, x}:
59 sh2
60
61def 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)) -> {DA.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)) : DA.DynArray<&2, T> & List<&2, E.Obs<T>>}:
62 match r:
63 case Tuple{sh2, Tuple{e, x}}:
64 e
65
66def ro_good(-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.good(T, ro_sh(T, ops, sh, acc, r)) == True{} : Bool}:
67 match r:
68 case Tuple{sh2, Tuple{e, Tuple{g, m}}}:
69 g
70
71def 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)) : S.Model<T>}:
72 match r:
73 case Tuple{sh2, Tuple{e, Tuple{g, m}}}:
74 m
75
76def run_ok(-T: Data, +ops: List<&2, E.Op<T>>, +sh: ST.Shadow<T>, +acc: List<&2, E.Obs<T>>, +g: {ST.good(T, sh) == True{} : Bool}) -> RunOK(T, ops, sh, acc):
77 match ops:
78 case Nil{}:
79 (sh, ({==}, (g, {==})))
80 case Con{+op, +rest}:
81 +m = ST.model(T, sh)
82 +sh1 = so_sh(T, sh, op, SP.step_ok(T, sh, op, g))
83 +o = so_obs(T, sh, op, SP.step_ok(T, sh, op, g))
84 +g1 = so_good(T, sh, op, SP.step_ok(T, sh, op, g))
85 +m1 = ST.model(T, sh1)
86 +acc1 = {Con{o, acc} : List<&2, E.Obs<T>>}
87 +sh2 = ro_sh(T, rest, sh1, acc1, run_ok(T, rest, sh1, acc1, g1))
88 +es = spec_run_cons(T, op, rest, m, m1, o, so_spec(T, sh, op, SP.step_ok(T, sh, op, g)))
89 -R = S.run(T, rest, m1)
90 (sh2, (
91 %Equal.sym(DA.DynArray<&2, T> & E.Obs<T>, DA.step(T, ST.real(T, sh), op), (ST.real(T, sh1), o), so_step(T, sh, op, SP.step_ok(T, sh, op, g))) : {DA.run_acc(T, rest, DA.record(T, acc, _)) == (ST.real(T, sh2), List.reverse.go(&2, E.Obs<T>, srun_obs(T, Con{op, rest}, m), acc)) : DA.DynArray<&2, T> & List<&2, E.Obs<T>>}
92 %Equal.sym(DA.DynArray<&2, T> & List<&2, E.Obs<T>>, DA.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, g1))) : {_ == (ST.real(T, sh2), List.reverse.go(&2, E.Obs<T>, srun_obs(T, Con{op, rest}, m), acc)) : DA.DynArray<&2, T> & List<&2, E.Obs<T>>}
93 %Equal.sym(S.Model<T> & List<&2, E.Obs<T>>, S.run(T, Con{op, rest}, m), (Pair.fst(S.Model<T>, List<&2, E.Obs<T>>, R), Con{o, Pair.snd(S.Model<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(S.Model<T>, List<&2, E.Obs<T>>, _), acc)) : DA.DynArray<&2, T> & List<&2, E.Obs<T>>}
94 {==},
95 (ro_good(T, rest, sh1, acc1, run_ok(T, rest, sh1, acc1, g1)),
96 %Equal.sym(S.Model<T> & List<&2, E.Obs<T>>, S.run(T, Con{op, rest}, m), (Pair.fst(S.Model<T>, List<&2, E.Obs<T>>, R), Con{o, Pair.snd(S.Model<T>, List<&2, E.Obs<T>>, R)}), es) : {ST.model(T, sh2) == Pair.fst(S.Model<T>, List<&2, E.Obs<T>>, _) : S.Model<T>}
97 ro_model(T, rest, sh1, acc1, run_ok(T, rest, sh1, acc1, g1)))))
98
99# ---- from the constructors ----
100
101def initial(-T: Data) -> ST.Shadow<T>:
102 ST.Sh{31n, 0n, 0n, AR.TLeaf{None{}}}
103
104def new_real(-T: Data) -> {DA.new(T) == ST.real(T, initial(T)) : DA.DynArray<&2, T>}:
105 {==}
106
107def new_good(-T: Data) -> {ST.good(T, initial(T)) == True{} : Bool}:
108 {==}
109
110def new_model(-T: Data) -> {ST.model(T, initial(T)) == S.new(T) : S.Model<T>}:
111 {==}
112
113def limited(-T: Data, +k: Nat) -> ST.Shadow<T>:
114 ST.Sh{DA.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, 0n, AR.TLeaf{None{}}}
115
116def clamp_case(+k: Nat, +b: Bool, +eb: {Nat.is_lt(k, 31n) == b : Bool}) -> {Nat.is_le(DA.clamp_limit(k, b), 31n) == True{} : Bool} & {DA.clamp_limit(k, b) == Nat.min(k, 31n) : Nat}:
117 match b:
118 case True{}:
119 (N.lt_le(k, 31n, eb), Equal.sym(Nat, Nat.min(k, 31n), k, N.min_left(k, 31n, eb)))
120 case False{}:
121 ({==}, Equal.sym(Nat, Nat.min(k, 31n), 31n, N.min_right(k, 31n, eb)))