~/bend-docscommunity

proofs/math/typed/fixbytes.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend as Fixbytes

19 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/generic.bend as SG
import ../../../spec/math/fixed.bend as SF
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../../src/math/fixed.bend as F
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/list.bend as LL
import ../../lib/u32.bend as U3
import ../../lib/u32div.bend as UD
import ./width.bend as WW
import ./w64add.bend as WA
import ./w64sh.bend as SH
import ./shrn.bend as SHN
import ./u32laws.bend as LW
import ./fixgen.bend as G
import ./fix32.bend as P32

Definitions

def v source · line 28 · raw

@+x:U32 -> Nat

def con_eq source · line 31 · raw

@+x:Nat -> @+y:Nat -> @xs:List<&2, Nat> -> @ys:List<&2, Nat> -> @+ex:{x == y : Nat} -> @+ets:{xs == ys : List<&2, Nat>} -> {x <> xs == y <> ys : List<&2, Nat>}

def byte_v source · line 36 · raw

@+x:U32 -> @+k:Nat -> {v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.byte32(x, k)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(Nat.mul(8n, k), v(x))) : Nat}

def to_le32 source · line 40 · raw

@+x:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_to_bytes_le(x)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.le_digits(4n, v(x)) : List<&2, Nat>}

def to_be32 source · line 46 · raw

@+x:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_to_bytes_be(x)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.reverse(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.le_digits(4n, v(x))) : List<&2, Nat>}

def u32_to_le source · line 52 · raw

@+a:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.ToBytes.le(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_to_bytes_le, 4n, a)

def u32_to_be source · line 55 · raw

@+a:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.ToBytes.be(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_to_bytes_be, 4n, a)

def bnd source · line 61 · raw

@+k:Nat -> @r:Maybe<&2, Nat> -> Bool

every value in r fits k bits

def fb source · line 68 · raw

@+b:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(8n, v(b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b) : Bool}

def step_fits source · line 72 · raw

@+k:Nat -> @+b:Nat -> @+z:Nat -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(8n, b) == True{} : Bool} -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, z) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(8n, k), Nat.add(b, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(8n, z))) == True{} : Bool}

b + 256 z fits 8 + k bits (Horner's step)

def to32 source · line 75 · raw

@+k:Nat -> @+hk:{Nat.is_le(Nat.add(8n, k), 32n) == True{} : Bool} -> @+n:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(8n, k), n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, n) == True{} : Bool}

def step32 source · line 78 · raw

@+k:Nat -> @+hk:{Nat.is_le(Nat.add(8n, k), 32n) == True{} : Bool} -> @+z:U32 -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, v(z)) == True{} : Bool} -> @+b:U32 -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(8n, v(b)) == True{} : Bool} -> {v(U32.add(b, U32.mul(z, 256))) == Nat.add(v(b), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(8n, v(z))) : Nat}

def d32_some source · line 85 · raw

@+k:Nat -> @+hk:{Nat.is_le(Nat.add(8n, k), 32n) == True{} : Bool} -> @+z:U32 -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, v(z)) == True{} : Bool} -> @+b:U32 -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig32(Some{z}, c, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.digit_on(Some{v(z)}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(8n, v(b)), v(b)) : Maybe<&2, Nat>}

def d32_sbnd source · line 96 · raw

@+k:Nat -> @+hk:{Nat.is_le(Nat.add(8n, k), 32n) == True{} : Bool} -> @+z:U32 -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, v(z)) == True{} : Bool} -> @+b:U32 -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b) == c : Bool} -> {bnd(Nat.add(8n, k), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig32(Some{z}, c, b))) == True{} : Bool}

def d32_val source · line 105 · raw

@+k:Nat -> @+hk:{Nat.is_le(Nat.add(8n, k), 32n) == True{} : Bool} -> @r:Maybe<&2, U32> -> @+hr:{bnd(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, r)) == True{} : Bool} -> @+b:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig32(r, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b), b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.digit_on(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, r), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(8n, v(b)), v(b)) : Maybe<&2, Nat>}

def d32_bnd source · line 112 · raw

@+k:Nat -> @+hk:{Nat.is_le(Nat.add(8n, k), 32n) == True{} : Bool} -> @r:Maybe<&2, U32> -> @+hr:{bnd(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, r)) == True{} : Bool} -> @+b:U32 -> {bnd(Nat.add(8n, k), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig32(r, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b), b))) == True{} : Bool}

def from4_ok source · line 119 · raw

@+b0:U32 -> @+b1:U32 -> @+b2:U32 -> @+b3:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.from4(b0, b1, b2, b3)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(4n, [v(b0), v(b1), v(b2), v(b3)]) : Maybe<&2, Nat>}

def fl_len source · line 144 · raw

