def trace_offset

bendtorch-core@0.1.0.0 · src/storage/route.bend:314

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

314def trace_offset(+d: Nat, +i: U32, z: Bool, +dz: {z == U32.is_lt(i, U32.shr(Size.capacity(d))) : Bool},
315  +h: {Nat.is_le(d, 20n) == True{} : Bool}, +inside: {Nat.is_lt(U32.to_nat(i), Model.capacity(d)) == True{} : Bool}) ->
316  {U32.to_nat(i) == Model.offset(d, Refinement.trace(d, Size.capacity(d), i, z)) : Nat}:
317  match d:
318    case 0n:
319      Equal.sym(Nat, 0n, U32.to_nat(i), Arith.lt_one(U32.to_nat(i), inside))
320    case 1n+p:
321      match z:
322        case True{}:
323          +hp = Arith.le_succ(p, 19n, h)
324          %shr_cap(p, h) : {U32.to_nat(i) == Model.offset(p, Refinement.trace(p, _, i, U32.is_lt(i, U32.shr(_)))) : Nat}
325          trace_offset(p, i, U32.is_lt(i, U32.shr(Size.capacity(p))), {==}, hp, low_inside(p, i, h, dz))
326        case False{}:
327          +hp = Arith.le_succ(p, 19n, h)
328          +le = high_le(p, i, h, dz)
329          %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}
330          +j = U32.sub(i, Size.capacity(p))
331          %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}
332          high_split(p, i, hp, le)