proofs/nat_to_u32_bounds.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Nat_to_u32_bounds

Safe Nat -> U32 -> Nat conversion over the candidate's finite envelope.

4 imports

import Base
import ./u32_successor.bend as U32Successor
import ./u32_comparison.bend as Comparison
import ./word_encoding.bend as WordEncoding

Laws

law roundtrip provedsource · line 71 · raw

@+n:Nat -> @+cap:U32 -> @+cap_ok:{U32.is_le(cap, 2147483648) == True{} : Bool} -> @h:{Nat.is_le(n, U32.to_nat(cap)) == True{} : Bool} -> {U32.to_nat(U32.from_nat(n)) == n : Nat}

Definitions

def predecessor_strict source · line 7 · raw

@+a:Nat -> @+b:Nat -> @h:{Nat.is_le(1n+a, b) == True{} : Bool} -> {Nat.is_lt(a, b) == True{} : Bool}

def strict_le source · line 18 · raw

@+a:Nat -> @+b:Nat -> @h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_le(a, b) == True{} : Bool}

def add_one source · line 29 · raw

@+i:U32 -> {U32.add(i, 1) == U32.inc(i) : U32}

def native_bound source · line 35 · raw

@+n:Nat -> @+cap:U32 -> @e:{U32.to_nat(U32.from_nat(n)) == n : Nat} -> @h:{Nat.is_lt(n, U32.to_nat(cap)) == True{} : Bool} -> {U32.is_lt(U32.from_nat(n), cap) == True{} : Bool}

def nat_trans source · line 42 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @ab:{Nat.is_lt(a, b) == True{} : Bool} -> @bc:{Nat.is_le(b, c) == True{} : Bool} -> {Nat.is_lt(a, c) == True{} : Bool}

def as_nat_lt source · line 58 · raw

@+a:U32 -> @+b:U32 -> @h:{U32.is_lt(a, b) == True{} : Bool} -> {Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == True{} : Bool}

def as_nat_le source · line 62 · raw

@+a:U32 -> @+b:U32 -> @h:{U32.is_le(a, b) == True{} : Bool} -> {Nat.is_le(U32.to_nat(a), U32.to_nat(b)) == True{} : Bool}

def uint_trans source · line 66 · raw

@+a:U32 -> @+b:U32 -> @+c:U32 -> @ab:{U32.is_lt(a, b) == True{} : Bool} -> @bc:{U32.is_le(b, c) == True{} : Bool} -> {U32.is_lt(a, c) == True{} : Bool}