@+k:Nat -> @xs:List<&2, Nat> -> @+h:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.length(Nat, xs), k) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(k, xs) == None{} : Maybe<&2, Nat>}

any other length parses to None

def rev_none source · line 156 · raw

@+k:Nat -> @+xs:List<&2, Nat> -> @+h:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.length(Nat, xs), k) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.reverse(Nat, xs)) == None{} : Maybe<&2, Nat>}

def fle4 source · line 160 · raw

@+b0:U32 -> @+b1:U32 -> @+b2:U32 -> @+b3:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_from_bytes_le(b0 <> b1 <> b2 <> b3 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(4n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(b0 <> b1 <> b2 <> b3 <> t)) : Maybe<&2, Nat>}

the list cases: exactly four bytes, or None on both sides

def fle3 source · line 167 · raw

@+b0:U32 -> @+b1:U32 -> @+b2:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_from_bytes_le(b0 <> b1 <> b2 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(4n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(b0 <> b1 <> b2 <> t)) : Maybe<&2, Nat>}

def fle2 source · line 174 · raw

@+b0:U32 -> @+b1:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_from_bytes_le(b0 <> b1 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(4n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(b0 <> b1 <> t)) : Maybe<&2, Nat>}

def fle1 source · line 181 · raw

@+b0:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_from_bytes_le(b0 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(4n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(b0 <> t)) : Maybe<&2, Nat>}

def u32_from_le source · line 188 · raw

@bs:List<&2, U32> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.FromBytes.le(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_from_bytes_le, 4n, bs)

def fbe4 source · line 195 · raw

@+b3:U32 -> @+b2:U32 -> @+b1:U32 -> @+b0:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_from_bytes_be(b3 <> b2 <> b1 <> b0 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(4n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.reverse(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(b3 <> b2 <> b1 <> b0 <> t))) : Maybe<&2, Nat>}

def fbe3 source · line 202 · raw

@+b3:U32 -> @+b2:U32 -> @+b1:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_from_bytes_be(b3 <> b2 <> b1 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(4n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.reverse(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(b3 <> b2 <> b1 <> t))) : Maybe<&2, Nat>}

def fbe2 source · line 209 · raw

@+b3:U32 -> @+b2:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_from_bytes_be(b3 <> b2 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(4n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.reverse(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(b3 <> b2 <> t))) : Maybe<&2, Nat>}

def fbe1 source · line 216 · raw

@+b3:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_from_bytes_be(b3 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(4n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.reverse(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(b3 <> t))) : Maybe<&2, Nat>}

def u32_from_be source · line 223 · raw

@bs:List<&2, U32> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.FromBytes.be(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u32_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u32_from_bytes_be, 4n, bs)

def w8 source · line 232 · raw

@k:Nat -> Nat

def fits0 source · line 239 · raw

@+n:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(0n, n) == True{} : Bool} -> {n == 0n : Nat}

def dsplit source · line 242 · raw

@+a:Nat -> @+b:Nat -> @+lo:Nat -> @+hi:Nat -> @+hlo:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(w8(a), lo) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.le_digits(Nat.add(a, b), Nat.add(lo, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(w8(a), hi))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.append(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.le_digits(a, lo), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.le_digits(b, hi)) : List<&2, Nat>}

def u64_to_le source · line 253 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.ToBytes.le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_to_bytes_le, 8n, a)

def u64_to_be source · line 261 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.ToBytes.be(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_to_bytes_be, 8n, a)

def to64 source · line 275 · raw

@+k:Nat -> @+hk:{Nat.is_le(Nat.add(8n, k), 64n) == True{} : Bool} -> @+n:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(8n, k), n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, n) == True{} : Bool}

def step64 source · line 278 · raw

@+k:Nat -> @+hk:{Nat.is_le(Nat.add(8n, k), 64n) == True{} : Bool} -> @+z:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val(z)) == True{} : Bool} -> @+b:U32 -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(8n, v(b)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{b, 0}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul(z, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{256, 0}))) == Nat.add(v(b), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val(z))) : Nat}

def d64_some source · line 289 · raw

@+k:Nat -> @+hk:{Nat.is_le(Nat.add(8n, k), 64n) == True{} : Bool} -> @+z:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val(z)) == True{} : Bool} -> @+b:U32 -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig64(Some{z}, c, b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.digit_on(Some{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val(z)}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(8n, v(b)), v(b)) : Maybe<&2, Nat>}

def d64_sbnd source · line 300 · raw

@+k:Nat -> @+hk:{Nat.is_le(Nat.add(8n, k), 64n) == True{} : Bool} -> @+z:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val(z)) == True{} : Bool} -> @+b:U32 -> @+c:Bool -> @+hc:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b) == c : Bool} -> {bnd(Nat.add(8n, k), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig64(Some{z}, c, b))) == True{} : Bool}

