~/bend-docscommunity

src/digits.bend checks

raw source on the hub · import 0x665ae73e3f32ce98f72c7cf6844cfd3f/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, and proofs/bytes.bend that the bytes of 2n digits, two digits per byte, read back as those digits.

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

Types

type Digits.Nil source · line 19 · 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 23 · raw

@-p:Nat -> Data

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

type NonZero source · line 112 · 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 28 · 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 36 · raw

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

The n lowercase characters of the digits, in order.

def Digits.is_zero source · line 46 · raw

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

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

def Digits.of_u32 source · line 57 · 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 63 · raw

@digits:Digits(8n) -> U32

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

def Digits.to_byte source · line 71 · raw

@digits:Digits(2n) -> U32

The byte of two digits, the high digit first: 16 times the high digit plus the low one, from 0 to 255. Its bits 7 to 4 are the high digit's, bits 3 to 0 the low digit's, and the other 24 bits are zero.

def Digits.of_byte source · line 79 · raw

@byte:U32 -> Digits(2n)

The two digits of a byte, the high digit first: bits 7 to 4, then bits 3 to 0. The other bits are not read, so the caller first checks that the word is at most 255.

def Digits.to_bytes source · line 86 · raw

@n:Nat -> @digits:Digits(Nat.double(n)) -> List<&2, U32>

The n bytes of 2n digits, most significant first: each byte takes the next two digits, the first of them high.

def Digits.append source · line 97 · 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 117 · 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 126 · 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 130 · raw

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

The digits, without their proof.

def NonZero.to_string source · line 136 · raw

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

The n lowercase characters of the digits.