proofs/bounded_u32_arithmetic.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as Bounded_u32_arithmetic

Machine operations -> unbounded Nat, with explicit no-overflow obligations.

8 imports

import Base
import ./word_arithmetic.bend as WordArithmetic
import ./word_multiplication.bend as Multiplication
import ./word_subtraction.bend as Subtraction
import ./nat_to_u32_bounds.bend as Bounds
import ./natural_addition.bend as Addition
import ./nat_order.bend as Order
import ./u32_comparison.bend as Comparison

Definitions

def count_within source · line 11 · raw

@+count:U32 -> @+length:Nat -> @+capacity:U32 -> @+upper:U32 -> @exact:{U32.to_nat(count) == length : Nat} -> @room:{Nat.is_le(length, U32.to_nat(capacity)) == True{} : Bool} -> @capacity_bound:{U32.is_le(capacity, upper) == True{} : Bool} -> {U32.is_le(count, upper) == True{} : Bool}

def native_roundtrip source · line 18 · raw

@+a:U32 -> {U32.from_nat(U32.to_nat(a)) == a : U32}

def native_add source · line 26 · raw

@+a:U32 -> @+b:U32 -> {U32.add(a, b) == U32.from_nat(Nat.add(U32.to_nat(a), U32.to_nat(b))) : U32}

def add_zero source · line 31 · raw

@+value:U32 -> {U32.add(value, 0) == value : U32}

def add_commutative source · line 36 · raw

@+left:U32 -> @+right:U32 -> {U32.add(left, right) == U32.add(right, left) : U32}

def add_zero_left source · line 45 · raw

@+value:U32 -> {U32.add(0, value) == value : U32}

def multiply_zero_left source · line 48 · raw

@+value:U32 -> {U32.mul(0, value) == 0 : U32}

def encoded_add_associative source · line 52 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {U32.add(U32.add(U32.from_nat(a), U32.from_nat(b)), U32.from_nat(c)) == U32.add(U32.from_nat(a), U32.add(U32.from_nat(b), U32.from_nat(c))) : U32}

These are modular identities, so they require no no-overflow assumption.

def add_associative source · line 63 · raw

@+a:U32 -> @+b:U32 -> @+c:U32 -> {U32.add(U32.add(a, b), c) == U32.add(a, U32.add(b, c)) : U32}

def subtract_from_sum source · line 69 · raw

@+a:U32 -> @+b:U32 -> @+c:U32 -> {U32.sub(U32.add(a, b), c) == U32.add(a, U32.sub(b, c)) : U32}

def add_after_subtract source · line 74 · raw

@+value:U32 -> @+padding:U32 -> @+offset:U32 -> {U32.add(U32.sub(value, padding), offset) == U32.sub(U32.add(value, offset), padding) : U32}

def native_subtract source · line 81 · raw

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

def add source · line 87 · raw

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

def subtract source · line 93 · raw

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

def remove_prefix source · line 100 · raw

@+value:U32 -> @+base:U32 -> @+local:Nat -> @+capacity:U32 -> @capacity_ok:{U32.is_le(capacity, 2147483648) == True{} : Bool} -> @+exact:{U32.to_nat(value) == Nat.add(U32.to_nat(base), local) : Nat} -> @room:{Nat.is_le(U32.to_nat(value), U32.to_nat(capacity)) == True{} : Bool} -> {U32.to_nat(U32.sub(value, base)) == local : Nat}

def subtract_zero source · line 113 · raw

@+value:U32 -> {U32.sub(value, 0) == value : U32}

def multiply source · line 118 · raw

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