1	import Base
2	import ../shape/core.bend as Shape
3	import ./core.bend as Core
4	import ./observation.bend as Observation
5	import ./read_write_records.bend as Records
6	
7	law read_inside:
8	  for +shape: Shape.Shape
9	  for +fill: F32
10	  for +index: U32
11	  for inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
12	  Records.ReadInside<shape, fill, index>
13	
14	law read_outside:
15	  for +shape: Shape.Shape
16	  for +fill: F32
17	  for +index: U32
18	  for outside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}
19	  Records.ReadContract<shape, fill, index, 8>
20	
21	law write_inside:
22	  for +shape: Shape.Shape
23	  for +fill: F32
24	  for +index: U32
25	  for +value: F32
26	  for inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
27	  Records.WriteInside<shape, fill, index, value>
28	
29	law write_outside:
30	  for +shape: Shape.Shape
31	  for +fill: F32
32	  for +index: U32
33	  for +value: F32
34	  for outside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}
35	  Records.WriteOutside<shape, fill, index, value>
36	
37	law coordinate_inside:
38	  for +shape: Shape.Shape
39	  for +fill: F32
40	  for +coordinates: List<&2, U32>
41	  for +index: U32
42	  for +value: F32
43	  for located: {Observation.coordinate_index(shape, Shape.flatten_checked(shape, coordinates)) == Some{index} : Maybe<&2, U32>}
44	  for inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
45	  Records.CoordinateInside<shape, fill, coordinates, index, value>
46	
47	law dynamic_read_inside:
48	  for +shape: Shape.Shape
49	  for +fill: F32
50	  for +index: U32
51	  for inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
52	  {Observation.dynamic_point(shape, index, Core.new(shape, fill)) == Some{fill} : Maybe<&2, F32>}