proofs/lib/lemmas/src/codec.bend
bend-collections-laws-containers@1.0.0.0 · 196 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
3
4# Identity preserves all Base String characters, including Chr{0}.
5def string_encode(s: String) -> String:
6 s
7
8def string_decode(s: String) -> String:
9 s
10
11# A unary integer codec: chosen for a simple total inverse, not speed.
12# Every character has code 0; the first character encodes the sign.
13def natural_encode(n: Nat) -> String:
14 match n:
15 case 0n:
16 SNil{}
17 case 1n+p:
18 SCon{Chr{0}, natural_encode(p)}
19
20def natural_decode(s: String) -> Nat:
21 String.length(s)
22
23def integer_encode(n: T.Integer) -> String:
24 match n:
25 case T.Positive{p}:
26 SCon{Chr{1}, natural_encode(p)}
27 case T.Negative{p}:
28 SCon{Chr{0}, natural_encode(p)}
29
30def integer_decode_sign(sign: Bool, n: Nat) -> T.Integer:
31 match sign:
32 case True{}:
33 T.Negative{n}
34 case False{}:
35 T.Positive{n}
36
37def integer_decode(s: String) -> T.Integer:
38 match s:
39 case SNil{}:
40 T.Positive{0n}
41 case SCon{Chr{c}, t}:
42 integer_decode_sign(U32.is_zero(c), natural_decode(t))
43
44law string_roundtrip:
45 for s: String
46 {string_decode(string_encode(s)) == s : String}
47def string_roundtrip(s):
48 {==}
49
50law natural_roundtrip:
51 for n: Nat
52 {natural_decode(natural_encode(n)) == n : Nat}
53def natural_roundtrip(n):
54 match n:
55 case 0n:
56 {==}
57 case 1n+p:
58 %natural_roundtrip(p) : {1n+natural_decode(natural_encode(p)) == 1n+_ : Nat}
59 {==}
60
61law integer_roundtrip:
62 for n: T.Integer
63 {integer_decode(integer_encode(n)) == n : T.Integer}
64def integer_roundtrip(n):
65 match n:
66 case T.Positive{p}:
67 Equal.cong(Nat, T.Integer, x => T.Positive{x}, natural_decode(natural_encode(p)), p, natural_roundtrip(p))
68 case T.Negative{p}:
69 Equal.cong(Nat, T.Integer, x => T.Negative{x}, natural_decode(natural_encode(p)), p, natural_roundtrip(p))
70
71law integer_injective:
72 for a: T.Integer
73 for b: T.Integer
74 for e: {integer_encode(a) == integer_encode(b) : String}
75 {a == b : T.Integer}
76def integer_injective(a, b, e):
77 Equal.trans(T.Integer, a, integer_decode(integer_encode(a)), b,
78 Equal.sym(T.Integer, integer_decode(integer_encode(a)), a, integer_roundtrip(a)),
79 Equal.trans(T.Integer, integer_decode(integer_encode(a)), integer_decode(integer_encode(b)), b,
80 Equal.cong(String, T.Integer, integer_decode, integer_encode(a), integer_encode(b), e), integer_roundtrip(b)))
81
82law string_injective:
83 for a: String
84 for b: String
85 for e: {string_encode(a) == string_encode(b) : String}
86 {a == b : String}
87def string_injective(a, b, e):
88 e
89
90# Fixed-width binary words are a practical integer codec; unlike unary Integer,
91# a 64-bit key always occupies 64 characters. Leading zero bits are retained.
92def bit_char(b: Bool) -> Char:
93 match b:
94 case False{}:
95 '0'
96 case True{}:
97 '1'
98
99def char_bit(c: Char) -> Bool:
100 match c:
101 case Chr{x}:
102 U32.is_eq(x, 49)
103
104def word_encode(n: Nat, w: Word(n)) -> String:
105 match n:
106 case 0n:
107 SNil{}
108 case 1n+p:
109 match w:
110 case WCon{b, rest}:
111 SCon{bit_char(b), word_encode(p, rest)}
112
113def word_decode(n: Nat, s: String) -> Word(n):
114 match n s:
115 case 0n rest:
116 WNil{}
117 case 1n+p SNil{}:
118 WCon{False{}, word_decode(p, SNil{})}
119 case 1n+p SCon{h, t}:
120 WCon{char_bit(h), word_decode(p, t)}
121
122law bit_roundtrip:
123 for b: Bool
124 {char_bit(bit_char(b)) == b : Bool}
125def bit_roundtrip(b):
126 match b:
127 case False{}:
128 {==}
129 case True{}:
130 {==}
131
132law word_roundtrip:
133 for n: Nat
134 for w: Word(n)
135 {word_decode(n, word_encode(n, w)) == w : Word(n)}
136def word_roundtrip(n, w):
137 match n:
138 case 0n:
139 match w:
140 case WNil{}:
141 {==}
142 case 1n+p:
143 match w:
144 case WCon{b, rest}:
145 %bit_roundtrip(b) : {WCon{char_bit(bit_char(b)), word_decode(p, word_encode(p, rest))} == WCon{_, rest} : Word(1n+p)}
146 %word_roundtrip(p, rest) : {WCon{char_bit(bit_char(b)), word_decode(p, word_encode(p, rest))} == WCon{char_bit(bit_char(b)), _} : Word(1n+p)}
147 {==}
148
149law word_injective:
150 for +n: Nat
151 for a: Word(n)
152 for b: Word(n)
153 for e: {word_encode(n, a) == word_encode(n, b) : String}
154 {a == b : Word(n)}
155def word_injective(n, a, b, e):
156 Equal.trans(Word(n), a, word_decode(n, word_encode(n, a)), b,
157 Equal.sym(Word(n), word_decode(n, word_encode(n, a)), a, word_roundtrip(n, a)),
158 Equal.trans(Word(n), word_decode(n, word_encode(n, a)), word_decode(n, word_encode(n, b)), b,
159 Equal.cong(String, Word(n), word_decode(n), word_encode(n, a), word_encode(n, b), e), word_roundtrip(n, b)))
160
161law string_equality_preserved:
162 for a: String
163 for b: String
164 for e: {a == b : String}
165 {string_encode(a) == string_encode(b) : String}
166def string_equality_preserved(a, b, e):
167 e
168
169law integer_equality_preserved:
170 for a: T.Integer
171 for b: T.Integer
172 for e: {a == b : T.Integer}
173 {integer_encode(a) == integer_encode(b) : String}
174def integer_equality_preserved(a, b, e):
175 Equal.cong(T.Integer, String, integer_encode, a, b, e)
176
177law word_equality_preserved:
178 for n: Nat
179 for a: Word(n)
180 for b: Word(n)
181 for e: {a == b : Word(n)}
182 {word_encode(n, a) == word_encode(n, b) : String}
183def word_equality_preserved(n, a, b, e):
184 Equal.cong(Word(n), String, word_encode(n), a, b, e)
185
186# The Word64 key codec used by the adapter for bigint keys.
187def word64_encode(w: Word(64n)) -> String:
188 word_encode(64n, w)
189
190law word64_injective:
191 for a: Word(64n)
192 for b: Word(64n)
193 for e: {word64_encode(a) == word64_encode(b) : String}
194 {a == b : Word(64n)}
195def word64_injective(a, b, e):
196 word_injective(64n, a, b, e)