core.bend

bend-schema-lib@0.4.1.0 · 1,962 lines · 126 definitions

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