1	import Base
2	import ../shape/core.bend as Shape
3	import ../shape/LAWS.bend as ShapeLaws
4	import ../shape/PROOF.bend as ShapeProof
5	import ../shape/nat_proofs.bend as Nats
6	import ../storage/main.bend as Storage
7	import ../storage/LAWS.bend as StorageLaws
8	import ../storage/PROOF.bend as StorageProof
9	import ../storage/arith.bend as Arith
10	import ./core.bend as Core
11	import ./lifecycle.bend as Lifecycle
12	import ./layout.bend as Layout
13	import ./transpose_spec.bend as Transpose
14	import ./transforms.bend as Transforms
15	import ./allocation_PROOF.bend as AllocationProof
16	import ./word_conversion.bend as Conversion
17	import ./read_contract.bend as Reads
18	import ./transform_observation.bend as Observation
19	import ./transform_records.bend as Laws
20	
21	def retained_code(+input: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill)) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +request: Observation.Request, +error: Transforms.Error,
22	  failed: {Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request) == (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}) ->
23	  {Observation.failure_code(input, request, Done{Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}}) == Some{Transforms.error_code(error)} : Maybe<&2, U32>}:
24	  Equal.cong(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, Maybe<&2, U32>, pair => Some{Observation.failure_code_pair(input, pair)},
25	    Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request), (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}), failed)
26	
27	def retained_dimensions(+input: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill)) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +request: Observation.Request, +error: Transforms.Error,
28	  failed: {Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request) == (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}) ->
29	  {Observation.kept_dimensions(input, request, Done{Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}}) == Some{Shape.dimensions(input)} : Maybe<&2, List<&2, U32>>}:
30	  Equal.cong(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, Maybe<&2, List<&2, U32>>, pair => Observation.kept_dimensions_pair(input, pair),
31	    Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request), (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}), failed)
32	
33	def retained_length(+input: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill)) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +request: Observation.Request, +error: Transforms.Error,
34	  failed: {Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request) == (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}) ->
35	  {Observation.kept_length(input, request, Done{Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}}) == Some{Shape.logical_numel(Shape.dimensions(input))} : Maybe<&2, Nat>}:
36	  Equal.trans(Maybe<&2, Nat>, Some{Observation.kept_length_pair(input, Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request))},
37	    Some{Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill))}, Some{Shape.logical_numel(Shape.dimensions(input))},
38	    Equal.cong(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, Maybe<&2, Nat>, pair => Some{Observation.kept_length_pair(input, pair)},
39	      Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request), (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}), failed),
40	    Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number}, Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill)), Shape.logical_numel(Shape.dimensions(input)), Reads.created_exact(input, fill)))
41	
42	def retained_count(+input: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill)) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +request: Observation.Request, +error: Transforms.Error,
43	  failed: {Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request) == (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}) ->
44	  {Observation.kept_count(input, request, Done{Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}}) == Some{Shape.count(input)} : Maybe<&2, U32>}:
45	  Equal.cong(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, Maybe<&2, U32>, pair => Observation.kept_count_pair(input, pair),
46	    Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request), (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}), failed)
47	
48	def retained_value(+input: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill)) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +request: Observation.Request, +error: Transforms.Error, +other: U32,
49	  inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(input))) == True{} : Bool}, failed: {Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request) == (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}) ->
50	  {Observation.kept_value(input, request, other, Done{Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}}) == Some{fill} : Maybe<&2, F32>}:
51	  Equal.trans(Maybe<&2, F32>, Observation.kept_value_pair(input, other, Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request)),
52	    Observation.kept_value_pair(input, other, (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error})), Some{fill},
53	    Equal.cong(Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, Maybe<&2, F32>, pair => Observation.kept_value_pair(input, other, pair),
54	      Observation.apply(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, request), (Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Fail{error}), failed),
55	    Reads.read_point_done(input, fill, valid, other, inside))
56	
57	def ranked_failure(+input: Shape.Shape, +axes: List<&2, U32>,
58	  decision: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))>,
59	  wrong: {Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) == False{} : Bool}) ->
60	  {Layout.plan_ranked(input, axes, decision) == Fail{Layout.AxesLengthMismatch{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
61	  match decision:
62	    case Shape.BFalse{no}:
63	      {==}
64	    case Shape.BTrue{yes}:
65	      Empty.absurd({Layout.plan_ranked(input, axes, Shape.BTrue{yes}) == Fail{Layout.AxesLengthMismatch{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
66	        Nats.contradiction(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), yes,
67	          Equal.sym(Bool, Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), False{}, wrong)))
68	
69	def ranked_pass(+input: Shape.Shape, +axes: List<&2, U32>,
70	  decision: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))>,
71	  ranked: {Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) == True{} : Bool}) ->
72	  {Layout.plan_ranked(input, axes, decision) == Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))) : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
73	  match decision:
74	    case Shape.BFalse{no}:
75	      Empty.absurd({Layout.plan_ranked(input, axes, Shape.BFalse{no}) == Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))) : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
76	        Nats.contradiction(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))),
77	          Equal.sym(Bool, Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))), True{}, ranked), no))
78	    case Shape.BTrue{yes}:
79	      {==}
80	
81	def bounded_failure(+input: Shape.Shape, +axes: List<&2, U32>, decision: Shape.BoolCase<Layout.bounded(axes, Shape.rank(input))>,
82	  outside: {Layout.bounded(axes, Shape.rank(input)) == False{} : Bool}) ->
83	  {Layout.plan_bounded(input, axes, decision) == Fail{Layout.AxisOutOfBounds{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
84	  match decision:
85	    case Shape.BFalse{no}:
86	      {==}
87	    case Shape.BTrue{yes}:
88	      Empty.absurd({Layout.plan_bounded(input, axes, Shape.BTrue{yes}) == Fail{Layout.AxisOutOfBounds{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
89	        Nats.contradiction(Layout.bounded(axes, Shape.rank(input)), yes, Equal.sym(Bool, Layout.bounded(axes, Shape.rank(input)), False{}, outside)))
90	
91	def bounded_pass(+input: Shape.Shape, +axes: List<&2, U32>, decision: Shape.BoolCase<Layout.bounded(axes, Shape.rank(input))>,
92	  bounded: {Layout.bounded(axes, Shape.rank(input)) == True{} : Bool}) ->
93	  {Layout.plan_bounded(input, axes, decision) == Layout.plan_unique(input, axes, Shape.bool_case(Layout.unique(axes))) : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
94	  match decision:
95	    case Shape.BFalse{no}:
96	      Empty.absurd({Layout.plan_bounded(input, axes, Shape.BFalse{no}) == Layout.plan_unique(input, axes, Shape.bool_case(Layout.unique(axes))) : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
97	        Nats.contradiction(Layout.bounded(axes, Shape.rank(input)), Equal.sym(Bool, Layout.bounded(axes, Shape.rank(input)), True{}, bounded), no))
98	    case Shape.BTrue{yes}:
99	      {==}
100	
101	def unique_failure(+input: Shape.Shape, +axes: List<&2, U32>, decision: Shape.BoolCase<Layout.unique(axes)>,
102	  duplicate: {Layout.unique(axes) == False{} : Bool}) ->
103	  {Layout.plan_unique(input, axes, decision) == Fail{Layout.DuplicateAxis{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}:
104	  match decision:
105	    case Shape.BFalse{no}:
106	      {==}
107	    case Shape.BTrue{yes}:
108	      Empty.absurd({Layout.plan_unique(input, axes, Shape.BTrue{yes}) == Fail{Layout.DuplicateAxis{}} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>},
109	        Nats.contradiction(Layout.unique(axes), yes, Equal.sym(Bool, Layout.unique(axes), False{}, duplicate)))
110	
111	def planned_failure(+input: Shape.Shape, -tensor: Core.Tensor<input>, +axes: List<&2, U32>, -error: Layout.Error,
112	  planned: {Layout.permutation(input, axes) == Fail{error} : Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>}) ->
113	  {Observation.apply(input, tensor, Observation.Permute{axes}) == (tensor, Fail{Transforms.LayoutError{error}}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}:
114	  Equal.cong(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>, result => Transforms.copy_planned(input, axes, tensor, result),
115	    Layout.permutation(input, axes), Fail{error}, planned)
116	
117	def transpose_failure(+input: Shape.Shape, -tensor: Core.Tensor<input>, +a: U32, +b: U32,
118	  decision: Shape.BoolCase<Transpose.valid(input, a, b)>, outside: {Transpose.valid(input, a, b) == False{} : Bool}) ->
119	  {Transforms.transpose_decided(input, tensor, a, b, decision) == (tensor, Fail{Transforms.LayoutError{Layout.AxisOutOfBounds{}}}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>}:
120	  match decision:
121	    case Shape.BFalse{no}:
122	      {==}
123	    case Shape.BTrue{yes}:
124	      Empty.absurd({Transforms.transpose_decided(input, tensor, a, b, Shape.BTrue{yes}) == (tensor, Fail{Transforms.LayoutError{Layout.AxisOutOfBounds{}}}) : Core.Tensor<input> & Result<&2, &1, Transforms.Error, Core.Dynamic>},
125	        Nats.contradiction(Transpose.valid(input, a, b), yes, Equal.sym(Bool, Transpose.valid(input, a, b), False{}, outside)))
126	
127	def permute_rank_mismatch(+input: Shape.Shape, +fill: F32, +axes: List<&2, U32>, wrong: {Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) == False{} : Bool}) -> Laws.RetainedFailure<input, fill, Observation.Permute{axes}, 12>:
128	  +wrong = wrong
129	  Laws.RetainedFailure{
130	    Reads.new_lift(input, fill, result => {Observation.failure_code(input, Observation.Permute{axes}, result) == Some{12} : Maybe<&2, U32>},
131	      valid => retained_code(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxesLengthMismatch{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxesLengthMismatch{}, ranked_failure(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), wrong)))),
132	    Reads.new_lift(input, fill, result => {Observation.kept_dimensions(input, Observation.Permute{axes}, result) == Some{Shape.dimensions(input)} : Maybe<&2, List<&2, U32>>},
133	      valid => retained_dimensions(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxesLengthMismatch{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxesLengthMismatch{}, ranked_failure(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), wrong)))),
134	    Reads.new_lift(input, fill, result => {Observation.kept_length(input, Observation.Permute{axes}, result) == Some{Shape.logical_numel(Shape.dimensions(input))} : Maybe<&2, Nat>},
135	      valid => retained_length(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxesLengthMismatch{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxesLengthMismatch{}, ranked_failure(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), wrong)))),
136	    Reads.new_lift(input, fill, result => {Observation.kept_count(input, Observation.Permute{axes}, result) == Some{Shape.count(input)} : Maybe<&2, U32>},
137	      valid => retained_count(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxesLengthMismatch{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxesLengthMismatch{}, ranked_failure(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), wrong)))),
138	    other => inside => Reads.new_lift(input, fill, result => {Observation.kept_value(input, Observation.Permute{axes}, other, result) == Some{fill} : Maybe<&2, F32>},
139	      valid => retained_value(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxesLengthMismatch{}}, other, inside, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxesLengthMismatch{}, ranked_failure(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), wrong))))}
140	
141	def permute_axis_out_of_bounds(+input: Shape.Shape, +fill: F32, +axes: List<&2, U32>, ranked: {Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) == True{} : Bool},
142	  outside: {Layout.bounded(axes, Shape.rank(input)) == False{} : Bool}) -> Laws.RetainedFailure<input, fill, Observation.Permute{axes}, 13>:
143	  +ranked = ranked
144	  +outside = outside
145	  Laws.RetainedFailure{
146	    Reads.new_lift(input, fill, result => {Observation.failure_code(input, Observation.Permute{axes}, result) == Some{13} : Maybe<&2, U32>},
147	      valid => retained_code(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxisOutOfBounds{},
148	        Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
149	          Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.AxisOutOfBounds{}},
150	          ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
151	          bounded_failure(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), outside))))),
152	    Reads.new_lift(input, fill, result => {Observation.kept_dimensions(input, Observation.Permute{axes}, result) == Some{Shape.dimensions(input)} : Maybe<&2, List<&2, U32>>},
153	      valid => retained_dimensions(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxisOutOfBounds{},
154	        Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
155	          Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.AxisOutOfBounds{}},
156	          ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
157	          bounded_failure(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), outside))))),
158	    Reads.new_lift(input, fill, result => {Observation.kept_length(input, Observation.Permute{axes}, result) == Some{Shape.logical_numel(Shape.dimensions(input))} : Maybe<&2, Nat>},
159	      valid => retained_length(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxisOutOfBounds{},
160	        Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
161	          Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.AxisOutOfBounds{}},
162	          ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
163	          bounded_failure(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), outside))))),
164	    Reads.new_lift(input, fill, result => {Observation.kept_count(input, Observation.Permute{axes}, result) == Some{Shape.count(input)} : Maybe<&2, U32>},
165	      valid => retained_count(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxisOutOfBounds{},
166	        Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
167	          Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.AxisOutOfBounds{}},
168	          ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
169	          bounded_failure(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), outside))))),
170	    other => inside => Reads.new_lift(input, fill, result => {Observation.kept_value(input, Observation.Permute{axes}, other, result) == Some{fill} : Maybe<&2, F32>},
171	      valid => retained_value(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, other, inside, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.AxisOutOfBounds{},
172	        Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
173	          Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.AxisOutOfBounds{}},
174	          ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
175	          bounded_failure(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), outside)))))}
176	
177	def permute_duplicate_axis(+input: Shape.Shape, +fill: F32, +axes: List<&2, U32>, ranked: {Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input))) == True{} : Bool},
178	  bounded: {Layout.bounded(axes, Shape.rank(input)) == True{} : Bool}, duplicate: {Layout.unique(axes) == False{} : Bool}) -> Laws.RetainedFailure<input, fill, Observation.Permute{axes}, 14>:
179	  +ranked = ranked
180	  +bounded = bounded
181	  +duplicate = duplicate
182	  Laws.RetainedFailure{
183	    Reads.new_lift(input, fill, result => {Observation.failure_code(input, Observation.Permute{axes}, result) == Some{14} : Maybe<&2, U32>},
184	      valid => retained_code(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.DuplicateAxis{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.DuplicateAxis{},
185	        Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
186	          Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.DuplicateAxis{}},
187	          ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
188	          Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))),
189	            Layout.plan_unique(input, axes, Shape.bool_case(Layout.unique(axes))), Fail{Layout.DuplicateAxis{}},
190	            bounded_pass(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), bounded),
191	            unique_failure(input, axes, Shape.bool_case(Layout.unique(axes)), duplicate)))))),
192	    Reads.new_lift(input, fill, result => {Observation.kept_dimensions(input, Observation.Permute{axes}, result) == Some{Shape.dimensions(input)} : Maybe<&2, List<&2, U32>>},
193	      valid => retained_dimensions(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.DuplicateAxis{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.DuplicateAxis{},
194	        Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
195	          Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.DuplicateAxis{}},
196	          ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
197	          Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))),
198	            Layout.plan_unique(input, axes, Shape.bool_case(Layout.unique(axes))), Fail{Layout.DuplicateAxis{}},
199	            bounded_pass(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), bounded),
200	            unique_failure(input, axes, Shape.bool_case(Layout.unique(axes)), duplicate)))))),
201	    Reads.new_lift(input, fill, result => {Observation.kept_length(input, Observation.Permute{axes}, result) == Some{Shape.logical_numel(Shape.dimensions(input))} : Maybe<&2, Nat>},
202	      valid => retained_length(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.DuplicateAxis{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.DuplicateAxis{},
203	        Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
204	          Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.DuplicateAxis{}},
205	          ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
206	          Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))),
207	            Layout.plan_unique(input, axes, Shape.bool_case(Layout.unique(axes))), Fail{Layout.DuplicateAxis{}},
208	            bounded_pass(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), bounded),
209	            unique_failure(input, axes, Shape.bool_case(Layout.unique(axes)), duplicate)))))),
210	    Reads.new_lift(input, fill, result => {Observation.kept_count(input, Observation.Permute{axes}, result) == Some{Shape.count(input)} : Maybe<&2, U32>},
211	      valid => retained_count(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.DuplicateAxis{}}, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.DuplicateAxis{},
212	        Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
213	          Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.DuplicateAxis{}},
214	          ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
215	          Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))),
216	            Layout.plan_unique(input, axes, Shape.bool_case(Layout.unique(axes))), Fail{Layout.DuplicateAxis{}},
217	            bounded_pass(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), bounded),
218	            unique_failure(input, axes, Shape.bool_case(Layout.unique(axes)), duplicate)))))),
219	    other => inside => Reads.new_lift(input, fill, result => {Observation.kept_value(input, Observation.Permute{axes}, other, result) == Some{fill} : Maybe<&2, F32>},
220	      valid => retained_value(input, fill, valid, Observation.Permute{axes}, Transforms.LayoutError{Layout.DuplicateAxis{}}, other, inside, planned_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, axes, Layout.DuplicateAxis{},
221	        Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.permutation(input, axes),
222	          Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))), Fail{Layout.DuplicateAxis{}},
223	          ranked_pass(input, axes, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(axes), Shape.rank_dimensions(Shape.dimensions(input)))), ranked),
224	          Equal.trans(Result<&2, &2, Layout.Error, Layout.Plan<input, axes>>, Layout.plan_bounded(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input)))),
225	            Layout.plan_unique(input, axes, Shape.bool_case(Layout.unique(axes))), Fail{Layout.DuplicateAxis{}},
226	            bounded_pass(input, axes, Shape.bool_case(Layout.bounded(axes, Shape.rank(input))), bounded),
227	            unique_failure(input, axes, Shape.bool_case(Layout.unique(axes)), duplicate))))))}
228	
229	def transpose_out_of_bounds(+input: Shape.Shape, +fill: F32, +a: U32, +b: U32, outside: {Transpose.valid(input, a, b) == False{} : Bool}) -> Laws.RetainedFailure<input, fill, Observation.Transpose{a, b}, 13>:
230	  +outside = outside
231	  Laws.RetainedFailure{
232	    Reads.new_lift(input, fill, result => {Observation.failure_code(input, Observation.Transpose{a, b}, result) == Some{13} : Maybe<&2, U32>},
233	      valid => retained_code(input, fill, valid, Observation.Transpose{a, b}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, transpose_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, a, b, Shape.bool_case(Transpose.valid(input, a, b)), outside))),
234	    Reads.new_lift(input, fill, result => {Observation.kept_dimensions(input, Observation.Transpose{a, b}, result) == Some{Shape.dimensions(input)} : Maybe<&2, List<&2, U32>>},
235	      valid => retained_dimensions(input, fill, valid, Observation.Transpose{a, b}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, transpose_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, a, b, Shape.bool_case(Transpose.valid(input, a, b)), outside))),
236	    Reads.new_lift(input, fill, result => {Observation.kept_length(input, Observation.Transpose{a, b}, result) == Some{Shape.logical_numel(Shape.dimensions(input))} : Maybe<&2, Nat>},
237	      valid => retained_length(input, fill, valid, Observation.Transpose{a, b}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, transpose_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, a, b, Shape.bool_case(Transpose.valid(input, a, b)), outside))),
238	    Reads.new_lift(input, fill, result => {Observation.kept_count(input, Observation.Transpose{a, b}, result) == Some{Shape.count(input)} : Maybe<&2, U32>},
239	      valid => retained_count(input, fill, valid, Observation.Transpose{a, b}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, transpose_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, a, b, Shape.bool_case(Transpose.valid(input, a, b)), outside))),
240	    other => inside => Reads.new_lift(input, fill, result => {Observation.kept_value(input, Observation.Transpose{a, b}, other, result) == Some{fill} : Maybe<&2, F32>},
241	      valid => retained_value(input, fill, valid, Observation.Transpose{a, b}, Transforms.LayoutError{Layout.AxisOutOfBounds{}}, other, inside, transpose_failure(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, a, b, Shape.bool_case(Transpose.valid(input, a, b)), outside)))}