1	import Base
2	import ./model.bend as Model
3	import ./array.bend as ArrayCore
4	import ./LAWS.bend as Laws
5	import ./refinement.bend as Refinement
6	import ./frame.bend as Frame
7	import ./main.bend as Storage
8	import ./api.bend as Api
9	
10	def Laws.write_read(T, d, array, path, value, valid):
11	  Frame.write_read(T, d, array, path, value, valid)
12	
13	def Laws.update_frame(T, d, array, i, j, value, valid):
14	  Frame.update_frame(T, d, array, i, j, value, valid)
15	
16	def Laws.read_refines(T, d, array, path, valid):
17	  Frame.read_refines(T, d, array, path, valid)
18	
19	def Laws.read_retains(T, d, array, path, valid):
20	  Frame.read_retains(T, d, array, path, valid)
21	
22	def Laws.primitive_update_frame(T, d, array, i, other, value, valid):
23	  Frame.primitive_update_frame(T, d, array, i, other, value, valid)
24	
25	def Laws.path_self_same(d, path):
26	  Frame.path_self_same(d, path)
27	
28	def Laws.primitive_write_read(T, d, array, i, value, valid):
29	  Frame.primitive_write_read(T, d, array, i, value, valid)
30	
31	def Laws.new_too_large(n, value, over):
32	  Api.new_refused(U32.to_nat(n), value, U32.is_le(n, 1048576), Equal.sym(Bool, U32.is_le(n, 1048576), False{}, over),
33	    Api.positive_of(U32.to_nat(n), U32.to_nat(1048576), Api.over_nat(n, over)))
34	
35	def Laws.get_outside(storage, i, outside):
36	  match storage:
37	    case Storage.Empty{}:
38	      {==}
39	    case Storage.Owned{+d, +n, array, balanced, valid}:
40	      Api.get_checked_miss(d, n, array, i, Nat.is_lt(U32.to_nat(i), n), {==}, balanced, valid,
41	        Equal.sym(Bool, Nat.is_lt(U32.to_nat(i), n), False{}, outside))
42	
43	def Laws.set_outside(storage, i, value, outside):
44	  match storage:
45	    case Storage.Empty{}:
46	      {==}
47	    case Storage.Owned{+d, +n, array, balanced, valid}:
48	      %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, Storage.set_checked(d, n, array, i, value, Nat.is_lt(U32.to_nat(i), n), {==}, balanced, valid),
49	        (Storage.Owned{d, n, array, balanced, valid}, Fail{Storage.OutOfBounds{}}),
50	        Api.set_checked_miss(d, n, array, i, value, Nat.is_lt(U32.to_nat(i), n), {==}, balanced, valid,
51	          Equal.sym(Bool, Nat.is_lt(U32.to_nat(i), n), False{}, outside))) :
52	        {Laws.outcome(Result<&2, &2, Storage.Error, Unit>, _) == Fail{Storage.OutOfBounds{}} : Result<&2, &2, Storage.Error, Unit>}
53	      {==}
54	
55	def Laws.replay_size(n, value, ops, fits):
56	  Api.new_size(U32.to_nat(n), value, U32.is_le(n, 1048576), ops, Equal.sym(Bool, U32.is_le(n, 1048576), True{}, fits), Api.cap_from(n, fits))
57	
58	def Laws.replay_get(n, value, ops, j, fits, inside):
59	  Api.new_read(U32.to_nat(n), value, U32.is_le(n, 1048576), ops, j, Equal.sym(Bool, U32.is_le(n, 1048576), True{}, fits),
60	    Api.cap_from(n, fits), inside)
61	
62	def Laws.new_fits(n, value, fits):
63	  Api.new_fits(U32.to_nat(n), value, U32.is_le(n, 1048576), Equal.sym(Bool, U32.is_le(n, 1048576), True{}, fits), Api.cap_from(n, fits))
64	
65	def Laws.new_empty(value):
66	  {==}
67	
68	def Laws.replay_set(n, value, ops, j, w, fits, inside):
69	  Api.new_status(U32.to_nat(n), value, U32.is_le(n, 1048576), ops, j, w, Equal.sym(Bool, U32.is_le(n, 1048576), True{}, fits),
70	    Api.cap_from(n, fits), inside)