src/tensor/allocation_PROOF.bend
bendtorch-core@0.1.0.0 · 122 lines · 12 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/nat_proofs.bend as Nats
4import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
5import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
6import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
7import bendtorch-core@0.1.0.0/src/storage/PROOF.bend as StorageProof
8import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
9import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
10import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
11import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation
12import bendtorch-core@0.1.0.0/src/tensor/allocation_LAWS.bend as Laws
13import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
14import bendtorch-core@0.1.0.0/src/tensor/word_conversion_PROOF.bend as ConversionProof
15
16def allocate_length(+depth: Nat, +length: Nat, +fill: F32, valid: Bool,
17 -decision: {valid == Storage.bounds(depth, length) : Bool}, accepted: {valid == True{} : Bool}) ->
18 {Allocation.storage_length(Storage.allocate(depth, length, fill, valid, decision)) == Some{length} : Maybe<&2, Nat>}:
19 match valid:
20 case False{}:
21 Empty.absurd({None{} == Some{length} : Maybe<&2, Nat>}, Arith.clash(accepted))
22 case True{}:
23 {==}
24
25def allocate_at_length(+length: Nat, +fill: F32, metadata: Nat & Nat,
26 valid: {Storage.bounds(Pair.fst(Nat, Nat, metadata), length) == True{} : Bool}) ->
27 {Allocation.storage_length(Storage.allocate_at(length, fill, metadata)) == Some{length} : Maybe<&2, Nat>}:
28 (+depth, capacity) = metadata
29 allocate_length(depth, length, fill, Storage.bounds(depth, length), {==}, valid)
30
31def new_checked_length(+length: Nat, +fill: F32, allowed: Bool, accepted: {allowed == True{} : Bool},
32 limit: {Nat.is_le(length, Model.capacity(20n)) == True{} : Bool}) ->
33 {Allocation.storage_length(Storage.new_checked(length, fill, allowed)) == Some{length} : Maybe<&2, Nat>}:
34 match length allowed:
35 case 0n False{}:
36 {==}
37 case 0n True{}:
38 {==}
39 case 1n+p False{}:
40 Empty.absurd({None{} == Some{1n+p} : Maybe<&2, Nat>}, Arith.clash(accepted))
41 case 1n+p True{}:
42 allocate_at_length(1n+p, fill, Storage.depth_seek(20n, 1n+p, 0n, 1n, Nat.is_le(1n+p, 1n)), Api.seek(1n+p, limit, {==}))
43
44def storage_new(+word: U32, +fill: F32, +within: {U32.is_le(word, 1048576) == True{} : Bool}) ->
45 {Allocation.storage_length(Storage.new(word, fill)) == Some{U32.to_nat(word)} : Maybe<&2, Nat>}:
46 new_checked_length(U32.to_nat(word), fill, U32.is_le(word, 1048576), within, Api.cap_from(word, within))
47
48def storage_zero(+fill: F32) -> {Storage.new(0, fill) == Done{Storage.Empty{}} : Result<&2, &1, Storage.Error, Storage.Storage>}:
49 {==}
50
51def natural_equal_true(+a: Nat, +b: Nat, equal: {a == b : Nat}) -> {True{} == Nat.is_eq(a, b) : Bool}:
52 Equal.sym(Bool, Nat.is_eq(a, b), True{},
53 Equal.trans(Bool, Nat.is_eq(a, b), Nat.is_eq(b, b), True{},
54 Equal.cong(Nat, Bool, n => Nat.is_eq(n, b), a, b, equal), Arith.eq_refl(b)))
55
56def attach_decided_length(+shape: Shape.Shape, +length: Nat, decision: Shape.BoolCase<Nat.is_eq(length, Shape.elements(shape))>,
57 storage: Storage.Storage, exact: {Lifecycle.logical_length(storage) == length : Nat}, accepted: {True{} == Nat.is_eq(length, Shape.elements(shape)) : Bool}) ->
58 {Allocation.tensor_length(shape, Core.attach_decided(shape, storage, length, exact, decision)) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
59 match decision:
60 case Shape.BFalse{equal}:
61 Empty.absurd({None{} == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}, Nats.contradiction(Nat.is_eq(length, Shape.elements(shape)), accepted, equal))
62 case Shape.BTrue{equal}:
63 Equal.cong(Nat, Maybe<&2, Nat>, n => Some{n}, Lifecycle.logical_length(storage), Shape.logical_numel(Shape.dimensions(shape)),
64 Equal.trans(Nat, Lifecycle.logical_length(storage), length, Shape.logical_numel(Shape.dimensions(shape)), exact,
65 Equal.trans(Nat, length, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)), Lifecycle.natural_equal(length, Shape.elements(shape), equal), Shape.elements_exact(shape))))
66
67def attach_length(+shape: Shape.Shape, storage: Storage.Storage, exact: {Lifecycle.logical_length(storage) == Shape.elements(shape) : Nat}) ->
68 {Allocation.tensor_length(shape, Core.attach(shape, storage)) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
69 match storage:
70 case Storage.Empty{}:
71 attach_decided_length(shape, 0n, Shape.bool_case(Nat.is_eq(0n, Shape.elements(shape))), Storage.Empty{}, {==}, natural_equal_true(0n, Shape.elements(shape), exact))
72 case Storage.Owned{+depth, +length, array, balanced, valid}:
73 attach_decided_length(shape, length, Shape.bool_case(Nat.is_eq(length, Shape.elements(shape))), Storage.Owned{depth, length, array, balanced, valid}, {==}, natural_equal_true(length, Shape.elements(shape), exact))
74
75def new_result_length(+shape: Shape.Shape, result: Result<&2, &1, Storage.Error, Storage.Storage>,
76 exact: {Allocation.storage_length(result) == Some{Shape.elements(shape)} : Maybe<&2, Nat>}) ->
77 {Allocation.tensor_length(shape, Core.new_result(shape, result)) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
78 match result:
79 case Fail{error}:
80 Empty.absurd({None{} == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
81 Arith.clash(Equal.cong(Maybe<&2, Nat>, Bool, value => Maybe.is_some(&2, Nat, value), None{}, Some{Shape.elements(shape)}, exact)))
82 case Done{storage}:
83 attach_length(shape, storage,
84 Equal.cong(Maybe<&2, Nat>, Nat, value => Maybe.default(&2, Nat, value, 0n), Some{Lifecycle.logical_length(storage)}, Some{Shape.elements(shape)}, exact))
85
86def tensor_done(+shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape>>,
87 exact: {Allocation.tensor_length(shape, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}) -> Allocation.TensorDone<shape, result>:
88 match result:
89 case Fail{error}:
90 Empty.absurd(Allocation.TensorDone<shape, Fail{error}>,
91 Arith.clash(Equal.cong(Maybe<&2, Nat>, Bool, value => Maybe.is_some(&2, Nat, value), None{}, Some{Shape.logical_numel(Shape.dimensions(shape))}, exact)))
92 case Done{tensor}:
93 Allocation.TensorDone{tensor, {==}}
94
95def core_new(+shape: Shape.Shape, +fill: F32) ->
96 {Allocation.tensor_length(shape, Core.new(shape, fill)) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
97 new_result_length(shape, Storage.new(Shape.count(shape), fill),
98 Equal.trans(Maybe<&2, Nat>, Allocation.storage_length(Storage.new(Shape.count(shape), fill)), Some{U32.to_nat(Shape.count(shape))}, Some{Shape.elements(shape)},
99 storage_new(Shape.count(shape), fill, Conversion.shape_count_within(shape)),
100 Equal.cong(Nat, Maybe<&2, Nat>, n => Some{n}, U32.to_nat(Shape.count(shape)), Shape.elements(shape), Conversion.shape_count_exact(shape))))
101
102def core_new_done(+shape: Shape.Shape, +fill: F32) -> Allocation.TensorDone<shape, Core.new(shape, fill)>:
103 tensor_done(shape, Core.new(shape, fill), core_new(shape, fill))
104
105def Laws.storage_new_complete(word, fill, within):
106 storage_new(word, fill, within)
107
108def Laws.storage_new_zero(fill):
109 storage_zero(fill)
110
111def Laws.storage_new_depth_bounds(word, within, positive):
112 Api.seek(U32.to_nat(word), Api.cap_from(word, within),
113 Equal.trans(Bool, Nat.is_lt(0n, U32.to_nat(word)), U32.is_lt(0, word), True{}, Arith.u32_lt(0, word), positive))
114
115def Laws.storage_seek_bounds(fuel, length, depth, capacity, done, decided, sized, left, limit, positive):
116 Api.seek_bounds(fuel, length, depth, capacity, done, decided, sized, left, limit, positive)
117
118def Laws.core_new_complete(shape, fill):
119 core_new(shape, fill)
120
121def Laws.core_new_done(shape, fill):
122 core_new_done(shape, fill)