def d64_val source · line 309 · raw

@+k:Nat -> @+hk:{Nat.is_le(Nat.add(8n, k), 64n) == True{} : Bool} -> @r:Maybe<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64> -> @+hr:{bnd(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, r)) == True{} : Bool} -> @+b:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig64(r, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b), b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.digit_on(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, r), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(8n, v(b)), v(b)) : Maybe<&2, Nat>}

def d64_bnd source · line 316 · raw

@+k:Nat -> @+hk:{Nat.is_le(Nat.add(8n, k), 64n) == True{} : Bool} -> @r:Maybe<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64> -> @+hr:{bnd(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, r)) == True{} : Bool} -> @+b:U32 -> {bnd(Nat.add(8n, k), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig64(r, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b), b))) == True{} : Bool}

def hstep source · line 324 · raw

@+k:Nat -> @+hk:{Nat.is_le(Nat.add(8n, k), 64n) == True{} : Bool} -> @r:Maybe<&2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64> -> @+S:Maybe<&2, Nat> -> @+es:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, r) == S : Maybe<&2, Nat>} -> @+hr:{bnd(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, r)) == True{} : Bool} -> @+b:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig64(r, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b), b)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.digit_on(S, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(8n, v(b)), v(b)) : Maybe<&2, Nat>}

one Horner step on both sides, carrying the bound

def from8_ok source · line 327 · raw

@+b0:U32 -> @+b1:U32 -> @+b2:U32 -> @+b3:U32 -> @+b4:U32 -> @+b5:U32 -> @+b6:U32 -> @+b7:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig64(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.dig64(Some{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{0, 0}}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b7), b7), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b6), b6), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b5), b5), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b4), b4), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b3), b3), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b2), b2), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b1), b1), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.is_byte(b0), b0)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, [v(b0), v(b1), v(b2), v(b3), v(b4), v(b5), v(b6), v(b7)]) : Maybe<&2, Nat>}

def gle8 source · line 362 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_le(x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> t)) : Maybe<&2, Nat>}

def gle7 source · line 369 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_le(x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> t)) : Maybe<&2, Nat>}

def gle6 source · line 376 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_le(x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> t)) : Maybe<&2, Nat>}

def gle5 source · line 383 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_le(x0 <> x1 <> x2 <> x3 <> x4 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(x0 <> x1 <> x2 <> x3 <> x4 <> t)) : Maybe<&2, Nat>}

def gle4 source · line 390 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_le(x0 <> x1 <> x2 <> x3 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(x0 <> x1 <> x2 <> x3 <> t)) : Maybe<&2, Nat>}

def gle3 source · line 397 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_le(x0 <> x1 <> x2 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(x0 <> x1 <> x2 <> t)) : Maybe<&2, Nat>}

def gle2 source · line 404 · raw

@+x0:U32 -> @+x1:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_le(x0 <> x1 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(x0 <> x1 <> t)) : Maybe<&2, Nat>}

def gle1 source · line 411 · raw

@+x0:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_le(x0 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(x0 <> t)) : Maybe<&2, Nat>}

def u64_from_le source · line 418 · raw

@bs:List<&2, U32> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.FromBytes.le(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_le, 8n, bs)

def gbe8 source · line 425 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_be(x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.reverse(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> t))) : Maybe<&2, Nat>}

def gbe7 source · line 432 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_be(x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.reverse(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> t))) : Maybe<&2, Nat>}

def gbe6 source · line 439 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_be(x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.reverse(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> t))) : Maybe<&2, Nat>}

def gbe5 source · line 446 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_be(x0 <> x1 <> x2 <> x3 <> x4 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.reverse(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(x0 <> x1 <> x2 <> x3 <> x4 <> t))) : Maybe<&2, Nat>}

def gbe4 source · line 453 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_be(x0 <> x1 <> x2 <> x3 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.reverse(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(x0 <> x1 <> x2 <> x3 <> t))) : Maybe<&2, Nat>}

def gbe3 source · line 460 · raw

@+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_be(x0 <> x1 <> x2 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.reverse(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(x0 <> x1 <> x2 <> t))) : Maybe<&2, Nat>}

def gbe2 source · line 467 · raw

@+x0:U32 -> @+x1:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_be(x0 <> x1 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.reverse(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(x0 <> x1 <> t))) : Maybe<&2, Nat>}

def gbe1 source · line 474 · raw

@+x0:U32 -> @t:List<&2, U32> -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.mval(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_be(x0 <> t)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.from_le(8n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.reverse(Nat, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.nats(x0 <> t))) : Maybe<&2, Nat>}

def u64_from_be source · line 481 · raw

@bs:List<&2, U32> -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/fixed.FromBytes.be(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/generic.u64_val, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/fixed.u64_from_bytes_be, 8n, bs)