src/tensor/metadata_contract.bend
bendtorch-core@0.1.0.0 · 97 lines · 10 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
4import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
5import bendtorch-core@0.1.0.0/src/storage/PROOF.bend as StorageProof
6import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
7import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
8import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
9import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation
10import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads
11import bendtorch-core@0.1.0.0/src/tensor/clone_metadata_records.bend as Laws
12
13def owner_value_projection(-shape: Shape.Shape, -original: Storage.Storage, -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +other: U32,
14 pair: Storage.Storage & Nat, -same: {pair == Storage.length(original) : Storage.Storage & Nat}) ->
15 {Observation.length_owner_value_pair(shape, other, Core.length_result(shape, original, valid, pair, same)) ==
16 Lifecycle.read_value(Storage.get(StorageLaws.owner(Nat, pair), other)) : Maybe<&2, F32>}:
17 (storage, number) = pair
18 Core.read_result_value(shape, storage,
19 Equal.trans(Nat, Lifecycle.logical_length(storage), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(shape)),
20 %Equal.sym(Storage.Storage & Nat, (storage, number), Storage.length(original), same) :
21 {Lifecycle.length_owner(_) == Lifecycle.logical_length(original) : Nat}
22 Lifecycle.length_preserved(original), valid),
23 other, Storage.get(storage, other), {==})
24
25def number_projection(-shape: Shape.Shape, -original: Storage.Storage, -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, pair: Storage.Storage & Nat, -same: {pair == Storage.length(original) : Storage.Storage & Nat}) ->
26 {Observation.length_number(shape, Core.length_result(shape, original, valid, pair, same)) == Lifecycle.length_value(pair) : Nat}:
27 (storage, number) = pair
28 {==}
29
30def owner_length_projection(-shape: Shape.Shape, -original: Storage.Storage, -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, pair: Storage.Storage & Nat, -same: {pair == Storage.length(original) : Storage.Storage & Nat}) ->
31 {Observation.length_owner_length_pair(shape, Core.length_result(shape, original, valid, pair, same)) == Lifecycle.length_owner(pair) : Nat}:
32 (storage, number) = pair
33 {==}
34
35def owner_dimensions_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Nat) ->
36 {Observation.length_owner_dimensions_pair(shape, pair) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}:
37 (tensor, number) = pair
38 {==}
39
40def owner_count_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Nat) ->
41 {Observation.length_owner_count_pair(shape, pair) == Some{Shape.count(shape)} : Maybe<&2, U32>}:
42 (tensor, number) = pair
43 {==}
44
45def length_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
46 {Observation.length_value(shape, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
47 Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number}, Observation.length_number(shape, Core.length(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})), Shape.logical_numel(Shape.dimensions(shape)),
48 Equal.trans(Nat, Observation.length_number(shape, Core.length(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})), Lifecycle.length_value(Storage.length(StorageLaws.created(Shape.count(shape), fill))), Shape.logical_numel(Shape.dimensions(shape)),
49 number_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, Storage.length(StorageLaws.created(Shape.count(shape), fill)), {==}),
50 Equal.trans(Nat, Lifecycle.length_value(Storage.length(StorageLaws.created(Shape.count(shape), fill))), Lifecycle.length_owner(Storage.length(StorageLaws.created(Shape.count(shape), fill))), Shape.logical_numel(Shape.dimensions(shape)),
51 Equal.sym(Nat, Lifecycle.length_owner(Storage.length(StorageLaws.created(Shape.count(shape), fill))), Lifecycle.length_value(Storage.length(StorageLaws.created(Shape.count(shape), fill))), Lifecycle.length_exact(StorageLaws.created(Shape.count(shape), fill))),
52 Equal.trans(Nat, Lifecycle.length_owner(Storage.length(StorageLaws.created(Shape.count(shape), fill))), Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)), Shape.logical_numel(Shape.dimensions(shape)),
53 Lifecycle.length_preserved(StorageLaws.created(Shape.count(shape), fill)), Reads.created_exact(shape, fill)))))
54
55def owner_length_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
56 {Observation.length_owner_length(shape, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
57 Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number}, Observation.length_owner_length_pair(shape, Core.length(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})), Shape.logical_numel(Shape.dimensions(shape)),
58 Equal.trans(Nat, Observation.length_owner_length_pair(shape, Core.length(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})), Lifecycle.length_owner(Storage.length(StorageLaws.created(Shape.count(shape), fill))), Shape.logical_numel(Shape.dimensions(shape)),
59 owner_length_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, Storage.length(StorageLaws.created(Shape.count(shape), fill)), {==}),
60 Equal.trans(Nat, Lifecycle.length_owner(Storage.length(StorageLaws.created(Shape.count(shape), fill))), Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)), Shape.logical_numel(Shape.dimensions(shape)),
61 Lifecycle.length_preserved(StorageLaws.created(Shape.count(shape), fill)), Reads.created_exact(shape, fill))))
62
63def owner_value_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +other: U32, inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
64 {Observation.length_owner_value(shape, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{fill} : Maybe<&2, F32>}:
65 Equal.trans(Maybe<&2, F32>, Observation.length_owner_value_pair(shape, other, Core.length(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})),
66 Lifecycle.read_value(Storage.get(StorageLaws.owner(Nat, Storage.length(StorageLaws.created(Shape.count(shape), fill))), other)), Some{fill},
67 owner_value_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, other, Storage.length(StorageLaws.created(Shape.count(shape), fill)), {==}),
68 Reads.stored_value(StorageLaws.owner(Nat, Storage.length(StorageLaws.created(Shape.count(shape), fill))), other, fill,
69 StorageLaws.replay_get(Shape.count(shape), fill, [StorageLaws.Length{}], other, Conversion.shape_count_within(shape), Reads.word_inside(shape, other, inside))))
70
71def dynamic_value_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +other: U32, inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
72 {Observation.dynamic_owner_value(other, Core.Packed{shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{fill} : Maybe<&2, F32>}:
73 Equal.trans(Maybe<&2, F32>, Observation.dynamic_owner_value(other, Core.Packed{shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}),
74 Core.read_value(shape, Core.read_flat(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}, other)), Some{fill},
75 Core.dynamic_result_value(shape, Core.read_flat(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}, other)),
76 Reads.read_point_done(shape, fill, valid, other, inside))
77
78def metadata_contract(+shape: Shape.Shape, +fill: F32) -> Laws.MetadataContract<shape, fill>:
79 Laws.MetadataContract{
80 Reads.new_lift(shape, fill, result => {Observation.length_value(shape, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
81 valid => length_done(shape, fill, valid)),
82 Reads.new_lift(shape, fill, result => {Observation.length_owner_dimensions(shape, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>},
83 valid => owner_dimensions_pair(shape, Core.length(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}))),
84 Reads.new_lift(shape, fill, result => {Observation.length_owner_length(shape, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
85 valid => owner_length_done(shape, fill, valid)),
86 Reads.new_lift(shape, fill, result => {Observation.length_owner_count(shape, result) == Some{Shape.count(shape)} : Maybe<&2, U32>},
87 valid => owner_count_pair(shape, Core.length(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}))),
88 Reads.new_lift(shape, fill, result => {Observation.dimensions(shape, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>},
89 valid => {==}),
90 Reads.new_lift(shape, fill, result => {Observation.count(shape, result) == Some{Shape.count(shape)} : Maybe<&2, U32>},
91 valid => {==}),
92 other => inside => Reads.new_lift(shape, fill, result => {Observation.length_owner_value(shape, other, result) == Some{fill} : Maybe<&2, F32>},
93 valid => owner_value_done(shape, fill, valid, other, inside)),
94 other => inside => Reads.new_lift(shape, fill, result => {Observation.shape_owner_value(shape, other, result) == Some{fill} : Maybe<&2, F32>},
95 valid => dynamic_value_done(shape, fill, valid, other, inside)),
96 other => inside => Reads.new_lift(shape, fill, result => {Observation.count_owner_value(shape, other, result) == Some{fill} : Maybe<&2, F32>},
97 valid => dynamic_value_done(shape, fill, valid, other, inside))}