1 import Base 2 import ../shape/core.bend as Shape 3 import ../shape/flat.bend as Flat 4 import ../shape/nat_proofs.bend as Nats 5 import ../shape/index_proofs.bend as Index 6 import ../shape/plan_proofs.bend as PlanProof 7 import ../shape/LAWS.bend as ShapeLaws 8 # Proves the shape laws that importing ShapeLaws would otherwise leave open. 9 import ../shape/PROOF.bend as ShapeProof 10 import ../storage/model.bend as Model 11 import ../storage/refinement.bend as Refinement 12 import ../storage/clone.bend as Clone 13 import ../storage/arith.bend as Arith 14 import ../storage/main.bend as Storage 15 import ../storage/route.bend as Route 16 import ../storage/certificates.bend as Certificates 17 import ./core.bend as Core 18 import ./lifecycle.bend as Lifecycle 19 import ./elementwise.bend as Elementwise 20 import ./elementwise_totality.bend as Totality 21 import ./word_conversion.bend as WordConversion 22 import ./parallel_proofs.bend as Generic 23 import ./elementwise_walk_proof.bend as WalkProof 24 25 # Proofs that the parallel elementwise build writes, at every output index, 26 # the value `Elementwise.expected` names there. 27 28 type Fact<-P: Type> is Data: 29 Fact{-proof: P} 30 31 # The value a cell gets from the two observed input cells. 32 def pick(operation: Elementwise.Operation, left: Maybe<&2, F32>, right: Maybe<&2, F32>) -> Maybe<&2, F32>: 33 match left: 34 case None{}: 35 None{} 36 case Some{value}: 37 Elementwise.expected_right(operation, value, right) 38 39 def want(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, A: Array, B: Array, +position: Nat) -> 40 Maybe<&2, F32>: 41 pick(operation, Model.observe(F32, dl, A, Refinement.route(dl, U32.from_nat(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)))), Model.observe(F32, dr, B, Refinement.route(dr, U32.from_nat(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))))) 42 43 def transport_balanced(-d: Nat, -a: Array, -b: Array, -same: {a == b : Array}, -valid: Model.Balanced(F32, d, b)) -> 44 Fact: 45 Fact{ 46 %Equal.sym(Array, a, b, same) : Model.Balanced(F32, d, _) 47 valid} 48 49 # A read keeps the array and returns the observed cell. 50 def read_keeps(-d: Nat, -original: Array, -target: Array, -i: U32, -pair: Array & F32, 51 -exact: {pair == Array.get(F32, original, i) : Array & F32}, -same: {original == target : Array}, 52 -valid: Model.Balanced(F32, d, target)) -> Fact<{Refinement.first(F32, pair) == target : Array}>: 53 Fact{Equal.trans(Array, Refinement.first(F32, pair), Refinement.first(F32, Array.get(F32, original, i)), target, 54 Equal.cong(Array & F32, Array, p => Refinement.first(F32, p), pair, Array.get(F32, original, i), exact), 55 Equal.trans(Array, Refinement.first(F32, Array.get(F32, original, i)), original, target, 56 Refinement.law_get_retains(F32, d, original, i, {\{Fact: p => p} : Fact<(Model.Balanced(F32, d, original))> -> Model.Balanced(F32, d, original)}(transport_balanced(d, original, target, same, valid))), 57 same))} 58 59 def read_value(-d: Nat, -original: Array, -target: Array, -i: U32, -pair: Array & F32, 60 -exact: {pair == Array.get(F32, original, i) : Array & F32}, -same: {original == target : Array}, 61 -valid: Model.Balanced(F32, d, target)) -> 62 Fact<{Some{Refinement.second(F32, pair)} == Model.observe(F32, d, target, Refinement.route(d, i)) : Maybe<&2, F32>}>: 63 Fact{Equal.trans(Maybe<&2, F32>, Some{Refinement.second(F32, pair)}, Some{Refinement.second(F32, Array.get(F32, original, i))}, 64 Model.observe(F32, d, target, Refinement.route(d, i)), 65 Equal.cong(Array & F32, Maybe<&2, F32>, p => Some{Refinement.second(F32, p)}, pair, Array.get(F32, original, i), exact), 66 Equal.trans(Maybe<&2, F32>, Some{Refinement.second(F32, Array.get(F32, original, i))}, 67 Model.observe(F32, d, original, Refinement.route(d, i)), Model.observe(F32, d, target, Refinement.route(d, i)), 68 Refinement.law_get_refines(F32, d, original, i, {\{Fact: p => p} : Fact<(Model.Balanced(F32, d, original))> -> Model.Balanced(F32, d, original)}(transport_balanced(d, original, target, same, valid))), 69 Equal.cong(Array, Maybe<&2, F32>, a => Model.observe(F32, d, a, Refinement.route(d, i)), original, target, same)))} 70 71 def pick_value(+operation: Elementwise.Operation, -x: F32, -y: F32, -lm: Maybe<&2, F32>, -rm: Maybe<&2, F32>, 72 -ex: {Some{x} == lm : Maybe<&2, F32>}, -ey: {Some{y} == rm : Maybe<&2, F32>}) -> 73 Fact<{Some{Elementwise.scalar(operation, x, y)} == pick(operation, lm, rm) : Maybe<&2, F32>}>: 74 Fact{ 75 %ex : {Some{Elementwise.scalar(operation, x, y)} == pick(operation, _, rm) : Maybe<&2, F32>} 76 %ey : {Some{Elementwise.scalar(operation, x, y)} == Elementwise.expected_right(operation, x, _) : Maybe<&2, F32>} 77 {==}} 78 79 def clone_first(-d: Nat, -original: Array, -target: Array, -pair: Array & Array, 80 -exact: {pair == Array.clone(F32, original) : Array & Array}, -same: {original == target : Array}, 81 -valid: Model.Balanced(F32, d, target)) -> Fact<{Pair.fst(Array, Array, pair) == target : Array}>: 82 Fact{Equal.trans(Array, Pair.fst(Array, Array, pair), Pair.fst(Array, Array, Array.clone(F32, original)), target, 83 Equal.cong(Array & Array, Array, p => Pair.fst(Array, Array, p), pair, Array.clone(F32, original), exact), 84 Equal.trans(Array, Pair.fst(Array, Array, Array.clone(F32, original)), original, target, 85 Clone.first_equal(F32, d, original, Clone.certify(F32, d, original, {\{Fact: p => p} : Fact<(Model.Balanced(F32, d, original))> -> Model.Balanced(F32, d, original)}(transport_balanced(d, original, target, same, valid)))), 86 same))} 87 88 def clone_second(-d: Nat, -original: Array, -target: Array, -pair: Array & Array, 89 -exact: {pair == Array.clone(F32, original) : Array & Array}, -same: {original == target : Array}, 90 -valid: Model.Balanced(F32, d, target)) -> Fact<{Pair.snd(Array, Array, pair) == target : Array}>: 91 Fact{Equal.trans(Array, Pair.snd(Array, Array, pair), Pair.snd(Array, Array, Array.clone(F32, original)), target, 92 Equal.cong(Array & Array, Array, p => Pair.snd(Array, Array, p), pair, Array.clone(F32, original), exact), 93 Equal.trans(Array, Pair.snd(Array, Array, Array.clone(F32, original)), original, target, 94 Clone.second_equal(F32, d, original, Clone.certify(F32, d, original, {\{Fact: p => p} : Fact<(Model.Balanced(F32, d, original))> -> Model.Balanced(F32, d, original)}(transport_balanced(d, original, target, same, valid)))), 95 same))} 96 97 # The input cells a build reads for output cell `position`. 98 def left_at(+plan: Shape.BroadcastPlan, +position: Nat) -> U32: 99 U32.from_nat(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)) 100 101 def right_at(+plan: Shape.BroadcastPlan, +position: Nat) -> U32: 102 U32.from_nat(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)) 103 104 def pair_equal(-a: Array, -b: Array, -A: Array, -B: Array, ea: {a == A : Array}, eb: {b == B : Array}) -> 105 {(a, b) == (A, B) : Array & Array}: 106 Equal.trans(Array & Array, (a, b), (A, b), (A, B), 107 Equal.cong(Array, Array & Array, x => (x, b), a, A, ea), 108 Equal.cong(Array, Array & Array, y => (A, y), b, B, eb)) 109 110 # What an inside cell of the build gives: both arrays back, and the F32 111 # `want` names. 112 def CellOut(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, -A: Array, -B: Array, +position: Nat, 113 -result: F32 & (Array & Array)) -> Type: 114 {Pair.snd(F32, Array & Array, result) == (A, B) : Array & Array} & 115 {Some{Pair.fst(F32, Array & Array, result)} == want(operation, plan, dl, dr, A, B, position) : Maybe<&2, F32>} 116 117 def right_out(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, -A: Array, -B: Array, +position: Nat, 118 -x: F32, -la: Array, pair: Array & F32, -exact: {pair == Array.get(F32, B, right_at(plan, position)) : Array & F32}, 119 -ex: {Some{x} == Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))) : Maybe<&2, F32>}, 120 -el: {la == A : Array}, -valid: Model.Balanced(F32, dr, B)) -> 121 Fact: 122 (kept, y) = pair 123 Fact{(pair_equal(la, kept, A, B, el, 124 {\{Fact: q => q} : Fact<({Refinement.first(F32, (kept, y)) == B : Array})> -> {Refinement.first(F32, (kept, y)) == B : Array}}( 125 read_keeps(dr, B, B, right_at(plan, position), (kept, y), exact, {==}, valid))), 126 {\{Fact: q => q} : Fact<({Some{Elementwise.scalar(operation, x, y)} == pick(operation, Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))), Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position)))) : Maybe<&2, F32>})> -> 127 {Some{Elementwise.scalar(operation, x, y)} == pick(operation, Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))), Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position)))) : Maybe<&2, F32>}}( 128 pick_value(operation, x, y, Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))), Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position))), ex, 129 {\{Fact: q => q} : Fact<({Some{Refinement.second(F32, (kept, y))} == Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position))) : Maybe<&2, F32>})> -> 130 {Some{Refinement.second(F32, (kept, y))} == Model.observe(F32, dr, B, Refinement.route(dr, right_at(plan, position))) : Maybe<&2, F32>}}( 131 read_value(dr, B, B, right_at(plan, position), (kept, y), exact, {==}, valid)))))} 132 133 def left_out(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, -A: Array, B: Array, +position: Nat, 134 pair: Array & F32, -exact: {pair == Array.get(F32, A, left_at(plan, position)) : Array & F32}, 135 -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) -> 136 Fact: 137 (kept, x) = pair 138 right_out(operation, plan, dl, dr, A, B, position, x, kept, Array.get(F32, B, right_at(plan, position)), {==}, 139 {\{Fact: q => q} : Fact<({Some{Refinement.second(F32, (kept, x))} == Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))) : Maybe<&2, F32>})> -> 140 {Some{Refinement.second(F32, (kept, x))} == Model.observe(F32, dl, A, Refinement.route(dl, left_at(plan, position))) : Maybe<&2, F32>}}( 141 read_value(dl, A, A, left_at(plan, position), (kept, x), exact, {==}, left_valid)), 142 {\{Fact: q => q} : Fact<({Refinement.first(F32, (kept, x)) == A : Array})> -> {Refinement.first(F32, (kept, x)) == A : Array}}( 143 read_keeps(dl, A, A, left_at(plan, position), (kept, x), exact, {==}, left_valid)), 144 right_valid) 145 146 # The elementwise cell function of `Parallel.build`, from the input arrays. 147 def cell_of(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +position: Nat, A: Array, B: Array, inside: Bool) -> 148 F32 & (Array & Array): 149 Elementwise.cell_at(Elementwise.walk(Elementwise.Request{operation, plan}), position, (A, B), inside) 150 151 def cell_out(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, A: Array, B: Array, +position: Nat, 152 -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) -> 153 Fact: 154 %Equal.sym(F32 & (Array & Array), cell_of(operation, plan, position, A, B, True{}), 155 Elementwise.cell(operation, Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), 156 Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position, A, B, True{}), 157 WalkProof.cell_at_walk(operation, plan, position, A, B, True{})) : 158 Fact 159 left_out(operation, plan, dl, dr, A, B, position, Array.get(F32, A, left_at(plan, position)), {==}, left_valid, right_valid) 160 161 # Every cell hands both input arrays back. 162 def cell_keeps(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, -A: Array, -B: Array, +position: Nat, 163 inside: Bool, -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) -> 164 Fact<{Pair.snd(F32, Array & Array, cell_of(operation, plan, position, A, B, inside)) == (A, B) : Array & Array}>: 165 match inside: 166 case False{}: 167 Fact{ 168 %Equal.sym(F32 & (Array & Array), cell_of(operation, plan, position, A, B, False{}), 169 Elementwise.cell(operation, Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), 170 Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position, A, B, False{}), 171 WalkProof.cell_at_walk(operation, plan, position, A, B, False{})) : 172 {Pair.snd(F32, Array & Array, _) == (A, B) : Array & Array} 173 {==}} 174 case True{}: 175 Fact{Pair.fst({Pair.snd(F32, Array & Array, cell_of(operation, plan, position, A, B, True{})) == (A, B) : Array & Array}, 176 {Some{Pair.fst(F32, Array & Array, cell_of(operation, plan, position, A, B, True{}))} == want(operation, plan, dl, dr, A, B, position) : Maybe<&2, F32>}, 177 {\{Fact: q => q} : Fact<(CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{})))> -> 178 CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{}))}( 179 cell_out(operation, plan, dl, dr, A, B, position, left_valid, right_valid)))} 180 181 # A split hands each half both input arrays. 182 def halves_equal(+dl: Nat, +dr: Nat, -A: Array, -B: Array, lp: Array & Array, rp: Array & Array, 183 -le: {lp == Array.clone(F32, A) : Array & Array}, -re: {rp == Array.clone(F32, B) : Array & Array}, 184 -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) -> 185 Fact<({Pair.fst(Array & Array, Array & Array, Elementwise.halves(lp, rp)) == (A, B) : Array & Array} & 186 {Pair.snd(Array & Array, Array & Array, Elementwise.halves(lp, rp)) == (A, B) : Array & Array})>: 187 (l1, l2) = lp 188 (r1, r2) = rp 189 Fact{(pair_equal(l1, r1, A, B, 190 {\{Fact: q => q} : Fact<({Pair.fst(Array, Array, (l1, l2)) == A : Array})> -> {Pair.fst(Array, Array, (l1, l2)) == A : Array}}( 191 clone_first(dl, A, A, (l1, l2), le, {==}, left_valid)), 192 {\{Fact: q => q} : Fact<({Pair.fst(Array, Array, (r1, r2)) == B : Array})> -> {Pair.fst(Array, Array, (r1, r2)) == B : Array}}( 193 clone_first(dr, B, B, (r1, r2), re, {==}, right_valid))), 194 pair_equal(l2, r2, A, B, 195 {\{Fact: q => q} : Fact<({Pair.snd(Array, Array, (l1, l2)) == A : Array})> -> {Pair.snd(Array, Array, (l1, l2)) == A : Array}}( 196 clone_second(dl, A, A, (l1, l2), le, {==}, left_valid)), 197 {\{Fact: q => q} : Fact<({Pair.snd(Array, Array, (r1, r2)) == B : Array})> -> {Pair.snd(Array, Array, (r1, r2)) == B : Array}}( 198 clone_second(dr, B, B, (r1, r2), re, {==}, right_valid))))} 199 200 def split_equal(+dl: Nat, +dr: Nat, A: Array, B: Array, -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) -> 201 Fact<({Pair.fst(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array} & 202 {Pair.snd(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array})>: 203 halves_equal(dl, dr, A, B, Array.clone(F32, A), Array.clone(F32, B), {==}, {==}, left_valid, right_valid) 204 205 # An inside cell of the parallel build holds what `want` names there: the 206 # generic law of `Parallel.build`, with the elementwise cell. 207 def build_cell(+depth: Nat, +splits: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +count: Nat, +base: Nat, 208 +dl: Nat, +dr: Nat, -A: Array, -B: Array, +path: Model.Path(depth), 209 -inside: {Nat.is_lt(Nat.add(Model.offset(depth, path), base), count) == True{} : Bool}, 210 -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) -> 211 Fact<{Model.observe(F32, depth, Elementwise.build(depth, splits, operation, plan, count, base, A, B), path) == 212 want(operation, plan, dl, dr, A, B, Nat.add(Model.offset(depth, path), base)) : Maybe<&2, F32>}>: 213 +position = Nat.add(Model.offset(depth, path), base) 214 -split = {\{Fact: q => q} : Fact<({Pair.fst(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array} & 215 {Pair.snd(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array})> -> 216 {Pair.fst(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array} & 217 {Pair.snd(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array}}( 218 split_equal(dl, dr, A, B, left_valid, right_valid)) 219 Fact{Equal.trans(Maybe<&2, F32>, Model.observe(F32, depth, Elementwise.build(depth, splits, operation, plan, count, base, A, B), path), 220 Some{Pair.fst(F32, Array & Array, cell_of(operation, plan, position, A, B, True{}))}, 221 want(operation, plan, dl, dr, A, B, position), 222 %inside : {Model.observe(F32, depth, Elementwise.build(depth, splits, operation, plan, count, base, A, B), path) == 223 Some{Pair.fst(F32, Array & Array, cell_of(operation, plan, position, A, B, _))} : Maybe<&2, F32>} 224 {\{Generic.Fact: q => q} : 225 Generic.Fact, ~Array, ~Elementwise.cell_at, Elementwise.walk(Elementwise.Request{operation, plan}), (A, B), depth, count, base, 226 Elementwise.build(depth, splits, operation, plan, count, base, A, B))> -> 227 Generic.Cells(~Elementwise.Walk, ~Array, ~Array, ~Elementwise.cell_at, Elementwise.walk(Elementwise.Request{operation, plan}), (A, B), depth, count, base, 228 Elementwise.build(depth, splits, operation, plan, count, base, A, B))}( 229 Generic.build_cells(~Elementwise.Request, ~Elementwise.Walk, ~Array, ~Array, ~Elementwise.walk, ~Elementwise.split, ~Elementwise.cell_at, 230 Elementwise.Request{operation, plan}, (A, B), depth, splits, count, base, (A, B), {==}, 231 at => inside => {\{Fact: q => q} : Fact<({Pair.snd(F32, Array & Array, cell_of(operation, plan, at, A, B, inside)) == (A, B) : Array & Array})> -> 232 {Pair.snd(F32, Array & Array, cell_of(operation, plan, at, A, B, inside)) == (A, B) : Array & Array}}( 233 cell_keeps(operation, plan, dl, dr, A, B, at, inside, left_valid, right_valid)), 234 Pair.fst({Pair.fst(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array}, 235 {Pair.snd(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array}, split), 236 Pair.snd({Pair.fst(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array}, 237 {Pair.snd(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array}, split)))(path), 238 Pair.snd({Pair.snd(F32, Array & Array, cell_of(operation, plan, position, A, B, True{})) == (A, B) : Array & Array}, 239 {Some{Pair.fst(F32, Array & Array, cell_of(operation, plan, position, A, B, True{}))} == want(operation, plan, dl, dr, A, B, position) : Maybe<&2, F32>}, 240 {\{Fact: q => q} : Fact<(CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{})))> -> 241 CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{}))}( 242 cell_out(operation, plan, dl, dr, A, B, position, left_valid, right_valid))))} 243 244 # What `take` hands back for one input: the copy for the build is balanced at 245 # some depth and, below the input's element count, holds what the checked 246 # observation of the input sees; the kept tensor observes like the input. 247 def SourceReads(-input: Core.Dynamic, -depth: Nat, -copy: Array) -> Type: 248 @+index: U32 -> @inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Totality.dimensions(input))) == True{} : Bool} -> 249 {Model.observe(F32, depth, copy, Refinement.route(depth, index)) == Core.checked_observe_dynamic(input, index) : Maybe<&2, F32>} 250 251 type Taken<-input: Core.Dynamic, -pair: Core.Dynamic & Array> is Data: 252 Taken{-depth: Nat, -balanced: Model.Balanced(F32, depth, Pair.snd(Core.Dynamic, Array, pair)), 253 -reads: SourceReads(input, depth, Pair.snd(Core.Dynamic, Array, pair)), 254 -retained: Totality.SameSource(input, Pair.fst(Core.Dynamic, Array, pair))} 255 256 def owned_inspect(+shape: Shape.Shape, +depth: Nat, +length: Nat, property: Totality.Property, array: Array) -> Totality.Inspection: 257 match property: 258 case Totality.Dimensions{}: 259 Totality.Dims{Shape.dimensions(shape)} 260 case Totality.Checked{+index}: 261 Totality.Value{Lifecycle.checked_observe_array(depth, length, array, index)} 262 case Totality.Raw{+index}: 263 Totality.Value{Model.observe(F32, depth, array, Refinement.route(depth, index))} 264 265 def owned_view(+shape: Shape.Shape, +depth: Nat, +length: Nat, property: Totality.Property, -array: Array, 266 -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool}, 267 -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) -> 268 {Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}) == 269 owned_inspect(shape, depth, length, property, array) : Totality.Inspection}: 270 match property: 271 case Totality.Dimensions{}: 272 {==} 273 case Totality.Checked{+index}: 274 {==} 275 case Totality.Raw{+index}: 276 {==} 277 278 def observe_allowed_equal(+depth: Nat, +length: Nat, -array: Array, +index: U32, allowed: Bool, 279 accepted: {allowed == True{} : Bool}, matched: {Storage.index_matches(depth, length, index) == True{} : Bool}) -> 280 {Lifecycle.observe_allowed(depth, length, array, index, allowed) == 281 Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>}: 282 match allowed: 283 case False{}: 284 Empty.absurd({None{} == Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>}, Arith.clash(accepted)) 285 case True{}: 286 %Equal.sym(Bool, Storage.index_matches(depth, length, index), True{}, matched) : 287 {Lifecycle.observe_index(depth, length, array, index, _) == Model.observe(F32, depth, array, Refinement.route(depth, index)) : Maybe<&2, F32>} 288 {==} 289 290 def taken_owned(+shape: Shape.Shape, +depth: Nat, +length: Nat, -array: Array, pair: Array & Array, 291 -same: {pair == Array.clone(F32, array) : Array & Array}, -balanced: Model.Balanced(F32, depth, array), 292 -valid: {Storage.bounds(depth, length) == True{} : Bool}, -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) -> 293 Taken: 295 (kept, copy) = pair 296 -kept_same = {\{Fact: p => p} : Fact<({Pair.fst(Array, Array, (kept, copy)) == array : Array})> -> {kept == array : Array}}( 297 clone_first(depth, array, array, (kept, copy), same, {==}, balanced)) 298 -copy_same = {\{Fact: p => p} : Fact<({Pair.snd(Array, Array, (kept, copy)) == array : Array})> -> {copy == array : Array}}( 299 clone_second(depth, array, array, (kept, copy), same, {==}, balanced)) 300 Taken{depth, 301 {\{Fact: p => p} : Fact<(Model.Balanced(F32, depth, copy))> -> Model.Balanced(F32, depth, copy)}(transport_balanced(depth, copy, array, copy_same, balanced)), 302 index => inside => Equal.trans(Maybe<&2, F32>, Model.observe(F32, depth, copy, Refinement.route(depth, index)), 303 Model.observe(F32, depth, array, Refinement.route(depth, index)), 304 Lifecycle.observe_allowed(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length)), 305 Equal.cong(Array, Maybe<&2, F32>, a => Model.observe(F32, depth, a, Refinement.route(depth, index)), copy, array, copy_same), 306 Equal.sym(Maybe<&2, F32>, Lifecycle.observe_allowed(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length)), 307 Model.observe(F32, depth, array, Refinement.route(depth, index)), 308 observe_allowed_equal(depth, length, array, index, Nat.is_lt(U32.to_nat(index), length), 309 %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool} 310 inside, 311 Equal.sym(Bool, True{}, Storage.index_matches(depth, length, index), 312 Route.index_complete(depth, length, index, valid, 313 %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool} 314 inside))))), 315 property => Equal.trans(Totality.Inspection, 316 Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, kept, 317 Certificates.clone_first(F32, depth, array, (kept, copy), same, balanced), valid}, exact}}), 318 owned_inspect(shape, depth, length, property, kept), 319 Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}), 320 owned_view(shape, depth, length, property, kept, Certificates.clone_first(F32, depth, array, (kept, copy), same, balanced), valid, exact), 321 Equal.trans(Totality.Inspection, owned_inspect(shape, depth, length, property, kept), owned_inspect(shape, depth, length, property, array), 322 Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}), 323 Equal.cong(Array, Totality.Inspection, a => owned_inspect(shape, depth, length, property, a), kept, array, kept_same), 324 Equal.sym(Totality.Inspection, Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}), 325 owned_inspect(shape, depth, length, property, array), owned_view(shape, depth, length, property, array, balanced, valid, exact))))} 326 327 def taken(dynamic: Core.Dynamic) -> Taken: 328 Core.Packed{+shape, Core.TTensor{storage, exact}} = dynamic 329 match storage: 330 case Storage.Empty{}: 331 Taken{0n, Unit{}, 332 index => inside => Empty.absurd({Model.observe(F32, 0n, Array.new(F32, 0n, 0.0), Refinement.route(0n, index)) == 333 Core.checked_observe_dynamic(Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}}, index) : Maybe<&2, F32>}, 334 Arith.lt_zero(U32.to_nat(index), 335 %Equal.sym(Nat, 0n, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool} 336 inside)), 337 property => {==}} 338 case Storage.Owned{+depth, +length, array, balanced, valid}: 339 taken_owned(shape, depth, length, array, Array.clone(F32, array), {==}, balanced, valid, exact) 340 341 def walk_pair(+plan: Shape.BroadcastPlan, 342 +map: Shape.Index, 343 +value: Nat, +bound: {True{} == Nat.is_lt(value, Shape.elements(Shape.output_shape(plan))) : Bool}) -> 344 {(Shape.index_value(Shape.left_shape(plan), Flat.project_left_index(plan, map, Shape.FIndex{value, bound})), 345 Shape.index_value(Shape.right_shape(plan), Flat.project_right_index(plan, map, Shape.FIndex{value, bound}))) == 346 (U32.from_nat(Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), map, value)), 347 U32.from_nat(Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), map, value))) : U32 & U32}: 348 match map: 349 case Shape.Indexed{rows, exact}: 350 {==} 351 case Shape.Unindexed{zero}: 352 Empty.absurd({(Shape.index_value(Shape.left_shape(plan), Flat.project_left_index(plan, Shape.Unindexed{zero}, Shape.FIndex{value, bound})), 353 Shape.index_value(Shape.right_shape(plan), Flat.project_right_index(plan, Shape.Unindexed{zero}, Shape.FIndex{value, bound}))) == (U32.from_nat(0n), U32.from_nat(0n)) : U32 & U32}, 354 Flat.hollow(Shape.output_shape(plan), value, zero, bound)) 355 356 def left_walk_bound(+plan: Shape.BroadcastPlan, 357 +map: Shape.Index, 358 +value: Nat, +bound: {True{} == Nat.is_lt(value, Shape.elements(Shape.output_shape(plan))) : Bool}) -> 359 {True{} == Nat.is_lt(Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), map, value), 360 Shape.elements(Shape.left_shape(plan))) : Bool}: 361 match map: 362 case Shape.Indexed{rows, exact}: 363 Flat.left_bound(plan, rows, exact, value, bound) 364 case Shape.Unindexed{zero}: 365 Empty.absurd({True{} == Nat.is_lt(0n, Shape.elements(Shape.left_shape(plan))) : Bool}, Flat.hollow(Shape.output_shape(plan), value, zero, bound)) 366 367 def right_walk_bound(+plan: Shape.BroadcastPlan, 368 +map: Shape.Index, 369 +value: Nat, +bound: {True{} == Nat.is_lt(value, Shape.elements(Shape.output_shape(plan))) : Bool}) -> 370 {True{} == Nat.is_lt(Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), map, value), 371 Shape.elements(Shape.right_shape(plan))) : Bool}: 372 match map: 373 case Shape.Indexed{rows, exact}: 374 Flat.right_bound(plan, rows, exact, value, bound) 375 case Shape.Unindexed{zero}: 376 Empty.absurd({True{} == Nat.is_lt(0n, Shape.elements(Shape.right_shape(plan))) : Bool}, Flat.hollow(Shape.output_shape(plan), value, zero, bound)) 377 378 # Below the output's element count, `expected` reads the inputs at the cells 379 # the build's index walks name. 380 def decided_walks(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, -left: Core.Dynamic, -right: Core.Dynamic, +position: Nat, 381 decision: Shape.BoolCase, 382 +bound: {True{} == Nat.is_lt(position, Shape.elements(Shape.output_shape(plan))) : Bool}) -> 383 {Elementwise.expected_indices(operation, left, right, Elementwise.flat_input_indices(plan, Shape.flat_checked.finish(Shape.output_shape(plan), position, decision))) == 384 Elementwise.expected_left(operation, right, 385 U32.from_nat(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)), 386 Core.checked_observe_dynamic(left, 387 U32.from_nat(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)))) : Maybe<&2, F32>}: 388 match decision: 389 case Shape.BFalse{equal}: 390 Empty.absurd({None{} == 391 Elementwise.expected_left(operation, right, 392 U32.from_nat(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)), 393 Core.checked_observe_dynamic(left, 394 U32.from_nat(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)))) : Maybe<&2, F32>}, 395 Arith.clash(Equal.trans(Bool, False{}, Nat.is_lt(position, Shape.elements(Shape.output_shape(plan))), True{}, equal, 396 Equal.sym(Bool, True{}, Nat.is_lt(position, Shape.elements(Shape.output_shape(plan))), bound)))) 397 case Shape.BTrue{equal}: 398 Equal.cong(U32 & U32, Maybe<&2, F32>, indices => Elementwise.expected_indices(operation, left, right, Done{indices}), 399 (Shape.index_value(Shape.left_shape(plan), Flat.project_left_index(plan, Shape.index_map(plan), Shape.FIndex{position, equal})), 400 Shape.index_value(Shape.right_shape(plan), Flat.project_right_index(plan, Shape.index_map(plan), Shape.FIndex{position, equal}))), 401 (U32.from_nat(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)), 402 U32.from_nat(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))), 403 walk_pair(plan, Shape.index_map(plan), position, equal)) 404 405 def pick_expected(+operation: Elementwise.Operation, value: Maybe<&2, F32>, -right: Core.Dynamic, -right_index: U32, -other: Maybe<&2, F32>, 406 same: {other == Core.checked_observe_dynamic(right, right_index) : Maybe<&2, F32>}) -> 407 {pick(operation, value, other) == Elementwise.expected_left(operation, right, right_index, value) : Maybe<&2, F32>}: 408 match value: 409 case None{}: 410 {==} 411 case Some{value}: 412 %same : {Elementwise.expected_right(operation, value, other) == Elementwise.expected_right(operation, value, _) : Maybe<&2, F32>} 413 {==} 414 415 def add_zero_right(+number: Nat) -> {Nat.add(number, 0n) == number : Nat}: 416 match number: 417 case 0n: 418 {==} 419 case 1n+p: 420 Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, 0n), p, add_zero_right(p)) 421 422 def output_offset(+depth: Nat, +length: Nat, +index: U32, +valid: {Storage.bounds(depth, length) == True{} : Bool}, 423 +inside: {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}) -> 424 {U32.to_nat(index) == Model.offset(depth, Refinement.route(depth, index)) : Nat}: 425 +rest = Arith.and_right(Nat.is_le(depth, 20n), Bool.and(Nat.is_lt(0n, length), Nat.is_le(length, Model.capacity(depth))), valid) 426 Route.route_offset(depth, index, 427 Arith.and_left(Nat.is_le(depth, 20n), Bool.and(Nat.is_lt(0n, length), Nat.is_le(length, Model.capacity(depth))), valid), 428 Arith.lt_le_trans(U32.to_nat(index), length, Model.capacity(depth), inside, 429 Arith.and_right(Nat.is_lt(0n, length), Nat.is_le(length, Model.capacity(depth)), rest))) 430 431 def word_exact(+shape: Shape.Shape, +cursor: Nat, within: {Nat.is_le(cursor, Shape.elements(shape)) == True{} : Bool}) -> 432 {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}: 433 WordConversion.natural_word_exact(cursor, Shape.count(shape), 434 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), WordConversion.shape_count_exact(shape)) : 435 {Nat.is_le(cursor, _) == True{} : Bool} 436 within) 437 438 # A cell an index walk names lies inside the input it reads. 439 def side_inside(-input: Core.Dynamic, +side: Shape.Shape, +walk: Nat, 440 fits: {Totality.dimensions(input) == Shape.dimensions(side) : List<&2, U32>}, 441 +bound: {True{} == Nat.is_lt(walk, Shape.elements(side)) : Bool}) -> 442 {Nat.is_lt(U32.to_nat(U32.from_nat(walk)), Shape.logical_numel(Totality.dimensions(input))) == True{} : Bool}: 443 %Equal.sym(Nat, U32.to_nat(U32.from_nat(walk)), walk, 444 word_exact(side, walk, WordConversion.lt_le(walk, Shape.elements(side), Equal.sym(Bool, True{}, Nat.is_lt(walk, Shape.elements(side)), bound)))) : 445 {Nat.is_lt(_, Shape.logical_numel(Totality.dimensions(input))) == True{} : Bool} 446 %Equal.sym(List<&2, U32>, Totality.dimensions(input), Shape.dimensions(side), fits) : 447 {Nat.is_lt(walk, Shape.logical_numel(_)) == True{} : Bool} 448 %Shape.elements_exact(side) : {Nat.is_lt(walk, _) == True{} : Bool} 449 Equal.sym(Bool, True{}, Nat.is_lt(walk, Shape.elements(side)), bound) 450 451 def output_inside(+plan: Shape.BroadcastPlan, +length: Nat, +index: U32, 452 +exact: {length == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat}, 453 +bound: Shape.LT(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))))) -> {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}: 454 %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool} 455 Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))), Nats.lt_true(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), bound)) 456 457 def output_bound(+plan: Shape.BroadcastPlan, +index: U32, +bound: Shape.LT(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))))) -> 458 {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))) : Bool}: 459 %Equal.sym(Nat, Shape.elements(Shape.output_shape(plan)), Shape.numel(Shape.extents(Shape.output_shape(plan))), Shape.elements_exact(Shape.output_shape(plan))) : 460 {True{} == Nat.is_lt(U32.to_nat(index), _) : Bool} 461 Nats.lt_true(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), bound) 462 463 def output_position(+depth: Nat, +length: Nat, +index: U32, +valid: {Storage.bounds(depth, length) == True{} : Bool}, 464 +inside: {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}) -> 465 {Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n) == U32.to_nat(index) : Nat}: 466 Equal.trans(Nat, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n), Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index), add_zero_right(Model.offset(depth, Refinement.route(depth, index))), 467 Equal.sym(Nat, U32.to_nat(index), Model.offset(depth, Refinement.route(depth, index)), output_offset(depth, length, index, valid, inside))) 468 469 # At an index below the output's element count, the parallel build holds the 470 # value `expected` names there. 471 def output_cell(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat, 472 +valid: {Storage.bounds(depth, length) == True{} : Bool}, +exact: {length == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat}, 473 -left: Core.Dynamic, -right: Core.Dynamic, la: Array, ra: Array, +dl: Nat, +dr: Nat, 474 -left_valid: Model.Balanced(F32, dl, la), -right_valid: Model.Balanced(F32, dr, ra), 475 -left_reads: SourceReads(left, dl, la), -right_reads: SourceReads(right, dr, ra), 476 +left_fits: {Totality.dimensions(left) == Shape.dimensions(Shape.left_shape(plan)) : List<&2, U32>}, 477 +right_fits: {Totality.dimensions(right) == Shape.dimensions(Shape.right_shape(plan)) : List<&2, U32>}, 478 +index: U32, +bound: Shape.LT(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))))) -> 479 Fact<{Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}>: 480 +inside = output_inside(plan, length, index, exact, bound) 481 +within = output_bound(plan, index, bound) 482 +position = output_position(depth, length, index, valid, inside) 483 Fact{Equal.trans(Maybe<&2, F32>, Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)), want(operation, plan, dl, dr, la, ra, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n)), Elementwise.expected(operation, plan, left, right, index), 484 {\{Fact: q => q} : Fact<({Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == want(operation, plan, dl, dr, la, ra, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n)) : Maybe<&2, F32>})> -> 485 {Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == want(operation, plan, dl, dr, la, ra, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n)) : Maybe<&2, F32>}}( 486 build_cell(depth, Elementwise.splits(depth), operation, plan, length, 0n, dl, dr, la, ra, Refinement.route(depth, index), 487 %Equal.sym(Nat, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n), U32.to_nat(index), position) : {Nat.is_lt(_, length) == True{} : Bool} 488 inside, left_valid, right_valid)), 489 Equal.trans(Maybe<&2, F32>, want(operation, plan, dl, dr, la, ra, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n)), want(operation, plan, dl, dr, la, ra, U32.to_nat(index)), Elementwise.expected(operation, plan, left, right, index), 490 Equal.cong(Nat, Maybe<&2, F32>, at => want(operation, plan, dl, dr, la, ra, at), Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n), U32.to_nat(index), position), 491 Equal.trans(Maybe<&2, F32>, want(operation, plan, dl, dr, la, ra, U32.to_nat(index)), Elementwise.expected_left(operation, right, U32.from_nat(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), U32.to_nat(index))), Model.observe(F32, dl, la, Refinement.route(dl, U32.from_nat(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), U32.to_nat(index)))))), Elementwise.expected(operation, plan, left, right, index), 492 pick_expected(operation, Model.observe(F32, dl, la, Refinement.route(dl, U32.from_nat(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), U32.to_nat(index))))), right, U32.from_nat(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), U32.to_nat(index))), Model.observe(F32, dr, ra, Refinement.route(dr, U32.from_nat(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), U32.to_nat(index))))), 493 right_reads(U32.from_nat(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), U32.to_nat(index))))(side_inside(right, Shape.right_shape(plan), 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), U32.to_nat(index)), right_fits, 494 right_walk_bound(plan, Shape.index_map(plan), U32.to_nat(index), within)))), 495 Equal.trans(Maybe<&2, F32>, Elementwise.expected_left(operation, right, U32.from_nat(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), U32.to_nat(index))), Model.observe(F32, dl, la, Refinement.route(dl, U32.from_nat(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), U32.to_nat(index)))))), Elementwise.expected_left(operation, right, U32.from_nat(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), U32.to_nat(index))), Core.checked_observe_dynamic(left, U32.from_nat(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), U32.to_nat(index))))), Elementwise.expected(operation, plan, left, right, index), 496 Equal.cong(Maybe<&2, F32>, Maybe<&2, F32>, value => Elementwise.expected_left(operation, right, U32.from_nat(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), U32.to_nat(index))), value), Model.observe(F32, dl, la, Refinement.route(dl, U32.from_nat(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), U32.to_nat(index))))), Core.checked_observe_dynamic(left, U32.from_nat(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), U32.to_nat(index)))), 497 left_reads(U32.from_nat(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), U32.to_nat(index))))(side_inside(left, Shape.left_shape(plan), 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), U32.to_nat(index)), left_fits, 498 left_walk_bound(plan, Shape.index_map(plan), U32.to_nat(index), within)))), 499 Equal.sym(Maybe<&2, F32>, Elementwise.expected(operation, plan, left, right, index), Elementwise.expected_left(operation, right, U32.from_nat(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), U32.to_nat(index))), Core.checked_observe_dynamic(left, U32.from_nat(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), U32.to_nat(index))))), 500 decided_walks(operation, plan, left, right, U32.to_nat(index), Shape.bool_case(Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan)))), within))))))} 501 502 def output_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat, 503 -valid: {Storage.bounds(depth, length) == True{} : Bool}, -exact: {length == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat}, 504 -left: Core.Dynamic, -right: Core.Dynamic, taken_left: Core.Dynamic & Array, taken_right: Core.Dynamic & Array, 505 -left_taken: Taken, -right_taken: Taken, 506 +left_fits: {Totality.dimensions(left) == Shape.dimensions(Shape.left_shape(plan)) : List<&2, U32>}, 507 +right_fits: {Totality.dimensions(right) == Shape.dimensions(Shape.right_shape(plan)) : List<&2, U32>}) -> 508 Elementwise.MappingModel: 509 (kept_left, la) = taken_left 510 (kept_right, ra) = taken_right 511 Elementwise.MappingModel{index => bound => 512 {\{Taken: dl => left_valid => left_reads => left_same => 513 {\{Taken: dr => right_valid => right_reads => right_same => 514 {\{Fact: equal => equal} : Fact<({Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>})> -> {Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}}( 515 output_cell(operation, plan, depth, length, valid, exact, left, right, la, ra, dl, dr, left_valid, right_valid, left_reads, right_reads, 516 left_fits, right_fits, index, bound))} : Taken -> {Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}}(right_taken)} : Taken -> {Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}}(left_taken)} 517 518 def allocated_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, left: Core.Dynamic, right: Core.Dynamic, 519 result: Result<&2, &1, Core.Error, Core.Tensor>, 520 +left_fits: {Totality.dimensions(left) == Shape.dimensions(Shape.left_shape(plan)) : List<&2, U32>}, 521 +right_fits: {Totality.dimensions(right) == Shape.dimensions(Shape.right_shape(plan)) : List<&2, U32>}) -> 522 Elementwise.MappingModel: 523 match result: 524 case Fail{error}: 525 Elementwise.MappingModel{Unit{}} 526 case Done{Core.TTensor{storage, exact}}: 527 match storage: 528 case Storage.Empty{}: 529 Elementwise.MappingModel{index => bound => Empty.absurd( 530 {Core.observe_dynamic(Core.Packed{Shape.output_shape(plan), Core.TTensor{Storage.Empty{}, exact}}, index) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}, 531 Arith.lt_zero(U32.to_nat(index), 532 %Equal.sym(Nat, 0n, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), exact) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool} 533 Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))), Nats.lt_true(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), bound))))} 534 case Storage.Owned{+depth, +length, array, balanced, valid}: 535 output_mapping(operation, plan, depth, length, valid, exact, left, right, Elementwise.take(left), Elementwise.take(right), 536 taken(left), taken(right), left_fits, right_fits) 537 538 def planned_mapping(+operation: Elementwise.Operation, +left_shape: Shape.Shape, +right_shape: Shape.Shape, 539 result: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>, left: Core.Tensor, right: Core.Tensor, 540 -same: {result == Elementwise.plan_for(Core.Packed{left_shape, left}, Core.Packed{right_shape, right}) : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, 541 +sources: {ShapeLaws.planned_dimensions(left_shape, right_shape, result) == (Shape.dimensions(left_shape), Shape.dimensions(right_shape)) : List<&2, U32> & List<&2, U32>}) -> 542 Elementwise.BinaryModel: 543 match result: 544 case Fail{error}: 545 Elementwise.BinaryModel{ 546 %same : Elementwise.PlannedMeaning(operation, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Elementwise.parallel_planned(operation, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Fail{error}), _) 547 Unit{}} 548 case Done{+plan}: 549 Elementwise.BinaryModel{ 550 %same : Elementwise.PlannedMeaning(operation, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Elementwise.parallel_planned(operation, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Done{plan}), _) 551 {\{Elementwise.MappingModel: mapping => mapping} : 552 Elementwise.MappingModel -> Elementwise.SuccessfulMapping(operation, plan, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Elementwise.parallel_allocated(operation, plan, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Core.new(Shape.output_shape(plan), 0.0)))}( 553 allocated_mapping(operation, plan, Core.Packed{left_shape, left}, Core.Packed{right_shape, right}, Core.new(Shape.output_shape(plan), 0.0), 554 Equal.sym(List<&2, U32>, Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(left_shape), 555 Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, Pair.fst(List<&2, U32>, List<&2, U32>), 556 (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(left_shape), Shape.dimensions(right_shape)), sources)), 557 Equal.sym(List<&2, U32>, Shape.dimensions(Shape.right_shape(plan)), Shape.dimensions(right_shape), 558 Equal.cong(List<&2, U32> & List<&2, U32>, List<&2, U32>, Pair.snd(List<&2, U32>, List<&2, U32>), 559 (Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(Shape.right_shape(plan))), (Shape.dimensions(left_shape), Shape.dimensions(right_shape)), sources))))} 560 561 # The parallel `binary` meets the same `BinaryModel` as the sequential loop. 562 def binary_mapping(+operation: Elementwise.Operation, left: Core.Dynamic, right: Core.Dynamic) -> 563 Elementwise.BinaryModel: 564 Core.Packed{+left_shape, left_tensor} = left 565 Core.Packed{+right_shape, right_tensor} = right 566 planned_mapping(operation, left_shape, right_shape, Shape.broadcast_checked(left_shape, right_shape), left_tensor, right_tensor, {==}, 567 PlanProof.broadcast_checked_plan(left_shape, right_shape))