src/digits.bend

bend-trace-context@0.2.0.0 · 137 lines · 16 definitions

1# Digit sequences of a known length
2# =================================
3#
4# Digits(n) is a sequence of exactly n hexadecimal digits: the length is part
5# of the type, so a trace ID is a Digits(32n) and a flag byte a Digits(2n).
6# NonZero<n> adds the proof that the digits are not all zero, which W3C 3.2.2.3
7# and 3.2.2.4 require of trace and parent IDs. This module is internal to the
8# package. proofs/digits.bend proves that n digits always format as n
9# characters, and proofs/bytes.bend that the bytes of 2n digits, two digits
10# per byte, read back as those digits.
11
12import Base
13import bend-trace-context@0.2.0.0/src/hex.bend as Hex
14
15# The length is part of the type. A Digits(32n) cannot contain 31 or 33 digits.
16# This is the same type-family pattern that Base uses for Word(n).
17#
18# The empty sequence: the only value of Digits(0n).
19type Digits.Nil is Data:
20  DNil{}
21
22# A first digit followed by a sequence of p digits: a value of Digits(1n+p).
23type Digits.Con<-p: Nat> is Data:
24  DCon{head: Hex.Digit, tail: Digits(p)}
25
26# The type of sequences of exactly n digits, computed from n: Digits(0n) is
27# Digits.Nil and Digits(1n+p) is Digits.Con<p>.
28def Digits(n: Nat) -> Data:
29  match n:
30    case 0n:
31      Digits.Nil
32    case 1n+p:
33      Digits.Con<p>
34
35# The n lowercase characters of the digits, in order.
36def Digits.to_string(n: Nat, digits: Digits(n)) -> String:
37  match n:
38    case 0n:
39      ""
40    case 1n+p:
41      match digits:
42        case DCon{head, tail}:
43          SCon{Hex.Digit.to_char(head), Digits.to_string(p, tail)}
44
45# Whether every digit is 0. The empty sequence counts as zero.
46def Digits.is_zero(n: Nat, digits: Digits(n)) -> Bool:
47  match n:
48    case 0n:
49      True{}
50    case 1n+p:
51      match digits:
52        case DCon{head, tail}:
53          Bool.and(Hex.Digit.is_zero(head), Digits.is_zero(p, tail))
54
55# The eight digits of a word, most significant first: the first digit holds
56# bits 31 to 28 and the last digit bits 3 to 0.
57def Digits.of_u32(word: U32) -> Digits(8n):
58  match word:
59    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
60      DCon{Hex.Digit.from_bits(b28, b29, b30, b31), DCon{Hex.Digit.from_bits(b24, b25, b26, b27), DCon{Hex.Digit.from_bits(b20, b21, b22, b23), DCon{Hex.Digit.from_bits(b16, b17, b18, b19), DCon{Hex.Digit.from_bits(b12, b13, b14, b15), DCon{Hex.Digit.from_bits(b8, b9, b10, b11), DCon{Hex.Digit.from_bits(b4, b5, b6, b7), DCon{Hex.Digit.from_bits(b0, b1, b2, b3), DNil{}}}}}}}}}
61
62# The word whose eight digits these are, most significant first.
63def Digits.to_u32(digits: Digits(8n)) -> U32:
64  match digits:
65    case DCon{+d7, DCon{+d6, DCon{+d5, DCon{+d4, DCon{+d3, DCon{+d2, DCon{+d1, DCon{+d0, DNil{}}}}}}}}}:
66      U32{WCon{Hex.Digit.is_odd(d0), WCon{Hex.Digit.has_bit1(d0), WCon{Hex.Digit.has_bit2(d0), WCon{Hex.Digit.has_bit3(d0), WCon{Hex.Digit.is_odd(d1), WCon{Hex.Digit.has_bit1(d1), WCon{Hex.Digit.has_bit2(d1), WCon{Hex.Digit.has_bit3(d1), WCon{Hex.Digit.is_odd(d2), WCon{Hex.Digit.has_bit1(d2), WCon{Hex.Digit.has_bit2(d2), WCon{Hex.Digit.has_bit3(d2), WCon{Hex.Digit.is_odd(d3), WCon{Hex.Digit.has_bit1(d3), WCon{Hex.Digit.has_bit2(d3), WCon{Hex.Digit.has_bit3(d3), WCon{Hex.Digit.is_odd(d4), WCon{Hex.Digit.has_bit1(d4), WCon{Hex.Digit.has_bit2(d4), WCon{Hex.Digit.has_bit3(d4), WCon{Hex.Digit.is_odd(d5), WCon{Hex.Digit.has_bit1(d5), WCon{Hex.Digit.has_bit2(d5), WCon{Hex.Digit.has_bit3(d5), WCon{Hex.Digit.is_odd(d6), WCon{Hex.Digit.has_bit1(d6), WCon{Hex.Digit.has_bit2(d6), WCon{Hex.Digit.has_bit3(d6), WCon{Hex.Digit.is_odd(d7), WCon{Hex.Digit.has_bit1(d7), WCon{Hex.Digit.has_bit2(d7), WCon{Hex.Digit.has_bit3(d7), WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
67
68# The byte of two digits, the high digit first: 16 times the high digit plus
69# the low one, from 0 to 255. Its bits 7 to 4 are the high digit's, bits 3 to
70# 0 the low digit's, and the other 24 bits are zero.
71def Digits.to_byte(digits: Digits(2n)) -> U32:
72  match digits:
73    case DCon{+high, DCon{+low, DNil{}}}:
74      U32{WCon{Hex.Digit.is_odd(low), WCon{Hex.Digit.has_bit1(low), WCon{Hex.Digit.has_bit2(low), WCon{Hex.Digit.has_bit3(low), WCon{Hex.Digit.is_odd(high), WCon{Hex.Digit.has_bit1(high), WCon{Hex.Digit.has_bit2(high), WCon{Hex.Digit.has_bit3(high), Word.zero(24n)}}}}}}}}}
75
76# The two digits of a byte, the high digit first: bits 7 to 4, then bits 3 to
77# 0. The other bits are not read, so the caller first checks that the word is
78# at most 255.
79def Digits.of_byte(byte: U32) -> Digits(2n):
80  match byte:
81    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, rest}}}}}}}}}:
82      DCon{Hex.Digit.from_bits(b4, b5, b6, b7), DCon{Hex.Digit.from_bits(b0, b1, b2, b3), DNil{}}}
83
84# The n bytes of 2n digits, most significant first: each byte takes the next
85# two digits, the first of them high.
86def Digits.to_bytes(n: Nat, digits: Digits(Nat.double(n))) -> List<&2, U32>:
87  match n:
88    case 0n:
89      Nil{}
90    case 1n+p:
91      match digits:
92        case DCon{high, DCon{low, rest}}:
93          Con{Digits.to_byte(DCon{high, DCon{low, DNil{}}}), Digits.to_bytes(p, rest)}
94
95# The digits of `left` followed by those of `right`: m + n digits. Identifiers
96# are built from source words this way, eight digits per word.
97def Digits.append(m: Nat, -n: Nat, left: Digits(m), right: Digits(n)) -> Digits(Nat.add(m, n)):
98  match m:
99    case 0n:
100      match left:
101        case DNil{}:
102          right
103    case 1n+p:
104      match left:
105        case DCon{head, tail}:
106          DCon{head, Digits.append(p, n, tail, right)}
107
108# n digits that are not all zero. `evidence` is the proof. The equality is
109# checked statically; compiled evidence is a null placeholder. Keeping its
110# binder usable lets later proofs recover and reuse this guarantee. Even direct
111# construction must supply a proof that these digits are not zero.
112type NonZero<-n: Nat> is Data:
113  NonZero{digits: Digits(n), evidence: {Digits.is_zero(n, digits) == False{} : Bool}}
114
115# Carry the equation into the branch: matching status refines its right side.
116# The value is built only in the False case, where the equation is the proof.
117def NonZero.new.checked(-n: Nat, digits: Digits(n), status: Bool,
118  evidence: {Digits.is_zero(n, digits) == status : Bool}) -> Maybe<&2, NonZero<n>>:
119  match status:
120    case True{}:
121      None{}
122    case False{}:
123      Some{NonZero{digits, evidence}}
124
125# Attach the proof that the digits are not all zero, or None when they are.
126def NonZero.new(+n: Nat, +digits: Digits(n)) -> Maybe<&2, NonZero<n>>:
127  NonZero.new.checked(n, digits, Digits.is_zero(n, digits), {==})
128
129# The digits, without their proof.
130def NonZero.digits(-n: Nat, value: NonZero<n>) -> Digits(n):
131  match value:
132    case NonZero{digits, evidence}:
133      digits
134
135# The n lowercase characters of the digits.
136def NonZero.to_string(n: Nat, value: NonZero<n>) -> String:
137  Digits.to_string(n, NonZero.digits(n, value))