src/tensor/transform_contract_LAWS.bend
bendtorch-core@0.1.0.0 · 63 lines · 7 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
4import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
5import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as Transpose
6import bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend as Observation
7import bendtorch-core@0.1.0.0/src/tensor/transform_records.bend as Records
8
9law 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
16law 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
26law 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
33law 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
40law 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
48law 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
57law 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>