src/tensor/contracts/build_facts.bend
bendtorch-core@0.1.0.0 · 170 lines · 14 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/nat_proofs.bend as Nats
5import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
6import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
7import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
8import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore
9import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
10import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
11import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
12import bendtorch-core@0.1.0.0/src/storage/route.bend as Route
13import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
14import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
15import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
16import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend as Owned
17
18
19
20
21
22
23def lt_zero_false(+x: Nat) -> {Nat.is_lt(x, 0n) == False{} : Bool}:
24 match x:
25 case 0n:
26 {==}
27 case 1n+p:
28 {==}
29
30def lt_self_succ(+k: Nat) -> {Nat.is_lt(k, 1n+k) == True{} : Bool}:
31 match k:
32 case 0n:
33 {==}
34 case 1n+p:
35 lt_self_succ(p)
36
37def lt_succ_right(+b: Nat, +k: Nat, h: {Nat.is_lt(b, k) == True{} : Bool}) -> {Nat.is_lt(b, 1n+k) == True{} : Bool}:
38 match b k:
39 case 0n _:
40 {==}
41 case 1n+p 0n:
42 Empty.absurd({Nat.is_lt(1n+p, 1n) == True{} : Bool}, Arith.clash(h))
43 case 1n+p 1n+q:
44 lt_succ_right(p, q, h)
45
46
47
48def above_false(+k: Nat, +b: Nat, h: {Nat.is_lt(k, b) == True{} : Bool}) -> {Nat.is_lt(b, 1n+k) == False{} : Bool}:
49 match k b:
50 case 0n 0n:
51 Empty.absurd({Nat.is_lt(0n, 1n) == False{} : Bool}, Arith.clash(h))
52 case 0n 1n+q:
53 lt_zero_false(q)
54 case 1n+p 0n:
55 Empty.absurd({Nat.is_lt(0n, 1n+(1n+p)) == False{} : Bool}, Arith.clash(h))
56 case 1n+p 1n+q:
57 above_false(p, q, h)
58
59def lt_asym(+k: Nat, +b: Nat, h: {Nat.is_lt(k, b) == True{} : Bool}) -> {Nat.is_lt(b, k) == False{} : Bool}:
60 match k b:
61 case 0n 0n:
62 {==}
63 case 0n 1n+q:
64 {==}
65 case 1n+p 0n:
66 Empty.absurd({Nat.is_lt(0n, 1n+p) == False{} : Bool}, Arith.clash(h))
67 case 1n+p 1n+q:
68 lt_asym(p, q, h)
69
70
71
72def below_true(+b: Nat, +k: Nat, h: {Nat.is_le(1n+b, k) == True{} : Bool}) -> {Nat.is_lt(b, k) == True{} : Bool}:
73 match b k:
74 case 0n 0n:
75 Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, Arith.clash(h))
76 case 0n 1n+q:
77 {==}
78 case 1n+p 0n:
79 Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, Arith.clash(h))
80 case 1n+p 1n+q:
81 below_true(p, q, h)
82
83def lt_add_right(+a: Nat, +c: Nat, +b: Nat, h: {Nat.is_lt(a, c) == True{} : Bool}) ->
84 {Nat.is_lt(Nat.add(a, b), Nat.add(c, b)) == True{} : Bool}:
85 match a c:
86 case 0n 0n:
87 Empty.absurd({Nat.is_lt(b, b) == True{} : Bool}, Arith.clash(h))
88 case 0n 1n+q:
89 Arith.lt_succ(b, Nat.add(q, b), Api.le_add_left(q, b))
90 case 1n+p 0n:
91 Empty.absurd({Nat.is_lt(1n+Nat.add(p, b), b) == True{} : Bool}, Arith.clash(h))
92 case 1n+p 1n+q:
93 lt_add_right(p, q, b, h)
94
95def le_add_cong(+c: Nat, +x: Nat, +y: Nat, h: {Nat.is_le(x, y) == True{} : Bool}) ->
96 {Nat.is_le(Nat.add(c, x), Nat.add(c, y)) == True{} : Bool}:
97 match c:
98 case 0n:
99 h
100 case 1n+r:
101 le_add_cong(r, x, y, h)
102
103def le_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_le(a, b) == True{} : Bool}, bc: {Nat.is_le(b, c) == True{} : Bool}) ->
104 {Nat.is_le(a, c) == True{} : Bool}:
105 match a b c:
106 case 0n _ _:
107 Arith.le_zero(c)
108 case 1n+p 0n _:
109 Empty.absurd({Nat.is_le(1n+p, c) == True{} : Bool}, Arith.clash(ab))
110 case 1n+p 1n+q 0n:
111 Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, Arith.clash(bc))
112 case 1n+p 1n+q 1n+r:
113 le_trans(p, q, r, ab, bc)
114
115def position_step(+capacity: Nat, +offset: Nat, +base: Nat) ->
116 {Nat.add(offset, Nat.add(capacity, base)) == Nat.add(Nat.add(capacity, offset), base) : Nat}:
117 Equal.trans(Nat, Nat.add(offset, Nat.add(capacity, base)), Nat.add(capacity, Nat.add(offset, base)), Nat.add(Nat.add(capacity, offset), base),
118 Nats.add_swap(offset, capacity, base), Index.add_assoc(capacity, offset, base))
119
120def add_zero_right(+number: Nat) -> {Nat.add(number, 0n) == number : Nat}:
121 match number:
122 case 0n:
123 {==}
124 case 1n+p:
125 Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, 0n), p, add_zero_right(p))
126
127
128
129def output_position(+depth: Nat, +length: Nat, +index: U32, +valid: {Storage.bounds(depth, length) == True{} : Bool},
130 +inside: {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}) ->
131 {Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n) == U32.to_nat(index) : Nat}:
132 +rest = Arith.and_right(Nat.is_le(depth, 20n), Bool.and(Nat.is_lt(0n, length), Nat.is_le(length, Model.capacity(depth))), valid)
133 Equal.trans(Nat, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n), Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index),
134 add_zero_right(Model.offset(depth, Refinement.route(depth, index))),
135 Equal.sym(Nat, U32.to_nat(index), Model.offset(depth, Refinement.route(depth, index)),
136 Route.route_offset(depth, index,
137 Arith.and_left(Nat.is_le(depth, 20n), Bool.and(Nat.is_lt(0n, length), Nat.is_le(length, Model.capacity(depth))), valid),
138 Arith.lt_le_trans(U32.to_nat(index), length, Model.capacity(depth), inside,
139 Arith.and_right(Nat.is_lt(0n, length), Nat.is_le(length, Model.capacity(depth)), rest)))))
140
141
142
143
144def storage_shift(-shape: Shape.Shape, -s: Storage.Storage, -t: Storage.Storage, e: {s == t : Storage.Storage},
145 -R: @st: Storage.Storage -> @-k: {Lifecycle.logical_length(st) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> Type,
146 h: @-k: {Lifecycle.logical_length(s) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> R(s, k)) ->
147 @-k: {Lifecycle.logical_length(t) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> R(t, k):
148 %e : (@-k: {Lifecycle.logical_length(_) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> R(_, k))
149 h
150
151
152
153def input_lift(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>,
154 +nonzero: {Nat.is_lt(0n, U32.to_nat(Shape.count(shape))) == True{} : Bool}, -Q: Storage.Storage -> Type,
155 owned: @+d: Nat -> @+fits: {Storage.bounds(d, U32.to_nat(Shape.count(shape))) == True{} : Bool} ->
156 @-b: Model.Balanced(F32, d, Api.arr(Owned.norm(U32.to_nat(Shape.count(shape)), ops, Nil{}), d, fill)) ->
157 @-f: {Storage.bounds(d, U32.to_nat(Shape.count(shape))) == True{} : Bool} ->
158 Q(Storage.Owned{d, U32.to_nat(Shape.count(shape)), Api.arr(Owned.norm(U32.to_nat(Shape.count(shape)), ops, Nil{}), d, fill), b, f})) ->
159 Q(Replayed.storage(shape, fill, ops)):
160 Owned.created_lift(Shape.count(shape), fill, Conversion.shape_count_within(shape), s => Q(StorageLaws.replay(ops, s)),
161 zero => Empty.absurd(Q(StorageLaws.replay(ops, Storage.Empty{})),
162 Arith.clash(Equal.trans(Bool, False{}, Nat.is_lt(0n, U32.to_nat(Shape.count(shape))), True{},
163 Equal.cong(Nat, Bool, x => Nat.is_lt(0n, x), 0n, U32.to_nat(Shape.count(shape)), Equal.sym(Nat, U32.to_nat(Shape.count(shape)), 0n, zero)),
164 nonzero))),
165 d => fits => f => Owned.replay_lift(ops, d, U32.to_nat(Shape.count(shape)), fill, Nil{}, Api.hit_of(U32.to_nat(Shape.count(shape)), ops), {==},
166 ArrayCore.new_balanced(F32, d, fill), f, fits, Q, c => owned(d, fits, c, f)))
167
168
169
170