proofs/u32_comparison.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/u32_comparison.bend as U32_comparison

import Base

Laws

@+a:Nat -> @+b:Nat -> @+ab:Bool -> @+bb:Bool -> {Nat.cmp(digit(ab, a), digit(bb, b)) == Word.cmp.fin(ab, bb, Nat.cmp(a, b)) : Cmp}

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}

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

Definitions

@bit:Bool -> @n:Nat -> Nat

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

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

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

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