ReduceFiberProof.kept_hit_step: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as ReduceFiberProof Lines 714-768 of bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&start_line=714&end_line=768 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith def kept_hit_step(+g: Nat, +stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +target: Nat, +base: Nat, +digit: Nat, decision: Shape.BoolCase, +from: {Nat.is_le(digit, Nat.div(target, left)) == True{} : Bool}, +until: {Nat.is_lt(Nat.div(target, left), Nat.add(digit, 1n+g)) == True{} : Bool}, +given: Decomposed, +bound: BoundBy, rec: @+next: Nat -> @+from: {Nat.is_le(next, Nat.div(target, left)) == True{} : Bool} -> @+until: {Nat.is_lt(Nat.div(target, left), Nat.add(next, g)) == True{} : Bool} -> {masked(Nat.mul(g, stride), Shape.Row{stride, left, right} <> rest, target, base, Nat.mul(next, stride)) == masked(stride, rest, Nat.mod(target, left), Nat.add(base, Nat.mul(right, Nat.div(target, left))), 0n) : List<&2, Nat>}) -> {masked(Nat.mul(1n+g, stride), Shape.Row{stride, left, right} <> rest, target, base, Nat.mul(digit, stride)) == masked(stride, rest, Nat.mod(target, left), Nat.add(base, Nat.mul(right, Nat.div(target, left))), 0n) : List<&2, Nat>}: match decision: case Shape.BTrue{equal}: +rows : List<&2, Shape.Row> = Shape.Row{stride, left, right} <> rest +c = Nat.mul(digit, stride) +dt = Nat.div(target, left) +tr = Nat.mod(target, left) +hit = masked(stride, rest, tr, Nat.add(base, Nat.mul(right, dt)), 0n) +same = Arith.eq_true(digit, dt, Equal.sym(Bool, True{}, Nat.is_eq(digit, dt), equal)) +mine = masked(stride, rest, tr, Nat.add(base, Nat.mul(right, digit)), 0n) %Equal.sym(List<&2, Nat>, masked(Nat.add(stride, Nat.mul(g, stride)), rows, target, base, c), List.append(&2, Nat, masked(stride, rows, target, base, c), masked(Nat.mul(g, stride), rows, target, base, Nat.add(c, stride))), masked_split(stride, Nat.mul(g, stride), rows, target, base, c)) : {_ == hit : List<&2, Nat>} %Equal.sym(List<&2, Nat>, masked(stride, rows, target, base, c), mine, block(stride, left, right, rest, target, tr, base, digit, Hit{given, same, {==}})) : {List.append(&2, Nat, _, masked(Nat.mul(g, stride), rows, target, base, Nat.add(c, stride))) == hit : List<&2, Nat>} %next_cursor(digit, stride) : {List.append(&2, Nat, mine, masked(Nat.mul(g, stride), rows, target, base, _)) == hit : List<&2, Nat>} %Equal.sym(List<&2, Nat>, masked(Nat.mul(g, stride), rows, target, base, Nat.mul(1n+digit, stride)), Nil{}, kept_after(g, stride, left, right, rest, target, base, 1n+digit, %same : {Nat.is_lt(_, 1n+digit) == True{} : Bool} lt_self_succ(digit), bound)) : {List.append(&2, Nat, mine, _) == hit : List<&2, Nat>} %Equal.sym(List<&2, Nat>, List.append(&2, Nat, mine, Nil{}), mine, append_nil(mine)) : {_ == hit : List<&2, Nat>} Equal.cong(Nat, List<&2, Nat>, d => masked(stride, rest, tr, Nat.add(base, Nat.mul(right, d)), 0n), digit, dt, same) case Shape.BFalse{equal}: +rows : List<&2, Shape.Row> = Shape.Row{stride, left, right} <> rest +c = Nat.mul(digit, stride) +dt = Nat.div(target, left) +tr = Nat.mod(target, left) +hit = masked(stride, rest, tr, Nat.add(base, Nat.mul(right, dt)), 0n) +differ = Equal.sym(Bool, False{}, Nat.is_eq(digit, dt), equal) %Equal.sym(List<&2, Nat>, masked(Nat.add(stride, Nat.mul(g, stride)), rows, target, base, c), List.append(&2, Nat, masked(stride, rows, target, base, c), masked(Nat.mul(g, stride), rows, target, base, Nat.add(c, stride))), masked_split(stride, Nat.mul(g, stride), rows, target, base, c)) : {_ == hit : List<&2, Nat>} %Equal.sym(List<&2, Nat>, masked(stride, rows, target, base, c), Nil{}, block_off(stride, left, right, rest, target, base, digit, Off{bound, differ})) : {List.append(&2, Nat, _, masked(Nat.mul(g, stride), rows, target, base, Nat.add(c, stride))) == hit : List<&2, Nat>} %next_cursor(digit, stride) : {masked(Nat.mul(g, stride), rows, target, base, _) == hit : List<&2, Nat>} rec(1n+digit, le_ne_succ(digit, dt, from, differ), %Arith.add_succ(digit, g) : {Nat.is_lt(dt, _) == True{} : Bool} until) Uses (30): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=BoundBy https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=Decomposed https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=MaskMode https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=OffMode https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=append_nil https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=block https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=block_off https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=kept_after https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=le_ne_succ https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=lt_self_succ https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=masked https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=masked_split https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=next_cursor https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BoolCase https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Row https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=add_succ https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=eq_true