1 import Base 2 import ../../shape/core.bend as Shape 3 import ../../shape/LAWS.bend as ShapeLaws 4 import ../../shape/plan_proofs.bend as PlanProof 5 import ../../shape/index_proofs.bend as Index 6 import ../../storage/model.bend as Model 7 import ../../storage/main.bend as Storage 8 import ../../storage/LAWS.bend as StorageLaws 9 import ../../storage/array.bend as ArrayCore 10 import ../../storage/refinement.bend as Refinement 11 import ../../storage/certificates.bend as Certificates 12 import ../../storage/api.bend as Api 13 import ../../storage/arith.bend as Arith 14 import ../core.bend as Core 15 import ../lifecycle.bend as Lifecycle 16 import ../elementwise.bend as Elementwise 17 import ../word_conversion.bend as Conversion 18 import ../read_contract.bend as Reads 19 import ../from_values_contract.bend as FromValues 20 import ./replayed.bend as Replayed 21 import ./pointwise.bend as Pointwise 22 import ./pointwise_proof.bend as PointwiseProof 23 import ./broadcast.bend as Broadcast 24 import ./broadcast_proof.bend as BroadcastProof 25 import ./LAWS.bend as Contracts 26 import ./binary_LAWS.bend as Laws 27 import ./binary_build_proof.bend as Build 28 import ./binary_storage_proof.bend as Owned 29 import ./build_facts.bend as Facts 30 31 def cell(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +index: Nat) -> F32: 32 Pointwise.cell(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, index) 33 34 def out_leaf(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +position: Nat, inside: Bool) -> F32: 35 match inside: 36 case False{}: 37 0.0 38 case True{}: 39 cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, position) 40 41 def out_spec(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +count: Nat, +depth: Nat, +base: Nat) -> Array: 42 match depth: 43 case 0n: 44 ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, base, Nat.is_lt(base, count))} 45 case 1n+inner: 46 ANode{out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, inner, base), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, inner, Nat.add(Model.capacity(inner), base))} 47 48 def out_balanced(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +count: Nat, +depth: Nat, +base: Nat) -> Model.Balanced(F32, depth, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, depth, base)): 49 match depth: 50 case 0n: 51 Unit{} 52 case 1n+inner: 53 (out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, inner, base), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, inner, Nat.add(Model.capacity(inner), base))) 54 55 def new_spec(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +depth: Nat, +base: Nat) -> {Array.new(F32, depth, 0.0) == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, depth, base) : Array}: 56 match depth: 57 case 0n: 58 %Equal.sym(Bool, Nat.is_lt(base, 0n), False{}, Facts.lt_zero_false(base)) : 59 {ALeaf{0.0} == ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, base, _)} : Array} 60 {==} 61 case 1n+inner: 62 %Equal.sym(Array, Array.new(F32, inner, 0.0), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, inner, base), new_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, inner, base)) : 63 {ANode{_, Array.new(F32, inner, 0.0)} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, 1n+inner, base) : Array} 64 %Equal.sym(Array, Array.new(F32, inner, 0.0), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, inner, Nat.add(Model.capacity(inner), base)), 65 new_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, inner, Nat.add(Model.capacity(inner), base))) : 66 {ANode{out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, inner, base), _} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, 1n+inner, base) : Array} 67 {==} 68 69 # A subtree whose positions all lie above k is the same for k and 1 + k. 70 def above(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +k: Nat, +depth: Nat, +b: Nat, +h: {Nat.is_lt(k, b) == True{} : Bool}) -> 71 {out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, depth, b) == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, depth, b) : Array}: 72 match depth: 73 case 0n: 74 %Equal.sym(Bool, Nat.is_lt(b, k), False{}, Facts.lt_asym(k, b, h)) : 75 {ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, b, _)} == ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, b, Nat.is_lt(b, 1n+k))} : Array} 76 %Equal.sym(Bool, Nat.is_lt(b, 1n+k), False{}, Facts.above_false(k, b, h)) : 77 {ALeaf{0.0} == ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, b, _)} : Array} 78 {==} 79 case 1n+inner: 80 +high = Nat.add(Model.capacity(inner), b) 81 %Equal.sym(Array, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, b), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, b), above(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, b, h)) : 82 {ANode{_, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high)} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, b) : Array} 83 %Equal.sym(Array, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, high), 84 above(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high, Arith.lt_le_trans(k, b, high, h, Api.le_add_left(Model.capacity(inner), b)))) : 85 {ANode{out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, b), _} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, b) : Array} 86 {==} 87 88 # A subtree whose positions all lie below k is the same for k and 1 + k. 89 def below(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +k: Nat, +depth: Nat, +b: Nat, +h: {Nat.is_le(Nat.add(Model.capacity(depth), b), k) == True{} : Bool}) -> 90 {out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, depth, b) == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, depth, b) : Array}: 91 match depth: 92 case 0n: 93 +lower = Facts.below_true(b, k, h) 94 %Equal.sym(Bool, Nat.is_lt(b, k), True{}, lower) : 95 {ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, b, _)} == ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, b, Nat.is_lt(b, 1n+k))} : Array} 96 %Equal.sym(Bool, Nat.is_lt(b, 1n+k), True{}, Facts.lt_succ_right(b, k, lower)) : 97 {ALeaf{cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, b)} == ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, b, _)} : Array} 98 {==} 99 case 1n+inner: 100 +c = Model.capacity(inner) 101 +high = Nat.add(c, b) 102 +nested = Equal.trans(Bool, Nat.is_le(Nat.add(c, high), k), Nat.is_le(Nat.add(Nat.add(c, c), b), k), True{}, 103 Equal.cong(Nat, Bool, x => Nat.is_le(x, k), Nat.add(c, high), Nat.add(Nat.add(c, c), b), Index.add_assoc(c, c, b)), h) 104 +low_h = Facts.le_trans(high, Nat.add(c, high), k, Facts.le_add_cong(c, b, high, Api.le_add_left(c, b)), nested) 105 %Equal.sym(Array, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, b), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, b), below(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, b, low_h)) : 106 {ANode{_, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high)} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, b) : Array} 107 %Equal.sym(Array, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, high), below(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high, nested)) : 108 {ANode{out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, b), _} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, b) : Array} 109 {==} 110 111 # Writing cell k at the path whose position is k turns the spec for k into 112 # the spec for 1 + k. 113 def write_spec(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +k: Nat, +depth: Nat, +base: Nat, +path: Model.Path(depth), 114 +h: {Nat.add(Model.offset(depth, path), base) == k : Nat}) -> 115 {ArrayCore.write_path(F32, depth, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, depth, base), path, cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k)) == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, depth, base) : Array}: 116 match depth: 117 case 0n: 118 %h : {ALeaf{cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, _)} == ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, base, Nat.is_lt(base, 1n+_))} : Array} 119 %Equal.sym(Bool, Nat.is_lt(base, 1n+base), True{}, Facts.lt_self_succ(base)) : 120 {ALeaf{cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, base)} == ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, base, _)} : Array} 121 {==} 122 case 1n+inner: 123 Model.Step{+bit, +rest} = path 124 match bit: 125 case False{}: 126 +c = Model.capacity(inner) 127 +high = Nat.add(c, base) 128 +inside = Equal.trans(Bool, Nat.is_lt(k, high), Nat.is_lt(Nat.add(Model.offset(inner, rest), base), high), True{}, 129 Equal.cong(Nat, Bool, x => Nat.is_lt(x, high), k, Nat.add(Model.offset(inner, rest), base), 130 Equal.sym(Nat, Nat.add(Model.offset(inner, rest), base), k, h)), 131 Facts.lt_add_right(Model.offset(inner, rest), c, base, Api.offset_lt(inner, rest))) 132 %Equal.sym(Array, ArrayCore.write_path(F32, inner, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, base), rest, cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k)), 133 out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, base), write_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, base, rest, h)) : 134 {ANode{_, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high)} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, base) : Array} 135 %Equal.sym(Array, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, high), above(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high, inside)) : 136 {ANode{out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, base), _} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, base) : Array} 137 {==} 138 case True{}: 139 +c = Model.capacity(inner) 140 +high = Nat.add(c, base) 141 +off = Model.offset(inner, rest) 142 +lower = Equal.trans(Bool, Nat.is_le(high, k), Nat.is_le(high, Nat.add(c, Nat.add(off, base))), True{}, 143 Equal.cong(Nat, Bool, x => Nat.is_le(high, x), k, Nat.add(c, Nat.add(off, base)), 144 Equal.trans(Nat, k, Nat.add(Nat.add(c, off), base), Nat.add(c, Nat.add(off, base)), 145 Equal.sym(Nat, Nat.add(Nat.add(c, off), base), k, h), 146 Equal.sym(Nat, Nat.add(c, Nat.add(off, base)), Nat.add(Nat.add(c, off), base), Index.add_assoc(c, off, base)))), 147 Facts.le_add_cong(c, base, Nat.add(off, base), Api.le_add_left(off, base))) 148 +shifted = Equal.trans(Nat, Nat.add(off, high), Nat.add(Nat.add(c, off), base), k, Facts.position_step(c, off, base), h) 149 %Equal.sym(Array, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, base), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, base), below(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, base, lower)) : 150 {ANode{_, ArrayCore.write_path(F32, inner, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), rest, cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k))} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, base) : Array} 151 %Equal.sym(Array, ArrayCore.write_path(F32, inner, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), rest, cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k)), 152 out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, high), write_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high, rest, shifted)) : 153 {ANode{out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, base), _} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, base) : Array} 154 {==} 155 156 # The family history, replayed on the owned storage that `created` makes, 157 # is the owned storage that holds the output spec. 158 def chain(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +d: Nat, +n: Nat, -f: {Storage.bounds(d, n) == True{} : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool}, 159 +limit: U32, +n_limit: {Nat.is_le(n, U32.to_nat(limit)) == True{} : Bool}, 160 +k: Nat, +room: {Nat.is_le(k, n) == True{} : Bool}) -> 161 {StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, k, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}) == Storage.Owned{d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, d, 0n), f} : Storage.Storage}: 162 match k: 163 case 0n: 164 Owned.owned_eq(d, n, Array.new(F32, d, 0.0), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, d, 0n), new_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, d, 0n), ArrayCore.new_balanced(F32, d, 0.0), f)( 165 out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, d, 0n)) 166 case 1n+j: 167 +index = U32.from_nat(j) 168 +value = cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j) 169 +below_n = Conversion.le_successor_lt(j, n, room) 170 +exact = Conversion.natural_word_exact(j, limit, Facts.le_trans(j, n, U32.to_nat(limit), Conversion.lt_le(j, n, below_n), n_limit)) 171 +inside = Equal.trans(Bool, Nat.is_lt(U32.to_nat(index), n), Nat.is_lt(j, n), True{}, 172 Equal.cong(Nat, Bool, x => Nat.is_lt(x, n), U32.to_nat(index), j, exact), below_n) 173 +offset = Equal.trans(Nat, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), U32.to_nat(index), j, 174 Facts.output_position(d, n, index, fits, inside), exact) 175 +written = Equal.trans(Array, Array.set(F32, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), ArrayCore.write_path(F32, d, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), Refinement.route(d, index), value), 176 out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), Refinement.law_set_refines(F32, d, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n)), 177 write_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n, Refinement.route(d, index), offset)) 178 Equal.trans(Storage.Storage, StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, 1n+j, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), 179 StorageLaws.step(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, j, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), StorageLaws.Write{index, value}), 180 Storage.Owned{d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), f}, 181 FromValues.replay_snoc(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, j, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), StorageLaws.Write{index, value}, Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), 182 %Equal.sym(Storage.Storage, StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, j, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), Storage.Owned{d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), f}, 183 chain(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, d, n, f, fits, limit, n_limit, j, Conversion.le_predecessor(j, n, room))) : 184 {StorageLaws.step(_, StorageLaws.Write{index, value}) == Storage.Owned{d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), f} : Storage.Storage} 185 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, 186 Storage.set_checked(d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Nat.is_lt(U32.to_nat(index), n), {==}, out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), f), 187 (Storage.Owned{d, n, Array.set(F32, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), 188 Certificates.set_result(F32, d, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Array.set(F32, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), {==}, out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n)), f}, Done{Unit{}}), 189 Api.set_checked_hit(d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Nat.is_lt(U32.to_nat(index), n), {==}, out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), f, 190 Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), n), True{}, inside), fits, inside)) : 191 {StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, _) == Storage.Owned{d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), f} : Storage.Storage} 192 Owned.owned_eq(d, n, Array.set(F32, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), written, 193 Certificates.set_result(F32, d, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Array.set(F32, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), {==}, out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n)), f)( 194 out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n))) 195 196 # The plan's input shapes have the inputs' dimensions. 197 def left_dims(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan, 198 +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}) -> 199 {Shape.dimensions(Shape.left_shape(plan)) == Shape.dimensions(left) : List<&2, U32>}: 200 Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, p => Pair.fst(List<&2, U32>, List<&2, U32>, p), 201 (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(left), Shape.dimensions(right)), 202 %planned : {ShapeLaws.planned_dimensions(left, right, _) == (Shape.dimensions(left), Shape.dimensions(right)) : List<&2, U32> & List<&2, U32>} 203 PlanProof.broadcast_checked_plan(left, right)) 204 205 def right_dims(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan, 206 +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}) -> 207 {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(right) : List<&2, U32>}: 208 Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, p => Pair.snd(List<&2, U32>, List<&2, U32>, p), 209 (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(left), Shape.dimensions(right)), 210 %planned : {ShapeLaws.planned_dimensions(left, right, _) == (Shape.dimensions(left), Shape.dimensions(right)) : List<&2, U32> & List<&2, U32>} 211 PlanProof.broadcast_checked_plan(left, right)) 212 213 def left_count(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan, 214 +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}) -> 215 {U32.to_nat(Shape.count(left)) == Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan))) : Nat}: 216 Equal.trans(Nat, U32.to_nat(Shape.count(left)), Shape.logical_numel(Shape.dimensions(left)), Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan))), Reads.count_exact(left), 217 Equal.cong(List<&2, U32>, Nat, dims => Shape.logical_numel(dims), Shape.dimensions(left), Shape.dimensions(Shape.left_shape(plan)), 218 Equal.sym(List<&2, U32>, Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(left), left_dims(left, right, plan, planned)))) 219 220 def right_count(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan, 221 +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}) -> 222 {U32.to_nat(Shape.count(right)) == Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan))) : Nat}: 223 Equal.trans(Nat, U32.to_nat(Shape.count(right)), Shape.logical_numel(Shape.dimensions(right)), Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan))), Reads.count_exact(right), 224 Equal.cong(List<&2, U32>, Nat, dims => Shape.logical_numel(dims), Shape.dimensions(right), Shape.dimensions(Shape.right_shape(plan)), 225 Equal.sym(List<&2, U32>, Shape.dimensions(Shape.right_shape(plan)), Shape.dimensions(right), right_dims(left, right, plan, planned)))) 226 227 def scalar_cong(+operation: Elementwise.Operation, -x: F32, -y: F32, -u: F32, -v: F32, ex: {x == y : F32}, eu: {u == v : F32}) -> 228 {Elementwise.scalar(operation, x, u) == Elementwise.scalar(operation, y, v) : F32}: 229 %ex : {Elementwise.scalar(operation, x, u) == Elementwise.scalar(operation, _, v) : F32} 230 %eu : {Elementwise.scalar(operation, x, u) == Elementwise.scalar(operation, x, _) : F32} 231 {==} 232 233 # The build's leaf reads the replayed words the family cell names. 234 def leaf_same(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +dl: Nat, +dr: Nat, +position: Nat, inside: Bool) -> 235 {Build.leaf(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), position, inside) == out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, position, inside) : F32}: 236 match inside: 237 case False{}: 238 {==} 239 case True{}: 240 +li = Build.left_index(plan, position) 241 +ri = Build.right_index(plan, position) 242 +bli = U32.from_nat(Broadcast.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position)) 243 +bri = U32.from_nat(Broadcast.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position)) 244 Equal.trans(F32, Build.word(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), position), 245 Elementwise.scalar(operation, StorageLaws.expected(left_ops, U32.to_nat(Shape.count(left)), li, left_fill), StorageLaws.expected(right_ops, U32.to_nat(Shape.count(right)), ri, right_fill)), 246 cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, position), 247 scalar_cong(operation, Api.current(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), li, left_fill), StorageLaws.expected(left_ops, U32.to_nat(Shape.count(left)), li, left_fill), 248 Api.current(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), ri, right_fill), StorageLaws.expected(right_ops, U32.to_nat(Shape.count(right)), ri, right_fill), 249 Owned.norm_current(U32.to_nat(Shape.count(left)), left_ops, Nil{}, li, left_fill, Api.hit_of(U32.to_nat(Shape.count(left)), left_ops), {==}), 250 Owned.norm_current(U32.to_nat(Shape.count(right)), right_ops, Nil{}, ri, right_fill, Api.hit_of(U32.to_nat(Shape.count(right)), right_ops), {==})), 251 scalar_cong(operation, StorageLaws.expected(left_ops, U32.to_nat(Shape.count(left)), li, left_fill), StorageLaws.expected(left_ops, U32.to_nat(Shape.count(left)), bli, left_fill), 252 StorageLaws.expected(right_ops, U32.to_nat(Shape.count(right)), ri, right_fill), StorageLaws.expected(right_ops, U32.to_nat(Shape.count(right)), bri, right_fill), 253 Equal.cong(Nat, F32, w => StorageLaws.expected(left_ops, U32.to_nat(Shape.count(left)), U32.from_nat(w), left_fill), 254 Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position), Broadcast.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position), Build.walk_left_same(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position)), 255 Equal.cong(Nat, F32, w => StorageLaws.expected(right_ops, U32.to_nat(Shape.count(right)), U32.from_nat(w), right_fill), 256 Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position), Broadcast.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position), Build.walk_right_same(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position)))) 257 258 def spec_same(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +dl: Nat, +dr: Nat, +depth: Nat, +base: Nat) -> 259 {Build.spec(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), depth, base) == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), depth, base) : Array}: 260 match depth: 261 case 0n: 262 Equal.cong(F32, Array, x => ALeaf{x}, Build.leaf(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), base, Nat.is_lt(base, U32.to_nat(Shape.count(Shape.output_shape(plan))))), out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, base, Nat.is_lt(base, U32.to_nat(Shape.count(Shape.output_shape(plan))))), 263 leaf_same(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, dl, dr, base, Nat.is_lt(base, U32.to_nat(Shape.count(Shape.output_shape(plan)))))) 264 case 1n+inner: 265 +high = Nat.add(Model.capacity(inner), base) 266 %Equal.sym(Array, Build.spec(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), inner, base), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), inner, base), spec_same(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, dl, dr, inner, base)) : 267 {ANode{_, Build.spec(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), inner, high)} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), 1n+inner, base) : Array} 268 %Equal.sym(Array, Build.spec(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), inner, high), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), inner, high), spec_same(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, dl, dr, inner, high)) : 269 {ANode{out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), inner, base), _} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), 1n+inner, base) : Array} 270 {==} 271 272 def cells_snoc(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +previous: Nat, +before: List<&2, F32>, +word: F32, +other: F32, 273 rest: {before == Laws.cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous) : List<&2, F32>}, last: {word == other : F32}) -> 274 {List.append(&2, F32, before, [word]) == List.append(&2, F32, Laws.cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous), [other]) : List<&2, F32>}: 275 Equal.trans(List<&2, F32>, List.append(&2, F32, before, [word]), List.append(&2, F32, Laws.cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous), [word]), 276 List.append(&2, F32, Laws.cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous), [other]), 277 Equal.cong(List<&2, F32>, List<&2, F32>, values => List.append(&2, F32, values, [word]), before, Laws.cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous), rest), 278 Equal.cong(F32, List<&2, F32>, value => List.append(&2, F32, Laws.cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous), [value]), word, other, last)) 279 280 # The words of the family history are `cells`. 281 def words_cells(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +count: Nat, +room: {Nat.is_le(count, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) == True{} : Bool}) -> 282 {Contracts.words(Shape.output_shape(plan), 0.0, Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), count) == Laws.cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count) : List<&2, F32>}: 283 match count: 284 case 0n: 285 {==} 286 case 1n+previous: 287 +output = Shape.output_shape(plan) 288 +total = Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) 289 +below = Conversion.le_successor_lt(previous, total, room) 290 +position = U32.from_nat(previous) 291 cells_snoc(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous, Contracts.words(output, 0.0, Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), previous), Replayed.value(output, 0.0, Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), position), 292 cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous), words_cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous, Conversion.le_predecessor(previous, total, room)), 293 Equal.trans(F32, Replayed.value(output, 0.0, Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), position), cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(position)), cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous), 294 PointwiseProof.writes_value(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, total, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, output, position, 295 PointwiseProof.word_inside(previous, output, below), Conversion.le_reflexive(total)), 296 Equal.cong(Nat, F32, number => cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, number), U32.to_nat(position), previous, PointwiseProof.word_exact(previous, output, below)))) 297 298 def half_keeps(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +index: U32) -> 299 {Replayed.value(shape, fill, Replayed.snoc(ops, StorageLaws.First{}), index) == Replayed.value(shape, fill, ops, index) : F32}: 300 Replayed.expected_snoc(ops, StorageLaws.First{}, U32.to_nat(Shape.count(shape)), index, fill) 301 302 def words_snoc(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +previous: Nat, +word: F32, +other: F32, 303 +before: List<&2, F32>, rest: {Contracts.words(shape, fill, ops, previous) == before : List<&2, F32>}, last: {word == other : F32}) -> 304 {List.append(&2, F32, Contracts.words(shape, fill, ops, previous), [word]) == List.append(&2, F32, before, [other]) : List<&2, F32>}: 305 Equal.trans(List<&2, F32>, List.append(&2, F32, Contracts.words(shape, fill, ops, previous), [word]), 306 List.append(&2, F32, before, [word]), List.append(&2, F32, before, [other]), 307 Equal.cong(List<&2, F32>, List<&2, F32>, values => List.append(&2, F32, values, [word]), Contracts.words(shape, fill, ops, previous), before, rest), 308 Equal.cong(F32, List<&2, F32>, value => List.append(&2, F32, before, [value]), word, other, last)) 309 310 # The First half of a clone lists the same words. 311 def words_first(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat) -> 312 {Contracts.words(shape, fill, Replayed.snoc(ops, StorageLaws.First{}), count) == Contracts.words(shape, fill, ops, count) : List<&2, F32>}: 313 match count: 314 case 0n: 315 {==} 316 case 1n+previous: 317 +position = U32.from_nat(previous) 318 words_snoc(shape, fill, Replayed.snoc(ops, StorageLaws.First{}), previous, 319 Replayed.value(shape, fill, Replayed.snoc(ops, StorageLaws.First{}), position), Replayed.value(shape, fill, ops, position), 320 Contracts.words(shape, fill, ops, previous), words_first(shape, fill, ops, previous), half_keeps(shape, fill, ops, position)) 321 322 # `take` of an owned tensor hands back the First half of its clone and the 323 # Second half's array. 324 def take_owned_lift(+shape: Shape.Shape, +d: Nat, +n: Nat, -array: Array, pair: Array & Array, 325 -same: {pair == Array.clone(F32, array) : Array & Array}, -b: Model.Balanced(F32, d, array), 326 -f: {Storage.bounds(d, n) == True{} : Bool}, -fits: {n == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, 327 -Q: (Core.Dynamic & Array) -> Type, 328 h: @-kept: {Lifecycle.logical_length(StorageLaws.owner(Storage.Storage, Storage.finish_clone(d, n, array, pair, same, b, f))) == 329 Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> 330 Q((Core.Packed{shape, Core.TTensor{StorageLaws.owner(Storage.Storage, Storage.finish_clone(d, n, array, pair, same, b, f)), kept}}, 331 Pair.snd(Array, Array, pair)))) -> 332 Q(Elementwise.take_owned(shape, d, n, array, pair, same, b, f, fits)): 333 (kept, copy) = pair 334 h(fits) 335 336 def positive_of_lt(+w: Nat, +n: Nat, h: {Nat.is_lt(w, n) == True{} : Bool}) -> {Nat.is_lt(0n, n) == True{} : Bool}: 337 match n: 338 case 0n: 339 Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, Arith.lt_zero(w, h)) 340 case 1n+q: 341 {==} 342 343 def output_positive(+plan: Shape.BroadcastPlan, +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}) -> 344 {Nat.is_lt(0n, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) == True{} : Bool}: 345 Equal.trans(Bool, Nat.is_lt(0n, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))), Nat.is_lt(0n, U32.to_nat(Shape.count(Shape.output_shape(plan)))), True{}, 346 Equal.cong(Nat, Bool, x => Nat.is_lt(0n, x), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), U32.to_nat(Shape.count(Shape.output_shape(plan))), Equal.sym(Nat, U32.to_nat(Shape.count(Shape.output_shape(plan))), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), Reads.count_exact(Shape.output_shape(plan)))), 347 Arith.and_left(Nat.is_lt(0n, U32.to_nat(Shape.count(Shape.output_shape(plan)))), Nat.is_le(U32.to_nat(Shape.count(Shape.output_shape(plan))), Model.capacity(d)), 348 Arith.and_right(Nat.is_le(d, 20n), Bool.and(Nat.is_lt(0n, U32.to_nat(Shape.count(Shape.output_shape(plan)))), Nat.is_le(U32.to_nat(Shape.count(Shape.output_shape(plan))), Model.capacity(d))), fits))) 349 350 # An output with a cell reads a cell of each input, so neither input is empty. 351 def left_positive(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan, 352 +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, 353 +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}) -> {Nat.is_lt(0n, U32.to_nat(Shape.count(left))) == True{} : Bool}: 354 +walk = Broadcast.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), 0n) 355 positive_of_lt(walk, U32.to_nat(Shape.count(left)), 356 Equal.trans(Bool, Nat.is_lt(walk, U32.to_nat(Shape.count(left))), Nat.is_lt(walk, Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan)))), True{}, 357 Equal.cong(Nat, Bool, x => Nat.is_lt(walk, x), U32.to_nat(Shape.count(left)), Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan))), left_count(left, right, plan, planned)), 358 BroadcastProof.left_walk_bound(plan, Shape.index_map(plan), 0n, output_positive(plan, d, fits)))) 359 360 def right_positive(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan, 361 +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, 362 +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}) -> {Nat.is_lt(0n, U32.to_nat(Shape.count(right))) == True{} : Bool}: 363 +walk = Broadcast.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), 0n) 364 positive_of_lt(walk, U32.to_nat(Shape.count(right)), 365 Equal.trans(Bool, Nat.is_lt(walk, U32.to_nat(Shape.count(right))), Nat.is_lt(walk, Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan)))), True{}, 366 Equal.cong(Nat, Bool, x => Nat.is_lt(walk, x), U32.to_nat(Shape.count(right)), Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan))), right_count(left, right, plan, planned)), 367 BroadcastProof.right_walk_bound(plan, Shape.index_map(plan), 0n, output_positive(plan, d, fits)))) 368 369 def output_eq(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, +dl: Nat, +fitsl: {Storage.bounds(dl, U32.to_nat(Shape.count(left))) == True{} : Bool}, 370 +dr: Nat, +fitsr: {Storage.bounds(dr, U32.to_nat(Shape.count(right))) == True{} : Bool}, 371 +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}, -f: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}) -> {StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}) == Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Elementwise.build(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), Elementwise.build_balanced(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), f} : Storage.Storage}: 372 +spec = Equal.trans(Array, Elementwise.build(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), Build.spec(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), d, 0n), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), d, 0n), 373 Build.build_eq(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), fitsl, fitsr, 374 Owned.norm_written(U32.to_nat(Shape.count(left)), left_ops, Nil{}, Api.hit_of(U32.to_nat(Shape.count(left)), left_ops), {==}, {==}), 375 Owned.norm_written(U32.to_nat(Shape.count(right)), right_ops, Nil{}, Api.hit_of(U32.to_nat(Shape.count(right)), right_ops), {==}, {==}), 376 Reads.count_exact(Shape.output_shape(plan)), left_count(left, right, plan, planned), right_count(left, right, plan, planned), 377 d, Elementwise.splits(d), 0n), 378 spec_same(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, dl, dr, d, 0n)) 379 Equal.trans(Storage.Storage, StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, U32.to_nat(Shape.count(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), 380 Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Elementwise.build(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), Elementwise.build_balanced(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), f}, 381 Equal.cong(Nat, Storage.Storage, count => StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, count, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), U32.to_nat(Shape.count(Shape.output_shape(plan))), 382 Equal.sym(Nat, U32.to_nat(Shape.count(Shape.output_shape(plan))), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), Reads.count_exact(Shape.output_shape(plan)))), 383 Equal.trans(Storage.Storage, StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, U32.to_nat(Shape.count(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), d, 0n), f}, 384 Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Elementwise.build(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), Elementwise.build_balanced(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), f}, 385 chain(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fits, Shape.count(Shape.output_shape(plan)), Conversion.le_reflexive(U32.to_nat(Shape.count(Shape.output_shape(plan)))), U32.to_nat(Shape.count(Shape.output_shape(plan))), Conversion.le_reflexive(U32.to_nat(Shape.count(Shape.output_shape(plan))))), 386 Owned.owned_eq(d, U32.to_nat(Shape.count(Shape.output_shape(plan))), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), d, 0n), Elementwise.build(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), Equal.sym(Array, Elementwise.build(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), d, 0n), spec), 387 out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(Shape.output_shape(plan))), d, 0n), f)(Elementwise.build_balanced(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill))))) 388 389 def core(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, +dl: Nat, +fitsl: {Storage.bounds(dl, U32.to_nat(Shape.count(left))) == True{} : Bool}, -bl: Model.Balanced(F32, dl, Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill)), 390 -fl: {Storage.bounds(dl, U32.to_nat(Shape.count(left))) == True{} : Bool}, 391 +dr: Nat, +fitsr: {Storage.bounds(dr, U32.to_nat(Shape.count(right))) == True{} : Bool}, -br: Model.Balanced(F32, dr, Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), 392 -fr: {Storage.bounds(dr, U32.to_nat(Shape.count(right))) == True{} : Bool}, 393 +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}, -f: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}, 394 -P: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type, 395 hyp: @-kl: {Lifecycle.logical_length(StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{})) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @-kr: {Lifecycle.logical_length(StorageLaws.step(Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}, StorageLaws.First{})) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> @-ko: {Lifecycle.logical_length(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f})) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{}), kl}}, Core.Packed{right, Core.TTensor{StorageLaws.step(Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}, StorageLaws.First{}), kr}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f} 396 @-lfits: {Lifecycle.logical_length(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @-rfits: {Lifecycle.logical_length(Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> 397 @-fo: {U32.to_nat(Shape.count(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> 398 P(Elementwise.parallel_output(operation, plan, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fo, Elementwise.take(Core.Packed{left, Core.TTensor{Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, lfits}}), 399 Elementwise.take(Core.Packed{right, Core.TTensor{Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}, rfits}}))): 400 lfits => rfits => fo => 401 take_owned_lift(left, dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Array.clone(F32, Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill)), {==}, bl, fl, lfits, 402 t => P(Elementwise.parallel_output(operation, plan, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fo, t, Elementwise.take(Core.Packed{right, Core.TTensor{Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}, rfits}}))), 403 kl => take_owned_lift(right, dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), Array.clone(F32, Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), {==}, br, fr, rfits, 404 t => P(Elementwise.parallel_output(operation, plan, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fo, (Core.Packed{left, Core.TTensor{StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{}), kl}}, Pair.snd(Array, Array, Array.clone(F32, Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill)))), t)), 405 kr => Facts.storage_shift(Shape.output_shape(plan), StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Elementwise.build(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), Elementwise.build_balanced(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), f}, 406 output_eq(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, planned, dl, fitsl, dr, fitsr, d, fits, f), 407 st => k => P(((Core.Packed{left, Core.TTensor{StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{}), kl}}, Core.Packed{right, Core.TTensor{StorageLaws.step(Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}, StorageLaws.First{}), kr}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{st, k}}})), hyp(kl, kr))(fo))) 408 409 # The output storage is owned: normalize the left input, then the right one, 410 # and run `core`. 411 def owned_case(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, -lfits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat}, 412 -rfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat}, 413 -P: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type, 414 +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}, -f: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}) -> 415 (@+left_kept: List<&2, StorageLaws.Op> -> @left_words: {Contracts.words(left, left_fill, left_kept, Shape.logical_numel(Shape.dimensions(left))) == Contracts.words(left, left_fill, left_ops, Shape.logical_numel(Shape.dimensions(left))) : List<&2, F32>} -> @-left_kfits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_kept)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @+right_kept: List<&2, StorageLaws.Op> -> @right_words: {Contracts.words(right, right_fill, right_kept, Shape.logical_numel(Shape.dimensions(right))) == Contracts.words(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))) : List<&2, F32>} -> @-right_kfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_kept)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> @-ko: {Lifecycle.logical_length(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f})) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_kept), left_kfits}}, Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_kept), right_kfits}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 416 P(Elementwise.parallel_output(operation, plan, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fo, Elementwise.take(Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits})), Elementwise.take(Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits})))): 417 ho => fo => 418 Facts.input_lift(left, left_fill, left_ops, left_positive(left, right, plan, planned, d, fits), 419 sl => (@-lf: {Lifecycle.logical_length(sl) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> (@-kl: {Lifecycle.logical_length(StorageLaws.step(sl, StorageLaws.First{})) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @+right_kept: List<&2, StorageLaws.Op> -> @right_words: {Contracts.words(right, right_fill, right_kept, Shape.logical_numel(Shape.dimensions(right))) == Contracts.words(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))) : List<&2, F32>} -> @-right_kfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_kept)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> @-ko: {Lifecycle.logical_length(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f})) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{StorageLaws.step(sl, StorageLaws.First{}), kl}}, Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_kept), right_kfits}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), ko}}}))) -> 420 P(Elementwise.parallel_output(operation, plan, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fo, Elementwise.take(Core.Packed{left, Core.TTensor{sl, lf}}), Elementwise.take(Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}))))), 421 dl => fitsl => bl => fl => lf => hl => 422 Facts.input_lift(right, right_fill, right_ops, right_positive(left, right, plan, planned, d, fits), 423 sr => (@-rf: {Lifecycle.logical_length(sr) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> (@-kl: {Lifecycle.logical_length(StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{})) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @-kr: {Lifecycle.logical_length(StorageLaws.step(sr, StorageLaws.First{})) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> @-ko: {Lifecycle.logical_length(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f})) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{}), kl}}, Core.Packed{right, Core.TTensor{StorageLaws.step(sr, StorageLaws.First{}), kr}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), ko}}}))) -> 424 P(Elementwise.parallel_output(operation, plan, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fo, Elementwise.take(Core.Packed{left, Core.TTensor{Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, lf}}), 425 Elementwise.take(Core.Packed{right, Core.TTensor{sr, rf}})))), 426 dr => fitsr => br => fr => rf => hr => core(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, planned, dl, fitsl, bl, fl, dr, fitsr, br, fr, d, fits, f, P, hr)(lf, rf, fo))( 427 rfits, 428 kl => Facts.storage_shift(right, Replayed.storage(right, right_fill, Replayed.snoc(right_ops, StorageLaws.First{})), 429 StorageLaws.step(Replayed.storage(right, right_fill, right_ops), StorageLaws.First{}), Replayed.replay_snoc(right_ops, StorageLaws.First{}, right, right_fill), 430 st => k => (@-ko: {Lifecycle.logical_length(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f})) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{}), kl}}, Core.Packed{right, Core.TTensor{st, k}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), ko}}}))), 431 rk => hl(kl, Replayed.snoc(right_ops, StorageLaws.First{}), words_first(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))), rk))))( 432 lfits, 433 Facts.storage_shift(left, Replayed.storage(left, left_fill, Replayed.snoc(left_ops, StorageLaws.First{})), 434 StorageLaws.step(Replayed.storage(left, left_fill, left_ops), StorageLaws.First{}), Replayed.replay_snoc(left_ops, StorageLaws.First{}, left, left_fill), 435 st => k => (@+right_kept: List<&2, StorageLaws.Op> -> @right_words: {Contracts.words(right, right_fill, right_kept, Shape.logical_numel(Shape.dimensions(right))) == Contracts.words(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))) : List<&2, F32>} -> @-right_kfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_kept)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> @-ko: {Lifecycle.logical_length(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f})) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{st, k}}, Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_kept), right_kfits}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), ko}}}))), 436 lk => ho(Replayed.snoc(left_ops, StorageLaws.First{}), words_first(left, left_fill, left_ops, Shape.logical_numel(Shape.dimensions(left))), lk))) 437 438 # The parallel build on two replayed inputs into an output that `Core.new` 439 # allocates: binary_replayed below the planner, which broadcast_to shares. 440 def allocated_replayed(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, -P: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type, 441 h: Laws.BinaryWith(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, P)) -> 442 @-lfits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @-rfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> 443 P(Elementwise.parallel_allocated(operation, plan, Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}), Core.new(Shape.output_shape(plan), 0.0))): 444 lfits => rfits => 445 Replayed.new_lift(Shape.output_shape(plan), 0.0, result => P(Elementwise.parallel_allocated(operation, plan, Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}), result)), 446 fo => Owned.created_lift(Shape.count(Shape.output_shape(plan)), 0.0, Conversion.shape_count_within(Shape.output_shape(plan)), 447 s => ((@+left_kept: List<&2, StorageLaws.Op> -> @left_words: {Contracts.words(left, left_fill, left_kept, Shape.logical_numel(Shape.dimensions(left))) == Contracts.words(left, left_fill, left_ops, Shape.logical_numel(Shape.dimensions(left))) : List<&2, F32>} -> @-left_kfits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_kept)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @+right_kept: List<&2, StorageLaws.Op> -> @right_words: {Contracts.words(right, right_fill, right_kept, Shape.logical_numel(Shape.dimensions(right))) == Contracts.words(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))) : List<&2, F32>} -> @-right_kfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_kept)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> @-ko: {Lifecycle.logical_length(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), s)) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_kept), left_kfits}}, Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_kept), right_kfits}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), s), ko}}}))) -> @-fo: {Lifecycle.logical_length(s) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> 448 P(Elementwise.parallel_allocated(operation, plan, Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}), Done{Core.TTensor{s, fo}}))), 449 zero => ho => fo => 450 Facts.storage_shift(Shape.output_shape(plan), StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Empty{}), Storage.Empty{}, Owned.replay_empty(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops)), 451 st => k => P(((Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits})), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{st, k}}})), 452 ho(left_ops, {==}, lfits, right_ops, {==}, rfits))(fo), 453 d => fits => f => owned_case(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, planned, lfits, rfits, P, d, fits, f))( 454 left_kept => left_words => left_kfits => right_kept => right_words => right_kfits => ko => 455 h(left_kept, left_words, left_kfits, right_kept, right_words, right_kfits, Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), 456 words_cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), Conversion.le_reflexive(Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))))), ko), fo)) 457 458 def binary_replayed(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, -P: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type, 459 h: Laws.BinaryWith(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, P)) -> 460 @-lfits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @-rfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> 461 P(Elementwise.binary(operation, Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}}, Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}})): 462 lfits => rfits => 463 %Equal.sym(Result<&2, &2, Shape.Error, Shape.BroadcastPlan>, Shape.broadcast_checked(left, right), Done{plan}, planned) : 464 P(Elementwise.parallel_planned(operation, Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}), _)) 465 allocated_replayed(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, planned, P, h)(lfits, rfits)