feat(lexicon): lexicon v2 schema as a Nickel contract; loader learns relations and evidence (stage 6c PR 1)

.github/workflows/dogfood-proofs-ci.yml

@@ -219,7 +219,11 @@ jobs:
 
   agda:
     name: Agda
-    runs-on: ubuntu-latest
+    # Pinned: ubuntu-latest moved to 26.04, whose apt agda 2.8.0 rejects the
+    # options agda-stdlib v1.7.3 sets ("Unrecognized option:
+    # --warn=noUserWarning"). 24.04 ships agda 2.6.3, the version the corpus
+    # is verified against. Unpin when the stdlib moves to a 2.8-compatible tag.
+    runs-on: ubuntu-24.04
     timeout-minutes: 20
     steps:
       - uses: actions/checkout@v7.0.1

.github/workflows/rust-ci.yml

@@ -77,6 +77,20 @@ jobs:
           repository: ${{ github.repository }}
           ref: ${{ github.ref }}
 
+      - name: Lexicon v2 contract (Nickel)
+        # data/synonyms/schema.ncl applied to every shipped table, plus the
+        # accept/reject fixtures that prove the contract still bites.
+        # Nickel is a pinned release binary checked by SHA-256 (no action, so
+        # no actions.lock record). Bump both lines together.
+        env:
+          NICKEL_VERSION: 1.12.2
+          NICKEL_SHA256: dae58ae8a96bbcacf141d61a5f93a971c89341f9d7164f763aa170459336ea46
+        run: |
+          curl -sSfL -o "$RUNNER_TEMP/nickel" "https://github.com/tweag/nickel/releases/download/${NICKEL_VERSION}/nickel-x86_64-linux"
+          echo "${NICKEL_SHA256}  $RUNNER_TEMP/nickel" | sha256sum -c -
+          chmod +x "$RUNNER_TEMP/nickel"
+          NICKEL="$RUNNER_TEMP/nickel" scripts/lexicon-check.sh
+
       - name: Install Rust toolchain
         # `toolchain:` is mandatory because the ref is `@v1` (pinned to a commit
         # through actions.lock), not a toolchain name:

Justfile

@@ -1138,6 +1138,12 @@ corpus-stats-all:
 synonym-load-test:
     cargo test --lib --quiet suggest::synonyms 2>&1 | tail -20
 
+# Lexicon v2: apply the Nickel contract (data/synonyms/schema.ncl) to every
+# synonym table and to the accept/reject fixtures. Needs nickel >= 1.12.
+lexicon-check:
+    scripts/lexicon-check.sh
+    cargo test --locked --test lexicon_v2_test
+
 # Run the saturation-campaign cargo tests only (139 cases + 1 ignored).
 test-saturation:
     cargo test --lib -- \

data/synonyms/README.adoc

@@ -51,7 +51,7 @@ Each `[[synonym]]` entry has:
 
 | `aliases`
 | yes
-| Array of equivalent names.  Order is *not* significant.
+| Array of non-empty names; `relation` says how they relate to `canonical`.  Order is *not* significant.
 
 | `tactic_class`
 | no
@@ -68,6 +68,63 @@ Each `[[synonym]]` entry has:
 | Version range over which the alias applies.  Empty means "always".
 |===
 
