1	import Base
2	import ../shape/core.bend as Shape
3	import ./core.bend as Core
4	import ./layout.bend as Layout
5	import ./transpose_spec.bend as Transpose
6	import ./transform_observation.bend as Observation
7	import ./transform_records.bend as Records
8	
9	law reshape_contract:
10	  for +input: Shape.Shape
11	  for +fill: F32
12	  for +target: Shape.Shape
13	  for same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}
14	  Records.ReshapeContract<input, fill, target>
15	
16	law reshape_write:
17	  for +input: Shape.Shape
18	  for +fill: F32
19	  for +target: Shape.Shape
20	  for +index: U32
21	  for +value: F32
22	  for inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(input))) == True{} : Bool}
23	  for same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}
24	  Records.ReshapeWrite<input, fill, target, index, value>
25	
26	law reshape_count_mismatch:
27	  for +input: Shape.Shape
28	  for +fill: F32
29	  for +target: Shape.Shape
30	  for different: {Nat.is_eq(Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target))) == False{} : Bool}
31	  {Observation.reshape_code(input, Shape.dimensions(target), Core.new(input, fill)) == Some{15} : Maybe<&2, U32>}
32	
33	law permute_rank_mismatch:
34	  for +input: Shape.Shape
35	  for +fill: F32
36	  for +axes: List<&2, U32>
37	  for wrong: {Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) == False{} : Bool}
38	  Records.RetainedFailure<input, fill, Observation.Permute{axes}, 12>
39	
40	law permute_axis_out_of_bounds:
41	  for +input: Shape.Shape
42	  for +fill: F32
43	  for +axes: List<&2, U32>
44	  for ranked: {Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) == True{} : Bool}
45	  for outside: {Layout.bounded(axes, Shape.rank(input)) == False{} : Bool}
46	  Records.RetainedFailure<input, fill, Observation.Permute{axes}, 13>
47	
48	law permute_duplicate_axis:
49	  for +input: Shape.Shape
50	  for +fill: F32
51	  for +axes: List<&2, U32>
52	  for ranked: {Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) == True{} : Bool}
53	  for bounded: {Layout.bounded(axes, Shape.rank(input)) == True{} : Bool}
54	  for duplicate: {Layout.unique(axes) == False{} : Bool}
55	  Records.RetainedFailure<input, fill, Observation.Permute{axes}, 14>
56	
57	law transpose_out_of_bounds:
58	  for +input: Shape.Shape
59	  for +fill: F32
60	  for +a: U32
61	  for +b: U32
62	  for outside: {Transpose.valid(input, a, b) == False{} : Bool}
63	  Records.RetainedFailure<input, fill, Observation.Transpose{a, b}, 13>