Route.trace_offset: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/route.bend as Route
Lines 314-332 of bendtorch-core@0.1.0.0/src/storage/route.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/route.bend&start_line=314&end_line=332

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/size.bend as Size
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

def trace_offset(+d: Nat, +i: U32, z: Bool, +dz: {z == U32.is_lt(i, U32.shr(Size.capacity(d))) : Bool},
  +h: {Nat.is_le(d, 20n) == True{} : Bool}, +inside: {Nat.is_lt(U32.to_nat(i), Model.capacity(d)) == True{} : Bool}) ->
  {U32.to_nat(i) == Model.offset(d, Refinement.trace(d, Size.capacity(d), i, z)) : Nat}:
  match d:
    case 0n:
      Equal.sym(Nat, 0n, U32.to_nat(i), Arith.lt_one(U32.to_nat(i), inside))
    case 1n+p:
      match z:
        case True{}:
          +hp = Arith.le_succ(p, 19n, h)
          %shr_cap(p, h) : {U32.to_nat(i) == Model.offset(p, Refinement.trace(p, _, i, U32.is_lt(i, U32.shr(_)))) : Nat}
          trace_offset(p, i, U32.is_lt(i, U32.shr(Size.capacity(p))), {==}, hp, low_inside(p, i, h, dz))
        case False{}:
          +hp = Arith.le_succ(p, 19n, h)
          +le = high_le(p, i, h, dz)
          %shr_cap(p, h) : {U32.to_nat(i) == Nat.add(Model.capacity(p), Model.offset(p, Refinement.trace(p, _, U32.sub(i, _), U32.is_lt(U32.sub(i, _), U32.shr(_))))) : Nat}
          +j = U32.sub(i, Size.capacity(p))
          %trace_offset(p, j, U32.is_lt(j, U32.shr(Size.capacity(p))), {==}, hp, high_inside(p, i, hp, le, inside)) : {U32.to_nat(i) == Nat.add(Model.capacity(p), _) : Nat}
          high_split(p, i, hp, le)

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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.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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shr
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=le_succ
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=lt_one
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=capacity
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=trace
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/route.bend&name=high_inside
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/route.bend&name=high_le
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/route.bend&name=high_split
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/route.bend&name=low_inside
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/route.bend&name=shr_cap
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/size.bend&name=capacity