+== Lexicon v2 fields
+
+Owner decisions 2026-10-19 (D2, D4) in
+`docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc`.
+All fields are optional; v1 rows load unchanged. The schema of record is the
+Nickel contract `schema.ncl`; `scripts/lexicon-check.sh` (or
+`just lexicon-check`) applies it to every table here and to the fixtures in
+`tests/lexicon_fixtures/`, and CI runs it in the `rust-ci` check job.
+
+[cols="1,3"]
+|===
+| Field | Meaning
+
+| `relation`
+| How `aliases` relate to `canonical`: `synonym` (default, interchangeable),
+  `specialisation` (each alias is a special case), `generalisation`,
+  `false_friend` (looks alike, is not; never substituted) or `phrase`
+  (`canonical` is a multi-token idiom). Only `synonym` and `phrase` rows feed
+  the variant tester; the others are reported by `SynonymTable::related`.
+  Phrase substitution runs one way for now: an alias at a tactic site can be
+  replaced by the phrase spelling, but the extractors see single identifiers,
+  so a canonical phrase in a proof is not yet replaced by an alias.
+
+| `phrase`
+| Token list of a multi-token idiom. Required with, and only allowed with,
+  `relation = "phrase"`.
+
+| `false_friends`
+| Look-alike names in other tables, each `{ name, table }` where `table` is
+  the other file's stem.
+
+| `evidence`
+| The witness behind the row: `{ kind = "none" }` (default), `"curated"`,
+  `"probe"` with `tests` and `failures`, or `"kernel"` with `format`,
+  `checked_by` and a 64-hex BLAKE3 `term_hash`; counts are integers that fit
+  a u32. Evidence attests the row's relation, whatever it is, but lifts into
+  the arbiter's `FidelityEvidence` (`SynonymEntry::fidelity_evidence`) only
+  for an identity claim: a `synonym` or `phrase` row that is not `lossy`.
+  There `probe` lifts to `DeclaredCorrespondence` and `kernel` to
+  `KernelTranslation`; `none`, `curated` (provenance, not fidelity
+  evidence) and every other row lift to `None`. A lexicon row never raises
+  a verdict above its own evidence.
+
+| `fidelity`, `residue`
+| `exact` or `lossy`; a lossy row must say what is lost in `residue`.
+
+| `scope`
+| `{ library, version }` the relation holds in.
+|===
+
+Corpus-mined candidates (owner decision D4) are flag-only: they carry
+`evidence = { kind = "none" }` and never set `semantic_class` on their own.
+
+Nickel checks shape and the cross-field rules; serde checks that
+`checked_by` names a `ProverKind` and `format` an `ExchangeFormat` when Rust
+loads a table (`tests/lexicon_v2_test.rs`).
+
 == Variant-tester contract
 
 When `echidna suggest` encounters a tactic name in a failing proof, it:

data/synonyms/hol4.toml

@@ -108,7 +108,7 @@ aliases      = ["Induct_on", "recInduct", "completeInduct_on"]
 tactic_class = "induction"
 notes        = """
 `Induct` does induction on the *outermost* universally-quantified
-variable. `Induct_on \`x\`` picks the variable explicitly.
+variable. `Induct_on `x`` picks the variable explicitly.
 `recInduct` uses the recursion induction principle generated from a
 `Define`. `completeInduct_on` is strong (course-of-values) induction.
 """
@@ -128,7 +128,7 @@ canonical    = "Cases"
 aliases      = ["Cases_on", "FULL_CASES_TAC"]
 tactic_class = "case"
 notes        = """
-Case split on the outermost universal. `Cases_on \`x\`` picks the
+Case split on the outermost universal. `Cases_on `x`` picks the
 variable. `FULL_CASES_TAC` is the legacy form that also splits
 hypotheses by case.
 """
@@ -161,7 +161,7 @@ canonical    = "EXISTS_TAC"
 aliases      = ["Q.EXISTS_TAC", "qexists_tac", "MAP_EVERY EXISTS_TAC"]
 tactic_class = "structural"
 notes        = """
-Witness an existential. `Q.EXISTS_TAC \`t\`` accepts a quotation
+Witness an existential. `Q.EXISTS_TAC `t`` accepts a quotation
 (parses `t` in the current goal's context). `qexists_tac` is the
 modern lower-case alias.
 """
@@ -172,7 +172,7 @@ aliases      = ["Q.SPECL", "ISPEC", "SPEC"]
 tactic_class = "lemma"
 notes        = """
 Specialise a universally-quantified theorem to a quoted term.
-`Q.SPECL [\`a\`,\`b\`]` does multiple at once. `ISPEC` infers the type
+`Q.SPECL [`a`,`b`]` does multiple at once. `ISPEC` infers the type
 from the term; bare `SPEC` requires a term of the matching type.
 """
 
@@ -230,7 +230,7 @@ canonical    = "Definition"
 aliases      = ["Define", "tDefine", "Hol_reln"]
 tactic_class = "term_builder"
 notes        = """
-`Definition name: eqn End` (modern) / `Define \`eqn\`` (classic).
+`Definition name: eqn End` (modern) / `Define `eqn`` (classic).
 `tDefine` accepts a termination-measure annotation for definitions
 whose termination isn't structural. `Hol_reln` is the inductive-
 relation variant (corresponds to `Inductive`).
@@ -315,7 +315,7 @@ canonical    = "by"
 aliases      = ["sg", "SUBGOAL_THEN", "qsuff_tac"]
 tactic_class = "structural"
 notes        = """
