~/bend-docscommunity

proofs/lib/lemmas/spec/numeric.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as Numeric

3 imports
import Base
import ../types/model.bend as T
import ../../../../spec/lib/numeric.bend as W

Definitions

def bit_value source · line 9 · raw

@b:Bool -> Nat

def unsigned source · line 12 · raw

@n:Nat -> @w:Word(n) -> Nat

def sign_threshold source · line 15 · raw

@n:Nat -> Word(1n+n)

def negative source · line 18 · raw

@+w:Word(64n) -> Bool

def zero source · line 21 · raw

@w:Word(64n) -> Bool

def order source · line 24 · raw

@a:Word(64n) -> @b:Word(64n) -> @sign_a:Bool -> @sign_b:Bool -> Bool

def expired source · line 27 · raw

@deadline:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64 -> @now:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64 -> Bool

def from_nat source · line 32 · raw

@n:Nat -> @+value:Nat -> Word(n)

def modulus source · line 35 · raw

Nat

def unsigned_quotient source · line 38 · raw

@n:Nat -> @word:Word(n) -> @d:U32 -> Word(n)

def negative_quotient source · line 41 · raw

@n:Nat -> @word:Word(n) -> @d:U32 -> Word(n)

def quotient_signed source · line 44 · raw

@bits:Word(64n) -> @negative:Bool -> Word(64n)

def milliseconds source · line 47 · raw

@duration:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64

def add source · line 51 · raw

@a:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64 -> @b:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64

def expiry_choose source · line 56 · raw

@now:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64 -> @duration:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64 -> @forever:Bool -> 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64

def deadline source · line 63 · raw

@now:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64 -> @duration:0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/types/model.Int64

def scale_binary source · line 67 · raw

@places:Nat -> @value:Nat -> Nat