src/shape/PROOF.bend
bendtorch-core@0.1.0.0 · 100 lines · 3 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index
4import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast
5import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
6import bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend as Construct
7import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as Boundary
8import bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend as Unique
9import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as Plan
10import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as Laws
11
12def Laws.row_major_bounded(dims, coordinate):
13 %Index.flatten_row_major(dims, coordinate) : Shape.LT(_, Shape.numel(dims))
14 Shape.Fin.bound(Shape.numel(dims), Shape.flatten(dims, coordinate))
15
16def Laws.flatten_unflatten(dims, index):
17 Index.flatten_unflatten(dims, index)
18
19def Laws.unflatten_flatten(dims, coordinate):
20 Index.unflatten_flatten(dims, coordinate)
21
22def Laws.flatten_row_major(dims, coordinate):
23 Index.flatten_row_major(dims, coordinate)
24
25def Laws.broadcast_left_projection(left, right, output, alignment, coordinate):
26 Broadcast.project_left(left, right, output, alignment, coordinate)
27
28def Laws.broadcast_right_projection(left, right, output, alignment, coordinate):
29 Broadcast.project_right(left, right, output, alignment, coordinate)
30
31def Laws.construction_complete(input, rank_bound, capacity_bound):
32 Construct.construction_complete(input, Shape.bool_case(Nat.is_le(Shape.rank_dimensions(input), 4n)), Nats.le_true(Shape.rank_dimensions(input), 4n, rank_bound), capacity_bound)
33
34def Laws.flatten_checked_refines(shape, values):
35 Boundary.flatten_checked(shape, values)
36
37def Laws.unflatten_checked_refines(shape, index):
38 Boundary.unflatten_checked(shape, index)
39
40def Laws.broadcast_output_unique(left, right, output, other, first, second):
41 Unique.broadcast_unique(left, right, output, other, first, second)
42
43def Laws.broadcast_checked_plan(left, right):
44 Plan.broadcast_checked_plan(left, right)
45
46def Laws.broadcast_checked_complete(left, right, output, alignment, rank_bound, capacity_bound):
47 Plan.broadcast_checked_complete(left, right, output, alignment, rank_bound, capacity_bound)
48
49def Laws.project_left_checked_refines(plan, values):
50 Boundary.project_left_checked(plan, values)
51
52def Laws.project_right_checked_refines(plan, values):
53 Boundary.project_right_checked(plan, values)
54
55def Laws.project_left_index_refines(plan, map, index):
56 Boundary.project_left_index(plan, map, index)
57
58def Laws.project_right_index_refines(plan, map, index):
59 Boundary.project_right_index(plan, map, index)
60
61def flatten_fits_bounds(+shape: Shape.Shape, +values: List<&2, U32>, verdict: Shape.BoolCase<Shape.fit_words(Shape.dimensions(shape), values)>,
62 outside: {Shape.fit_words(Shape.dimensions(shape), values) == False{} : Bool}) ->
63 {Shape.flatten_checked.fits(shape, values, verdict) == Fail{Shape.CoordinateOutOfBounds{}} : Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>}:
64 match verdict:
65 case Shape.BFalse{equal}:
66 {==}
67 case Shape.BTrue{equal}:
68 Empty.absurd({Shape.flatten_checked.fits(shape, values, Shape.BTrue{equal}) == Fail{Shape.CoordinateOutOfBounds{}} : Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>},
69 Shape.clash(Equal.trans(Bool, True{}, Shape.fit_words(Shape.dimensions(shape), values), False{}, equal, outside)))
70
71def flatten_ranked_rank(+shape: Shape.Shape, +values: List<&2, U32>,
72 same_rank: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values))>,
73 differ: {Shape.rank_dimensions(Shape.dimensions(shape)) != Shape.rank_dimensions(values) : Nat}) ->
74 {Shape.flatten_checked.ranked(shape, values, same_rank) == Fail{Shape.CoordinateRankMismatch{}} : Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>}:
75 match same_rank:
76 case Shape.BFalse{equal}:
77 {==}
78 case Shape.BTrue{equal}:
79 Empty.absurd({Shape.flatten_checked.ranked(shape, values, Shape.BTrue{equal}) == Fail{Shape.CoordinateRankMismatch{}} : Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>},
80 differ(Shape.equal_decided(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values), equal)))
81
82def flatten_ranked_bounds(+shape: Shape.Shape, +values: List<&2, U32>,
83 same_rank: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values))>,
84 same: {Shape.rank_dimensions(Shape.dimensions(shape)) == Shape.rank_dimensions(values) : Nat},
85 outside: {Shape.fit_words(Shape.dimensions(shape), values) == False{} : Bool}) ->
86 {Shape.flatten_checked.ranked(shape, values, same_rank) == Fail{Shape.CoordinateOutOfBounds{}} : Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>}:
87 match same_rank:
88 case Shape.BFalse{equal}:
89 Empty.absurd({Shape.flatten_checked.ranked(shape, values, Shape.BFalse{equal}) == Fail{Shape.CoordinateOutOfBounds{}} : Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>},
90 Shape.clash(Equal.trans(Bool, True{}, Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values)), False{},
91 Plan.eq_true(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values), same),
92 Equal.sym(Bool, False{}, Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values)), equal))))
93 case Shape.BTrue{equal}:
94 flatten_fits_bounds(shape, values, Shape.bool_case(Shape.fit_words(Shape.dimensions(shape), values)), outside)
95
96def Laws.flatten_rank_error(shape, values, differ):
97 flatten_ranked_rank(shape, values, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values))), differ)
98
99def Laws.flatten_bounds_error(shape, values, same, outside):
100 flatten_ranked_bounds(shape, values, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(shape)), Shape.rank_dimensions(values))), same, outside)