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