1	import Base
2	import ./model.bend as Model
3	import ./array.bend as ArrayCore
4	import ./refinement.bend as Refinement
5	import ./main.bend as Storage
6	
7	law write_read:
8	  for -T: Data
9	  for +d: Nat
10	  for array: Array<T>
11	  for +path: Model.Path(d)
12	  for value: T
13	  for valid: Model.Balanced(T, d, array)
14	  {Model.observe(T, d, ArrayCore.write_path(T, d, array, path, value), path) == Some{value} : Maybe<&2, T>}
15	
16	law update_frame:
17	  for -T: Data
18	  for +d: Nat
19	  for array: Array<T>
20	  for +i: Model.Path(d)
21	  for +j: Model.Path(d)
22	  for +value: T
23	  for valid: Model.Balanced(T, d, array)
24	  {Model.observe(T, d, ArrayCore.write_path(T, d, array, i, value), j) == Model.select(T, Model.same(d, i, j), value, Model.observe(T, d, array, j)) : Maybe<&2, T>}
25	
26	law read_refines:
27	  for -T: Data
28	  for +d: Nat
29	  for array: Array<T>
30	  for +path: Model.Path(d)
31	  for valid: Model.Balanced(T, d, array)
32	  {ArrayCore.observation(T, d, array, path, ArrayCore.read_path(T, d, array, path, valid)) == Model.observe(T, d, array, path) : Maybe<&2, T>}
33	
34	law read_retains:
35	  for -T: Data
36	  for +d: Nat
37	  for array: Array<T>
38	  for +path: Model.Path(d)
39	  for valid: Model.Balanced(T, d, array)
40	  {ArrayCore.retained(T, d, array, path, ArrayCore.read_path(T, d, array, path, valid)) == array : Array<T>}
41	
42	law primitive_update_frame:
43	  for -T: Data
44	  for +d: Nat
45	  for array: Array<T>
46	  for +i: U32
47	  for +other: Model.Path(d)
48	  for +value: T
49	  for valid: Model.Balanced(T, d, array)
50	  {Model.observe(T, d, Array.set(T, array, i, value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, array, other)) : Maybe<&2, T>}
51	
52	law path_self_same:
53	  for +d: Nat
54	  for +path: Model.Path(d)
55	  {Model.same(d, path, path) == True{} : Bool}
56	
57	law primitive_write_read:
58	  for -T: Data
59	  for +d: Nat
60	  for array: Array<T>
61	  for +i: U32
62	  for +value: T
63	  for valid: Model.Balanced(T, d, array)
64	  {Model.observe(T, d, Array.set(T, array, i, value), Refinement.route(d, i)) == Some{value} : Maybe<&2, T>}
65	
66	def outcome(-A: Type, pair: Storage.Storage & A) -> A:
67	  (storage, result) = pair
68	  result
69	
70	def size(storage: Storage.Storage) -> Nat:
71	  outcome(Nat, Storage.length(storage))
72	
73	def owner(-A: Type, pair: Storage.Storage & A) -> Storage.Storage:
74	  (storage, result) = pair
75	  storage
76	
77	def read(storage: Storage.Storage, +i: U32) -> Result<&2, &2, Storage.Error, F32>:
78	  outcome(Result<&2, &2, Storage.Error, F32>, Storage.get(storage, i))
79	
80	def kept(storage: Storage.Storage, +i: U32) -> Storage.Storage:
81	  owner(Result<&2, &2, Storage.Error, F32>, Storage.get(storage, i))
82	
83	def written(storage: Storage.Storage, +i: U32, value: F32) -> Storage.Storage:
84	  owner(Result<&2, &2, Storage.Error, Unit>, Storage.set(storage, i, value))
85	
86	def status(storage: Storage.Storage, +i: U32, value: F32) -> Result<&2, &2, Storage.Error, Unit>:
87	  outcome(Result<&2, &2, Storage.Error, Unit>, Storage.set(storage, i, value))
88	
89	def created.of(result: Result<&2, &1, Storage.Error, Storage.Storage>) -> Storage.Storage:
90	  match result:
91	    case Fail{error}:
92	      Storage.Empty{}
93	    case Done{storage}:
94	      storage
95	
96	def created(+n: U32, value: F32) -> Storage.Storage:
97	  created.of(Storage.new(n, value))
98	
99	def refused.of(result: Result<&2, &1, Storage.Error, Storage.Storage>) -> Maybe<&2, Storage.Error>:
100	  match result:
101	    case Fail{error}:
102	      Some{error}
103	    case Done{storage}:
104	      None{}
105	
106	def refused(+n: U32, value: F32) -> Maybe<&2, Storage.Error>:
107	  refused.of(Storage.new(n, value))
108	
109	def first(storage: Storage.Storage) -> Storage.Storage:
110	  owner(Storage.Storage, Storage.clone(storage))
111	
112	def second(storage: Storage.Storage) -> Storage.Storage:
113	  outcome(Storage.Storage, Storage.clone(storage))
114	
115	type Op is Data:
116	  Write{index: U32, value: F32}
117	  Read{index: U32}
118	  First{}
119	  Second{}
120	  Length{}
121	
122	def step(storage: Storage.Storage, op: Op) -> Storage.Storage:
123	  match op:
124	    case Write{+i, value}:
125	      written(storage, i, value)
126	    case Read{+i}:
127	      kept(storage, i)
128	    case First{}:
129	      first(storage)
130	    case Second{}:
131	      second(storage)
132	    case Length{}:
133	      owner(Nat, Storage.length(storage))
134	
135	def replay(ops: List<&2, Op>, storage: Storage.Storage) -> Storage.Storage:
136	  match ops:
137	    case Nil{}:
138	      storage
139	    case op <> rest:
140	      replay(rest, step(storage, op))
141	
142	def latest(+n: Nat, op: Op, +j: U32, value: F32) -> F32:
143	  match op:
144	    case Write{+i, new}:
145	      Bool.pick(F32, Bool.and(Nat.is_lt(U32.to_nat(i), n), Nat.is_eq(U32.to_nat(i), U32.to_nat(j))), new, value)
146	    case Read{i}:
147	      value
148	    case First{}:
149	      value
150	    case Second{}:
151	      value
152	    case Length{}:
153	      value
154	
155	def expected(ops: List<&2, Op>, +n: Nat, +j: U32, value: F32) -> F32:
156	  match ops:
157	    case Nil{}:
158	      value
159	    case op <> rest:
160	      expected(rest, n, j, latest(n, op, j, value))
161	
162	law new_too_large:
163	  for +n: U32
164	  for value: F32
165	  for +over: {U32.is_le(n, 1048576) == False{} : Bool}
166	  {refused(n, value) == Some{Storage.TooLarge{}} : Maybe<&2, Storage.Error>}
167	
168	law new_fits:
169	  for +n: U32
170	  for value: F32
171	  for +fits: {U32.is_le(n, 1048576) == True{} : Bool}
172	  {refused(n, value) == None{} : Maybe<&2, Storage.Error>}
173	
174	law new_empty:
175	  for value: F32
176	  {Storage.new(0, value) == Done{Storage.Empty{}} : Result<&2, &1, Storage.Error, Storage.Storage>}
177	
178	law get_outside:
179	  for storage: Storage.Storage
180	  for +i: U32
181	  for outside: {Nat.is_lt(U32.to_nat(i), size(storage)) == False{} : Bool}
182	  {read(storage, i) == Fail{Storage.OutOfBounds{}} : Result<&2, &2, Storage.Error, F32>}
183	
184	law set_outside:
185	  for storage: Storage.Storage
186	  for +i: U32
187	  for value: F32
188	  for outside: {Nat.is_lt(U32.to_nat(i), size(storage)) == False{} : Bool}
189	  {status(storage, i, value) == Fail{Storage.OutOfBounds{}} : Result<&2, &2, Storage.Error, Unit>}
190	
191	law replay_size:
192	  for +n: U32
193	  for +value: F32
194	  for +ops: List<&2, Op>
195	  for +fits: {U32.is_le(n, 1048576) == True{} : Bool}
196	  {size(replay(ops, created(n, value))) == U32.to_nat(n) : Nat}
197	
198	law replay_get:
199	  for +n: U32
200	  for +value: F32
201	  for +ops: List<&2, Op>
202	  for +j: U32
203	  for +fits: {U32.is_le(n, 1048576) == True{} : Bool}
204	  for inside: {Nat.is_lt(U32.to_nat(j), U32.to_nat(n)) == True{} : Bool}
205	  {read(replay(ops, created(n, value)), j) == Done{expected(ops, U32.to_nat(n), j, value)} : Result<&2, &2, Storage.Error, F32>}
206	
207	law replay_set:
208	  for +n: U32
209	  for +value: F32
210	  for +ops: List<&2, Op>
211	  for +j: U32
212	  for +w: F32
213	  for +fits: {U32.is_le(n, 1048576) == True{} : Bool}
214	  for inside: {Nat.is_lt(U32.to_nat(j), U32.to_nat(n)) == True{} : Bool}
215	  {status(replay(ops, created(n, value)), j, w) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}