1	import Base
2	
3	# bend-schema: a schema, and one check for every schema, proved once.
4	#
5	# Source, laws, proofs and the TypeScript package (npm: bend-schema):
6	# https://github.com/nohzafk/bend-schema
7	#
8	# THE INPUT (Raw)
9	#
10	# The host makes a Raw from a JSON value in two steps.
11	#
12	# 1. One universal codec makes the Raw. It knows no schema.
13	#    - A whole number from 0 to 2^48-1 becomes RNum.
14	#    - A whole number from -(2^48-1) to -1 becomes RNeg.
15	#    - A boolean becomes RBool, null becomes RNull, a string becomes RStr.
16	#    - An array becomes a chain of RCons that ends in RNil.
17	#    - A plain object becomes a chain of RKey that ends in REnd.
18	#    - All other values become RBad: a fraction, a number out of range, NaN,
19	#      undefined, and an object that is not plain (for example a Date).
20	#    The codec also counts elements and keys, and the nesting depth. An array
21	#    or an object that goes past a limit becomes one RTooBig in its place.
22	#    The core reports RTooBig as TooLarge at the path of that node. The codec
23	#    applies a limit because the core cannot: a limit is about size, not shape.
24	#
25	# 2. At each SJson position of the schema, the host replaces the Raw with
26	#    RJson. RJson holds a Json value, which keeps any number as its binary64
27	#    bits. A value that is not JSON stays RBad. If a limit was hit anywhere
28	#    inside the position, the whole position becomes RTooBig.
29	#
30	# The codec never makes RMissing. A lookup of a key that is not there gives
31	# RMissing.
32	#
33	# THE CHECK
34	#
35	# A Schema tells what a valid value is (`conforms`). `check` finds the first
36	# error and gives its path. The order is:
37	#   - depth first;
38	#   - list elements in order;
39	#   - object fields in the order of the schema;
40	#   - for a bounded string, the inner value first and then the bound;
41	#   - for an SListLen, the element count first and then the elements.
42	#
43	# The check ignores keys that the schema does not name. A key that the schema
44	# names must be there. Two constructors allow less:
45	#   - SOpt: the value may be null.
46	#   - SOptional: the field may be absent. The host then writes no key. SOptional
47	#     is well-formed only as the schema of a field.
48	#
49	# `conforms` and `check` each walk the schema and the value together, in one
50	# self-recursive def. A step into a field or an optional makes the schema
51	# smaller. A step along a list keeps the schema and makes the value smaller.
52	# The termination checker reads the arguments from left to right until one
53	# gets smaller.
54	#
55	# RULES
56	#
57	# A project gives its rules as one template parameter,
58	# `~rule: Nat -> Raw -> Maybe<Err>`. At an SRule, the value must first conform
59	# to the schema of the rule. Then the rule decides. The tag selects the rule.
60	# The error path of a rule is relative to the value that the rule gets.
61	# A template def cannot go through the bundler, so the host calls the closed
62	# forms below (check0, conforms0). The check carries `prev`, but no case reads
63	# it now. A combinator with state can use it.
64	
65	type NumberBits is Data:
66	  NumberBits{hi: U32, lo: U32}
67	
68	type Json is Data:
69	  JNull{}
70	  JBool{value: Bool}
71	  JNumber{value: NumberBits}
72	  JString{value: String}
73	  JArray{values: List<&2, Json>}
74	  JObject{members: List<&2, JMember>}
75	
76	type JMember is Data:
77	  JMember{key: String, value: Json}
78	
79	# A whole number of either sign: IPos{n} is n, INeg{n} is -(n+1), so every
80	# integer has exactly one form (there is no -0).
81	type Int is Data:
82	  IPos{n: Nat}
83	  INeg{n: Nat}
84	
85	type Raw is Data:
86	  RNum{n: Nat}
87	  RBool{b: Bool}
88	  RNull{}
89	  RStr{s: String}
90	  RBad{}
91	  RTooBig{}
92	  RMissing{}
93	  RNil{}
94	  RCons{head: Raw, tail: Raw}
95	  REnd{}
96	  RKey{key: String, val: Raw, rest: Raw}
97	  RJson{value: Json}
98	  RNeg{n: Nat}
99	
100	type Schema is Data:
101	  SNat{}
102	  SNatIn{lo: Nat, hi: Nat}
103	  SStr{}
104	  SStrLen{lo: Nat, hi: Nat, s: Schema}
105	  SOpt{inner: Schema}
106	  SList{elem: Schema}
107	  SField{name: String, s: Schema, rest: Schema}
108	  SEnd{}
109	  SRule{s: Schema, tag: Nat}
110	  SStrict{s: Schema}
111	  STagged{key: String, name: String, s: Schema, rest: Schema}
112	  STagEnd{key: String}
113	  SBool{}
114	  STrue{}
115	  SEnum{names: List<&2, String>}
116	  SVariant{name: String, s: Schema, rest: Schema}
117	  SVEnd{}
118	  STuple{s: Schema, rest: Schema}
119	  STEnd{}
120	  SOptional{inner: Schema}
121	  SListLen{lo: Nat, hi: Nat, s: Schema}
122	  SJson{}
123	  SInt{}
124	  SIntIn{lo: Int, hi: Int}
125	  SEither{l: Schema, r: Schema}
126	
127	# A step of a path. Positions count what was passed on the way, so that
128	# following a path never compares two names: AtIndex{i} is element i of a
129	# list, AtField{skip, name} the field `skip` places after this one in the
130	# schema, BoundAt{i, key} the bound of element i of a bounded list. The names
131	# are for the host to print.
132	type Step is Data:
133	  AtIndex{i: Nat}
134	  AtField{skip: Nat, name: String}
135	  BoundAt{i: Nat, key: String}
136	  AtKey{key: String}
137	
138	type Why is Data:
139	  Missing{}
140	  NotNat{}
141	  NotString{}
142	  NotBool{}
143	  NotList{}
144	  NotObject{}
145	  NoElements{}
146	  OpenNotLast{}
147	  LastNotOpen{}
148	  NotIncreasing{prev: Nat, got: Nat}
149	  NotTrue{}
150	  NotOneOf{}
151	  NoVariant{}
152	  TwoVariants{}
153	  TooShort{}
154	  TooLong{}
155	  LengthNotIn{lo: Nat, hi: Nat}
156	  NotIn{lo: Nat, hi: Nat}
157	  UnknownKey{}
158	  RepeatedKey{key: String}
159	  TooLarge{}
160	  CountNotIn{lo: Nat, hi: Nat}
161	  NotJson{}
162	  NotInt{}
163	  IntNotIn{lo: Int, hi: Int}
164	  NoAlternative{num: Bool, str: Bool, bool: Bool, list: Bool, obj: Bool, null: Bool}
165	
166	type Err is Data:
167	  Err{path: List<&2, Step>, why: Why}
168	
169	# JSON numbers use IEEE-754 binary64 bits. The exponent occupies the high
170	# word's bits 20 through 30; all ones denotes infinity or NaN.
171	def finite_number(bits: NumberBits) -> Bool:
172	  match bits:
173	    case NumberBits{+hi, lo}:
174	      Bool.not(U32.is_eq(U32.and(hi, 2146435072), 2146435072))
175	
176	# Whether a name is already taken among the members that follow.
177	def key_in(+key: String, members: List<&2, JMember>) -> Bool:
178	  match members:
179	    case Nil{}:
180	      False{}
181	    case JMember{other, val} <> rest:
182	      Bool.or(String.eq(key, other), key_in(key, rest))
183	
184	# A value is valid when every number in it is finite and no object holds a name
185	# twice. An object is a list of members, so a name's uniqueness is read off the
186	# members themselves, not off any layout.
187	def valid_json(value: Json) -> Bool:
188	  match value:
189	    case JNull{}:
190	      True{}
191	    case JBool{value}:
192	      True{}
193	    case JNumber{bits}:
194	      finite_number(bits)
195	    case JString{text}:
196	      True{}
197	    case JArray{Nil{}}:
198	      True{}
199	    case JArray{head <> tail}:
200	      Bool.and(valid_json(head), valid_json(JArray{tail}))
201	    case JObject{Nil{}}:
202	      True{}
203	    case JObject{JMember{key, val} <> +tail}:
204	      Bool.and(valid_json(val), Bool.and(Bool.not(key_in(key, tail)), valid_json(JObject{tail})))
205	
206	# ---- reading a value ----
207	
208	def pick_raw(b: Bool, +x: Raw, +y: Raw) -> Raw:
209	  match b:
210	    case True{}:
211	      x
212	    case False{}:
213	      y
214	
215	# The value under `name` in an object, or RMissing.
216	def lookup(+name: String, r: Raw) -> Raw:
217	  match r:
218	    case RKey{k, +v, rest}:
219	      pick_raw(String.eq(k, name), v, lookup(name, rest))
220	    case _:
221	      RMissing{}
222	
223	def pick_bool(b: Bool, +x: Bool, +y: Bool) -> Bool:
224	  match b:
225	    case True{}:
226	      x
227	    case False{}:
228	      y
229	
230	def is_rnil(r: Raw) -> Bool:
231	  match r:
232	    case RNil{}:
233	      True{}
234	    case _:
235	      False{}
236	
237	# ---- the helpers of the choices: true, one of some names, one of some keys ----
238	
239	def is_missing(v: Raw) -> Bool:
240	  match v:
241	    case RMissing{}:
242	      True{}
243	    case _:
244	      False{}
245	
246	def in_names(+x: String, names: List<&2, String>) -> Bool:
247	  match names:
248	    case Nil{}:
249	      False{}
250	    case n <> t:
251	      Bool.or(String.eq(x, n), in_names(x, t))
252	
253	# None of the keys of a variant chain is in the object r.
254	def none_present(s: Schema, +r: Raw) -> Bool:
255	  match s:
256	    case SVariant{n, vs, rest}:
257	      Bool.and(is_missing(lookup(n, r)), none_present(rest, r))
258	    case _:
259	      True{}
260	
261	# ---- a strict object: its keys ----
262	#
263	# The names a record or variant chain declares. SStrict refuses a key that is
264	# not one of them; wf asks that SStrict wrap such a chain.
265	def key_names(s: Schema) -> List<&2, String>:
266	  match s:
267	    case SField{n, fs, rest}:
268	      n <> key_names(rest)
269	    case SVariant{n, vs, rest}:
270	      n <> key_names(rest)
271	    case _:
272	      Nil{}
273	
274	# Every key of the object r is one of ns (anything but an object has none).
275	def no_extra(+ns: List<&2, String>, r: Raw) -> Bool:
276	  match r:
277	    case RKey{+k, v, o}:
278	      Bool.and(in_names(k, ns), no_extra(ns, o))
279	    case _:
280	      True{}
281	
282	# ---- a tagged union: its tag, and the object a case sees ----
283	#
284	# STagged{key, name, s, rest} is one case of a chain ending in STagEnd{key}:
285	# when the value under `key` is the string `name`, the object without that
286	# key must conform to s; otherwise the chain goes on. The case does not see
287	# the tag, so an SStrict case need not name it.
288	
289	# The object r without its first key k (what lookup(k, r) reads).
290	def drop_key(+k: String, r: Raw) -> Raw:
291	  match r:
292	    case RKey{+j, +v, +o}:
293	      pick_raw(String.eq(j, k), o, RKey{j, v, drop_key(k, o)})
294	    case x:
295	      x
296	
297	def is_str(+n: String, v: Raw) -> Bool:
298	  match v:
299	    case RStr{x}:
300	      String.eq(x, n)
301	    case _:
302	      False{}
303	
304	# The tag under k is the string n.
305	def is_tag(+k: String, +n: String, r: Raw) -> Bool:
306	  is_str(n, lookup(k, r))
307	
308	# ---- a bound, as a test and as a reason ----
309	#
310	# SStrLen{lo, hi, s} is a string in the bounds that also satisfies s, SListLen
311	# the same over a list's elements, SNatIn is a number in the bounds, and SBool
312	# is a boolean. The bound travels with the schema instead of with a rule's tag,
313	# which is what lets a host build one (a rule is chosen by a number, and a
314	# number carries no bounds).
315	#
316	# A rule and a constructor state the same bounds, and these defs are where they
317	# are written once: str_len_ok and num_ok are the tests, in_err is how a failing
318	# test becomes an error at the value's own path, and len_ok is the same test
319	# read as a Bool (what conforms asks at an SStrLen). Both ends are included;
320	# lo > hi is not an error but an empty range, in which nothing is in bounds.
321	
322	def in_err(b: Bool, w: Why) -> Maybe<&2, Err>:
323	  match b:
324	    case True{}:
325	      None{}
326	    case False{}:
327	      Some{Err{Nil{}, w}}
328	
329	def str_len_ok(+lo: Nat, +hi: Nat, +x: String) -> Bool:
330	  Bool.and(Nat.is_le(lo, String.length(x)), Nat.is_le(String.length(x), hi))
331	
332	def num_ok(+lo: Nat, +hi: Nat, +n: Nat) -> Bool:
333	  Bool.and(Nat.is_le(lo, n), Nat.is_le(n, hi))
334	
335	# a <= b on integers. A negative is below every non-negative, and between two
336	# negatives the larger offset is the smaller number.
337	def int_le(a: Int, b: Int) -> Bool:
338	  match a b:
339	    case IPos{m} IPos{n}:
340	      Nat.is_le(m, n)
341	    case IPos{m} INeg{n}:
342	      False{}
343	    case INeg{m} IPos{n}:
344	      True{}
345	    case INeg{m} INeg{n}:
346	      Nat.is_le(n, m)
347	
348	def int_ok(+lo: Int, +hi: Int, +i: Int) -> Bool:
349	  Bool.and(int_le(lo, i), int_le(i, hi))
350	
351	# How an integer is written: a non-negative as RNum, a negative as RNeg.
352	def int_raw(i: Int) -> Raw:
353	  match i:
354	    case IPos{n}:
355	      RNum{n}
356	    case INeg{n}:
357	      RNeg{n}
358	
359	# r is a string whose length is in the bounds: what conforms reads at an
360	# SStrLen, and what len_err refuses exactly when it fails.
361	def len_ok(+lo: Nat, +hi: Nat, r: Raw) -> Bool:
362	  match r:
363	    case RStr{+x}:
364	      str_len_ok(lo, hi, x)
365	    case _:
366	      False{}
367	
368	# The same bounds as ready-made rules: a project's rule calls them by tag
369	# (`case 0n: str_len_in(1n, 64n, r)`), since a tag carries no numbers. Each
370	# refuses only the value it is about -- a string, a number -- and leaves any
371	# other kind to the schema's own check; the constructors below read the tests
372	# directly, because their bound is in the schema.
373	def str_len_in(+lo: Nat, +hi: Nat, r: Raw) -> Maybe<&2, Err>:
374	  match r:
375	    case RStr{+x}:
376	      in_err(str_len_ok(lo, hi, x), LengthNotIn{lo, hi})
377	    case _:
378	      None{}
379	
380	def nat_in(+lo: Nat, +hi: Nat, r: Raw) -> Maybe<&2, Err>:
381	  match r:
382	    case RNum{+n}:
383	      in_err(num_ok(lo, hi, n), NotIn{lo, hi})
384	    case _:
385	      None{}
386	
387	def is_bool(r: Raw) -> Bool:
388	  match r:
389	    case RBool{b}:
390	      True{}
391	    case _:
392	      False{}
393	
394	# A list's element count, as a test. SListLen{lo, hi, s} is a list whose
395	# element count is in the bounds that also satisfies s: the same shape an
396	# SStrLen has, over elements instead of characters. raw_list is "r is a list at
397	# all", raw_len counts a proper list's elements (0 for anything else, which is
398	# why every use asks raw_list too), count_ok is the bound read as a Bool, and
399	# list_len_ok is both together -- what conforms asks at an SListLen, and what
400	# count_err refuses exactly when it fails. Both ends are included; lo > hi is
401	# not an error but an empty range, in which no list is in bounds.
402	
403	def raw_list(r: Raw) -> Bool:
404	  match r:
405	    case RNil{}:
406	      True{}
407	    case RCons{h, t}:
408	      raw_list(t)
409	    case _:
410	      False{}
411	
412	def raw_len(r: Raw) -> Nat:
413	  match r:
414	    case RCons{h, t}:
415	      1n+raw_len(t)
416	    case _:
417	      0n
418	
419	def count_ok(+lo: Nat, +hi: Nat, +r: Raw) -> Bool:
420	  Bool.and(Nat.is_le(lo, raw_len(r)), Nat.is_le(raw_len(r), hi))
421	
422	def list_len_ok(+lo: Nat, +hi: Nat, +r: Raw) -> Bool:
423	  Bool.and(raw_list(r), count_ok(lo, hi, r))
424	
425	# ---- a key the schema reads ----
426	#
427	# A key the schema reads as a field key (SField) or as a variant key (SVariant)
428	# must appear at most once in the value: with a key repeated, lookup reads the
429	# first one and the second is unreachable, so the value says something the
430	# schema cannot mean. A key the schema does not name is never read, so
431	# repeating it is unobservable and is left alone.
432	#
433	# The tag key of a tagged case is read the same way -- it is how the chain
434	# picks its case -- so it is checked the same way, and at the case the tag
435	# names: conforms, check and defect all ask key_once at the value's own tag
436	# key, and a case whose tag matched is refused when the key is there twice.
437	# The check sits at the case and not at the chain because a value whose tag
438	# names no case is refused at the chain's end whatever its keys are, and
439	# because the case is the only place the question has an answer: the case is
440	# checked against the object with the tag key taken out, which is the object
441	# its own schema is about.
442	#
443	# So the other half is wf's: a case's own schema may not read the tag key at
444	# all (no_key, above wf). If it did, enc would write that key twice -- the tag
445	# first, then the case's own field -- and the host builds the object as a JS
446	# object, where the second write overwrites the first, so the value written
447	# could not be read back. Refusing the schema is what keeps encode_conforms
448	# true.
449	
450	# k is a key of the object r.
451	def has_key(+k: String, r: Raw) -> Bool:
452	  match r:
453	    case RKey{j, v, o}:
454	      Bool.or(String.eq(k, j), has_key(k, o))
455	    case _:
456	      False{}
457	
458	# name appears at most once among the keys of the object r. b is whether a key
459	# read before r was already name; the flag carries forward, and a key that is
460	# name while the flag is set is the second one -- refused here and nowhere
461	# else. The value is the first argument because a self-call must read its
462	# arguments left to right, unchanged until one shrinks, and only the value
463	# shrinks; the value is matched first because a match cannot be nested inside
464	# the branch of a match on another parameter. One pass, so a walk costs one
465	# key per key, the same as the lookup beside it.
466	def key_once_at(r: Raw, +b: Bool, +name: String) -> Bool:
467	  match r:
468	    case RKey{+k, +v, +o}:
469	      Bool.and(Bool.not(Bool.and(b, String.eq(k, name))), key_once_at(o, Bool.or(b, String.eq(k, name)), name))
470	    case _:
471	      True{}
472	
473	# name appears at most once among the keys of the object r: nothing has been
474	# read yet.
475	def key_once(+name: String, r: Raw) -> Bool:
476	  key_once_at(r, False{}, name)
477	
478	# The repeated key as check reports it: at the key's own name, with no step
479	# after it (the second occurrence is not a place in the schema). The test is
480	# passed in rather than read here (a match cannot scrutinize a computed value):
481	# b is key_once(name, r), so nothing is reported exactly when key_once holds,
482	# which is what check_exact needs.
483	def key_err(b: Bool, +name: String) -> Maybe<&2, Err>:
484	  match b:
485	    case True{}:
486	      None{}
487	    case False{}:
488	      Some{Err{AtField{0n, name} <> Nil{}, RepeatedKey{name}}}
489	
490	# ---- what a valid value is ----
491	
492	# ---- the kind of a value, and the kinds a schema can accept ----
493	#
494	# An SEither picks its alternative by the value's JSON kind, so its
495	# alternatives must take disjoint kinds (wf). has_kind(s, k) says that s may
496	# accept a value of kind k: it never misses one s accepts (a schema accepts
497	# only values of its kinds), and it may claim more (an STagEnd claims an
498	# object it never accepts), which only makes wf stricter.
499	
500	type JKind is Data:
501	  KNum{}
502	  KStr{}
503	  KBool{}
504	  KList{}
505	  KObj{}
506	  KNull{}
507	  KAbsent{}
508	  KJson{}
509	  KOther{}
510	
511	def kind_eq(a: JKind, b: JKind) -> Bool:
512	  match a b:
513	    case KNum{} KNum{}:
514	      True{}
515	    case KStr{} KStr{}:
516	      True{}
517	    case KBool{} KBool{}:
518	      True{}
519	    case KList{} KList{}:
520	      True{}
521	    case KObj{} KObj{}:
522	      True{}
523	    case KNull{} KNull{}:
524	      True{}
525	    case KAbsent{} KAbsent{}:
526	      True{}
527	    case KJson{} KJson{}:
528	      True{}
529	    case KOther{} KOther{}:
530	      True{}
531	    case _ _:
532	      False{}
533	
534	def kind_of(r: Raw) -> JKind:
535	  match r:
536	    case RNum{n}:
537	      KNum{}
538	    case RNeg{n}:
539	      KNum{}
540	    case RStr{x}:
541	      KStr{}
542	    case RBool{b}:
543	      KBool{}
544	    case RNil{}:
545	      KList{}
546	    case RCons{h, t}:
547	      KList{}
548	    case REnd{}:
549	      KObj{}
550	    case RKey{k, v, o}:
551	      KObj{}
552	    case RNull{}:
553	      KNull{}
554	    case RMissing{}:
555	      KAbsent{}
556	    case RJson{value}:
557	      KJson{}
558	    case _:
559	      KOther{}
560	
561	def has_kind(s: Schema, +k: JKind) -> Bool:
562	  match s:
563	    case SNat{}:
564	      kind_eq(KNum{}, k)
565	    case SNatIn{lo, hi}:
566	      kind_eq(KNum{}, k)
567	    case SInt{}:
568	      kind_eq(KNum{}, k)
569	    case SIntIn{lo, hi}:
570	      kind_eq(KNum{}, k)
571	    case SStr{}:
572	      kind_eq(KStr{}, k)
573	    case SEnum{names}:
574	      kind_eq(KStr{}, k)
575	    case SBool{}:
576	      kind_eq(KBool{}, k)
577	    case STrue{}:
578	      kind_eq(KBool{}, k)
579	    case SList{e}:
580	      kind_eq(KList{}, k)
581	    case STuple{ts, rest}:
582	      kind_eq(KList{}, k)
583	    case STEnd{}:
584	      kind_eq(KList{}, k)
585	    case SField{n, fs, rest}:
586	      kind_eq(KObj{}, k)
587	    case SEnd{}:
588	      kind_eq(KObj{}, k)
589	    case STagged{key, n, cs, rest}:
590	      kind_eq(KObj{}, k)
591	    case STagEnd{key}:
592	      kind_eq(KObj{}, k)
593	    case SVariant{n, vs, rest}:
594	      kind_eq(KObj{}, k)
595	    case SVEnd{}:
596	      kind_eq(KObj{}, k)
597	    case SJson{}:
598	      kind_eq(KJson{}, k)
599	    case SOpt{i}:
600	      Bool.or(kind_eq(KNull{}, k), has_kind(i, k))
601	    case SOptional{i}:
602	      Bool.or(kind_eq(KAbsent{}, k), has_kind(i, k))
603	    case SStrLen{lo, hi, s2}:
604	      has_kind(s2, k)
605	    case SListLen{lo, hi, s2}:
606	      has_kind(s2, k)
607	    case SRule{s2, tag}:
608	      has_kind(s2, k)
609	    case SStrict{s2}:
610	      has_kind(s2, k)
611	    case SEither{l, r}:
612	      Bool.or(has_kind(l, k), has_kind(r, k))
613	
614	# No value of kind k is claimed by both.
615	def apart(+l: Schema, +r: Schema, +k: JKind) -> Bool:
616	  Bool.not(Bool.and(has_kind(l, k), has_kind(r, k)))
617	
618	def disjoint(+l: Schema, +r: Schema) -> Bool:
619	  Bool.and(apart(l, r, KNum{}), Bool.and(apart(l, r, KStr{}), Bool.and(apart(l, r, KBool{}), Bool.and(apart(l, r, KList{}), Bool.and(apart(l, r, KObj{}), Bool.and(apart(l, r, KNull{}), Bool.and(apart(l, r, KAbsent{}), Bool.and(apart(l, r, KJson{}), apart(l, r, KOther{})))))))))
620	
621	# An alternative is a value that is present and has a kind of its own: not an
622	# absent field (the host writes no key, so no kind is there to pick by), and
623	# not s.json(), which takes every kind.
624	def alt_ok(+s: Schema) -> Bool:
625	  Bool.and(Bool.not(has_kind(s, KAbsent{})), Bool.not(has_kind(s, KJson{})))
626	
627	# What an SEither would have taken, for the host to say.
628	def no_alt(+s: Schema) -> Why:
629	  NoAlternative{has_kind(s, KNum{}), has_kind(s, KStr{}), has_kind(s, KBool{}), has_kind(s, KList{}), has_kind(s, KObj{}), has_kind(s, KNull{})}
630	
631	def conforms(~rule: Nat -> Raw -> Maybe<&2, Err>, s: Schema, r: Raw, +prev: Maybe<&2, Nat>) -> Bool:
632	  match s r:
633	    case SNat{} RNum{n}:
634	      True{}
635	    case SNatIn{+lo, +hi} RNum{+n}:
636	      num_ok(lo, hi, n)
637	    case SStr{} RStr{x}:
638	      True{}
639	    case SStrLen{+lo, +hi, +s2} +x:
640	      Bool.and(conforms(~rule, s2, x, prev), len_ok(lo, hi, x))
641	    case SListLen{+lo, +hi, +s2} +r:
642	      Bool.and(list_len_ok(lo, hi, r), conforms(~rule, s2, r, None{}))
643	    case SOpt{inner} RNull{}:
644	      True{}
645	    case SOpt{inner} x:
646	      conforms(~rule, inner, x, None{})
647	    case SOptional{+inner} +x:
648	      Bool.or(is_missing(x), conforms(~rule, inner, x, None{}))
649	    case SList{e} RNil{}:
650	      True{}
651	    case SList{+e} RCons{h, t}:
652	      Bool.and(conforms(~rule, e, h, None{}), conforms(~rule, SList{e}, t, None{}))
653	    case SJson{} RJson{value}:
654	      valid_json(value)
655	    case SInt{} RNum{n}:
656	      True{}
657	    case SInt{} RNeg{n}:
658	      True{}
659	    case SIntIn{+lo, +hi} RNum{+n}:
660	      int_ok(lo, hi, IPos{n})
661	    case SIntIn{+lo, +hi} RNeg{+n}:
662	      int_ok(lo, hi, INeg{n})
663	    case SField{+name, fs, rest} REnd{}:
664	      Bool.and(conforms(~rule, fs, RMissing{}, None{}), conforms(~rule, rest, REnd{}, None{}))
665	    case SField{+name, fs, rest} RKey{+k, +v, +o}:
666	      Bool.and(key_once(name, RKey{k, v, o}), Bool.and(conforms(~rule, fs, lookup(name, RKey{k, v, o}), None{}), conforms(~rule, rest, RKey{k, v, o}, None{})))
667	    case SEnd{} REnd{}:
668	      True{}
669	    case SEnd{} RKey{k, v, o}:
670	      True{}
671	    case SRule{+s2, +tag} +x:
672	      Bool.and(conforms(~rule, s2, x, prev), Maybe.is_none(&2, Err, rule(tag, x)))
673	    case SStrict{+s2} +x:
674	      Bool.and(conforms(~rule, s2, x, prev), no_extra(key_names(s2), x))
675	    case STagged{+k, +n, cs, rest} +x:
676	      pick_bool(is_tag(k, n, x), Bool.and(key_once(k, x), conforms(~rule, cs, drop_key(k, x), None{})), conforms(~rule, rest, x, None{}))
677	    case STagEnd{k} x:
678	      False{}  # the end of a tagged chain: no case matched
679	    case SBool{} RBool{b}:
680	      True{}  # any boolean is a boolean, and nothing else is
681	    case STrue{} RBool{b}:
682	      b
683	    case SEnum{names} RStr{+x}:
684	      in_names(x, names)
685	    case SVariant{+name, +vs, +rest} REnd{}:
686	      conforms(~rule, rest, REnd{}, None{})
687	    case SVariant{+name, +vs, +rest} RKey{+k, +v, +o}:
688	      pick_bool(is_missing(lookup(name, RKey{k, v, o})), conforms(~rule, rest, RKey{k, v, o}, None{}), Bool.and(key_once(name, RKey{k, v, o}), Bool.and(conforms(~rule, vs, lookup(name, RKey{k, v, o}), None{}), none_present(rest, RKey{k, v, o}))))
689	    case STuple{ts, rest} RCons{h, t}:
690	      Bool.and(conforms(~rule, ts, h, None{}), conforms(~rule, rest, t, None{}))
691	    case STEnd{} RNil{}:
692	      True{}
693	    case SEither{+l, +r} +x:
694	      pick_bool(has_kind(l, kind_of(x)), conforms(~rule, l, x, prev), Bool.and(has_kind(r, kind_of(x)), conforms(~rule, r, x, prev)))
695	    case _ _:
696	      False{}
697	
698	# ---- the first thing wrong ----
699	
700	def here(w: Why) -> Maybe<&2, Err>:
701	  Some{Err{Nil{}, w}}
702	
703	# An error found under a step gets the step in front of its path.
704	def under(+st: Step, m: Maybe<&2, Err>) -> Maybe<&2, Err>:
705	  match m:
706	    case None{}:
707	      None{}
708	    case Some{Err{p, w}}:
709	      Some{Err{st <> p, w}}
710	
711	# At an SStrLen the shape comes first, as everywhere else: a value that is not
712	# a string is NotString, a string out of its bounds is LengthNotIn, and a node
713	# the codec refused to build or that is absent reads as it does at every kind.
714	def len_err(+lo: Nat, +hi: Nat, r: Raw) -> Maybe<&2, Err>:
715	  match r:
716	    case RStr{+x}:
717	      in_err(str_len_ok(lo, hi, x), LengthNotIn{lo, hi})
718	    case RMissing{}:
719	      here(Missing{})
720	    case RTooBig{}:
721	      here(TooLarge{})
722	    case _:
723	      here(NotString{})
724	
725	# An error found further along a list is one element further: its first
726	# step, if it counts elements, counts one more. A plain list's steps are
727	# AtIndex; a bounded list's are AtIndex and BoundAt.
728	def later_l_path(p: List<&2, Step>) -> List<&2, Step>:
729	  match p:
730	    case AtIndex{j} <> q:
731	      AtIndex{1n+j} <> q
732	    case q:
733	      q
734	
735	def later_l(m: Maybe<&2, Err>) -> Maybe<&2, Err>:
736	  match m:
737	    case None{}:
738	      None{}
739	    case Some{Err{p, w}}:
740	      Some{Err{later_l_path(p), w}}
741	
742	def later_i_path(p: List<&2, Step>) -> List<&2, Step>:
743	  match p:
744	    case AtIndex{j} <> q:
745	      AtIndex{1n+j} <> q
746	    case BoundAt{j, key} <> q:
747	      BoundAt{1n+j, key} <> q
748	    case q:
749	      q
750	
751	def later_i(m: Maybe<&2, Err>) -> Maybe<&2, Err>:
752	  match m:
753	    case None{}:
754	      None{}
755	    case Some{Err{p, w}}:
756	      Some{Err{later_i_path(p), w}}
757	
758	# An error found in a later field is one field further.
759	def later_f_path(p: List<&2, Step>) -> List<&2, Step>:
760	  match p:
761	    case AtField{k, n} <> q:
762	      AtField{1n+k, n} <> q
763	    case q:
764	      q
765	
766	def later_f(m: Maybe<&2, Err>) -> Maybe<&2, Err>:
767	  match m:
768	    case None{}:
769	      None{}
770	    case Some{Err{p, w}}:
771	      Some{Err{later_f_path(p), w}}
772	
773	# The first of two: the second counts only when the first found nothing.
774	def first(m: Maybe<&2, Err>, n: Maybe<&2, Err>) -> Maybe<&2, Err>:
775	  match m:
776	    case None{}:
777	      n
778	    case Some{e}:
779	      Some{e}
780	
781	# The reason a value that is not the shape is refused, at the place it was
782	# found: an absent slot is Missing, a node the host refused to build (RTooBig)
783	# is TooLarge, anything else is the schema kind's own reason. check and the
784	# defect helpers both answer through here, so the reason a path reports is the
785	# same one for both.
786	def missing_or(r: Raw, w: Why) -> Why:
787	  match r:
788	    case RMissing{}:
789	      Missing{}
790	    case RTooBig{}:
791	      TooLarge{}
792	    case _:
793	      w
794	
795	def pick_err(b: Bool, +x: Maybe<&2, Err>, +y: Maybe<&2, Err>) -> Maybe<&2, Err>:
796	  match b:
797	    case True{}:
798	      x
799	    case False{}:
800	      y
801	
802	def true_err(b: Bool) -> Maybe<&2, Err>:
803	  match b:
804	    case True{}:
805	      None{}
806	    case False{}:
807	      here(NotTrue{})
808	
809	def enum_err(b: Bool) -> Maybe<&2, Err>:
810	  match b:
811	    case True{}:
812	      None{}
813	    case False{}:
814	      here(NotOneOf{})
815	
816	# A second key of a variant chain in the object r: the first one found.
817	def dup_err(s: Schema, +r: Raw) -> Maybe<&2, Err>:
818	  match s:
819	    case SVariant{+n, vs, rest}:
820	      pick_err(is_missing(lookup(n, r)), later_f(dup_err(rest, r)), Some{Err{AtField{0n, n} <> Nil{}, TwoVariants{}}})
821	    case _:
822	      None{}
823	
824	# The first key of r that is not one of ns, at its own name.
825	def extra_err(+ns: List<&2, String>, r: Raw) -> Maybe<&2, Err>:
826	  match r:
827	    case RKey{+k, v, o}:
828	      pick_err(in_names(k, ns), extra_err(ns, o), Some{Err{AtKey{k} <> Nil{}, UnknownKey{}}})
829	    case _:
830	      None{}
831	
832	# At the end of a tagged chain no case matched: the value is not an object,
833	# or its tag is missing, or it names no case.
834	def tag_err(+k: String, r: Raw) -> Maybe<&2, Err>:
835	  match r:
836	    case REnd{}:
837	      Some{Err{AtKey{k} <> Nil{}, Missing{}}}
838	    case RKey{j, v, o}:
839	      Some{Err{AtKey{k} <> Nil{}, missing_or(lookup(k, RKey{j, v, o}), NotOneOf{})}}
840	    case x:
841	      here(missing_or(x, NotObject{}))
842	
843	# The count, as an error: at an SListLen the count is read before any element,
844	# so a list out of bounds is CountNotIn at the list's own path. A value that is
845	# not a list has no count to object to, and is refused as a list schema refuses
846	# it: NotList, or Missing/TooLarge for the two nodes that are never a shape
847	# (the same reasons check's own arms give them).
848	def count_err(+lo: Nat, +hi: Nat, r: Raw) -> Maybe<&2, Err>:
849	  match r:
850	    case RNil{}:
851	      in_err(list_len_ok(lo, hi, r), CountNotIn{lo, hi})
852	    case RCons{h, t}:
853	      in_err(list_len_ok(lo, hi, r), CountNotIn{lo, hi})
854	    case _:
855	      here(missing_or(r, NotList{}))
856	
857	def check(~rule: Nat -> Raw -> Maybe<&2, Err>, s: Schema, r: Raw, +prev: Maybe<&2, Nat>) -> Maybe<&2, Err>:
858	  match s r:
859	    case SNat{} RNum{n}:
860	      None{}
861	    case SNat{} x:
862	      here(missing_or(x, NotNat{}))
863	    case SStr{} RStr{x}:
864	      None{}
865	    case SStr{} x:
866	      here(missing_or(x, NotString{}))
867	    case SNatIn{+lo, +hi} RNum{+n}:
868	      nat_in(lo, hi, RNum{n})
869	    case SNatIn{lo_, hi_} +x:
870	      here(missing_or(x, NotNat{}))
871	    case SStrLen{+lo, +hi, +s2} +x:
872	      first(check(~rule, s2, x, prev), len_err(lo, hi, x))
873	    case SListLen{+lo, +hi, +s2} +r:
874	      first(count_err(lo, hi, r), check(~rule, s2, r, None{}))
875	    case SOpt{inner} RNull{}:
876	      None{}
877	    case SOpt{inner} x:
878	      check(~rule, inner, x, None{})
879	    case SOptional{inner} RMissing{}:
880	      None{}
881	    case SOptional{inner} x:
882	      check(~rule, inner, x, None{})
883	    case SList{e} RNil{}:
884	      None{}
885	    case SList{+e} RCons{h, t}:
886	      first(under(AtIndex{0n}, check(~rule, e, h, None{})), later_l(check(~rule, SList{e}, t, None{})))
887	    case SJson{} RJson{value}:
888	      in_err(valid_json(value), NotJson{})
889	    case SJson{} x:
890	      here(missing_or(x, NotJson{}))
891	    case SInt{} RNum{n}:
892	      None{}
893	    case SInt{} RNeg{n}:
894	      None{}
895	    case SInt{} x:
896	      here(missing_or(x, NotInt{}))
897	    case SIntIn{+lo, +hi} RNum{+n}:
898	      in_err(int_ok(lo, hi, IPos{n}), IntNotIn{lo, hi})
899	    case SIntIn{+lo, +hi} RNeg{+n}:
900	      in_err(int_ok(lo, hi, INeg{n}), IntNotIn{lo, hi})
901	    case SIntIn{lo_, hi_} x:
902	      here(missing_or(x, NotInt{}))
903	    case SList{e} x:
904	      here(missing_or(x, NotList{}))
905	    case SField{+name, fs, rest} REnd{}:
906	      first(under(AtField{0n, name}, check(~rule, fs, RMissing{}, None{})), later_f(check(~rule, rest, REnd{}, None{})))
907	    case SField{+name, fs, rest} RKey{+k, +v, +o}:
908	      first(key_err(key_once(name, RKey{k, v, o}), name), first(under(AtField{0n, name}, check(~rule, fs, lookup(name, RKey{k, v, o}), None{})), later_f(check(~rule, rest, RKey{k, v, o}, None{}))))
909	    case SField{name, fs, rest} x:
910	      here(missing_or(x, NotObject{}))
911	    case SEnd{} REnd{}:
912	      None{}
913	    case SEnd{} RKey{k, v, o}:
914	      None{}
915	    case SEnd{} x:
916	      here(missing_or(x, NotObject{}))
917	    case SRule{+s2, +tag} +x:
918	      first(check(~rule, s2, x, prev), rule(tag, x))
919	    case SStrict{+s2} +x:
920	      first(check(~rule, s2, x, prev), extra_err(key_names(s2), x))
921	    case STagged{+k, +n, cs, rest} +x:
922	      pick_err(is_tag(k, n, x), first(key_err(key_once(k, x), k), check(~rule, cs, drop_key(k, x), None{})), check(~rule, rest, x, None{}))
923	    case STagEnd{k} x:
924	      tag_err(k, x)
925	    case SBool{} RBool{b}:
926	      None{}
927	    case SBool{} +x:
928	      here(missing_or(x, NotBool{}))
929	    case STrue{} RBool{b}:
930	      true_err(b)
931	    case STrue{} x:
932	      here(missing_or(x, NotTrue{}))
933	    case SEnum{names} RStr{+x}:
934	      enum_err(in_names(x, names))
935	    case SEnum{names} x:
936	      here(missing_or(x, NotOneOf{}))
937	    case SVariant{+name, +vs, +rest} REnd{}:
938	      later_f(check(~rule, rest, REnd{}, None{}))
939	    case SVariant{+name, +vs, +rest} RKey{+k, +v, +o}:
940	      pick_err(is_missing(lookup(name, RKey{k, v, o})), later_f(check(~rule, rest, RKey{k, v, o}, None{})), first(key_err(key_once(name, RKey{k, v, o}), name), first(under(AtField{0n, name}, check(~rule, vs, lookup(name, RKey{k, v, o}), None{})), later_f(dup_err(rest, RKey{k, v, o})))))
941	    case SVariant{+name, +vs, +rest} x:
942	      here(missing_or(x, NotObject{}))
943	    case SVEnd{} REnd{}:
944	      here(NoVariant{})
945	    case SVEnd{} RKey{k, v, o}:
946	      here(NoVariant{})
947	    case SVEnd{} x:
948	      here(missing_or(x, NotObject{}))
949	    case STuple{ts, rest} RCons{h, t}:
950	      first(under(AtIndex{0n}, check(~rule, ts, h, None{})), later_l(check(~rule, rest, t, None{})))
951	    case STuple{ts, rest} RNil{}:
952	      here(TooShort{})
953	    case STuple{ts, rest} x:
954	      here(missing_or(x, NotList{}))
955	    case STEnd{} RNil{}:
956	      None{}
957	    case STEnd{} RCons{h, t}:
958	      here(TooLong{})
959	    case STEnd{} x:
960	      here(missing_or(x, NotList{}))
961	    case SEither{+l, +r} +x:
962	      pick_err(has_kind(l, kind_of(x)), check(~rule, l, x, prev), pick_err(has_kind(r, kind_of(x)), check(~rule, r, x, prev), here(missing_or(x, no_alt(SEither{l, r})))))
963	
964	# ---- the claim the accuracy law makes ----
965	#
966	# defect follows a path instead of searching for one. Everything it passes on
967	# the way must conform, a step's name must be the schema's, and at the end of
968	# the path it answers what is wrong there. A path that does not fit the value
969	# leads nowhere (None).
970	
971	def guard(b: Bool, m: Maybe<&2, Why>) -> Maybe<&2, Why>:
972	  match b:
973	    case True{}:
974	      m
975	    case False{}:
976	      None{}
977	
978	# The same two reasons at an SNatIn and an SBool, replayed along a path: the
979	# value's own kind is the defect when the path ends here, and it is not a
980	# defect at all further along (the walk passed it).
981	def nat_in_defect(+lo: Nat, +hi: Nat, r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
982	  match r p:
983	    case RNum{+n} Nil{}:
984	      guard(Bool.not(num_ok(lo, hi, n)), Some{NotIn{lo, hi}})
985	    case RNum{n} st <> q:
986	      None{}
987	    case x Nil{}:
988	      Some{missing_or(x, NotNat{})}
989	    case x st <> q:
990	      None{}
991	
992	# The same two reasons at an SInt and an SIntIn: a number of either sign is not
993	# the defect, and its bound is the defect only where the path ends.
994	def int_defect(r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
995	  match r p:
996	    case RNum{n} _:
997	      None{}
998	    case RNeg{n} _:
999	      None{}
1000	    case x Nil{}:
1001	      Some{missing_or(x, NotInt{})}
1002	    case x st <> q:
1003	      None{}
1004	
1005	def int_in_defect(+lo: Int, +hi: Int, r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
1006	  match r p:
1007	    case RNum{+n} Nil{}:
1008	      guard(Bool.not(int_ok(lo, hi, IPos{n})), Some{IntNotIn{lo, hi}})
1009	    case RNeg{+n} Nil{}:
1010	      guard(Bool.not(int_ok(lo, hi, INeg{n})), Some{IntNotIn{lo, hi}})
1011	    case RNum{n} st <> q:
1012	      None{}
1013	    case RNeg{n} st <> q:
1014	      None{}
1015	    case x Nil{}:
1016	      Some{missing_or(x, NotInt{})}
1017	    case x st <> q:
1018	      None{}
1019	
1020	def bool_defect(r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
1021	  match r p:
1022	    case RBool{b} _:
1023	      None{}
1024	    case x Nil{}:
1025	      Some{missing_or(x, NotBool{})}
1026	    case x st <> q:
1027	      None{}
1028	
1029	# ---- a rule, its replay, and the closed forms ----
1030	#
1031	# A rule reports its first error with a path relative to the value it was
1032	# given. defect replays it by running the rule again: its path must be the
1033	# reported one (path_eq, which never compares two names), and the claim of
1034	# the accuracy law at an SRule is that the value conforms to the rule's
1035	# schema and the rule itself reported this error.
1036	
1037	def no_rule(tag: Nat, r: Raw) -> Maybe<&2, Err>:
1038	  None{}
1039	
1040	def first_why(m: Maybe<&2, Why>, +n: Maybe<&2, Why>) -> Maybe<&2, Why>:
1041	  match m:
1042	    case None{}:
1043	      n
1044	    case Some{w}:
1045	      Some{w}
1046	
1047	def step_eq(x: Step, y: Step) -> Bool:
1048	  match x y:
1049	    case AtIndex{i} AtIndex{j}:
1050	      Nat.is_eq(i, j)
1051	    case AtField{a, n} AtField{b, m}:
1052	      Bool.and(Nat.is_eq(a, b), String.eq(n, m))
1053	    case BoundAt{i, k} BoundAt{j, m}:
1054	      Bool.and(Nat.is_eq(i, j), String.eq(k, m))
1055	    case AtKey{k} AtKey{m}:
1056	      String.eq(k, m)
1057	    case _ _:
1058	      False{}
1059	
1060	def path_eq(x: List<&2, Step>, y: List<&2, Step>) -> Bool:
1061	  match x y:
1062	    case Nil{} Nil{}:
1063	      True{}
1064	    case a <> at b <> bt:
1065	      Bool.and(step_eq(a, b), path_eq(at, bt))
1066	    case _ _:
1067	      False{}
1068	
1069	def rule_defect(m: Maybe<&2, Err>, +p: List<&2, Step>) -> Maybe<&2, Why>:
1070	  match m:
1071	    case Some{Err{q, w}}:
1072	      guard(path_eq(q, p), Some{w})
1073	    case None{}:
1074	      None{}
1075	
1076	def not_list(x: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
1077	  match p:
1078	    case Nil{}:
1079	      Some{missing_or(x, NotList{})}
1080	    case st <> q:
1081	      None{}
1082	
1083	def not_object(x: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
1084	  match p:
1085	    case Nil{}:
1086	      Some{missing_or(x, NotObject{})}
1087	    case st <> q:
1088	      None{}
1089	
1090	def nat_defect(r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
1091	  match r p:
1092	    case RNum{n} _:
1093	      None{}
1094	    case x Nil{}:
1095	      Some{missing_or(x, NotNat{})}
1096	    case x st <> q:
1097	      None{}
1098	
1099	def str_defect(r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
1100	  match r p:
1101	    case RStr{x} _:
1102	      None{}
1103	    case x Nil{}:
1104	      Some{missing_or(x, NotString{})}
1105	    case x st <> q:
1106	      None{}
1107	
1108	def pick_why(b: Bool, +x: Maybe<&2, Why>, +y: Maybe<&2, Why>) -> Maybe<&2, Why>:
1109	  match b:
1110	    case True{}:
1111	      x
1112	    case False{}:
1113	      y
1114	
1115	def true_defect(r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
1116	  match r p:
1117	    case RBool{True{}} _:
1118	      None{}
1119	    case RBool{False{}} Nil{}:
1120	      Some{NotTrue{}}
1121	    case x Nil{}:
1122	      Some{missing_or(x, NotTrue{})}
1123	    case x st <> q:
1124	      None{}
1125	
1126	def enum_defect(names: List<&2, String>, r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
1127	  match r p:
1128	    case RStr{x} Nil{}:
1129	      guard(Bool.not(in_names(x, names)), Some{NotOneOf{}})
1130	    case RStr{x} st <> q:
1131	      None{}
1132	    case x Nil{}:
1133	      Some{missing_or(x, NotOneOf{})}
1134	    case x st <> q:
1135	      None{}
1136	
1137	def no_variant(p: List<&2, Step>) -> Maybe<&2, Why>:
1138	  match p:
1139	    case Nil{}:
1140	      Some{NoVariant{}}
1141	    case st <> q:
1142	      None{}
1143	
1144	# The claim about a second key: every key passed is absent, and the key the
1145	# path names is there.
1146	def dup_defect(s: Schema, +r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
1147	  match s p:
1148	    case SVariant{+n2, vs, rr} AtField{0n, m} <> Nil{}:
1149	      guard(Bool.and(String.eq(m, n2), Bool.not(is_missing(lookup(n2, r)))), Some{TwoVariants{}})
1150	    case SVariant{+n2, vs, rr} AtField{1n+j, m} <> q:
1151	      guard(is_missing(lookup(n2, r)), dup_defect(rr, r, AtField{j, m} <> q))
1152	    case _ _:
1153	      None{}
1154	
1155	def at_end(w: Why, p: List<&2, Step>) -> Maybe<&2, Why>:
1156	  match p:
1157	    case Nil{}:
1158	      Some{w}
1159	    case st <> q:
1160	      None{}
1161	
1162	# At a strict object the path is one key, and the replay checks it on its
1163	# own: the key is there, and it is not one of the names.
1164	def extra_defect(ns: List<&2, String>, +r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
1165	  match p:
1166	    case AtKey{+k} <> Nil{}:
1167	      guard(Bool.and(has_key(k, r), Bool.not(in_names(k, ns))), Some{UnknownKey{}})
1168	    case _:
1169	      None{}
1170	
1171	def tag_defect(+k: String, r: Raw, p: List<&2, Step>) -> Maybe<&2, Why>:
1172	  match r p:
1173	    case REnd{} AtKey{j} <> Nil{}:
1174	      guard(String.eq(j, k), Some{Missing{}})
1175	    case RKey{+j, +v, +o} AtKey{i} <> Nil{}:
1176	      guard(String.eq(i, k), Some{missing_or(lookup(k, RKey{j, v, o}), NotOneOf{})})
1177	    case REnd{} q:
1178	      None{}
1179	    case RKey{j, v, o} q:
1180	      None{}
1181	    case x Nil{}:
1182	      Some{missing_or(x, NotObject{})}
1183	    case x q:
1184	      None{}
1185	
1186	# The tag key of a tagged case, taken twice, as defect replays it. check
1187	# reports it before the case's own schema is walked -- there is no place in the
1188	# schema for the second occurrence -- so the path is one field step at the
1189	# tag's own name and nothing after it. b is whether the key is not read once,
1190	# so nothing is reported exactly when key_once holds; a path of any other shape
1191	# is the case's own report, which the walk below answers.
1192	def tag_key_defect(b: Bool, +k: String, p: List<&2, Step>) -> Maybe<&2, Why>:
1193	  match b p:
1194	    case False{} q:
1195	      None{}
1196	    case True{} AtField{0n, +j} <> Nil{}:
1197	      pick_why(String.eq(j, k), Some{RepeatedKey{k}}, None{})
1198	    case True{} q:
1199	      None{}
1200	
1201	def defect(~rule: Nat -> Raw -> Maybe<&2, Err>, s: Schema, r: Raw, +prev: Maybe<&2, Nat>, p: List<&2, Step>) -> Maybe<&2, Why>:
1202	  match s r p:
1203	    case SJson{} RJson{value} q:
1204	      guard(Bool.not(valid_json(value)), at_end(NotJson{}, q))
1205	    case SJson{} x q:
1206	      at_end(missing_or(x, NotJson{}), q)
1207	    case SInt{} x q:
1208	      int_defect(x, q)
1209	    case SIntIn{+lo, +hi} x q:
1210	      int_in_defect(lo, hi, x, q)
1211	    case SNat{} x q:
1212	      nat_defect(x, q)
1213	    case SStr{} x q:
1214	      str_defect(x, q)
1215	    case SNatIn{+lo, +hi} x q:
1216	      nat_in_defect(lo, hi, x, q)
1217	    case SStrLen{+lo, +hi, +s2} +x +q:
1218	      pick_why(conforms(~rule, s2, x, prev), rule_defect(len_err(lo, hi, x), q), defect(~rule, s2, x, prev, q))
1219	    case SListLen{+lo, +hi, +s2} +r +q:
1220	      # The count came first in check, so the count's own error is the one
1221	      # reported here exactly when there was one to report -- for a list out of
1222	      # bounds and for a value that is not a list at all (list_len_ok is False
1223	      # for both, and count_err reported something for both).
1224	      pick_why(Bool.not(list_len_ok(lo, hi, r)), rule_defect(count_err(lo, hi, r), q), defect(~rule, s2, r, None{}, q))
1225	    case SOpt{inner} RNull{} q:
1226	      None{}
1227	    case SOpt{inner} x q:
1228	      defect(~rule, inner, x, None{}, q)
1229	    case SOptional{inner} RMissing{} q:
1230	      None{}  # absent is not wrong, at this path or below it
1231	    case SOptional{inner} x q:
1232	      defect(~rule, inner, x, None{}, q)
1233	    case SList{e} RNil{} q:
1234	      None{}
1235	    case SList{e} RCons{h, t} AtIndex{0n} <> q:
1236	      defect(~rule, e, h, None{}, q)
1237	    case SList{+e} RCons{h, t} AtIndex{1n+j} <> q:
1238	      guard(conforms(~rule, e, h, None{}), defect(~rule, SList{e}, t, None{}, AtIndex{j} <> q))
1239	    case SList{+e} RCons{h, t} q:
1240	      guard(conforms(~rule, e, h, None{}), defect(~rule, SList{e}, t, None{}, q))
1241	    case SList{e} x q:
1242	      not_list(x, q)
1243	    case SField{+name, fs, rest} REnd{} AtField{0n, n} <> q:
1244	      guard(String.eq(n, name), defect(~rule, fs, RMissing{}, None{}, q))
1245	    case SField{+name, fs, rest} REnd{} AtField{1n+k, n} <> q:
1246	      guard(conforms(~rule, fs, RMissing{}, None{}), defect(~rule, rest, REnd{}, None{}, AtField{k, n} <> q))
1247	    case SField{+name, fs, rest} REnd{} q:
1248	      guard(conforms(~rule, fs, RMissing{}, None{}), defect(~rule, rest, REnd{}, None{}, q))
1249	    case SField{+name, fs, rest} RKey{+k, +v, +o} AtField{0n, n} <> +q:
1250	      pick_why(Bool.not(key_once(name, RKey{k, v, o})), at_end(RepeatedKey{name}, q), guard(String.eq(n, name), defect(~rule, fs, lookup(name, RKey{k, v, o}), None{}, q)))
1251	    case SField{+name, fs, rest} RKey{+k, +v, +o} AtField{1n+j, n} <> q:
1252	      guard(conforms(~rule, fs, lookup(name, RKey{k, v, o}), None{}), defect(~rule, rest, RKey{k, v, o}, None{}, AtField{j, n} <> q))
1253	    case SField{+name, fs, rest} RKey{+k, +v, +o} q:
1254	      guard(conforms(~rule, fs, lookup(name, RKey{k, v, o}), None{}), defect(~rule, rest, RKey{k, v, o}, None{}, q))
1255	    case SField{name, fs, rest} x q:
1256	      not_object(x, q)
1257	    case SEnd{} REnd{} q:
1258	      None{}
1259	    case SEnd{} RKey{k, v, o} q:
1260	      None{}
1261	    case SEnd{} x q:
1262	      not_object(x, q)
1263	    case SRule{+s2, +tag} +x +q:
1264	      pick_why(conforms(~rule, s2, x, prev), rule_defect(rule(tag, x), q), defect(~rule, s2, x, prev, q))
1265	    case SStrict{+s2} +x +q:
1266	      pick_why(conforms(~rule, s2, x, prev), extra_defect(key_names(s2), x, q), defect(~rule, s2, x, prev, q))
1267	    case STagged{+k, +n, cs, rest} +x +q:
1268	      pick_why(is_tag(k, n, x), first_why(tag_key_defect(Bool.not(key_once(k, x)), k, q), defect(~rule, cs, drop_key(k, x), None{}, q)), defect(~rule, rest, x, None{}, q))
1269	    case STagEnd{k} x q:
1270	      tag_defect(k, x, q)
1271	    case SBool{} x q:
1272	      bool_defect(x, q)
1273	    case STrue{} x q:
1274	      true_defect(x, q)
1275	    case SEnum{names} x q:
1276	      enum_defect(names, x, q)
1277	    case SVariant{+name, +vs, +rest} REnd{} AtField{1n+j, n} <> q:
1278	      defect(~rule, rest, REnd{}, None{}, AtField{j, n} <> q)
1279	    case SVariant{+name, +vs, +rest} REnd{} q:
1280	      defect(~rule, rest, REnd{}, None{}, q)
1281	    case SVariant{+name, +vs, +rest} RKey{+k, +v, +o} AtField{0n, +n} <> +q:
1282	      pick_why(is_missing(lookup(name, RKey{k, v, o})), defect(~rule, rest, RKey{k, v, o}, None{}, AtField{0n, n} <> q), pick_why(Bool.not(key_once(name, RKey{k, v, o})), at_end(RepeatedKey{name}, q), guard(String.eq(n, name), defect(~rule, vs, lookup(name, RKey{k, v, o}), None{}, q))))
1283	    case SVariant{+name, +vs, +rest} RKey{+k, +v, +o} AtField{1n+j, +n} <> +q:
1284	      pick_why(is_missing(lookup(name, RKey{k, v, o})), defect(~rule, rest, RKey{k, v, o}, None{}, AtField{j, n} <> q), guard(conforms(~rule, vs, lookup(name, RKey{k, v, o}), None{}), dup_defect(rest, RKey{k, v, o}, AtField{j, n} <> q)))
1285	    case SVariant{+name, +vs, +rest} RKey{+k, +v, +o} +q:
1286	      pick_why(is_missing(lookup(name, RKey{k, v, o})), defect(~rule, rest, RKey{k, v, o}, None{}, q), None{})
1287	    case SVariant{+name, +vs, +rest} x q:
1288	      not_object(x, q)
1289	    case SVEnd{} REnd{} q:
1290	      no_variant(q)
1291	    case SVEnd{} RKey{k, v, o} q:
1292	      no_variant(q)
1293	    case SVEnd{} x q:
1294	      not_object(x, q)
1295	    case STuple{ts, rest} RCons{h, t} AtIndex{0n} <> q:
1296	      defect(~rule, ts, h, None{}, q)
1297	    case STuple{+ts, rest} RCons{h, t} AtIndex{1n+j} <> q:
1298	      guard(conforms(~rule, ts, h, None{}), defect(~rule, rest, t, None{}, AtIndex{j} <> q))
1299	    case STuple{+ts, rest} RCons{h, t} q:
1300	      guard(conforms(~rule, ts, h, None{}), defect(~rule, rest, t, None{}, q))
1301	    case STuple{ts, rest} RNil{} q:
1302	      at_end(TooShort{}, q)
1303	    case STuple{ts, rest} x q:
1304	      not_list(x, q)
1305	    case STEnd{} RNil{} q:
1306	      None{}
1307	    case STEnd{} RCons{h, t} q:
1308	      at_end(TooLong{}, q)
1309	    case STEnd{} x q:
1310	      not_list(x, q)
1311	    case SEither{+l, +r} +x +q:
1312	      pick_why(has_kind(l, kind_of(x)), defect(~rule, l, x, prev, q), pick_why(has_kind(r, kind_of(x)), defect(~rule, r, x, prev, q), at_end(missing_or(x, no_alt(SEither{l, r})), q)))
1313	
1314	# The closed forms: template defs cannot cross the bundler, so the host
1315	# calls these (a project with no rules).
1316	
1317	def check0(s: Schema, r: Raw) -> Maybe<&2, Err>:
1318	  check(~no_rule, s, r, None{})
1319	
1320	def conforms0(s: Schema, r: Raw) -> Bool:
1321	  conforms(~no_rule, s, r, None{})
1322	
1323	# ---- the claims the choice laws make ----
1324	#
1325	# A second reading of a variant chain, by counting: the value is an object,
1326	# exactly one of the chain's keys is in it, and every key that is there holds
1327	# a value that conforms. A key that is there is read the way conforms reads
1328	# it, key_once included: a key the chain names, taken twice, is not read once,
1329	# so the counting reading refuses it exactly where conforms does.
1330	
1331	def is_chain(s: Schema) -> Bool:
1332	  match s:
1333	    case SVariant{n, vs, rest}:
1334	      is_chain(rest)
1335	    case SVEnd{}:
1336	      True{}
1337	    case _:
1338	      False{}
1339	
1340	def is_object(r: Raw) -> Bool:
1341	  match r:
1342	    case REnd{}:
1343	      True{}
1344	    case RKey{k, v, o}:
1345	      True{}
1346	    case _:
1347	      False{}
1348	
1349	def one_if_there(b: Bool) -> Nat:
1350	  match b:
1351	    case True{}:
1352	      0n
1353	    case False{}:
1354	      1n
1355	
1356	def count_present(s: Schema, +r: Raw) -> Nat:
1357	  match s:
1358	    case SVariant{+n, vs, rest}:
1359	      Nat.add(one_if_there(is_missing(lookup(n, r))), count_present(rest, r))
1360	    case _:
1361	      0n
1362	
1363	def present_conform(~rule: Nat -> Raw -> Maybe<&2, Err>, +s: Schema, +r: Raw) -> Bool:
1364	  match s:
1365	    case SVariant{+n, vs, rest}:
1366	      pick_bool(is_missing(lookup(n, r)), present_conform(~rule, rest, r), Bool.and(key_once(n, r), Bool.and(conforms(~rule, vs, lookup(n, r), None{}), present_conform(~rule, rest, r))))
1367	    case _:
1368	      True{}
1369	
1370	# ---- the claim the tuple law makes ----
1371	#
1372	# A second reading of a tuple, over plain lists: the schema is built from a
1373	# list of schemas, and the value conforms when it is a list of the same
1374	# length and each position conforms to the schema at the same position.
1375	
1376	def tuple_of(ss: List<&2, Schema>) -> Schema:
1377	  match ss:
1378	    case Nil{}:
1379	      STEnd{}
1380	    case h <> t:
1381	      STuple{h, tuple_of(t)}
1382	
1383	# raw_list and raw_len (a list, and how many elements it has) sit with the
1384	# other bound helpers, above: an SListLen's test reads them.
1385	
1386	def at_raw(r: Raw, +i: Nat) -> Raw:
1387	  match r i:
1388	    case RCons{h, t} 0n:
1389	      h
1390	    case RCons{h, t} 1n+j:
1391	      at_raw(t, j)
1392	    case _ _:
1393	      RMissing{}
1394	
1395	def each_pos(~rule: Nat -> Raw -> Maybe<&2, Err>, ss: List<&2, Schema>, +r: Raw, +i: Nat) -> Bool:
1396	  match ss:
1397	    case Nil{}:
1398	      True{}
1399	    case h <> t:
1400	      Bool.and(conforms(~rule, h, at_raw(r, i), None{}), each_pos(~rule, t, r, 1n+i))
1401	
1402	# ---- the claim the strict law makes ----
1403	#
1404	# How many keys of r are not in ns, counted rather than walked with a
1405	# Bool.and: a second algorithm, so that a no_extra that lets a key through
1406	# (or refuses a named one) disagrees with it.
1407	def count_unknown(+ns: List<&2, String>, r: Raw) -> Nat:
1408	  match r:
1409	    case RKey{+k, v, o}:
1410	      Nat.add(one_if_there(in_names(k, ns)), count_unknown(ns, o))
1411	    case _:
1412	      0n
1413	
1414	# ---- a schema's meaning, and reading a value into it ----
1415	#
1416	# Meaning(s) is the Bend type a schema describes: a record is its fields,
1417	# nested pairs ending in Unit; a variant chain is nested Eithers ending in
1418	# Empty; a value that may be null (SOpt) or absent (SOptional) is a Maybe. A
1419	# rule refines a shape and does not change its meaning. `enc` writes a
1420	# meaning as the host's JSON would be; `dec` reads one back. Both are written
1421	# once, for every schema, and LAWS.bend proves the round trip once.
1422	#
1423	# dec is a reader, not a check: run it on a value check accepted
1424	# (checked_decodes says it then succeeds). On a value check refuses it may
1425	# still read something, since a record reads its keys and ignores the rest.
1426	#
1427	# The round trip needs a well-formed schema (wf): a key named once in its
1428	# object or chain (lookup reads the first), and an optional value that is not
1429	# itself nullable (Some{None} and None would both be written null).
1430	
1431	type Both<A: Data, B: Data> is Data:
1432	  Both{a: A, b: B}
1433	
1434	def Meaning(s: Schema) -> Data:
1435	  match s:
1436	    case SNat{}:
1437	      Nat
1438	    case SNatIn{lo, hi}:
1439	      Nat
1440	    case SStr{}:
1441	      String
1442	    case SStrLen{lo, hi, s2}:
1443	      Meaning(s2)
1444	    case SListLen{lo, hi, s2}:
1445	      Meaning(s2)
1446	    case SOpt{i}:
1447	      Maybe<&2, Meaning(i)>
1448	    case SOptional{i}:
1449	      Maybe<&2, Meaning(i)>
1450	    case SList{e}:
1451	      List<&2, Meaning(e)>
1452	    case SField{n, fs, rest}:
1453	      Both<Meaning(fs), Meaning(rest)>
1454	    case SEnd{}:
1455	      Unit
1456	    case SRule{s2, tag}:
1457	      Meaning(s2)
1458	    case SStrict{s2}:
1459	      Meaning(s2)
1460	    case STagged{k, n, cs, rest}:
1461	      Either<&2, &2, Meaning(cs), Meaning(rest)>
1462	    case STagEnd{k}:
1463	      Empty
1464	    case SBool{}:
1465	      Bool
1466	    case STrue{}:
1467	      Unit
1468	    case SEnum{names}:
1469	      String
1470	    case SVariant{n, vs, rest}:
1471	      Either<&2, &2, Meaning(vs), Meaning(rest)>
1472	    case SVEnd{}:
1473	      Empty
1474	    case STuple{ts, rest}:
1475	      Both<Meaning(ts), Meaning(rest)>
1476	    case STEnd{}:
1477	      Unit
1478	    case SJson{}:
1479	      Json
1480	    case SInt{}:
1481	      Int
1482	    case SIntIn{lo, hi}:
1483	      Int
1484	    case SEither{l, r}:
1485	      Either<&2, &2, Meaning(l), Meaning(r)>
1486	
1487	def enc(s: Schema, x: Meaning(s)) -> Raw:
1488	  match s x:
1489	    case SNat{} n:
1490	      RNum{n}
1491	    case SNatIn{lo_, hi_} n:
1492	      RNum{n}
1493	    case SStr{} x:
1494	      RStr{x}
1495	    case SStrLen{lo_, hi_, s2} v:
1496	      enc(s2, v)
1497	    case SListLen{lo_, hi_, s2} v:
1498	      enc(s2, v)
1499	    case SOpt{i} None{}:
1500	      RNull{}
1501	    case SOpt{i} Some{v}:
1502	      enc(i, v)
1503	    case SOptional{i} None{}:
1504	      RMissing{}  # absent: the host writes no key where this one lands
1505	    case SOptional{i} Some{v}:
1506	      enc(i, v)
1507	    case SList{e} Nil{}:
1508	      RNil{}
1509	    case SList{+e} h <> t:
1510	      RCons{enc(e, h), enc(SList{e}, t)}
1511	    case SField{n, fs, rest} Both{a, b}:
1512	      RKey{n, enc(fs, a), enc(rest, b)}
1513	    case SEnd{} Unit{}:
1514	      REnd{}
1515	    case SRule{s2, tag} v:
1516	      enc(s2, v)
1517	    case SStrict{s2} v:
1518	      enc(s2, v)
1519	    case STagged{k, n, cs, rest} Inl{a}:
1520	      RKey{k, RStr{n}, enc(cs, a)}
1521	    case STagged{k, n, cs, rest} Inr{b}:
1522	      enc(rest, b)
1523	    case STagEnd{k} e:
1524	      Empty.absurd(Raw, e)
1525	    case STrue{} Unit{}:
1526	      RBool{True{}}
1527	    case SBool{} b:
1528	      RBool{b}
1529	    case SEnum{names} x:
1530	      RStr{x}
1531	    case SVariant{n, vs, rest} Inl{a}:
1532	      RKey{n, enc(vs, a), REnd{}}
1533	    case SVariant{n, vs, rest} Inr{b}:
1534	      enc(rest, b)
1535	    case SVEnd{} e:
1536	      Empty.absurd(Raw, e)
1537	    case STuple{ts, rest} Both{a, b}:
1538	      RCons{enc(ts, a), enc(rest, b)}
1539	    case STEnd{} Unit{}:
1540	      RNil{}
1541	    case SJson{} value:
1542	      RJson{value}
1543	    case SInt{} i:
1544	      int_raw(i)
1545	    case SIntIn{lo_, hi_} i:
1546	      int_raw(i)
1547	    case SEither{l, r} Inl{a}:
1548	      enc(l, a)
1549	    case SEither{l, r} Inr{b}:
1550	      enc(r, b)
1551	
1552	def lcons(-A: Data, h: Maybe<&2, A>, t: Maybe<&2, List<&2, A>>) -> Maybe<&2, List<&2, A>>:
1553	  match h t:
1554	    case Some{x} Some{xs}:
1555	      Some{x <> xs}
1556	    case _ _:
1557	      None{}
1558	
1559	def both(-A: Data, -B: Data, p: Maybe<&2, A>, q: Maybe<&2, B>) -> Maybe<&2, Both<A, B>>:
1560	  match p q:
1561	    case Some{x} Some{y}:
1562	      Some{Both{x, y}}
1563	    case _ _:
1564	      None{}
1565	
1566	def opt_some(-A: Data, m: Maybe<&2, A>) -> Maybe<&2, Maybe<&2, A>>:
1567	  match m:
1568	    case Some{v}:
1569	      Some{Some{v}}
1570	    case None{}:
1571	      None{}
1572	
1573	def map_inl(-A: Data, -B: Data, m: Maybe<&2, A>) -> Maybe<&2, Either<&2, &2, A, B>>:
1574	  match m:
1575	    case Some{v}:
1576	      Some{Inl{v}}
1577	    case None{}:
1578	      None{}
1579	
1580	def map_inr(-A: Data, -B: Data, m: Maybe<&2, B>) -> Maybe<&2, Either<&2, &2, A, B>>:
1581	  match m:
1582	    case Some{v}:
1583	      Some{Inr{v}}
1584	    case None{}:
1585	      None{}
1586	
1587	def pick_m(-A: Data, b: Bool, x: A, y: A) -> A:
1588	  match b:
1589	    case True{}:
1590	      x
1591	    case False{}:
1592	      y
1593	
1594	def true_unit(b: Bool) -> Maybe<&2, Unit>:
1595	  match b:
1596	    case True{}:
1597	      Some{Unit{}}
1598	    case False{}:
1599	      None{}
1600	
1601	def nullish(r: Raw) -> Bool:
1602	  match r:
1603	    case RNull{}:
1604	      True{}
1605	    case RMissing{}:
1606	      True{}
1607	    case _:
1608	      False{}
1609	
1610	def dec(s: Schema, r: Raw) -> Maybe<&2, Meaning(s)>:
1611	  match s r:
1612	    case SNat{} RNum{n}:
1613	      Some{n}
1614	    case SNatIn{lo_, hi_} RNum{n}:
1615	      Some{n}
1616	    case SStr{} RStr{x}:
1617	      Some{x}
1618	    case SStrLen{lo_, hi_, s2} x:
1619	      dec(s2, x)
1620	    case SListLen{lo_, hi_, s2} x:
1621	      dec(s2, x)
1622	    case SOpt{+i} +x:
1623	      pick_m(Maybe<&2, Maybe<&2, Meaning(i)>>, nullish(x), Some{None{}}, opt_some(Meaning(i), dec(i, x)))
1624	    case SOptional{+i} +x:
1625	      pick_m(Maybe<&2, Maybe<&2, Meaning(i)>>, is_missing(x), Some{None{}}, opt_some(Meaning(i), dec(i, x)))
1626	    case SList{e} RNil{}:
1627	      Some{Nil{}}
1628	    case SList{+e} RCons{h, t}:
1629	      lcons(Meaning(e), dec(e, h), dec(SList{e}, t))
1630	    case SField{+n, +fs, +rest} +x:
1631	      both(Meaning(fs), Meaning(rest), dec(fs, lookup(n, x)), dec(rest, x))
1632	    case SEnd{} x:
1633	      Some{Unit{}}
1634	    case SRule{s2, tag} x:
1635	      dec(s2, x)
1636	    case SStrict{s2} x:
1637	      dec(s2, x)
1638	    case STagged{+k, +n, +cs, +rest} +x:
1639	      pick_m(Maybe<&2, Either<&2, &2, Meaning(cs), Meaning(rest)>>, is_tag(k, n, x), map_inl(Meaning(cs), Meaning(rest), dec(cs, drop_key(k, x))), map_inr(Meaning(cs), Meaning(rest), dec(rest, x)))
1640	    case STrue{} RBool{b}:
1641	      true_unit(b)
1642	    case SBool{} RBool{b}:
1643	      Some{b}
1644	    case SEnum{names} RStr{x}:
1645	      Some{x}
1646	    case SVariant{+n, +vs, +rest} +x:
1647	      pick_m(Maybe<&2, Either<&2, &2, Meaning(vs), Meaning(rest)>>, is_missing(lookup(n, x)), map_inr(Meaning(vs), Meaning(rest), dec(rest, x)), map_inl(Meaning(vs), Meaning(rest), dec(vs, lookup(n, x))))
1648	    case STuple{+ts, +rest} RCons{h, t}:
1649	      both(Meaning(ts), Meaning(rest), dec(ts, h), dec(rest, t))
1650	    case STEnd{} RNil{}:
1651	      Some{Unit{}}
1652	    case SJson{} RJson{value}:
1653	      Some{value}
1654	    case SInt{} RNum{n}:
1655	      Some{IPos{n}}
1656	    case SInt{} RNeg{n}:
1657	      Some{INeg{n}}
1658	    case SIntIn{lo_, hi_} RNum{n}:
1659	      Some{IPos{n}}
1660	    case SIntIn{lo_, hi_} RNeg{n}:
1661	      Some{INeg{n}}
1662	    case SEither{+l, +r} +x:
1663	      pick_m(Maybe<&2, Either<&2, &2, Meaning(l), Meaning(r)>>, has_kind(l, kind_of(x)), map_inl(Meaning(l), Meaning(r), dec(l, x)), pick_m(Maybe<&2, Either<&2, &2, Meaning(l), Meaning(r)>>, has_kind(r, kind_of(x)), map_inr(Meaning(l), Meaning(r), dec(r, x)), None{}))
1664	    case _ _:
1665	      None{}
1666	
1667	# ---- a well-formed schema ----
1668	#
1669	# wf is what the round trip needs: a key named once in its object or chain
1670	# (lookup reads the first), an optional value that is not itself nullable, and
1671	# a tagged case whose own schema leaves the tag key alone.
1672	# Three constructors ask more than their own shape:
1673	#
1674	#   STagged writes its key and then the case's own object beside it, so the
1675	#   case's schema may not put that key anywhere in the same object (no_key).
1676	#   A case that names its own tag key encodes to a document holding the key
1677	#   twice: enc writes the tag and the case's own field writes it again, and
1678	#   the host builds that document as a JS object, where the second write --
1679	#   the spread of the case's own fields -- overwrites the first. What the
1680	#   encoder wrote is then not what the decoder reads, so refusing the schema
1681	#   is what keeps encode_conforms true.
1682	#
1683	#   SOptional is where a field may be absent, so it belongs immediately under
1684	#   a field and nowhere else: every other place a schema sits is guarded by
1685	#   opt_at, which asks whether an absent value can reach the top of what enc
1686	#   writes for it. That excludes an SOptional anywhere but a field's schema,
1687	#   and also a schema that would pass one straight through (SOpt{SOptional{i}}
1688	#   writes RMissing for Some{None}, where nothing can tell it from an absent
1689	#   key). An SOptional's own inner is guarded the same way: None and
1690	#   Some{None} would both be written as an absent key.
1691	#
1692	#   SOpt's inner may not be nullable at all (its own None and the inner's null
1693	#   would both be written null), and nullable asks an SOptional too.
1694	#
1695	#   SEither's alternatives take disjoint kinds, so the value's kind names
1696	#   the one alternative that reads it; neither may be an absent field or
1697	#   s.json() (alt_ok).
1698	
1699	# An absent value reaches the top of what enc writes for s: s is an SOptional,
1700	# or it hands the value it was given straight to a schema that is (a rule, a
1701	# strict object, a bound, or the tail of a variant or tagged chain -- and an
1702	# SOpt, whose Some case passes the value through). Everything else wraps what
1703	# it writes in a constructor of its own, so an absent value cannot surface.
1704	def opt_at(s: Schema) -> Bool:
1705	  match s:
1706	    case SOptional{i}:
1707	      True{}
1708	    case SOpt{i}:
1709	      opt_at(i)
1710	    case SRule{s2, tag}:
1711	      opt_at(s2)
1712	    case SStrict{s2}:
1713	      opt_at(s2)
1714	    case SStrLen{lo, hi, s2}:
1715	      opt_at(s2)
1716	    case SListLen{lo, hi, s2}:
1717	      opt_at(s2)
1718	    case STagged{k, n, cs, rest}:
1719	      opt_at(rest)
1720	    case SVariant{n, vs, rest}:
1721	      opt_at(rest)
1722	    case _:
1723	      False{}
1724	
1725	def nullable(s: Schema) -> Bool:
1726	  match s:
1727	    case SOpt{i}:
1728	      True{}
1729	    case SOptional{i}:
1730	      True{}  # absent and the inner's own null read as the same None
1731	    case SRule{s2, tag}:
1732	      nullable(s2)
1733	    case SStrict{s2}:
1734	      nullable(s2)
1735	    case SStrLen{lo, hi, s2}:
1736	      nullable(s2)
1737	    case SListLen{lo, hi, s2}:
1738	      nullable(s2)
1739	    case STagged{k, n, cs, rest}:
1740	      nullable(rest)
1741	    case SVariant{n, vs, rest}:
1742	      nullable(rest)
1743	    case SEither{l, r}:
1744	      Bool.or(nullable(l), nullable(r))  # a null would read as the inner's
1745	    case _:
1746	      False{}
1747	
1748	# ---- the object a schema's encoding lands in ----
1749	#
1750	# enc writes an object as one flat chain of keys. An SField writes its name and
1751	# its rest continues that object; an SVariant writes its name and the value
1752	# under it is a chain of its own (REnd ends it, so it is a value and not a
1753	# continuation). A wrapper -- a rule, a strict object, a bound, an optional --
1754	# writes no key of its own and hands its value straight to its inner schema,
1755	# so a key reaches the top of the object from inside any of them. A tagged
1756	# case's schema is the same object the tag key was written into, and so is the
1757	# rest of its chain.
1758	#
1759	# no_key is that, written down: k does not reach the top of the object enc
1760	# builds for s, for any value of s. wf asks it of a tagged case's own schema,
1761	# which is what keeps the tag key from being written twice.
1762	def no_key(+k: String, s: Schema) -> Bool:
1763	  match s:
1764	    case SField{+n, fs, rest}:
1765	      Bool.and(Bool.not(String.eq(n, k)), Bool.and(Bool.not(String.eq(k, n)), no_key(k, rest)))
1766	    case SVariant{+n, vs, rest}:
1767	      Bool.and(Bool.not(String.eq(n, k)), Bool.and(Bool.not(String.eq(k, n)), no_key(k, rest)))
1768	    case SStrict{s2}:
1769	      no_key(k, s2)
1770	    case SRule{s2, tag}:
1771	      no_key(k, s2)
1772	    case SStrLen{lo, hi, s2}:
1773	      no_key(k, s2)
1774	    case SListLen{lo, hi, s2}:
1775	      no_key(k, s2)
1776	    case SOpt{i}:
1777	      no_key(k, i)
1778	    case SOptional{i}:
1779	      no_key(k, i)
1780	    case SEither{l, r}:
1781	      Bool.and(no_key(k, l), no_key(k, r))
1782	    case STagged{+k2, n2, cs2, rest2}:
1783	      Bool.and(Bool.not(String.eq(k2, k)), Bool.and(Bool.not(String.eq(k, k2)), Bool.and(no_key(k, cs2), no_key(k, rest2))))
1784	    case _:
1785	      True{}
1786	
1787	# n is not a key of the record chain s (a chain ends in SEnd). Both orders are
1788	# asked, as fresh_v asks them: which of the two names a step puts first depends
1789	# on which of them is the value's key there, and asking both spares a proof
1790	# that String.eq is symmetric.
1791	def fresh_f(+n: String, s: Schema) -> Bool:
1792	  match s:
1793	    case SField{+m, fs, rest}:
1794	      Bool.and(Bool.not(String.eq(m, n)), Bool.and(Bool.not(String.eq(n, m)), fresh_f(n, rest)))
1795	    case SEnd{}:
1796	      True{}
1797	    case _:
1798	      False{}
1799	
1800	# n is not a key of the variant chain s (a chain ends in SVEnd). Both orders
1801	# are asked: reading a key compares the names one way, reading past it the
1802	# other, and asking both spares a proof that String.eq is symmetric.
1803	def fresh_v(+n: String, s: Schema) -> Bool:
1804	  match s:
1805	    case SVariant{+m, vs, rest}:
1806	      Bool.and(Bool.not(String.eq(m, n)), Bool.and(Bool.not(String.eq(n, m)), fresh_v(n, rest)))
1807	    case SVEnd{}:
1808	      True{}
1809	    case _:
1810	      False{}
1811	
1812	# A record chain (ending in SEnd) or a variant chain (ending in SVEnd): what
1813	# SStrict may wrap, so every key its encoding writes is a declared name.
1814	# A chain of keys (SField or SVariant links, ending in SEnd or SVEnd): what
1815	# SStrict may wrap, so every key its encoding writes is a name it declares.
1816	def is_keyed(s: Schema) -> Bool:
1817	  match s:
1818	    case SField{n, fs, rest}:
1819	      is_keyed(rest)
1820	    case SEnd{}:
1821	      True{}
1822	    case SVariant{n, vs, rest}:
1823	      is_keyed(rest)
1824	    case SVEnd{}:
1825	      True{}
1826	    case _:
1827	      False{}
1828	
1829	# n names no case of the tagged chain s, whose key is k, and the chain ends
1830	# in STagEnd{k}: one key for the whole chain.
1831	def fresh_t(+k: String, +n: String, s: Schema) -> Bool:
1832	  match s:
1833	    case STagged{+k2, +m, cs, rest}:
1834	      Bool.and(String.eq(k2, k), Bool.and(Bool.not(String.eq(m, n)), fresh_t(k, n, rest)))
1835	    case STagEnd{k2}:
1836	      String.eq(k2, k)
1837	    case _:
1838	      False{}
1839	
1840	def wf(s: Schema) -> Bool:
1841	  match s:
1842	    case SOpt{+i}:
1843	      Bool.and(Bool.not(nullable(i)), wf(i))
1844	    case SOptional{+i}:
1845	      Bool.and(Bool.not(opt_at(i)), wf(i))
1846	    case SList{+e}:
1847	      Bool.and(Bool.not(opt_at(e)), wf(e))
1848	    case SListLen{lo_, hi_, +s2}:
1849	      Bool.and(Bool.not(opt_at(s2)), wf(s2))
1850	    case SStrLen{lo_, hi_, +s2}:
1851	      Bool.and(Bool.not(opt_at(s2)), wf(s2))
1852	    case SField{+n, fs, +rest}:
1853	      Bool.and(wf(fs), Bool.and(fresh_f(n, rest), wf(rest)))
1854	    case SRule{+s2, tag}:
1855	      Bool.and(Bool.not(opt_at(s2)), wf(s2))
1856	    case SStrict{+s2}:
1857	      Bool.and(is_keyed(s2), Bool.and(Bool.not(opt_at(s2)), wf(s2)))
1858	    case STagged{+k, +n, +cs, +rest}:
1859	      Bool.and(Bool.not(opt_at(cs)), Bool.and(wf(cs), Bool.and(no_key(k, cs), Bool.and(fresh_t(k, n, rest), wf(rest)))))
1860	    case SVariant{+n, +vs, +rest}:
1861	      Bool.and(Bool.not(opt_at(vs)), Bool.and(wf(vs), Bool.and(fresh_v(n, rest), wf(rest))))
1862	    case STuple{+ts, +rest}:
1863	      Bool.and(Bool.not(opt_at(ts)), Bool.and(wf(ts), Bool.and(Bool.not(opt_at(rest)), wf(rest))))
1864	    case SJson{}:
1865	      True{}
1866	    case SEither{+l, +r}:
1867	      Bool.and(alt_ok(l), Bool.and(alt_ok(r), Bool.and(disjoint(l, r), Bool.and(wf(l), wf(r)))))
1868	    case _:
1869	      True{}
1870	
1871	# Every enum value in x is one of its names (encode_conforms' premise).
1872	def names_ok(s: Schema, x: Meaning(s)) -> Bool:
1873	  match s x:
1874	    case SOpt{i} None{}:
1875	      True{}
1876	    case SOpt{i} Some{v}:
1877	      names_ok(i, v)
1878	    case SList{e} Nil{}:
1879	      True{}
1880	    case SList{+e} h <> t:
1881	      Bool.and(names_ok(e, h), names_ok(SList{e}, t))
1882	    case SField{n, fs, rest} Both{a, b}:
1883	      Bool.and(names_ok(fs, a), names_ok(rest, b))
1884	    case SRule{s2, tag} v:
1885	      names_ok(s2, v)
1886	    case SStrict{s2} v:
1887	      names_ok(s2, v)
1888	    case SStrLen{lo_, hi_, s2} v:
1889	      names_ok(s2, v)
1890	    case SListLen{lo_, hi_, s2} v:
1891	      names_ok(s2, v)
1892	    case SOptional{i} None{}:
1893	      True{}
1894	    case SOptional{i} Some{v}:
1895	      names_ok(i, v)
1896	    case STagged{k, n, cs, rest} Inl{a}:
1897	      names_ok(cs, a)
1898	    case STagged{k, n, cs, rest} Inr{b}:
1899	      names_ok(rest, b)
1900	    case SEnum{names} x:
1901	      in_names(x, names)
1902	    case SVariant{n, vs, rest} Inl{a}:
1903	      names_ok(vs, a)
1904	    case SVariant{n, vs, rest} Inr{b}:
1905	      names_ok(rest, b)
1906	    case STuple{ts, rest} Both{a, b}:
1907	      Bool.and(names_ok(ts, a), names_ok(rest, b))
1908	    case SJson{} value:
1909	      True{}
1910	    case SEither{l, r} Inl{a}:
1911	      names_ok(l, a)
1912	    case SEither{l, r} Inr{b}:
1913	      names_ok(r, b)
1914	    case _ _:
1915	      True{}
1916	
1917	# Every bound a constructor states holds of the value that will be written, at
1918	# every place one sits in the schema (encode_conforms' second premise, beside
1919	# names_ok). The encoder writes the meaning unchanged, so a value outside a
1920	# bound is written out as it is and refused by check on the way back: the host
1921	# that built it is at fault, and this is where it says so. An SStrLen's bound
1922	# is read off the string its own schema writes, and an SListLen's count off the
1923	# list it writes, which is why enc appears here.
1924	def bounds_ok(s: Schema, x: Meaning(s)) -> Bool:
1925	  match s x:
1926	    case SOpt{i} None{}:
1927	      True{}
1928	    case SOpt{i} Some{v}:
1929	      bounds_ok(i, v)
1930	    case SList{e} Nil{}:
1931	      True{}
1932	    case SList{+e} h <> t:
1933	      Bool.and(bounds_ok(e, h), bounds_ok(SList{e}, t))
1934	    case SField{n, fs, rest} Both{a, b}:
1935	      Bool.and(bounds_ok(fs, a), bounds_ok(rest, b))
1936	    case SRule{s2, tag} v:
1937	      bounds_ok(s2, v)
1938	    case SStrict{s2} v:
1939	      bounds_ok(s2, v)
1940	    case STagged{k, n, cs, rest} Inl{a}:
1941	      bounds_ok(cs, a)
1942	    case STagged{k, n, cs, rest} Inr{b}:
1943	      bounds_ok(rest, b)
1944	    case SNatIn{+lo, +hi} n:
1945	      num_ok(lo, hi, n)
1946	    case SStrLen{+lo, +hi, +s2} +v:
1947	      Bool.and(bounds_ok(s2, v), len_ok(lo, hi, enc(s2, v)))
1948	    case SListLen{+lo, +hi, +s2} +v:
1949	      Bool.and(bounds_ok(s2, v), list_len_ok(lo, hi, enc(s2, v)))
1950	    case SOptional{i} None{}:
1951	      True{}
1952	    case SOptional{i} Some{v}:
1953	      bounds_ok(i, v)
1954	    case SVariant{n, vs, rest} Inl{a}:
1955	      bounds_ok(vs, a)
1956	    case SVariant{n, vs, rest} Inr{b}:
1957	      bounds_ok(rest, b)
1958	    case STuple{ts, rest} Both{a, b}:
1959	      Bool.and(bounds_ok(ts, a), bounds_ok(rest, b))
1960	    case SJson{} value:
1961	      valid_json(value)
1962	    case SIntIn{+lo, +hi} i:
1963	      int_ok(lo, hi, i)
1964	    case SEither{l, r} Inl{a}:
1965	      bounds_ok(l, a)
1966	    case SEither{l, r} Inr{b}:
1967	      bounds_ok(r, b)
1968	    case _ _:
1969	      True{}