1 import Base 2 import ../shape/core.bend as Shape 3 import ../shape/nat_proofs.bend as Nats 4 import ../storage/main.bend as Storage 5 import ../storage/LAWS.bend as StorageLaws 6 import ../storage/PROOF.bend as StorageProof 7 import ../storage/arith.bend as Arith 8 import ./core.bend as Core 9 import ./lifecycle.bend as Lifecycle 10 import ./allocation_spec.bend as Allocation 11 import ./allocation_PROOF.bend as AllocationProof 12 import ./word_conversion.bend as Conversion 13 import ./observation.bend as Observation 14 import ./read_write_records.bend as Laws 15 16 def count_exact(+shape: Shape.Shape) -> {U32.to_nat(Shape.count(shape)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}: 17 Equal.trans(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)), Conversion.shape_count_exact(shape), Shape.elements_exact(shape)) 18 19 def word_inside(+shape: Shape.Shape, +index: U32, inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> 20 {Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))) == True{} : Bool}: 21 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)), count_exact(shape)) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool} 22 inside 23 24 def word_outside(+shape: Shape.Shape, +index: U32, outside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}) -> 25 {Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))) == False{} : Bool}: 26 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)), count_exact(shape)) : {Nat.is_lt(U32.to_nat(index), _) == False{} : Bool} 27 outside 28 29 def created_size(+shape: Shape.Shape, +fill: F32) -> {StorageLaws.size(StorageLaws.created(Shape.count(shape), fill)) == U32.to_nat(Shape.count(shape)) : Nat}: 30 StorageLaws.replay_size(Shape.count(shape), fill, [], Conversion.shape_count_within(shape)) 31 32 def size_is_length(storage: Storage.Storage) -> {StorageLaws.size(storage) == Lifecycle.logical_length(storage) : Nat}: 33 match storage: 34 case Storage.Empty{}: 35 {==} 36 case Storage.Owned{depth, length, array, balanced, valid}: 37 {==} 38 39 def created_exact(+shape: Shape.Shape, +fill: F32) -> {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}: 40 Equal.trans(Nat, Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)), StorageLaws.size(StorageLaws.created(Shape.count(shape), fill)), Shape.logical_numel(Shape.dimensions(shape)), 41 Equal.sym(Nat, StorageLaws.size(StorageLaws.created(Shape.count(shape), fill)), Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)), size_is_length(StorageLaws.created(Shape.count(shape), fill))), 42 Equal.trans(Nat, StorageLaws.size(StorageLaws.created(Shape.count(shape), fill)), U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)), created_size(shape, fill), count_exact(shape))) 43 44 def size_outside(+shape: Shape.Shape, +fill: F32, +index: U32, outside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}) -> 45 {Nat.is_lt(U32.to_nat(index), StorageLaws.size(StorageLaws.created(Shape.count(shape), fill))) == False{} : Bool}: 46 %Equal.sym(Nat, StorageLaws.size(StorageLaws.created(Shape.count(shape), fill)), U32.to_nat(Shape.count(shape)), created_size(shape, fill)) : {Nat.is_lt(U32.to_nat(index), _) == False{} : Bool} 47 word_outside(shape, index, outside) 48 49 def attached(+shape: Shape.Shape, -storage: Storage.Storage, +n: Nat, -exact: {Lifecycle.logical_length(storage) == n : Nat}, 50 decision: Shape.BoolCase, counted: {n == Shape.elements(shape) : Nat}, 51 -P: Result<&2, &1, Core.Error, Core.Tensor> -> Type, 52 h: @-valid: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> P(Done{Core.TTensor{storage, valid}})) -> 53 P(Core.attach_decided(shape, storage, n, exact, decision)): 54 match decision: 55 case Shape.BFalse{no}: 56 Empty.absurd(P(Core.attach_decided(shape, storage, n, exact, Shape.BFalse{no})), 57 Nats.contradiction(Nat.is_eq(n, Shape.elements(shape)), AllocationProof.natural_equal_true(n, Shape.elements(shape), counted), no)) 58 case Shape.BTrue{yes}: 59 h(Equal.trans(Nat, Lifecycle.logical_length(storage), n, Shape.logical_numel(Shape.dimensions(shape)), exact, 60 Equal.trans(Nat, n, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)), Lifecycle.natural_equal(n, Shape.elements(shape), yes), Shape.elements_exact(shape)))) 61 62 def attach_lift(+shape: Shape.Shape, storage: Storage.Storage, counted: {Lifecycle.logical_length(storage) == Shape.elements(shape) : Nat}, 63 -P: Result<&2, &1, Core.Error, Core.Tensor> -> Type, 64 h: @-valid: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> P(Done{Core.TTensor{storage, valid}})) -> 65 P(Core.attach(shape, storage)): 66 match storage: 67 case Storage.Empty{}: 68 attached(shape, Storage.Empty{}, 0n, {==}, Shape.bool_case(Nat.is_eq(0n, Shape.elements(shape))), counted, P, h) 69 case Storage.Owned{+depth, +length, array, balanced, valid}: 70 attached(shape, Storage.Owned{depth, length, array, balanced, valid}, length, {==}, 71 Shape.bool_case(Nat.is_eq(length, Shape.elements(shape))), counted, P, h) 72 73 def result_lift(+shape: Shape.Shape, result: Result<&2, &1, Storage.Error, Storage.Storage>, 74 counted: {Allocation.storage_length(result) == Some{Shape.elements(shape)} : Maybe<&2, Nat>}, 75 -P: Result<&2, &1, Core.Error, Core.Tensor> -> Type, 76 h: @-valid: {Lifecycle.logical_length(StorageLaws.created.of(result)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> 77 P(Done{Core.TTensor{StorageLaws.created.of(result), valid}})) -> 78 P(Core.new_result(shape, result)): 79 match result: 80 case Fail{error}: 81 Empty.absurd(P(Core.new_result(shape, Fail{error})), 82 Arith.clash(Equal.cong(Maybe<&2, Nat>, Bool, value => Maybe.is_some(&2, Nat, value), None{}, Some{Shape.elements(shape)}, counted))) 83 case Done{storage}: 84 attach_lift(shape, storage, 85 Equal.cong(Maybe<&2, Nat>, Nat, value => Maybe.default(&2, Nat, value, 0n), 86 Some{Lifecycle.logical_length(storage)}, Some{Shape.elements(shape)}, counted), P, h) 87 88 def new_lift(+shape: Shape.Shape, +fill: F32, -P: Result<&2, &1, Core.Error, Core.Tensor> -> Type, 89 h: @-valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> P(Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}})) -> P(Core.new(shape, fill)): 90 result_lift(shape, Storage.new(Shape.count(shape), fill), 91 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)}, 92 AllocationProof.storage_new(Shape.count(shape), fill, Conversion.shape_count_within(shape)), 93 Equal.cong(Nat, Maybe<&2, Nat>, value => Some{value}, U32.to_nat(Shape.count(shape)), Shape.elements(shape), Conversion.shape_count_exact(shape))), 94 P, h) 95 96 def storage_value(result: Result<&2, &2, Storage.Error, F32>) -> Maybe<&2, F32>: 97 match result: 98 case Fail{error}: 99 None{} 100 case Done{value}: 101 Some{value} 102 103 def storage_pair_value(pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>) -> 104 {Lifecycle.read_value(pair) == storage_value(StorageLaws.outcome(Result<&2, &2, Storage.Error, F32>, pair)) : Maybe<&2, F32>}: 105 (storage, result) = pair 106 match result: 107 case Fail{error}: 108 {==} 109 case Done{value}: 110 {==} 111 112 def stored_value(storage: Storage.Storage, +other: U32, -expected: F32, 113 read: {StorageLaws.read(storage, other) == Done{expected} : Result<&2, &2, Storage.Error, F32>}) -> 114 {Lifecycle.read_value(Storage.get(storage, other)) == Some{expected} : Maybe<&2, F32>}: 115 Equal.trans(Maybe<&2, F32>, Lifecycle.read_value(Storage.get(storage, other)), storage_value(StorageLaws.read(storage, other)), Some{expected}, 116 storage_pair_value(Storage.get(storage, other)), 117 Equal.cong(Result<&2, &2, Storage.Error, F32>, Maybe<&2, F32>, storage_value, StorageLaws.read(storage, other), Done{expected}, read)) 118 119 def read_code_projection(-shape: Shape.Shape, -original: Storage.Storage, 120 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, 121 pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>, -same: {pair == Storage.get(original, index) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}) -> 122 {Observation.read_code_pair(shape, Core.read_result(shape, original, valid, index, pair, same)) == 123 Observation.read_status(Core.storage_read_error(StorageLaws.outcome(Result<&2, &2, Storage.Error, F32>, pair))) : U32}: 124 (storage, result) = pair 125 {==} 126 127 def read_code_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, -expected: Result<&2, &2, Storage.Error, F32>, 128 read: {StorageLaws.read(StorageLaws.created(Shape.count(shape), fill), index) == expected : Result<&2, &2, Storage.Error, F32>}) -> 129 {Observation.read_code(shape, index, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{Observation.read_status(Core.storage_read_error(expected))} : Maybe<&2, U32>}: 130 Equal.cong(U32, Maybe<&2, U32>, code => Some{code}, 131 Observation.read_code_pair(shape, Core.read_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==})), 132 Observation.read_status(Core.storage_read_error(expected)), 133 Equal.trans(U32, Observation.read_code_pair(shape, Core.read_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==})), 134 Observation.read_status(Core.storage_read_error(StorageLaws.read(StorageLaws.created(Shape.count(shape), fill), index))), Observation.read_status(Core.storage_read_error(expected)), 135 read_code_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==}), 136 Equal.cong(Result<&2, &2, Storage.Error, F32>, U32, result => Observation.read_status(Core.storage_read_error(result)), StorageLaws.read(StorageLaws.created(Shape.count(shape), fill), index), expected, read))) 137 138 def read_dimensions_pair(+shape: Shape.Shape, pair: Core.Tensor & Result<&2, &2, Core.Error, F32>) -> 139 {Observation.after_dimensions_pair(shape, pair) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}: 140 (tensor, result) = pair 141 {==} 142 143 def read_count_pair(+shape: Shape.Shape, pair: Core.Tensor & Result<&2, &2, Core.Error, F32>) -> 144 {Observation.after_count_pair(shape, pair) == Some{Shape.count(shape)} : Maybe<&2, U32>}: 145 (tensor, result) = pair 146 {==} 147 148 def read_length_projection(-shape: Shape.Shape, -original: Storage.Storage, 149 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, 150 pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>, -same: {pair == Storage.get(original, index) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}) -> 151 {Observation.after_length_pair(shape, Core.read_result(shape, original, valid, index, pair, same)) == Lifecycle.retained_read(pair) : Nat}: 152 (storage, result) = pair 153 {==} 154 155 def read_length_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32) -> 156 {Observation.after_length(shape, index, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}: 157 Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number}, 158 Observation.after_length_pair(shape, Core.read_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==})), Shape.logical_numel(Shape.dimensions(shape)), 159 Equal.trans(Nat, Observation.after_length_pair(shape, Core.read_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==})), 160 Lifecycle.retained_read(Storage.get(StorageLaws.created(Shape.count(shape), fill), index)), Shape.logical_numel(Shape.dimensions(shape)), 161 read_length_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==}), 162 Equal.trans(Nat, Lifecycle.retained_read(Storage.get(StorageLaws.created(Shape.count(shape), fill), index)), Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)), Shape.logical_numel(Shape.dimensions(shape)), 163 Lifecycle.get_length(StorageLaws.created(Shape.count(shape), fill), index), created_exact(shape, fill)))) 164 165 def read_value_projection(-shape: Shape.Shape, -original: Storage.Storage, 166 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +other: U32, 167 pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>, -same: {pair == Storage.get(original, index) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}) -> 168 {Observation.after_value_pair(shape, other, Core.read_result(shape, original, valid, index, pair, same)) == 169 Lifecycle.read_value(Storage.get(StorageLaws.owner(Result<&2, &2, Storage.Error, F32>, pair), other)) : Maybe<&2, F32>}: 170 (storage, result) = pair 171 Core.read_result_value(shape, storage, 172 Equal.trans(Nat, Lifecycle.logical_length(storage), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(shape)), 173 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, F32>, (storage, result), Storage.get(original, index), same) : 174 {Lifecycle.retained_read(_) == Lifecycle.logical_length(original) : Nat} 175 Lifecycle.get_length(original, index), valid), 176 other, Storage.get(storage, other), {==}) 177 178 def read_after_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +other: U32, inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> 179 {Observation.after_value(shape, index, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{fill} : Maybe<&2, F32>}: 180 Equal.trans(Maybe<&2, F32>, 181 Observation.after_value_pair(shape, other, Core.read_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==})), 182 Lifecycle.read_value(Storage.get(StorageLaws.kept(StorageLaws.created(Shape.count(shape), fill), index), other)), Some{fill}, 183 read_value_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, other, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==}), 184 stored_value(StorageLaws.kept(StorageLaws.created(Shape.count(shape), fill), index), other, fill, 185 StorageLaws.replay_get(Shape.count(shape), fill, [StorageLaws.Read{index}], other, Conversion.shape_count_within(shape), word_inside(shape, other, inside)))) 186 187 def read_point_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> 188 {Observation.point(shape, index, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{fill} : Maybe<&2, F32>}: 189 Equal.trans(Maybe<&2, F32>, 190 Core.read_value(shape, Core.read_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==})), 191 Lifecycle.read_value(Storage.get(StorageLaws.created(Shape.count(shape), fill), index)), Some{fill}, 192 Core.read_result_value(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, Storage.get(StorageLaws.created(Shape.count(shape), fill), index), {==}), 193 stored_value(StorageLaws.created(Shape.count(shape), fill), index, fill, 194 StorageLaws.replay_get(Shape.count(shape), fill, [], index, Conversion.shape_count_within(shape), word_inside(shape, index, inside)))) 195 196 def read_contract(+shape: Shape.Shape, +fill: F32, +index: U32, -expected: Result<&2, &2, Storage.Error, F32>, 197 read: {StorageLaws.read(StorageLaws.created(Shape.count(shape), fill), index) == expected : Result<&2, &2, Storage.Error, F32>}) -> 198 Laws.ReadContract: 199 Laws.ReadContract{ 200 new_lift(shape, fill, result => {Observation.read_code(shape, index, result) == Some{Observation.read_status(Core.storage_read_error(expected))} : Maybe<&2, U32>}, 201 valid => read_code_done(shape, fill, valid, index, expected, read)), 202 new_lift(shape, fill, result => {Observation.after_dimensions(shape, index, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}, 203 valid => read_dimensions_pair(shape, Core.read_flat(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}, index))), 204 new_lift(shape, fill, result => {Observation.after_length(shape, index, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}, 205 valid => read_length_done(shape, fill, valid, index)), 206 new_lift(shape, fill, result => {Observation.after_count(shape, index, result) == Some{Shape.count(shape)} : Maybe<&2, U32>}, 207 valid => read_count_pair(shape, Core.read_flat(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}, index))), 208 other => inside => new_lift(shape, fill, result => {Observation.after_value(shape, index, other, result) == Some{fill} : Maybe<&2, F32>}, 209 valid => read_after_done(shape, fill, valid, index, other, inside))} 210 211 def dynamic_point_result(+shape: Shape.Shape, +index: U32, result: Result<&2, &1, Core.Error, Core.Tensor>) -> 212 {Observation.dynamic_point(shape, index, result) == Observation.point(shape, index, result) : Maybe<&2, F32>}: 213 match result: 214 case Fail{error}: 215 {==} 216 case Done{tensor}: 217 Core.dynamic_result_value(shape, Core.read_flat(shape, tensor, index)) 218 219 def read_inside(+shape: Shape.Shape, +fill: F32, +index: U32, 220 inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> Laws.ReadInside: 221 +inside = inside 222 Laws.ReadInside{ 223 read_contract(shape, fill, index, Done{fill}, 224 StorageLaws.replay_get(Shape.count(shape), fill, [], index, Conversion.shape_count_within(shape), word_inside(shape, index, inside))), 225 new_lift(shape, fill, result => {Observation.point(shape, index, result) == Some{fill} : Maybe<&2, F32>}, 226 valid => read_point_done(shape, fill, valid, index, inside))} 227 228 def read_outside(+shape: Shape.Shape, +fill: F32, +index: U32, 229 outside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}) -> Laws.ReadContract: 230 read_contract(shape, fill, index, Fail{Storage.OutOfBounds{}}, 231 StorageLaws.get_outside(StorageLaws.created(Shape.count(shape), fill), index, size_outside(shape, fill, index, outside))) 232 233 def dynamic_read_inside(+shape: Shape.Shape, +fill: F32, +index: U32, 234 inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> 235 {Observation.dynamic_point(shape, index, Core.new(shape, fill)) == Some{fill} : Maybe<&2, F32>}: 236 Equal.trans(Maybe<&2, F32>, Observation.dynamic_point(shape, index, Core.new(shape, fill)), Observation.point(shape, index, Core.new(shape, fill)), Some{fill}, 237 dynamic_point_result(shape, index, Core.new(shape, fill)), 238 new_lift(shape, fill, result => {Observation.point(shape, index, result) == Some{fill} : Maybe<&2, F32>}, 239 valid => read_point_done(shape, fill, valid, index, inside)))