src/hex.bend checks

raw source on the hub · import 0x665ae73e3f32ce98f72c7cf6844cfd3f/src/hex.bend as Hex

Hexadecimal digits ==================

The sixteen lowercase hexadecimal digits as a closed type, with their characters, values and bits. The codec reads identifiers and flags into this type, so anything other than a lowercase hexadecimal digit (W3C 3.2.2, HEXDIGLC) cannot appear in a parsed value. This module is internal: callers handle identifiers as text through trace_context.bend. proofs/hex.bend proves that decoding inverts encoding: every digit's character decodes back to it, and an accepted character is exactly the encoding of the digit returned.

1 import

import Base

Types

type Digit source · line 16 · raw

Data

A hexadecimal digit has exactly these sixteen values, H0 to Hf, in value order. Encoding is lowercase.

H0
```
Digit
```
H1
```
Digit
```
H2
```
Digit
```
H3
```
Digit
```
H4
```
Digit
```
H5
```
Digit
```
H6
```
Digit
```
H7
```
Digit
```
H8
```
Digit
```
H9
```
Digit
```
Ha
```
Digit
```
Hb
```
Digit
```
Hc
```
Digit
```
Hd
```
Digit
```
He
```
Digit
```
Hf
```
Digit
```

Definitions

def Digit.to_char source · line 35 · raw

@digit:Digit -> Char

The lowercase character of a digit: '0' to '9', then 'a' to 'f'.

def Digit.to_u32 source · line 71 · raw

@digit:Digit -> U32

The value of a digit, 0 to 15.

def Digit.is_zero source · line 107 · raw

@digit:Digit -> Bool

Whether the digit is 0. An identifier is all zero when every digit is.

def Digit.is_odd source · line 144 · raw

@digit:Digit -> Bool

Whether bit 0 (value 1) of the digit is set. In the last digit of the flags this is the sampled flag (W3C 3.2.2.5.1).

def Digit.has_bit1 source · line 181 · raw

@digit:Digit -> Bool

Whether bit 1 (value 2) of the digit is set. In the last digit of the flags this is the random-trace-id flag (W3C 3.2.2.5.2).

def Digit.has_bit2 source · line 217 · raw

@digit:Digit -> Bool

Whether bit 2 (value 4) of the digit is set.

def Digit.has_bit3 source · line 253 · raw

@digit:Digit -> Bool

Whether bit 3 (value 8) of the digit is set.

def Digit.from_bits source · line 289 · raw

@bit0:Bool -> @bit1:Bool -> @bit2:Bool -> @bit3:Bool -> Digit

The digit whose value is bit0 + 2 * bit1 + 4 * bit2 + 8 * bit3.

def Digit.all source · line 325 · raw

List<&2, Digit>

Every digit, in encoding order.

def Digit.from_char.find source · line 331 · raw

@digits:List<&2, Digit> -> @+char:Char -> Maybe<&2, Digit>

Search the encoder's own alphabet, so an accepted character is exactly the encoding of the digit returned for it.

def Digit.from_char source · line 341 · raw

@char:Char -> Maybe<&2, Digit>

The digit a character encodes. Uppercase and every non-hexadecimal character are rejected with None.