1 import Base 2 import ../shape/core.bend as Shape 3 import ../storage/main.bend as Storage 4 import ../storage/LAWS.bend as StorageLaws 5 import ../storage/PROOF.bend as StorageProof 6 import ./core.bend as Core 7 import ./lifecycle.bend as Lifecycle 8 import ./word_conversion.bend as Conversion 9 import ./observation.bend as Observation 10 import ./read_contract.bend as Reads 11 import ./clone_metadata_records.bend as Laws 12 13 def 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 25 def 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 30 def 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 35 def owner_dimensions_pair(+shape: Shape.Shape, pair: Core.Tensor & Nat) -> 36 {Observation.length_owner_dimensions_pair(shape, pair) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}: 37 (tensor, number) = pair 38 {==} 39 40 def owner_count_pair(+shape: Shape.Shape, pair: Core.Tensor & Nat) -> 41 {Observation.length_owner_count_pair(shape, pair) == Some{Shape.count(shape)} : Maybe<&2, U32>}: 42 (tensor, number) = pair 43 {==} 44 45 def 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 55 def 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 63 def 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 71 def 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 78 def metadata_contract(+shape: Shape.Shape, +fill: F32) -> Laws.MetadataContract: 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))}