1 import Base 2 import ../../shape/core.bend as Shape 3 import ../../shape/index_proofs.bend as Index 4 import ../../shape/nat_proofs.bend as Nats 5 import ../../storage/model.bend as Model 6 import ../../storage/main.bend as Storage 7 import ../../storage/LAWS.bend as StorageLaws 8 import ../../storage/array.bend as ArrayCore 9 import ../../storage/refinement.bend as Refinement 10 import ../../storage/api.bend as Api 11 import ../../storage/arith.bend as Arith 12 import ../../storage/route.bend as Route 13 import ../lifecycle.bend as Lifecycle 14 import ../word_conversion.bend as Conversion 15 import ./replayed.bend as Replayed 16 import ./binary_storage_proof.bend as Owned 17 18 # Facts the exports of the parallel builds share: natural-number facts about 19 # the positions of a balanced tree, and two lifts of replayed storages. The 20 # elementwise export (binary_proofs.bend) and the permute export 21 # (../permute_build_proof.bend) use them. 22 23 def 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 30 def 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 37 def 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 # k < b gives b < 1 + k false. 47 48 def 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 59 def 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 # 1 + b <= k gives b < k. 71 72 def 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 83 def 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 95 def 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 103 def 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 115 def 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 120 def 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 # A word index below the storage length is the offset of its own route. 128 129 def 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 # The output spec: cell `base` of the tree holds the family cell below 142 # `count` and +0.0 above it. 143 144 def 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 # A replayed tensor with a cell is an owned storage whose array is `arr` of 152 # its normalized history. 153 def 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 # Both inputs are owned storages in normal form and the output storage is 169 # owned: the parallel build returns the replayed output of the family 170 # history, and the inputs come back as the First halves of their clones.