-HOL4 modern Theorem syntax: `\`stmt\` by tac` proves a side-lemma
+HOL4 modern Theorem syntax: ``stmt` by tac` proves a side-lemma
 and adds it as a hypothesis. `qsuff_tac` is the "it-suffices-to-show"
 form (turns the current goal into the lemma + a discharge step).
 """
@@ -325,7 +325,7 @@ canonical    = "first_assum"
 aliases      = ["pop_assum", "qpat_assum", "Q.PAT_ASSUM"]
 tactic_class = "structural"
 notes        = """
-Hypothesis lookup. `qpat_assum \`pat\` f` finds the first hypothesis
+Hypothesis lookup. `qpat_assum `pat` f` finds the first hypothesis
 matching `pat` and applies `f`. `pop_assum f` pops the most-recent
 hypothesis and applies `f` (typical use: `pop_assum mp_tac`).
 """

data/synonyms/schema.ncl

@@ -0,0 +1,166 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Lexicon v2 — the normative schema for every `data/synonyms/*.toml` table.
+#
+# Owner decision 2026-10-19 (D2): the lexicon schema is written in Nickel.
+# The tables stay TOML so the Rust loader (`src/rust/suggest/synonyms.rs`)
+# and the Julia mirror (`src/julia/saturation_synonyms.jl`) read them
+# unchanged; Nickel imports each table and applies `Table` to it.
+# Check one table:   nickel export <<< '(import "data/synonyms/coq.toml") | (import "data/synonyms/schema.ncl").Table'
+# Check all tables:  scripts/lexicon-check.sh
+#
+# Division of labour: this contract checks shape and the cross-field rules
+# below. Enum membership of `checked_by` (a `ProverKind` variant name) and
+# `format` (an `ExchangeFormat`) is checked by serde when Rust loads the
+# table (`tests/lexicon_v2_test.rs` loads every table), so neither list is
+# duplicated here.
+#
+# Design: docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc
+
+let fail = fun msg => 'Error { message = msg } in
+
+let is_nonempty_string = fun v => std.is_string v && v != "" in
+
+let all_nonempty_strings = fun v =>
+  std.is_array v && std.array.all is_nonempty_string v
+in
+
+# `LexiconEvidence::Probe` holds u32 counts; the contract must not certify
+# a count the Rust loader rejects.
+let is_u32 = fun v =>
+  std.is_number v && std.number.is_integer v && v >= 0 && v <= 4294967295
+in
+
+let only_fields = fun allowed r =>
+  std.array.all (fun f => std.array.elem f allowed) (std.record.fields r)
+in
+
+let unknown_fields = fun allowed r =>
+  std.array.filter (fun f => !(std.array.elem f allowed)) (std.record.fields r)
+in
+
+# How `aliases` relate to `canonical`.
+#   synonym         interchangeable names (the v1 meaning; the default)
+#   specialisation  each alias is a special case of `canonical`
+#   generalisation  each alias generalises `canonical`
+#   false_friend    each alias looks like `canonical` and is NOT it; the
+#                   variant tester never substitutes it
+#   phrase          `canonical` is a multi-token idiom spelled out in `phrase`
+let relations = ["synonym", "specialisation", "generalisation", "false_friend", "phrase"] in
+
+# The witness behind a row, mirroring the ECH-05 `FidelityEvidence` shapes.
+# Evidence attests the row's relation, whatever it is. It lifts to the
+# arbiter only for an identity claim: a `synonym` or `phrase` row whose
+# fidelity is not `lossy` (`SynonymEntry::fidelity_evidence` in Rust).
+# There `probe` lifts to `DeclaredCorrespondence` and `kernel` to
+# `KernelTranslation`; `none` and `curated` (provenance, not fidelity
+# evidence) lift to `FidelityEvidence::None`, as does every row that is
+# not an identity claim.
+let evidence_check = fun value =>
+  if !(std.is_record value) || !(std.record.has_field "kind" value) then
+    fail "evidence must be a table with a `kind` field"
+  else
+    let k = value.kind in
+    if k == "none" || k == "curated" then
+      if only_fields ["kind"] value then 'Ok value
+      else fail "evidence `%{k}` takes no other field"
+    else if k == "probe" then
+      if !(only_fields ["kind", "tests", "failures"] value)
+        || !(std.record.has_field "tests" value)
+        || !(std.record.has_field "failures" value) then
+        fail "probe evidence needs exactly `tests` and `failures`"
+      else if !(is_u32 value.tests) || !(is_u32 value.failures) then
+        fail "probe evidence `tests` and `failures` must be integers from 0 to 4294967295"
+      else if value.tests < 1 || value.failures > value.tests then
+        fail "probe evidence needs tests >= 1 and 0 <= failures <= tests"
+      else 'Ok value
+    else if k == "kernel" then
+      if !(only_fields ["kind", "format", "checked_by", "term_hash"] value)
+        || !(std.record.has_field "format" value)
+        || !(std.record.has_field "checked_by" value)
+        || !(std.record.has_field "term_hash" value) then
+        fail "kernel evidence needs exactly `format`, `checked_by` and `term_hash`"
+      else if !(is_nonempty_string value.format) || !(is_nonempty_string value.checked_by) then
+        fail "kernel evidence `format` and `checked_by` must be non-empty strings"
+      else if !(std.is_string value.term_hash)
+        || !(std.string.is_match "^[0-9a-f]{64}$" value.term_hash) then
+        fail "kernel evidence `term_hash` must be 64 lowercase hex digits (BLAKE3)"
+      else 'Ok value
+    else
+      fail "evidence kind must be one of none, curated, probe, kernel"
+in
+
+let evidence_contract = std.contract.custom (fun _label value => evidence_check value) in
+
+let entry_fields = [
+  "canonical", "aliases", "tactic_class", "semantic_class", "notes", "since", "until",
+  "relation", "phrase", "false_friends", "evidence", "fidelity", "residue", "scope",
+] in
+
+let optional_strings = ["tactic_class", "semantic_class", "notes", "since", "until"] in
+
+let entry_contract = std.contract.custom (fun _label e =>
+  if !(std.is_record e) then fail "each [[synonym]] must be a table"
+  else if !(only_fields entry_fields e) then
+    fail "unknown field(s): %{std.string.join ", " (unknown_fields entry_fields e)}"
+  else if !(std.record.has_field "canonical" e) || !(is_nonempty_string e.canonical) then
+    fail "`canonical` must be a non-empty string"
+  else if !(std.record.has_field "aliases" e) || !(all_nonempty_strings e.aliases) then
+    fail "`%{e.canonical}`: `aliases` must be an array of non-empty strings"
+  else if !(std.array.all
+      (fun f => !(std.record.has_field f e) || std.is_string (std.record.get f e))
+      optional_strings) then
+    fail "`%{e.canonical}`: tactic_class, semantic_class, notes, since and until must be strings"
+  else
+    let relation = if std.record.has_field "relation" e then e.relation else "synonym" in
+    if !(std.array.elem relation relations) then
+      fail "`%{e.canonical}`: relation must be one of %{std.string.join ", " relations}"
+    else if relation == "phrase" && !(std.record.has_field "phrase" e) then
+      fail "`%{e.canonical}`: relation `phrase` needs a `phrase` token list"
+    else if std.record.has_field "phrase" e && relation != "phrase" then
+      fail "`%{e.canonical}`: `phrase` is only allowed with relation `phrase`"
+    else if std.record.has_field "phrase" e
+      && (!(all_nonempty_strings e.phrase) || std.array.length e.phrase < 2) then
+      fail "`%{e.canonical}`: `phrase` must list at least two non-empty tokens"
+    else if relation != "synonym" && relation != "phrase" && std.array.length e.aliases == 0 then
+      fail "`%{e.canonical}`: relation `%{relation}` needs at least one alias to relate"
+    else if std.record.has_field "false_friends" e
+      && !(std.is_array e.false_friends
+        && std.array.all
+          (fun ff => std.is_record ff && only_fields ["name", "table"] ff
+            && std.record.has_field "name" ff && is_nonempty_string ff.name
+            && std.record.has_field "table" ff && is_nonempty_string ff.table)
+          e.false_friends) then
+      fail "`%{e.canonical}`: each false_friends item needs exactly a non-empty `name` and `table`"
+    else if std.record.has_field "fidelity" e && !(std.array.elem e.fidelity ["exact", "lossy"]) then
+      fail "`%{e.canonical}`: fidelity must be `exact` or `lossy`"
+    else if std.record.has_field "fidelity" e && e.fidelity == "lossy"
+      && !(std.record.has_field "residue" e && is_nonempty_string e.residue) then
+      fail "`%{e.canonical}`: a lossy correspondence must say what is lost in `residue`"
+    else if std.record.has_field "residue" e
+      && !(std.record.has_field "fidelity" e && e.fidelity == "lossy") then
+      fail "`%{e.canonical}`: `residue` is only allowed with fidelity `lossy`"
+    else if std.record.has_field "scope" e
+      && !(std.is_record e.scope && only_fields ["library", "version"] e.scope
+        && std.record.has_field "library" e.scope && is_nonempty_string e.scope.library
+        && (!(std.record.has_field "version" e.scope) || is_nonempty_string e.scope.version)) then
+      fail "`%{e.canonical}`: scope needs a non-empty `library` and optionally a `version`"
+    else
+      if std.record.has_field "evidence" e then
+        evidence_check e.evidence
+        |> match {
+          'Ok _ => 'Ok e,
+          'Error err => fail "`%{e.canonical}`: %{err.message}",
+        }
+      else
+        'Ok e
+)
+in
+
+{
+  Relation = std.contract.from_predicate (fun r => std.array.elem r relations),
+  Evidence = evidence_contract,
+  Entry = entry_contract,
+  Table = { synonym | Array entry_contract },
+}

docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc

@@ -2,7 +2,7 @@
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 = ADR: lexicon v2 (false friends, phrases, equivalences) and hub-and-probe identity arbitration (stage 6c)
 :revdate: 2026-10-19
-:status: proposed — owner decisions D1–D5 in §7 are open; nothing below is ruled
+:status: accepted in part — D1, D2 and D4 ruled 2026-10-19 (§7); D3 and D5 open
 
 == Context (measured on `main` at `ed6ef60`, 2026-10-19)
 
@@ -294,16 +294,20 @@ re-running `metrics/run_all.jl` to re-baseline `oov_rate` and
   verdict's `level` should surface in its trust bridge once dispatch attaches
   evidence.
 
-== Open owner decisions (the selector questions this session could not ask)
+== Owner decisions
 
-[cols="1,5,3",options="header"]
+Ruled 2026-10-19 through the selector: D1, D2 and D4. D3 and D5 remain open.
+The owner also ruled the pacing: PRs 1 and 3 proceed now; PRs 4–6 (arbiter
+and ABI changes, kernel translation) wait for the stronger model.
+
+[cols="1,5,3,3",options="header"]
 |===
-| # | Question | Recommended
-| D1 | Architecture for identity arbitration: hub and probe (A + B), super-language (C), or pairwise only (D)? | A + B
-| D2 | Lexicon v2 format: extend the TOML tables in place (loader-compatible) or move `data/synonyms/` to Nickel or deed? | TOML in place
-| D3 | First consequence-probe pair: Z3 ↔ CVC5 (runs in CI today) alongside the HOL4 ↔ HOL Light hub pilot, or wait for HOL binaries in CI? | Z3 ↔ CVC5 now
-| D4 | May corpus-mined candidates set `semantic_class` automatically? | No: `evidence = none`, flag-only until curated or probe-tested
-| D5 | Open the verisimdb consonance-subject issue (option E) now? | Yes
+| # | Question | Recommended | Ruling
+| D1 | Architecture for identity arbitration: hub and probe (A + B), super-language (C), or pairwise only (D)? | A + B | A + B (hub and probe)
+| D2 | Lexicon v2 format: extend the TOML tables in place (loader-compatible) or move `data/synonyms/` to Nickel or deed? | TOML in place | Nickel. Read as: the schema is a Nickel contract (`data/synonyms/schema.ncl`) applied to the TOML tables, which stay the data so the Rust and Julia loaders are unchanged. Converting the tables themselves to `.ncl` remains open.
+| D3 | First consequence-probe pair: Z3 ↔ CVC5 (runs in CI today) alongside the HOL4 ↔ HOL Light hub pilot, or wait for HOL binaries in CI? | Z3 ↔ CVC5 now | open
+| D4 | May corpus-mined candidates set `semantic_class` automatically? | No: `evidence = none`, flag-only until curated or probe-tested | as recommended
+| D5 | Open the verisimdb consonance-subject issue (option E) now? | Yes | open
 |===
 
 == Non-claims