~/bend-docscommunity

src/digits.bend checks

raw source on the hub · import 0xb6eebf6253ee268a21f3e308b12cacba/src/digits.bend as Digits

Digit sequences of a known length =================================

Digits(n) is a sequence of exactly n hexadecimal digits: the length is part of the type, so a trace ID is a Digits(32n) and a flag byte a Digits(2n). NonZero<n> adds the proof that the digits are not all zero, which W3C 3.2.2.3 and 3.2.2.4 require of trace and parent IDs. This module is internal to the package. proofs/digits.bend proves that n digits always format as n characters.

2 imports
import Base
import ./hex.bend as Hex

Types

type Digits.Nil source · line 18 · raw

Data

The length is part of the type. A Digits(32n) cannot contain 31 or 33 digits. This is the same type-family pattern that Base uses for Word(n).

The empty sequence: the only value of Digits(0n).

type Digits.Con source · line 22 · raw

@-p:Nat -> Data

A first digit followed by a sequence of p digits: a value of Digits(1n+p).

type NonZero source · line 84 · raw

@-n:Nat -> Data

n digits that are not all zero. evidence is the proof. The equality is checked statically; compiled evidence is a null placeholder. Keeping its binder usable lets later proofs recover and reuse this guarantee. Even direct construction must supply a proof that these digits are not zero.

Definitions

def Digits source · line 27 · raw

@n:Nat -> Data

The type of sequences of exactly n digits, computed from n: Digits(0n) is Digits.Nil and Digits(1n+p) is Digits.Con<p>.

def Digits.to_string source · line 35 · raw

@n:Nat -> @digits:Digits(n) -> String

The n lowercase characters of the digits, in order.

def Digits.is_zero source · line 45 · raw

@n:Nat -> @digits:Digits(n) -> Bool

Whether every digit is 0. The empty sequence counts as zero.

def Digits.of_u32 source · line 56 · raw

@word:U32 -> Digits(8n)

The eight digits of a word, most significant first: the first digit holds bits 31 to 28 and the last digit bits 3 to 0.

def Digits.to_u32 source · line 62 · raw

@digits:Digits(8n) -> U32

The word whose eight digits these are, most significant first.

def Digits.append source · line 69 · raw

@m:Nat -> @-n:Nat -> @left:Digits(m) -> @right:Digits(n) -> Digits(Nat.add(m, n))

The digits of left followed by those of right: m + n digits. Identifiers are built from source words this way, eight digits per word.

def NonZero.new.checked source · line 89 · raw

@-n:Nat -> @digits:Digits(n) -> @status:Bool -> @evidence:{Digits.is_zero(n, digits) == status : Bool} -> Maybe<&2, NonZero<n>>

Carry the equation into the branch: matching status refines its right side. The value is built only in the False case, where the equation is the proof.

def NonZero.new source · line 98 · raw

@+n:Nat -> @+digits:Digits(n) -> Maybe<&2, NonZero<n>>

Attach the proof that the digits are not all zero, or None when they are.

def NonZero.digits source · line 102 · raw

@-n:Nat -> @value:NonZero<n> -> Digits(n)

The digits, without their proof.

def NonZero.to_string source · line 108 · raw

@n:Nat -> @value:NonZero<n> -> String

The n lowercase characters of the digits.