1	import Base
2	import ../types/model.bend as T
3	
4	# Identity preserves all Base String characters, including Chr{0}.
5	def string_encode(s: String) -> String:
6	  s
7	
8	def 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.
13	def 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	
20	def natural_decode(s: String) -> Nat:
21	  String.length(s)
22	
23	def 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	
30	def 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	
37	def 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	
44	law string_roundtrip:
45	  for s: String
46	  {string_decode(string_encode(s)) == s : String}
47	def string_roundtrip(s):
48	  {==}
49	
50	law natural_roundtrip:
51	  for n: Nat
52	  {natural_decode(natural_encode(n)) == n : Nat}
53	def 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	
61	law integer_roundtrip:
62	  for n: T.Integer
63	  {integer_decode(integer_encode(n)) == n : T.Integer}
64	def 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	
71	law 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}
76	def 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	
82	law string_injective:
83	  for a: String
84	  for b: String
85	  for e: {string_encode(a) == string_encode(b) : String}
86	  {a == b : String}
87	def 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.
92	def bit_char(b: Bool) -> Char:
93	  match b:
94	    case False{}:
95	      '0'
96	    case True{}:
97	      '1'
98	
99	def char_bit(c: Char) -> Bool:
100	  match c:
101	    case Chr{x}:
102	      U32.is_eq(x, 49)
103	
104	def 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	
113	def 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	
122	law bit_roundtrip:
123	  for b: Bool
124	  {char_bit(bit_char(b)) == b : Bool}
125	def bit_roundtrip(b):
126	  match b:
127	    case False{}:
128	      {==}
129	    case True{}:
130	      {==}
131	
132	law word_roundtrip:
133	  for n: Nat
134	  for w: Word(n)
135	  {word_decode(n, word_encode(n, w)) == w : Word(n)}
136	def 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	
149	law 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)}
155	def 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	
161	law 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}
166	def string_equality_preserved(a, b, e):
167	  e
168	
169	law 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}
174	def integer_equality_preserved(a, b, e):
175	  Equal.cong(T.Integer, String, integer_encode, a, b, e)
176	
177	law 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}
183	def 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.
187	def word64_encode(w: Word(64n)) -> String:
188	  word_encode(64n, w)
189	
190	law 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)}
195	def word64_injective(a, b, e):
196	  word_injective(64n, a, b, e)