1	import Base
2	import bend-mathlib@0.7.0.0/string.bend as MString
3	import bend-mathlib@0.7.0.0/bool.bend as MBool
4	
5	# Total-order comparison for keys. Base's String.cmp hands the strings back
6	# beside the verdict ((s1, s2), c); we take reusable copies and unpack via a
7	# helper (a match cannot scrutinize the computed call directly).
8	def unpack(pair: (String & String) & Cmp) -> Cmp:
9	  match pair:
10	    case ((_, _), c):
11	      c
12	
13	# Handle cmp in the key ordering and comparison.
14	def cmp(+s1: String, +s2: String) -> Cmp:
15	  unpack(String.cmp(s1, s2))
16	
17	# Handle eq in the key ordering and comparison.
18	def eq(+s1: String, +s2: String) -> Bool:
19	  String.eq(s1, s2)
20	
21	# Small, coherent views of Cmp used by key-order laws and sorted-run code.
22	def cmp_is_lt(ord: Cmp) -> Bool:
23	  Cmp.is_lt(ord)
24	
25	# Compare whether is eq holds for the key ordering and comparison.
26	def cmp_is_eq(ord: Cmp) -> Bool:
27	  Cmp.is_eq(ord)
28	
29	# Compare whether is gt holds for the key ordering and comparison.
30	def cmp_is_gt(ord: Cmp) -> Bool:
31	  Cmp.is_gt(ord)
32	
33	# Compare whether is le holds for the key ordering and comparison.
34	def cmp_is_le(ord: Cmp) -> Bool:
35	  Cmp.is_le(ord)
36	
37	# Handle lt in the key ordering and comparison.
38	def lt(+s1: String, +s2: String) -> Bool:
39	  cmp_is_lt(cmp(s1, s2))
40	
41	# Handle le in the key ordering and comparison.
42	def le(+s1: String, +s2: String) -> Bool:
43	  cmp_is_le(cmp(s1, s2))
44	
45	# Compare whether reverse holds for the key ordering and comparison.
46	def cmp_reverse(ord: Cmp) -> Cmp:
47	  match ord:
48	    case LT{}:
49	      GT{}
50	    case EQ{}:
51	      EQ{}
52	    case GT{}:
53	      LT{}
54	
55	# Handle implies in the key ordering and comparison.
56	def implies(s1: Bool, s2: Bool) -> Bool:
57	  match s1:
58	    case False{}:
59	      True{}
60	    case True{}:
61	      s2
62	
63	# Select f for the key ordering and comparison.
64	def iff(+s1: Bool, +s2: Bool) -> Bool:
65	  Bool.and(implies(s1, s2), implies(s2, s1))
66	
67	# True exactly when one of three arbitrary predicates is true.
68	def one_hot3(first: Bool, second: Bool, third: Bool) -> Bool:
69	  match first second third:
70	    case True{} False{} False{}:
71	      True{}
72	    case False{} True{} False{}:
73	      True{}
74	    case False{} False{} True{}:
75	      True{}
76	    case _ _ _:
77	      False{}
78	
79	# Cmp is intrinsically one-hot; this predicate gives K6 a reusable statement.
80	def cmp_one_hot(+ord: Cmp) -> Bool:
81	  one_hot3(cmp_is_lt(ord), cmp_is_eq(ord), cmp_is_gt(ord))
82	
83	# Compare whether one hot proof holds for the key ordering and comparison.
84	def cmp_one_hot_proof(+ord: Cmp) -> {cmp_one_hot(ord) == True{} : Bool}:
85	  match ord:
86	    case LT{}:
87	      {==}
88	    case EQ{}:
89	      {==}
90	    case GT{}:
91	      {==}
92	
93	# `String.eq` is defined by the EQ projection of `String.cmp` (Cmp.is_eq of
94	# Pair.snd since bend 2.0.33); matching the handed-back comparison pair
95	# exposes that definitional correspondence.
96	def cmp_eq_pair(
97	  pair: (String & String) & Cmp
98	) -> {cmp_is_eq(unpack(pair)) == Cmp.is_eq(Pair.snd(String & String, Cmp, pair)) : Bool}:
99	  match pair:
100	    case ((a, b), c):
101	      match c:
102	        case LT{}:
103	          {==}
104	        case EQ{}:
105	          {==}
106	        case GT{}:
107	          {==}
108	
109	# Compare whether eq bridge holds for the key ordering and comparison.
110	def cmp_eq_bridge(+s1: String, +s2: String) -> {cmp_is_eq(cmp(s1, s2)) == eq(s1, s2) : Bool}:
111	  cmp_eq_pair(String.cmp(s1, s2))
112	
113	# Reflexivity chain for open keys. Every product law about keyed lookup
114	# rewrites with str_eq_refl; it rests on the layers below, down to bits,
115	# proved in bend-mathlib's bool and string modules (hash-pinned by version).
116	# (Proving Base's own primitives is the one exception to the trust-root
117	# rule: without open-key comparison facts, NO keyed law is provable.)
118	
119	# Evaluate refl for the key ordering and comparison.
120	def bool_refl(+flag: Bool) -> {Bool.cmp(flag, flag) == EQ{} : Cmp}:
121	  MBool.cmp_refl(flag)
122	
123	# Handle word refl in the key ordering and comparison.
124	def word_refl(width: Nat, +word: Word(width)) -> {Word.cmp(width, word, word) == EQ{} : Cmp}:
125	  match width word:
126	    case 0n WNil{}:
127	      {==}
128	    case 1n+p WCon{ab, at}:
129	      match ab:
130	        case False{}:
131	          %Equal.sym(Cmp, Word.cmp(p, at, at), EQ{}, word_refl(p, at)) : {Word.cmp.fin(False{}, False{}, _) == EQ{} : Cmp}
132	          {==}
133	        case True{}:
134	          %Equal.sym(Cmp, Word.cmp(p, at, at), EQ{}, word_refl(p, at)) : {Word.cmp.fin(True{}, True{}, _) == EQ{} : Cmp}
135	          {==}
136	
137	# Encode or decode a 32-bit word for refl for the key ordering and comparison.
138	def u32_refl(+val: U32) -> {U32.cmp(val, val) == EQ{} : Cmp}:
139	  MString.u32_cmp_refl(val)
140	
141	# Handle char refl in the key ordering and comparison.
142	def char_refl(+ch: Char) -> {Char.cmp(ch, ch) == ((ch, ch), EQ{}) : (Char & Char) & Cmp}:
143	  MString.char_cmp_refl(ch)
144	
145	# Handle s cmp pair refl in the key ordering and comparison.
146	def s_cmp_pair_refl(+str: String) -> {String.cmp(str, str) == ((str, str), EQ{}) : (String & String) & Cmp}:
147	  MString.cmp_refl(str)
148	
149	# Handle str refl in the key ordering and comparison.
150	def str_refl(+str: String) -> {cmp(str, str) == EQ{} : Cmp}:
151	  %Equal.sym((String & String) & Cmp, String.cmp(str, str), ((str, str), EQ{}), s_cmp_pair_refl(str)) : {unpack(_) == EQ{} : Cmp}
152	  {==}
153	
154	# Handle str eq refl in the key ordering and comparison.
155	def str_eq_refl(+str: String) -> {eq(str, str) == True{} : Bool}:
156	  MString.eq_refl(str)