1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/list.bend as LL
4	import ../../lib/nat.bend as N
5	import ../../lib/array.bend as AR
6	import ../../../spec/lib/common.bend as SC
7	import ../../../spec/containers/dynamic_array.bend as S
8	import ../../../src/containers/dynamic_array.bend as DA
9	import ../../../src/containers/types/dynamic_array.bend as E
10	import ./layout.bend as LY
11	import ./state.bend as ST
12	import ./steps.bend as SP
13	
14	# Arbitrary finite operation traces through DA.run.
15	
16	def 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	
21	def 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	
26	def 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	
31	def 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	
36	def 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	
41	def 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	
46	def 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	
49	def 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.
53	def 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	
56	def 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	
61	def 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	
66	def 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	
71	def 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	
76	def 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	
101	def initial(-T: Data) -> ST.Shadow<T>:
102	  ST.Sh{31n, 0n, 0n, AR.TLeaf{None{}}}
103	
104	def new_real(-T: Data) -> {DA.new(T) == ST.real(T, initial(T)) : DA.DynArray<&2, T>}:
105	  {==}
106	
107	def new_good(-T: Data) -> {ST.good(T, initial(T)) == True{} : Bool}:
108	  {==}
109	
110	def new_model(-T: Data) -> {ST.model(T, initial(T)) == S.new(T) : S.Model<T>}:
111	  {==}
112	
113	def 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	
116	def 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)))