diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0c90d1d..dc28085 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,5 +1,11 @@ name: ci on: [push, pull_request] + +# Every job here only reads the checkout. Artifact upload uses the runtime +# token, not this one, so read is enough. +permissions: + contents: read + jobs: test: runs-on: ubuntu-latest @@ -12,10 +18,74 @@ jobs: with: python-version: ${{ matrix.python-version }} - run: pip install -e ".[dev]" - - run: ruff check src tests + - run: ruff check src tests scripts/vv.py - run: pytest - run: realize demo three_state - run: realize demo max_formula - run: realize demo grid_recolor - run: python3 scripts/export_web_fixtures.py - run: git diff --exit-code web/fixtures + + vv: + # Verification & validation across every declared domain. See VV.md. + runs-on: ubuntu-latest + strategy: + fail-fast: false + matrix: + domain: + - formula.bounded_coeff_template + - encoder.finite_case_table + - term_series.typed_grid + - term_series.guarded_integer_sequence + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: "3.12" + - run: pip install -e ".[dev]" + - run: python3 scripts/vv.py --domain ${{ matrix.domain }} --report vv-report.json + - uses: actions/upload-artifact@v4 + if: always() + with: + name: vv-report-${{ matrix.domain }} + path: vv-report.json + + vv-lean: + # Independent corroboration of the finite facts. Lean agrees or disagrees; + # it never mints a verdict. A red job here means Lean and the Python kernel + # disagree, and one of them is wrong. + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: "3.12" + - run: pip install -e ".[dev]" + - name: cache lean toolchain + uses: actions/cache@v4 + with: + path: ~/.elan + key: elan-${{ runner.os }}-${{ hashFiles('vv/lean/lean-toolchain') }} + - name: install lean + # Pinned to an immutable revision and checksummed before it is executed. + # `master` is mutable, and this job runs on pull_request. + env: + ELAN_REV: 0e36a07b9bbcc5381fa6250df109f9a4f94d7bac + ELAN_SHA256: a620ff1641616222c8d37c54845492004bb84d6877cdbc944dd65c1aa685bf53 + run: | + set -euo pipefail + if [ ! -x "$HOME/.elan/bin/lean" ]; then + curl -sSfL \ + "https://raw.githubusercontent.com/leanprover/elan/${ELAN_REV}/elan-init.sh" \ + -o /tmp/elan-init.sh + echo "${ELAN_SHA256} /tmp/elan-init.sh" | sha256sum -c - + sh /tmp/elan-init.sh -y --default-toolchain "$(tr -d '[:space:]' < vv/lean/lean-toolchain)" + fi + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + - run: lean --version + - run: python3 scripts/vv.py --lean-required --report vv-report-lean.json + - uses: actions/upload-artifact@v4 + if: always() + with: + name: vv-report-lean + path: vv-report-lean.json diff --git a/.gitignore b/.gitignore index cbfdb11..bbdbbd0 100644 --- a/.gitignore +++ b/.gitignore @@ -8,3 +8,4 @@ build/ .ruff_cache/ .coverage htmlcov/ +vv-report*.json diff --git a/NONCLAIMS.md b/NONCLAIMS.md index bc7bb86..7161300 100644 --- a/NONCLAIMS.md +++ b/NONCLAIMS.md @@ -13,5 +13,7 @@ Read this before the README examples. 7. **Checker independence reduces one self-confirmation path.** Separate generator and checker implementations do not certify the Python runtime, the papers’ mathematics, or that a formal `R` matches anyone’s linguistic intention. 8. **`UNSAT` is scoped.** It means the declared finite class is empty (or the encoder fibre is obstructed). It never means “no operator exists.” 9. **Agents may propose. They may not certify.** Calling another model to judge an answer does not discharge `realize check`. +10. **Lean corroboration is not a verdict.** The files in `vv/lean/` re-state finite facts and check them in Lean's kernel. Agreement means two implementations, written by different means, reached the same answer about the same small finite object. It does not verify the Python code, the CLI, the CI, or the papers' mathematics, and a Lean file cannot mint `PASS`. Disagreement means one of the two is wrong and does not say which. +11. **A green V&V run is not validation.** `scripts/vv.py` checks that each declared domain does what it says it does (verification). Whether a formal `R` matches anyone's intention is a separate question this repository does not answer. See [VV.md](VV.md). If a README sentence appears to contradict this file, this file wins. diff --git a/README.md b/README.md index 32e23fc..4d30262 100644 --- a/README.md +++ b/README.md @@ -43,6 +43,34 @@ Stdout is the certificate JSON. `realize synthesize` emits candidates only and n See [NONCLAIMS.md](NONCLAIMS.md). No LLM proposer, no geometry, no sheaves, no dressings, no `realize solve`. Architecture: [papers/architecture.md](papers/architecture.md). Relational certificate pattern (not a DFM solver): [papers/relational-section.md](papers/relational-section.md). +## Verification & validation + +Four domains, where a domain is a `problem_family` paired with a `grammar`: + +| Domain | Semantics | Source | +|---|---|---| +| `formula.bounded_coeff_template` | `exact_rational` | VCOS §8.1 / Table 2 | +| `encoder.finite_case_table` | `finite_relation` | VCMS Example 4.3 | +| `term_series.typed_grid` | `finite_integer` | IGVF–CTS §7.1 | +| `term_series.guarded_integer_sequence` | `finite_integer` | VCOS §8.3 | + +```bash +python3 scripts/vv.py # every domain +python3 scripts/vv.py --lean # add the Lean corroboration +``` + +Every domain has to be *seen* reaching all four verdicts and an adapter reject — a domain that can +only be shown passing is a domain nobody has watched fail. Coverage is read out of +`realize.verdicts`, so a grammar added to the kernel breaks the run until a domain arrives with it. + +[`vv/lean/`](vv/lean/) re-states the same finite facts in Lean 4 and proves them with kernel-checked +`decide` — core Lean, no Mathlib, no `native_decide`, no `sorry`. The runner then recomputes all 29 +reported quantities from the Python kernel and compares. That is what catches a frozen count edited +to match a drifting kernel. Lean agrees or disagrees. It never mints a verdict. + +This is verification. It is not validation: whether a formal `R` matches anyone's intention stays +open, and no green run closes it. [VV.md](VV.md), then [NONCLAIMS.md](NONCLAIMS.md) §10–11. + ## Agent use Load the skill. Propose if you must. Then: @@ -74,7 +102,8 @@ Tools: `realize_check`, `realize_synthesize`, `realize_explain`, `realize_demo`. ```bash pip install -e ".[dev]" pytest -ruff check src tests +ruff check src tests scripts/vv.py +python3 scripts/vv.py ``` Python ≥ 3.11. Core extra is stdlib-only. diff --git a/VV.md b/VV.md new file mode 100644 index 0000000..ee61426 --- /dev/null +++ b/VV.md @@ -0,0 +1,136 @@ +# Verification & validation + +This file says what the repository now runs across every domain it declares, and — more +carefully — what that still does not establish. + +Read [NONCLAIMS.md](NONCLAIMS.md) first. Nothing here adds a claim that file denies. + +## Two questions wearing one abbreviation + +V&V is one abbreviation for two questions that are easy to run together (IEEE 1012, DO-178C): + +| | Academic name | The question | Said with the simplest words | +|---|---|---|---| +| **V₁** | Verification | Did we build the thing right? | Someone said what this thing must do. This thing does that. | +| **V₂** | Validation | Did we build the right thing? | Someone wanted something. The words say the same as what this someone wanted. | + +`realize check` is **verification**, and always was. A certificate says: at this declared finite +scope, under these bounds, this candidate does what `R` and `K` say. + +**Validation is the harder one, and this package cannot discharge it.** NONCLAIMS §7 already says +so: separating the generator from the checker does not certify "that a formal `R` matches anyone's +linguistic intention." No amount of green CI closes that gap. What *can* be configured is the +discipline that makes the gap visible instead of invisible — every clause that constrains must say +where it came from, and every certificate must carry the boundary its claim is good inside. That is +what the `provenance` and `scope_completeness` objectives below do. They are not validation. They +are the bookkeeping that keeps someone from mistaking verification for it. + +## The vocabulary, in the simplest words + +| Academic concept | Where it lives here | Said simply | +|---|---|---| +| Verification (IEEE 1012) | `realize check` | the thing does what the words say | +| Validation (IEEE 1012) | not dischargeable; only provenance and scope | the words say what someone wanted | +| The oracle problem | the spec is the oracle; the model is not | something else has to say what is true, and it cannot be the one that made the thing | +| Separation of duties | `tests/test_isolation.py`; `no_self_grading` | the one who makes a thing is not the one who says it is good | +| N-version / dissimilar redundancy (DO-178C) | [`vv/lean/`](vv/lean/) | two different ones do the same work apart; then you see if they say the same | +| Soundness | `PASS` is scoped, never global | when it says yes, it is true | +| Refusal of completeness | `UNKNOWN` is required (NONCLAIMS §2) | when it cannot know, it says so | +| Falsification (Popper) | `COUNTEREXAMPLE` | one thing is enough to show it is not true | +| Bounded / scoped model checking | `evidence_mode: exhaustive_finite` plus `bound` | it looked at all of a small part, not at everything | +| Trusted computing base | Lean kernel `decide` only; no `native_decide` | how much you must believe before you can believe the rest | +| Provenance / audit trail | `specification.provenance` | someone can see where these words came from | +| Tamper evidence | `spec_digest` binding | if someone changes the words, you can see it | + +## Domains + +A domain is a `problem_family` paired with a `grammar` — the axis the kernel already dispatches on. +Four are declared in [`vv/domains.json`](vv/domains.json): + +| Domain | Semantics | Source | +|---|---|---| +| `formula.bounded_coeff_template` | `exact_rational` | VCOS §8.1 / Table 2 | +| `encoder.finite_case_table` | `finite_relation` | VCMS Example 4.3 | +| `term_series.typed_grid` | `finite_integer` | IGVF–CTS §7.1 | +| `term_series.guarded_integer_sequence` | `finite_integer` | VCOS §8.3 | + +The last one was declared in `schema/realize.v0.json` and dispatched in `realize/checker.py`, and +until now shipped no spec at all — the CLI never ran it. [`vv/specs/series_seven.spec.json`](vv/specs/series_seven.spec.json) +and its siblings close that. + +Coverage is structural, not a habit: `grammar_coverage` reads `GRAMMARS` out of +`realize.verdicts` and fails if any declared grammar has no domain. Adding a grammar to the kernel +now breaks CI until a domain arrives with it. Same for `problem_family` and `semantics`. + +## Objectives + +Per case: + +| Objective | What has to hold | +|---|---| +| `outcome` | The observed verdict (or adapter reject) is the declared one. | +| `exit_table` | The exit code the matrix declares matches `realize.verdicts.EXIT`. | +| `exit_observed` | The process actually exited with that code. | +| `determinism` | Two runs of the same case agree byte for byte. | +| `scope_completeness` | The certificate carries its digest, scope, witness, and checker name. | + +Per domain: + +| Objective | What has to hold | +|---|---| +| `declared_semantics` | Matrix, kernel table, and every referenced spec agree on family / grammar / semantics. | +| `outcome_coverage` | The domain is seen reaching `PASS`, `COUNTEREXAMPLE`, `UNSAT`, `UNKNOWN`, and adapter reject. All five. | +| `tamper_evidence` | Change one field of the spec, and the passing candidate becomes an adapter reject. | +| `no_self_grading` | `realize synthesize` returns candidates and no `verdict`, anywhere in the payload. | +| `provenance` | Every non-null `R` and `K` clause cites a source. | + +`outcome_coverage` is the one worth reading twice. Every domain must be *observed* reaching all four +verdicts and the adapter reject — not merely be capable of it in principle. A domain that can only +be shown passing is a domain nobody has watched fail. + +## Running it + +```bash +python3 scripts/vv.py # every domain +python3 scripts/vv.py --domain encoder.finite_case_table # one domain +python3 scripts/vv.py --report vv-report.json # full observations as JSON +python3 scripts/vv.py --lean # add Lean, skip it if absent +python3 scripts/vv.py --lean-required # add Lean, fail if absent +pytest tests/test_vv.py # the same matrix under pytest +``` + +The runner exits `0` when every objective is met and `1` when one is not. That is deliberately +**not** the verdict scale — `0/1/2/3/4` belongs to `realize`, and a harness must not look like it is +issuing verdicts. `scripts/vv.py` is dev-only and is not part of the pip package. It cannot mint a +`PASS`; it only writes down what `realize` already decided. + +## Lean + +[`vv/lean/`](vv/lean/) re-states the finite facts of each domain in Lean 4 and proves them with +kernel-checked `decide`: core Lean only, no Mathlib, no `native_decide`, no `sorry`, no new axioms. +The runner refuses a file that reaches for any of those before `lean` is even invoked, because a +file that may assume things corroborates nothing. + +Proving things in a second language is not yet a cross-check, though: two implementations can drift +apart happily if nobody puts their answers side by side. So each Lean file also *reports* the +finite quantities it settled — 29 of them — and `scripts/vv.py` recomputes every one from the Python +kernel and compares. A disagreement fails the run; so does a fact that quietly stops being reported. + +What agreement buys: two implementations written in different languages, by different means, reached +the same answer about the same small finite object. NONCLAIMS §7 says checker independence "reduces +one self-confirmation path." This reduces a second one — and it is the one that catches a frozen +count edited to match a drifting kernel, which the Python suite alone cannot catch, because the +suite is what would have been edited. + +What it does not buy: Lean does not verify the Python kernel, the CLI, the CI, or the papers' +mathematics, and **a Lean file cannot mint a verdict**. If Lean and Python disagree, the V&V job goes +red and one of them is wrong — the job does not say which. + +## What this does not establish + +1. That `R` means what anyone intended. That is V₂, and it stays open. NONCLAIMS §7. +2. That a `PASS` says anything outside the declared finite scope. NONCLAIMS §6. +3. That the counts are a benchmark result. They are coverage. NONCLAIMS §5. +4. That the Python runtime, the OS, or GitHub Actions are correct. +5. That the domains here are the only ones that matter — only that every grammar the kernel + *declares* is exercised. A grammar nobody wrote down is still a grammar nobody checks. diff --git a/scripts/vv.py b/scripts/vv.py new file mode 100755 index 0000000..d40dcfc --- /dev/null +++ b/scripts/vv.py @@ -0,0 +1,602 @@ +#!/usr/bin/env python3 +"""Dev-only verification & validation runner. Not part of the pip package. + +This script cannot mint a verdict. It observes what `realize` already decides and +reports whether each declared domain was observed to behave as `vv/domains.json` +says it must. Its own exit status is 0 (every objective met) or 1 (something was +not met) — deliberately not the verdict exit codes, which belong to `realize`. + +Read VV.md before changing what counts as met. +""" + +from __future__ import annotations + +import argparse +import json +import re +import subprocess +import sys +import tempfile +from pathlib import Path +from typing import Any + +try: + from realize import __version__ + from realize.checker import check_search + from realize.digest import canonical_bytes + from realize.spec import load_spec + from realize.verdicts import EXIT, GRAMMARS, PROBLEM_FAMILIES, SEMANTICS, Verdict +except ModuleNotFoundError: # a bare checkout, before `pip install -e ".[dev]"` + sys.path.insert(0, str(Path(__file__).resolve().parents[1] / "src")) + from realize import __version__ + from realize.checker import check_search + from realize.digest import canonical_bytes + from realize.spec import load_spec + from realize.verdicts import EXIT, GRAMMARS, PROBLEM_FAMILIES, SEMANTICS, Verdict + +ROOT = Path(__file__).resolve().parents[1] + +CONFIG_VERSION = "realize.vv.v0" + +# A Lean file that may assume things, or that hands checking to the compiler instead +# of the kernel, corroborates nothing. These are refused before `lean` is even run. +LEAN_FORBIDDEN = ( + (re.compile(r"\bsorry\b"), "sorry"), + (re.compile(r"\bnative_decide\b"), "native_decide, which trusts the compiler, not the kernel"), + (re.compile(r"^\s*axiom\b", re.MULTILINE), "a new axiom"), + (re.compile(r"@\[(implemented_by|extern)"), "a compiler override"), +) +ADAPTER = "adapter" +OUTCOMES = frozenset({v.value for v in Verdict} | {ADAPTER}) +PROVENANCE_CLAUSES = ("R", "K") + + +# ---------------------------------------------------------------- primitives + + +def expected_exit(outcome: str) -> int: + """The exit status the documented table assigns to this outcome.""" + return EXIT[ADAPTER] if outcome == ADAPTER else EXIT[Verdict(outcome)] + + +def run_cli(spec: Path, candidate: Path) -> tuple[int, str, str]: + """Call `realize check` as a subprocess, so the exit code is tested as an interface.""" + proc = subprocess.run( + [sys.executable, "-m", "realize", "check", str(spec), str(candidate)], + capture_output=True, + text=True, + cwd=ROOT, + env={"PYTHONPATH": str(ROOT / "src"), "PATH": "/usr/bin:/bin", "HOME": str(ROOT)}, + check=False, + ) + return proc.returncode, proc.stdout, proc.stderr + + +def observe(case: dict) -> dict: + """Run one case and report what came back. No expectation is applied here.""" + spec = ROOT / case["spec"] + if case["entry"] == "cli": + code, out, err = run_cli(spec, ROOT / case["candidate"]) + if code == EXIT[ADAPTER]: + return {"outcome": ADAPTER, "exit": code, "certificate": None, "stderr": err.strip()} + try: + cert = json.loads(out) + except json.JSONDecodeError: + return {"outcome": None, "exit": code, "certificate": None, "stderr": err.strip()} + return {"outcome": cert.get("verdict"), "exit": code, "certificate": cert, "stderr": ""} + cert = check_search(spec) + verdict = cert["verdict"] + return {"outcome": verdict, "exit": expected_exit(verdict), "certificate": cert, "stderr": ""} + + +def fail(objective: str, detail: str) -> dict: + """Record an objective as not met, with the reason a reader will need.""" + return {"objective": objective, "met": False, "detail": detail} + + +def meet(objective: str, detail: str = "") -> dict: + """Record an objective as met, with what was observed.""" + return {"objective": objective, "met": True, "detail": detail} + + +# ---------------------------------------------------------------- objectives + + +def case_objectives(case: dict, seen: dict) -> list[dict]: + """Did this case do what the matrix says, through the interface it names?""" + want = case["expect"] + got = seen["outcome"] + out = [] + if got != want["outcome"]: + detail = f"expected {want['outcome']}, observed {got}" + if got == ADAPTER and seen.get("stderr"): + detail += f" ({seen['stderr']})" + out.append(fail("outcome", detail)) + else: + out.append(meet("outcome", want["outcome"])) + if want["exit"] != expected_exit(want["outcome"]): + out.append( + fail( + "exit_table", + f"matrix says exit {want['exit']} for {want['outcome']}, " + f"realize.verdicts.EXIT says {expected_exit(want['outcome'])}", + ) + ) + else: + out.append(meet("exit_table", f"{want['outcome']} -> {want['exit']}")) + if seen["exit"] != want["exit"]: + out.append(fail("exit_observed", f"expected exit {want['exit']}, observed {seen['exit']}")) + else: + out.append(meet("exit_observed", str(want["exit"]))) + return out + + +def objective_determinism(case: dict, first: dict) -> dict: + """Run the case a second time. A checker whose answer wanders is not a checker.""" + again = observe(case) + if first["certificate"] is None and again["certificate"] is None: + same = first["outcome"] == again["outcome"] and first["exit"] == again["exit"] + else: + same = canonical_bytes(first["certificate"]) == canonical_bytes(again["certificate"]) + if not same: + return fail("determinism", "two runs of the same case did not agree") + return meet("determinism", "two runs agree byte for byte") + + +def objective_scope(case: dict, seen: dict) -> dict: + """A certificate must carry the boundary its claim is good inside.""" + cert = seen["certificate"] + if cert is None: + return meet("scope_completeness", "adapter reject carries no certificate, by design") + missing = [k for k in ("spec_digest", "scope", "witness", "checker") if k not in cert] + scope = cert.get("scope") or {} + missing += [ + f"scope.{k}" + for k in ("problem_family", "grammar", "bound", "evidence_mode") + if k not in scope + ] + if missing: + return fail("scope_completeness", f"certificate is missing {sorted(missing)}") + if cert.get("checker", {}).get("name") != "realize.checker": + return fail("scope_completeness", "certificate does not name realize.checker") + return meet("scope_completeness", "digest, scope, witness and checker all present") + + +def objective_tamper(domain: dict) -> dict: + """One changed field in the spec must cost the candidate its binding.""" + passing = next( + (c for c in domain["cases"] if c["entry"] == "cli" and c["expect"]["outcome"] == "PASS"), + None, + ) + if passing is None: + return fail("tamper_evidence", "domain declares no CLI PASS case to tamper with") + spec = json.loads((ROOT / passing["spec"]).read_text(encoding="utf-8")) + spec["bound"]["budget"] = int(spec["bound"]["budget"]) - 1 + with tempfile.NamedTemporaryFile("w", suffix=".json", delete=False) as fh: + json.dump(spec, fh) + tampered = Path(fh.name) + try: + code, _out, _err = run_cli(tampered, ROOT / passing["candidate"]) + finally: + tampered.unlink(missing_ok=True) + if code != EXIT[ADAPTER]: + return fail( + "tamper_evidence", + f"budget changed by one and the candidate still scored exit {code}", + ) + return meet("tamper_evidence", "a one-field spec edit turns PASS into an adapter reject") + + +def objective_no_self_grading(domain: dict) -> dict: + """The proposer channel must never hand back something that reads as a verdict.""" + case = next((c for c in domain["cases"] if c["expect"]["outcome"] == "PASS"), None) + if case is None: + return fail("no_self_grading", "domain declares no PASS case to synthesize from") + proc = subprocess.run( + [sys.executable, "-m", "realize", "synthesize", case["spec"]], + capture_output=True, + text=True, + cwd=ROOT, + env={"PYTHONPATH": str(ROOT / "src"), "PATH": "/usr/bin:/bin", "HOME": str(ROOT)}, + check=False, + ) + if proc.returncode != 0: + return fail("no_self_grading", f"synthesize exited {proc.returncode}: {proc.stderr.strip()}") + payload = json.loads(proc.stdout) + if "verdict" in payload: + return fail("no_self_grading", "synthesize output carries a top-level verdict") + graded = [c for c in payload.get("candidates", []) if "verdict" in c] + if graded: + return fail("no_self_grading", f"{len(graded)} synthesized candidates carry a verdict") + return meet( + "no_self_grading", + f"{len(payload.get('candidates', []))} candidates, none carrying a verdict", + ) + + +def objective_provenance(domain: dict) -> dict: + """Validation gate: a clause that constrains must say where it came from.""" + gaps = [] + for path in sorted({c["spec"] for c in domain["cases"]}): + spec = load_spec(ROOT / path) + cited = {p.get("clause") for p in spec["specification"]["provenance"] if isinstance(p, dict)} + for clause in PROVENANCE_CLAUSES: + if spec["specification"][clause] is not None and clause not in cited: + gaps.append(f"{path}:{clause}") + if gaps: + return fail("provenance", f"clauses constrain but cite no source: {gaps}") + return meet("provenance", "every non-null R and K clause cites a source") + + +def objective_declared_semantics(domain: dict) -> dict: + """The matrix, the kernel's table, and every referenced spec must agree.""" + family, declared = domain["problem_family"], domain["semantics"] + if SEMANTICS.get(family) != declared: + return fail( + "declared_semantics", + f"matrix says {family} is {declared}, realize.verdicts.SEMANTICS says " + f"{SEMANTICS.get(family)}", + ) + for path in sorted({c["spec"] for c in domain["cases"]}): + spec = load_spec(ROOT / path) + if spec["problem_family"] != family: + return fail("declared_semantics", f"{path} is not family {family}") + if spec["library"]["grammar"] != domain["grammar"]: + return fail("declared_semantics", f"{path} is not grammar {domain['grammar']}") + if spec["context"]["semantics"] != declared: + return fail("declared_semantics", f"{path} is not semantics {declared}") + return meet("declared_semantics", f"{family} / {domain['grammar']} / {declared}") + + +def objective_outcome_coverage(domain: dict) -> dict: + """Every domain must be seen reaching every outcome the kernel can return.""" + reached = {c["expect"]["outcome"] for c in domain["cases"]} + missing = sorted(OUTCOMES - reached) + if missing: + return fail("outcome_coverage", f"domain never reaches {missing}") + return meet("outcome_coverage", f"reaches all {len(OUTCOMES)} outcomes") + + +# ---------------------------------------------------------------- the sweep + + +def run_domain(domain: dict) -> dict: + """Run every case in one domain, then the objectives that span the whole domain.""" + cases = [] + for case in domain["cases"]: + seen = observe(case) + objectives = case_objectives(case, seen) + objectives.append(objective_determinism(case, seen)) + objectives.append(objective_scope(case, seen)) + cases.append( + { + "id": case["id"], + "entry": case["entry"], + "spec": case["spec"], + "candidate": case.get("candidate"), + "expected": case["expect"], + "observed": {"outcome": seen["outcome"], "exit": seen["exit"]}, + "why": case.get("why", ""), + "objectives": objectives, + "ok": all(o["met"] for o in objectives), + } + ) + properties = [ + objective_declared_semantics(domain), + objective_outcome_coverage(domain), + objective_tamper(domain), + objective_no_self_grading(domain), + objective_provenance(domain), + ] + return { + "id": domain["id"], + "problem_family": domain["problem_family"], + "grammar": domain["grammar"], + "semantics": domain["semantics"], + "source": domain.get("source", ""), + "cases": cases, + "properties": properties, + "ok": all(c["ok"] for c in cases) and all(p["met"] for p in properties), + } + + +def run_coverage(domains: list[dict]) -> dict: + """Nothing the kernel declares may go unexercised.""" + families = {d["problem_family"] for d in domains} + grammars = {d["grammar"] for d in domains} + semantics = {d["semantics"] for d in domains} + objectives = [] + for label, declared, covered in ( + ("problem_family", set(PROBLEM_FAMILIES), families), + ("grammar", set(GRAMMARS), grammars), + ("semantics", set(SEMANTICS.values()), semantics), + ): + missing = sorted(declared - covered) + if missing: + objectives.append( + fail( + f"{label}_coverage", + f"declared in realize.verdicts but no domain covers {missing}", + ) + ) + else: + objectives.append(meet(f"{label}_coverage", f"{len(covered)} of {len(declared)}")) + stray = sorted(grammars - set(GRAMMARS)) + sorted(families - set(PROBLEM_FAMILIES)) + if stray: + objectives.append(fail("no_stray_domains", f"matrix declares unknown {stray}")) + else: + objectives.append(meet("no_stray_domains", "every domain names a known family and grammar")) + return { + "problem_families": sorted(families), + "grammars": sorted(grammars), + "semantics": sorted(semantics), + "objectives": objectives, + "ok": all(o["met"] for o in objectives), + } + + +# ---------------------------------------------------------------- lean layer + + +def python_facts() -> dict[str, str]: + """The same finite questions, answered by the Python kernel. + + Lean answers them in `vv/lean/`. The two are compared in `run_lean`; a proof + nobody compares to anything corroborates nothing. + """ + from realize.compose import eval_ops, goal_y + from realize.formula import all_coeffs, valid_tuples + from realize.kernel import adequate, fibres, lookup_R + from realize.series import classify, syntactic_count + + def halves(tuples) -> str: + """Coefficient tuples as whole numbers of halves, matching the Lean encoding.""" + return ";".join(",".join(str(int(2 * v)) for v in c) for c in tuples) + + def joined(values) -> str: + """Comma-joined, matching how the Lean side prints a list.""" + return ",".join(str(v) for v in values) + + out: dict[str, str] = { + "formula.template_card": str(len(all_coeffs())), + "formula.affine_card": str(len(all_coeffs(affine_only=True))), + "formula.affine_larger_count": str(len(valid_tuples("larger", affine_only=True))), + } + for phrase in ("larger", "smaller", "midpoint", "absdiff"): + solutions = valid_tuples(phrase) + out[f"formula.{phrase}_count"] = str(len(solutions)) + out[f"formula.{phrase}_solution"] = halves(solutions) + + odd = ["add1", "add3", "double"] + even = ["add2", "double"] + seven = classify(odd, 0, 8, 7, 4) + out["series.syntactic_121"] = str(syntactic_count(3, 4)) + out["series.syntactic_31"] = str(syntactic_count(2, 4)) + out["series.seven_valid"] = str(seven["n_valid"]) + out["series.seven_min_len"] = str(seven["min_len"]) + out["series.witness"] = joined(seven["min_seqs"][0]) if seven["min_seqs"] else "" + out["series.even_valid"] = str(classify(even, 0, 8, 7, 4)["n_valid"]) + out["series.nine_valid"] = str(classify(odd, 0, 8, 9, 4)["n_valid"]) + + R = {"0": [0, 1], "1": [1, 2], "2": [0, 2]} + dom = [0, 1, 2] + collapse = {"id": "collapse_all", "map": {"0": "z", "1": "z", "2": "z"}} + separate = {"id": "separate_all", "map": {"0": "a", "1": "b", "2": "c"}} + out["encoder.collapse_adequate"] = str(adequate(R, collapse, dom)[0]).lower() + out["encoder.separate_adequate"] = str(adequate(R, separate, dom)[0]).lower() + out["encoder.collapse_fibre"] = joined(fibres(collapse, dom)["z"]) + triple = lookup_R(R, 0) & lookup_R(R, 1) & lookup_R(R, 2) + out["encoder.obstruction"] = joined(sorted(triple)) + for a, b in ((0, 1), (1, 2), (0, 2)): + out[f"encoder.pair_{a}{b}"] = joined(sorted(lookup_R(R, a) & lookup_R(R, b))) + + grid = [[0, 3, 0], [4, 4, 0], [0, 0, 5]] + recolored = eval_ops(["Extract", "Render2"], grid) + out["grid.recolor_meets_R"] = str(recolored["Y"] == goal_y(grid)).lower() + out["grid.empty_series_meets_R"] = str(grid == goal_y(grid)).lower() + + def hist(g) -> str: + """Colour counts across the ten-symbol palette, in palette order.""" + flat = [v for row in g for v in row] + return joined(flat.count(v) for v in range(10)) + + out["grid.hist_input"] = hist(grid) + out["grid.hist_goal"] = hist(goal_y(grid)) + return out + + +def compare_facts(reported: dict[str, str], repeated: list[str]) -> dict: + """Two implementations, one set of questions. Every fact must be compared. + + A fact reported twice is a failure even when both copies agree: the second + would overwrite the first, so one file could quietly supply the value another + file got wrong. + """ + expected = python_facts() + disagreements = [ + {"fact": k, "lean": reported.get(k), "python": v} + for k, v in sorted(expected.items()) + if reported.get(k) != v + ] + unclaimed = sorted(set(reported) - set(expected)) + disagreements += [{"fact": k, "lean": reported[k], "python": None} for k in unclaimed] + disagreements += [ + {"fact": k, "lean": "reported more than once", "python": expected.get(k)} + for k in sorted(set(repeated)) + ] + return { + "ok": not disagreements, + "compared": len(expected), + "disagreements": disagreements, + } + + +def run_lean(require: bool) -> dict: + """Optional independent corroboration. Lean agrees or disagrees; it never grades.""" + lean_dir = ROOT / "vv" / "lean" + files = sorted(lean_dir.glob("*.lean")) + binary = None + for candidate in (Path.home() / ".elan" / "bin" / "lean", Path("/usr/local/bin/lean")): + if candidate.is_file(): + binary = str(candidate) + break + if binary is None: + from shutil import which + + binary = which("lean") + if binary is None or not files: + detail = "lean is not installed" if binary is None else "no .lean files found" + return { + "status": "unavailable" if require else "skipped", + "ok": not require, + "detail": detail, + "files": [], + } + results = [] + for path in files: + source = path.read_text(encoding="utf-8") + banned = [why for pattern, why in LEAN_FORBIDDEN if pattern.search(source)] + if banned: + results.append( + { + "file": str(path.relative_to(ROOT)), + "ok": False, + "exit": None, + "output": f"refused before checking: file uses {', '.join(banned)}", + } + ) + continue + proc = subprocess.run( + [binary, str(path)], capture_output=True, text=True, cwd=lean_dir, check=False + ) + output = (proc.stdout + proc.stderr).strip() + noise = [ln for ln in output.splitlines() if not ln.startswith("fact ")] + # Lean warns on `sorry` but still exits 0, so a clean exit is not enough. + clean = proc.returncode == 0 and not noise + results.append( + { + "file": str(path.relative_to(ROOT)), + "ok": clean, + "exit": proc.returncode, + "output": output[:2000], + } + ) + reported: dict[str, str] = {} + repeated: list[str] = [] + for row in results: + for match in re.finditer(r"^fact ([\w.]+)=(.*)$", row["output"], re.MULTILINE): + name = match.group(1) + if name in reported: + repeated.append(name) + reported[name] = match.group(2) + cross = compare_facts(reported, repeated) + return { + "status": "checked", + "ok": all(r["ok"] for r in results) and cross["ok"], + "detail": "Lean corroborates the finite facts. It does not certify the Python kernel.", + "files": results, + "cross_check": cross, + } + + +# ---------------------------------------------------------------- reporting + + +def render(report: dict) -> str: + """Lay the report out for whoever is reading CI output, failures indented under their case.""" + lines = [] + cov = report["coverage"] + lines.append("coverage") + for obj in cov["objectives"]: + lines.append(f" [{'ok' if obj['met'] else 'XX'}] {obj['objective']}: {obj['detail']}") + for domain in report["domains"]: + lines.append("") + lines.append(f"{domain['id']} ({domain['source']})") + for case in domain["cases"]: + mark = "ok" if case["ok"] else "XX" + observed = f"{case['observed']['outcome']}/{case['observed']['exit']}" + lines.append(f" [{mark}] {case['id']:<32} {case['entry']:<8} {observed}") + for obj in case["objectives"]: + if not obj["met"]: + lines.append(f" -> {obj['objective']}: {obj['detail']}") + for prop in domain["properties"]: + mark = "ok" if prop["met"] else "XX" + lines.append(f" [{mark}] {prop['objective']:<32} {prop['detail']}") + lean = report.get("lean") + if lean: + lines.append("") + lines.append(f"lean ({lean['status']}): {lean['detail']}") + for row in lean["files"]: + lines.append(f" [{'ok' if row['ok'] else 'XX'}] {row['file']}") + if not row["ok"]: + lines.append(f" -> {row['output'][:500]}") + cross = lean.get("cross_check") + if cross: + mark = "ok" if cross["ok"] else "XX" + lines.append( + f" [{mark}] {'cross_check':<32} " + f"{cross['compared']} facts compared against the Python kernel" + ) + for row in cross["disagreements"]: + lines.append( + f" -> {row['fact']}: lean {row['lean']!r} vs python {row['python']!r}" + ) + lines.append("") + lines.append("V&V objectives met" if report["ok"] else "V&V objectives NOT met") + return "\n".join(lines) + + +def main(argv: list[str] | None = None) -> int: + """Run the matrix, write the report, and return 0 (all objectives met) or 1.""" + parser = argparse.ArgumentParser( + prog="vv", + description="Run the realize verification & validation matrix across declared domains.", + ) + parser.add_argument("--config", default=str(ROOT / "vv" / "domains.json")) + parser.add_argument("--domain", action="append", default=None, help="run only these domain ids") + parser.add_argument("--report", default=None, help="write the full report JSON here") + parser.add_argument("--lean", action="store_true", help="also run the Lean corroboration") + parser.add_argument( + "--lean-required", + action="store_true", + help="fail instead of skipping when Lean is not installed", + ) + args = parser.parse_args(argv) + + config = json.loads(Path(args.config).read_text(encoding="utf-8")) + if config.get("schema_version") != CONFIG_VERSION: + sys.stderr.write(f"vv: unsupported config version {config.get('schema_version')!r}\n") + return 1 + domains = config["domains"] + if args.domain: + domains = [d for d in domains if d["id"] in set(args.domain)] + if not domains: + sys.stderr.write(f"vv: no domain matches {args.domain}\n") + return 1 + + coverage = run_coverage(config["domains"]) + results = [run_domain(d) for d in domains] + lean: dict[str, Any] | None = None + if args.lean or args.lean_required: + lean = run_lean(require=args.lean_required) + + report = { + "schema_version": CONFIG_VERSION, + "generated_by": "scripts/vv.py", + "realize_version": __version__, + "note": "This report records observations. It is not a certificate and it is not a verdict.", + "coverage": coverage, + "domains": results, + "lean": lean, + "ok": coverage["ok"] and all(d["ok"] for d in results) and (lean is None or lean["ok"]), + } + if args.report: + out = Path(args.report) + out.parent.mkdir(parents=True, exist_ok=True) + out.write_text(json.dumps(report, indent=2, sort_keys=True) + "\n", encoding="utf-8") + sys.stderr.write(render(report) + "\n") + return 0 if report["ok"] else 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tests/test_vv.py b/tests/test_vv.py new file mode 100644 index 0000000..cdd44c5 --- /dev/null +++ b/tests/test_vv.py @@ -0,0 +1,65 @@ +"""The V&V matrix under pytest. Do not relax an objective to make this green. + +The Lean corroboration is deliberately not run here: it needs a toolchain that +`pip install -e ".[dev]"` does not provide. CI runs it as its own job. +""" + +import importlib.util +import json +from pathlib import Path + +import pytest + +ROOT = Path(__file__).resolve().parents[1] + + +def _load_runner(): + """Import `scripts/vv.py` by path. + + The repo has both `scripts/vv.py` and a `vv/` data directory, so a plain + `import vv` would be free to pick the wrong one. + """ + spec = importlib.util.spec_from_file_location("realize_vv", ROOT / "scripts" / "vv.py") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +vv = _load_runner() +CONFIG = json.loads((ROOT / "vv" / "domains.json").read_text(encoding="utf-8")) +DOMAINS = CONFIG["domains"] +IDS = [d["id"] for d in DOMAINS] + + +def test_config_version_is_supported(): + """The matrix must declare a config version this runner accepts.""" + assert CONFIG["schema_version"] == vv.CONFIG_VERSION + + +def test_every_declared_domain_is_covered(): + """A grammar added to realize.verdicts must arrive with a domain that exercises it.""" + result = vv.run_coverage(DOMAINS) + unmet = [f"{o['objective']}: {o['detail']}" for o in result["objectives"] if not o["met"]] + assert not unmet, unmet + + +@pytest.mark.parametrize("domain", DOMAINS, ids=IDS) +def test_domain_meets_its_objectives(domain): + """Every per-case objective and every per-domain property, for one domain.""" + result = vv.run_domain(domain) + unmet = [] + for case in result["cases"]: + unmet += [ + f"{case['id']}: {o['objective']}: {o['detail']}" + for o in case["objectives"] + if not o["met"] + ] + unmet += [f"{p['objective']}: {p['detail']}" for p in result["properties"] if not p["met"]] + assert not unmet, unmet + + +@pytest.mark.parametrize("domain", DOMAINS, ids=IDS) +def test_domain_reaches_all_four_verdicts_and_the_adapter(domain): + """Four verdicts plus adapter reject, in every domain. No domain gets a pass on one.""" + reached = {c["expect"]["outcome"] for c in domain["cases"]} + assert reached >= vv.OUTCOMES, sorted(vv.OUTCOMES - reached) diff --git a/vv/README.md b/vv/README.md new file mode 100644 index 0000000..b34ebbd --- /dev/null +++ b/vv/README.md @@ -0,0 +1,44 @@ +# vv/ — the verification & validation matrix + +This directory is **not** the checker. It cannot mint `PASS`. + +It declares what every domain must be observed to do, and holds the specs and candidates that make +each domain reachable from the command line. The prose is in [../VV.md](../VV.md). + +``` +domains.json the matrix: four domains, their cases, their expected outcomes +specs/ specs the demos do not already ship +candidates/ candidates bound by digest to those specs +lean/ independent corroboration of the same finite facts +``` + +## Run + +```bash +python3 ../scripts/vv.py # from here, or scripts/vv.py from the repo root +``` + +## Adding a domain + +A domain is a `problem_family` paired with a `grammar`. Add one when the kernel learns a new +grammar — `grammar_coverage` will fail until you do. + +1. Add the grammar to `GRAMMARS` in `src/realize/verdicts.py` and to `schema/realize.v0.json`. +2. Add a domain entry to `domains.json` with cases reaching all five outcomes: `PASS`, + `COUNTEREXAMPLE`, `UNSAT`, `UNKNOWN`, adapter reject. `outcome_coverage` will fail until you do. +3. Write the specs under `specs/` with `provenance` for every clause that constrains. +4. Write the candidates under `candidates/`, each carrying the spec's digest. +5. Add a Lean file under `lean/` re-stating that domain's finite facts. + +## Editing a spec + +A candidate is bound to its spec by `spec_digest`. Editing a spec therefore breaks its candidates, +and `realize check` will refuse them with `adapter: spec_digest mismatch`. That is the binding +working, not a bug. + +There is deliberately no `--restamp` flag. Re-author the candidate with the new digest, on purpose: + +```bash +PYTHONPATH=src python3 -c "import json,sys; from realize.spec import load_spec; \ + from realize.digest import sha256_hex; print(sha256_hex(load_spec(sys.argv[1])))" vv/specs/your.spec.json +``` diff --git a/vv/candidates/encoder_separating.counterexample.json b/vv/candidates/encoder_separating.counterexample.json new file mode 100644 index 0000000..e5c32fe --- /dev/null +++ b/vv/candidates/encoder_separating.counterexample.json @@ -0,0 +1,14 @@ +{ + "schema_version": "realize.v0", + "spec_id": "vv.encoder.separating", + "spec_digest": "sha256:81ca6e1eb763ed82d74a6e0cb13843423d6d772fdbfe691309f876dc51753e05", + "term": { + "kind": "case_table", + "encoder_id": "separate_all", + "table": { + "a": 2, + "b": 1, + "c": 0 + } + } +} diff --git a/vv/candidates/encoder_separating.digest_mismatch.json b/vv/candidates/encoder_separating.digest_mismatch.json new file mode 100644 index 0000000..cb6a411 --- /dev/null +++ b/vv/candidates/encoder_separating.digest_mismatch.json @@ -0,0 +1,14 @@ +{ + "schema_version": "realize.v0", + "spec_id": "vv.encoder.separating", + "spec_digest": "sha256:0000000000000000000000000000000000000000000000000000000000000000", + "term": { + "kind": "case_table", + "encoder_id": "separate_all", + "table": { + "a": 0, + "b": 1, + "c": 0 + } + } +} diff --git a/vv/candidates/encoder_separating.pass.json b/vv/candidates/encoder_separating.pass.json new file mode 100644 index 0000000..b60e100 --- /dev/null +++ b/vv/candidates/encoder_separating.pass.json @@ -0,0 +1,14 @@ +{ + "schema_version": "realize.v0", + "spec_id": "vv.encoder.separating", + "spec_digest": "sha256:81ca6e1eb763ed82d74a6e0cb13843423d6d772fdbfe691309f876dc51753e05", + "term": { + "kind": "case_table", + "encoder_id": "separate_all", + "table": { + "a": 0, + "b": 1, + "c": 0 + } + } +} diff --git a/vv/candidates/formula_larger.counterexample.json b/vv/candidates/formula_larger.counterexample.json new file mode 100644 index 0000000..b60f816 --- /dev/null +++ b/vv/candidates/formula_larger.counterexample.json @@ -0,0 +1,14 @@ +{ + "schema_version": "realize.v0", + "spec_id": "vcos.table2.larger", + "spec_digest": "sha256:d291e0472f4469adcedccbecf8537c3008d7da423422befd1df15524661fb350", + "term": { + "kind": "formula", + "coeffs": [ + "0", + "1/2", + "1/2", + "-1/2" + ] + } +} diff --git a/vv/candidates/formula_larger.digest_mismatch.json b/vv/candidates/formula_larger.digest_mismatch.json new file mode 100644 index 0000000..21c4288 --- /dev/null +++ b/vv/candidates/formula_larger.digest_mismatch.json @@ -0,0 +1,14 @@ +{ + "schema_version": "realize.v0", + "spec_id": "vcos.table2.larger", + "spec_digest": "sha256:0000000000000000000000000000000000000000000000000000000000000000", + "term": { + "kind": "formula", + "coeffs": [ + "0", + "1/2", + "1/2", + "1/2" + ] + } +} diff --git a/vv/candidates/formula_larger.pass.json b/vv/candidates/formula_larger.pass.json new file mode 100644 index 0000000..36d7059 --- /dev/null +++ b/vv/candidates/formula_larger.pass.json @@ -0,0 +1,14 @@ +{ + "schema_version": "realize.v0", + "spec_id": "vcos.table2.larger", + "spec_digest": "sha256:d291e0472f4469adcedccbecf8537c3008d7da423422befd1df15524661fb350", + "term": { + "kind": "formula", + "coeffs": [ + "0", + "1/2", + "1/2", + "1/2" + ] + } +} diff --git a/vv/candidates/grid_recolor.counterexample.json b/vv/candidates/grid_recolor.counterexample.json new file mode 100644 index 0000000..43a20b9 --- /dev/null +++ b/vv/candidates/grid_recolor.counterexample.json @@ -0,0 +1,9 @@ +{ + "schema_version": "realize.v0", + "spec_id": "igvf.grid_recolor", + "spec_digest": "sha256:15aa99731c759af10e420753981adea770108ca05eac57a8c08f3b2332b4578b", + "term": { + "kind": "sequence", + "ops": [] + } +} diff --git a/vv/candidates/grid_recolor.digest_mismatch.json b/vv/candidates/grid_recolor.digest_mismatch.json new file mode 100644 index 0000000..eabcb60 --- /dev/null +++ b/vv/candidates/grid_recolor.digest_mismatch.json @@ -0,0 +1,12 @@ +{ + "schema_version": "realize.v0", + "spec_id": "igvf.grid_recolor", + "spec_digest": "sha256:0000000000000000000000000000000000000000000000000000000000000000", + "term": { + "kind": "sequence", + "ops": [ + "Extract", + "Render2" + ] + } +} diff --git a/vv/candidates/grid_recolor.pass.json b/vv/candidates/grid_recolor.pass.json new file mode 100644 index 0000000..442739b --- /dev/null +++ b/vv/candidates/grid_recolor.pass.json @@ -0,0 +1,12 @@ +{ + "schema_version": "realize.v0", + "spec_id": "igvf.grid_recolor", + "spec_digest": "sha256:15aa99731c759af10e420753981adea770108ca05eac57a8c08f3b2332b4578b", + "term": { + "kind": "sequence", + "ops": [ + "Extract", + "Render2" + ] + } +} diff --git a/vv/candidates/series_seven.counterexample.json b/vv/candidates/series_seven.counterexample.json new file mode 100644 index 0000000..01fa355 --- /dev/null +++ b/vv/candidates/series_seven.counterexample.json @@ -0,0 +1,13 @@ +{ + "schema_version": "realize.v0", + "spec_id": "vcos.series.seven", + "spec_digest": "sha256:02d15e3731ea4a971c8446a7dc32d679ea9bf788b68eb252908e6285cc5d4ec1", + "term": { + "kind": "sequence", + "ops": [ + "add3", + "double", + "double" + ] + } +} diff --git a/vv/candidates/series_seven.digest_mismatch.json b/vv/candidates/series_seven.digest_mismatch.json new file mode 100644 index 0000000..4bfb72f --- /dev/null +++ b/vv/candidates/series_seven.digest_mismatch.json @@ -0,0 +1,13 @@ +{ + "schema_version": "realize.v0", + "spec_id": "vcos.series.seven", + "spec_digest": "sha256:0000000000000000000000000000000000000000000000000000000000000000", + "term": { + "kind": "sequence", + "ops": [ + "add3", + "double", + "add1" + ] + } +} diff --git a/vv/candidates/series_seven.pass.json b/vv/candidates/series_seven.pass.json new file mode 100644 index 0000000..d35b418 --- /dev/null +++ b/vv/candidates/series_seven.pass.json @@ -0,0 +1,13 @@ +{ + "schema_version": "realize.v0", + "spec_id": "vcos.series.seven", + "spec_digest": "sha256:02d15e3731ea4a971c8446a7dc32d679ea9bf788b68eb252908e6285cc5d4ec1", + "term": { + "kind": "sequence", + "ops": [ + "add3", + "double", + "add1" + ] + } +} diff --git a/vv/domains.json b/vv/domains.json new file mode 100644 index 0000000..a7368a3 --- /dev/null +++ b/vv/domains.json @@ -0,0 +1,202 @@ +{ + "schema_version": "realize.vv.v0", + "note": "Verification & validation matrix. Dev-only. This file cannot mint a verdict; it only declares what each domain must be observed to do. See VV.md.", + "domains": [ + { + "id": "formula.bounded_coeff_template", + "problem_family": "formula", + "grammar": "bounded_coeff_template", + "semantics": "exact_rational", + "source": "VCOS §8.1 / Table 2", + "cases": [ + { + "id": "larger.pass", + "entry": "cli", + "spec": "demos/max_formula/spec.json", + "candidate": "vv/candidates/formula_larger.pass.json", + "expect": {"outcome": "PASS", "exit": 0}, + "why": "(0, 1/2, 1/2, 1/2) meets the target affine form on both half-planes" + }, + { + "id": "larger.counterexample", + "entry": "cli", + "spec": "demos/max_formula/spec.json", + "candidate": "vv/candidates/formula_larger.counterexample.json", + "expect": {"outcome": "COUNTEREXAMPLE", "exit": 2}, + "why": "the tuple for 'smaller' does not realize 'larger'" + }, + { + "id": "affine_only.unsat", + "entry": "library", + "spec": "vv/specs/formula_affine_only.spec.json", + "expect": {"outcome": "UNSAT", "exit": 3}, + "why": "no affine tuple realizes 'larger'; the declared class is empty at this grammar" + }, + { + "id": "unrecognized_phrase.unknown", + "entry": "library", + "spec": "vv/specs/formula_unrecognized_phrase.spec.json", + "expect": {"outcome": "UNKNOWN", "exit": 4}, + "why": "no R is invented from English; NONCLAIMS §1" + }, + { + "id": "digest_mismatch.adapter", + "entry": "cli", + "spec": "demos/max_formula/spec.json", + "candidate": "vv/candidates/formula_larger.digest_mismatch.json", + "expect": {"outcome": "adapter", "exit": 1}, + "why": "a candidate bound to a different spec is refused, not judged" + } + ] + }, + { + "id": "encoder.finite_case_table", + "problem_family": "encoder", + "grammar": "finite_case_table", + "semantics": "finite_relation", + "source": "VCMS Example 4.3", + "cases": [ + { + "id": "separating.pass", + "entry": "cli", + "spec": "vv/specs/encoder_separating.spec.json", + "candidate": "vv/candidates/encoder_separating.pass.json", + "expect": {"outcome": "PASS", "exit": 0}, + "why": "every fibre is a singleton, so the decoder can honour each acceptable set" + }, + { + "id": "separating.counterexample", + "entry": "cli", + "spec": "vv/specs/encoder_separating.spec.json", + "candidate": "vv/candidates/encoder_separating.counterexample.json", + "expect": {"outcome": "COUNTEREXAMPLE", "exit": 2}, + "why": "row a emits 2, which is outside A(0) = {0, 1}" + }, + { + "id": "three_state.unsat", + "entry": "cli", + "spec": "demos/three_state/spec.json", + "candidate": "demos/three_state/candidate.json", + "expect": {"outcome": "UNSAT", "exit": 3}, + "why": "one fibre carries all three inputs and their acceptable sets meet in the empty set" + }, + { + "id": "zero_budget.unknown", + "entry": "library", + "spec": "vv/specs/encoder_zero_budget.spec.json", + "expect": {"outcome": "UNKNOWN", "exit": 4}, + "why": "zero budget is UNKNOWN, never UNSAT; NONCLAIMS §2" + }, + { + "id": "digest_mismatch.adapter", + "entry": "cli", + "spec": "vv/specs/encoder_separating.spec.json", + "candidate": "vv/candidates/encoder_separating.digest_mismatch.json", + "expect": {"outcome": "adapter", "exit": 1}, + "why": "a candidate bound to a different spec is refused, not judged" + } + ] + }, + { + "id": "term_series.typed_grid", + "problem_family": "term_series", + "grammar": "typed_grid", + "semantics": "finite_integer", + "source": "IGVF-CTS §7.1", + "cases": [ + { + "id": "recolor.pass", + "entry": "cli", + "spec": "demos/grid_recolor/spec.json", + "candidate": "vv/candidates/grid_recolor.pass.json", + "expect": {"outcome": "PASS", "exit": 0}, + "why": "Extract then Render2 is well-typed Grid to Grid and meets R" + }, + { + "id": "empty_series.counterexample", + "entry": "cli", + "spec": "demos/grid_recolor/spec.json", + "candidate": "vv/candidates/grid_recolor.counterexample.json", + "expect": {"outcome": "COUNTEREXAMPLE", "exit": 2}, + "why": "the empty series is well-typed but leaves the grid uncoloured" + }, + { + "id": "preserve_histogram.unsat", + "entry": "library", + "spec": "vv/specs/grid_preserve_histogram.spec.json", + "expect": {"outcome": "UNSAT", "exit": 3}, + "why": "K asks the colour counts to be kept and R asks them to change" + }, + { + "id": "zero_budget.unknown", + "entry": "library", + "spec": "vv/specs/grid_zero_budget.spec.json", + "expect": {"outcome": "UNKNOWN", "exit": 4}, + "why": "zero budget is UNKNOWN, never UNSAT; NONCLAIMS §2" + }, + { + "id": "digest_mismatch.adapter", + "entry": "cli", + "spec": "demos/grid_recolor/spec.json", + "candidate": "vv/candidates/grid_recolor.digest_mismatch.json", + "expect": {"outcome": "adapter", "exit": 1}, + "why": "a candidate bound to a different spec is refused, not judged" + } + ] + }, + { + "id": "term_series.guarded_integer_sequence", + "problem_family": "term_series", + "grammar": "guarded_integer_sequence", + "semantics": "finite_integer", + "source": "VCOS §8.3", + "cases": [ + { + "id": "seven.pass", + "entry": "cli", + "spec": "vv/specs/series_seven.spec.json", + "candidate": "vv/candidates/series_seven.pass.json", + "expect": {"outcome": "PASS", "exit": 0}, + "why": "add3, double, add1 walks 0 to 3 to 6 to 7 and never leaves [0, 8]" + }, + { + "id": "seven.counterexample", + "entry": "cli", + "spec": "vv/specs/series_seven.spec.json", + "candidate": "vv/candidates/series_seven.counterexample.json", + "expect": {"outcome": "COUNTEREXAMPLE", "exit": 2}, + "why": "the third step would take the state to 12, outside the guard" + }, + { + "id": "even_repertoire.unsat", + "entry": "library", + "spec": "vv/specs/series_even_repertoire.spec.json", + "expect": {"outcome": "UNSAT", "exit": 3}, + "why": "add2 and double keep the state even, so an odd target is unreachable" + }, + { + "id": "target_nine.unsat", + "entry": "library", + "spec": "vv/specs/series_target_nine.spec.json", + "expect": {"outcome": "UNSAT", "exit": 3}, + "why": "the target is above the cap, so the guard rules it out before search" + }, + { + "id": "zero_budget.unknown", + "entry": "library", + "spec": "vv/specs/series_zero_budget.spec.json", + "expect": {"outcome": "UNKNOWN", "exit": 4}, + "why": "zero budget is UNKNOWN, never UNSAT; NONCLAIMS §2" + }, + { + "id": "digest_mismatch.adapter", + "entry": "cli", + "spec": "vv/specs/series_seven.spec.json", + "candidate": "vv/candidates/series_seven.digest_mismatch.json", + "expect": {"outcome": "adapter", "exit": 1}, + "why": "a candidate bound to a different spec is refused, not judged" + } + ] + } + ] +} diff --git a/vv/lean/Encoder.lean b/vv/lean/Encoder.lean new file mode 100644 index 0000000..3b09331 --- /dev/null +++ b/vv/lean/Encoder.lean @@ -0,0 +1,90 @@ +/- + Cross-check for the `encoder.finite_case_table` domain (VCMS Example 4.3). + + Lean agrees or disagrees with the finite facts the Python kernel reports. + It does not certify the Python kernel, and it cannot mint a verdict. +-/ + +namespace Realize.Encoder + +set_option maxRecDepth 4000 + +/-- The acceptable set A(x) for each input. Empty outside the declared domain. -/ +def A : Nat → List Nat + | 0 => [0, 1] + | 1 => [1, 2] + | 2 => [0, 2] + | _ => [] + +def dom : List Nat := [0, 1, 2] + +def inter (a b : List Nat) : List Nat := a.filter (fun x => b.contains x) + +def interAll : List (List Nat) → List Nat + | [] => [] + | [s] => s + | s :: rest => inter s (interAll rest) + +/-- Every input lands on one code: the encoder of the `three_state` demo. -/ +def collapseAll (_ : Nat) : Nat := 0 + +/-- Every input keeps its own code. -/ +def separateAll (x : Nat) : Nat := x + +def fibre (e : Nat → Nat) (code : Nat) : List Nat := dom.filter (fun x => e x == code) + +def codes (e : Nat → Nat) : List Nat := (dom.map e).eraseDups + +/-- Adequate: no fibre asks for two things at once. -/ +def adequate (e : Nat → Nat) : Bool := + (codes e).all (fun c => !(interAll ((fibre e c).map A)).isEmpty) + +/-! ## The UNSAT the checker reports for `three_state` -/ + +theorem collapse_one_fibre : fibre collapseAll 0 = [0, 1, 2] := by decide +theorem collapse_obstructed : interAll ((fibre collapseAll 0).map A) = [] := by decide +theorem collapse_inadequate : adequate collapseAll = false := by decide + +/-! ## The obstruction is three-wise, not pairwise — this is why it is interesting -/ + +theorem pair_01 : inter (A 0) (A 1) = [1] := by decide +theorem pair_12 : inter (A 1) (A 2) = [2] := by decide +theorem pair_02 : inter (A 0) (A 2) = [0] := by decide + +/-! ## The PASS the checker reports for the separating encoder -/ + +theorem separate_adequate : adequate separateAll = true := by decide + +/-- The decoder table in `vv/candidates/encoder_separating.pass.json`. -/ +def decoder : Nat → Nat + | 0 => 0 + | 1 => 1 + | 2 => 0 + | _ => 0 + +theorem decoder_sound : + dom.all (fun x => (A x).contains (decoder (separateAll x))) = true := by decide + +/-- The COUNTEREXAMPLE table: row `a` emits 2, which A(0) does not accept. -/ +def badDecoder : Nat → Nat + | 0 => 2 + | 1 => 1 + | 2 => 0 + | _ => 0 + +theorem bad_decoder_violates : + dom.all (fun x => (A x).contains (badDecoder (separateAll x))) = false := by decide + +/-! ## Facts reported back to `scripts/vv.py`, which compares them against the Python kernel. -/ + +def showList (l : List Nat) : String := String.intercalate "," (l.map toString) + +#eval IO.println s!"fact encoder.collapse_adequate={adequate collapseAll}" +#eval IO.println s!"fact encoder.separate_adequate={adequate separateAll}" +#eval IO.println s!"fact encoder.collapse_fibre={showList (fibre collapseAll 0)}" +#eval IO.println s!"fact encoder.obstruction={showList (interAll ((fibre collapseAll 0).map A))}" +#eval IO.println s!"fact encoder.pair_01={showList (inter (A 0) (A 1))}" +#eval IO.println s!"fact encoder.pair_12={showList (inter (A 1) (A 2))}" +#eval IO.println s!"fact encoder.pair_02={showList (inter (A 0) (A 2))}" + +end Realize.Encoder diff --git a/vv/lean/Formula.lean b/vv/lean/Formula.lean new file mode 100644 index 0000000..cf9f39f --- /dev/null +++ b/vv/lean/Formula.lean @@ -0,0 +1,97 @@ +/- + Cross-check for the `formula.bounded_coeff_template` domain (VCOS §8.1 / Table 2). + + Lean agrees or disagrees with the finite facts the Python kernel reports. + It does not certify the Python kernel, and it cannot mint a verdict. + + Every coefficient in D = {-1, -1/2, 0, 1/2, 1} is a whole number of halves, so + the template is carried here in halves: `h` stands for the value `h/2`. That + keeps the arithmetic exact in core Lean, with no rational type and no Mathlib. +-/ + +namespace Realize.Formula + +-- the template has 625 members; kernel reduction walks the whole list +set_option maxRecDepth 8000 + +/-- Twice a coefficient. `D` is {-1, -1/2, 0, 1/2, 1} doubled. -/ +abbrev Half := Int + +def D : List Half := [-2, -1, 0, 1, 2] + +structure Coeffs where + h0 : Half + h1 : Half + h2 : Half + h3 : Half +deriving DecidableEq, Repr, BEq + +/-- The declared finite class: every tuple the bounded template can name. -/ +def template : List Coeffs := + D.flatMap fun a => D.flatMap fun b => D.flatMap fun c => D.map fun d => ⟨a, b, c, d⟩ + +inductive Phrase where + | larger | smaller | midpoint | absdiff +deriving DecidableEq, Repr + +/-- `c0 + c1·a + c2·b + c3·|a-b|` restricted to a ≥ b, as an affine form in (1, a, b). -/ +def planeA (c : Coeffs) : Half × Half × Half := (c.h0, c.h1 + c.h3, c.h2 - c.h3) + +/-- The same form restricted to b ≥ a. -/ +def planeB (c : Coeffs) : Half × Half × Half := (c.h0, c.h1 - c.h3, c.h2 + c.h3) + +def targetA : Phrase → Half × Half × Half + | .larger => (0, 2, 0) + | .smaller => (0, 0, 2) + | .midpoint => (0, 1, 1) + | .absdiff => (0, 2, -2) + +def targetB : Phrase → Half × Half × Half + | .larger => (0, 0, 2) + | .smaller => (0, 2, 0) + | .midpoint => (0, 1, 1) + | .absdiff => (0, -2, 2) + +def realizes (c : Coeffs) (p : Phrase) : Bool := + planeA c == targetA p && planeB c == targetB p + +def solutions (p : Phrase) : List Coeffs := template.filter (realizes · p) + +/-- The affine sub-template: the |a-b| leg is not available. -/ +def affine : List Coeffs := template.filter (fun c => c.h3 == 0) + +/-! ## Counts the Python side freezes in tests/test_counts.py -/ + +theorem template_card : template.length = 625 := by decide +theorem affine_card : affine.length = 125 := by decide + +/-! ## Each phrase is realized by exactly one tuple, and it is the reported one -/ + +theorem larger_unique : solutions .larger = [⟨0, 1, 1, 1⟩] := by decide +theorem smaller_unique : solutions .smaller = [⟨0, 1, 1, -1⟩] := by decide +theorem midpoint_unique : solutions .midpoint = [⟨0, 1, 1, 0⟩] := by decide +theorem absdiff_unique : solutions .absdiff = [⟨0, 0, 0, 2⟩] := by decide + +/-! ## The UNSAT the checker reports for the affine-only spec -/ + +theorem affine_larger_empty : affine.filter (realizes · .larger) = [] := by decide + +/-! ## Facts reported back to `scripts/vv.py`, which compares them against the Python kernel. + A proof nobody compares to anything corroborates nothing. -/ + +def showHalves (cs : List Coeffs) : String := + String.intercalate ";" (cs.map fun c => s!"{c.h0},{c.h1},{c.h2},{c.h3}") + +#eval IO.println s!"fact formula.template_card={template.length}" +#eval IO.println s!"fact formula.affine_card={affine.length}" +#eval IO.println s!"fact formula.larger_count={(solutions .larger).length}" +#eval IO.println s!"fact formula.smaller_count={(solutions .smaller).length}" +#eval IO.println s!"fact formula.midpoint_count={(solutions .midpoint).length}" +#eval IO.println s!"fact formula.absdiff_count={(solutions .absdiff).length}" +#eval IO.println s!"fact formula.affine_larger_count={(affine.filter (realizes · .larger)).length}" +#eval IO.println s!"fact formula.larger_solution={showHalves (solutions .larger)}" +#eval IO.println s!"fact formula.smaller_solution={showHalves (solutions .smaller)}" +#eval IO.println s!"fact formula.midpoint_solution={showHalves (solutions .midpoint)}" +#eval IO.println s!"fact formula.absdiff_solution={showHalves (solutions .absdiff)}" + +end Realize.Formula diff --git a/vv/lean/Grid.lean b/vv/lean/Grid.lean new file mode 100644 index 0000000..5b523cc --- /dev/null +++ b/vv/lean/Grid.lean @@ -0,0 +1,64 @@ +/- + Cross-check for the `term_series.typed_grid` domain (IGVF-CTS §7.1). + + Lean agrees or disagrees with the finite facts the Python kernel reports. + It does not certify the Python kernel, and it cannot mint a verdict. +-/ + +namespace Realize.Grid + +set_option maxRecDepth 4000 + +abbrev Grid := List (List Nat) + +/-- The grid in `demos/grid_recolor/spec.json`. -/ +def X : Grid := [[0, 3, 0], [4, 4, 0], [0, 0, 5]] + +/-- `Extract : Grid → Mask`. -/ +def extract (g : Grid) : Grid := g.map (fun r => r.map (fun v => if v == 0 then 0 else 1)) + +/-- `Render2 : Mask → Grid`. -/ +def render2 (g : Grid) : Grid := g.map (fun r => r.map (fun v => if v == 0 then 0 else 2)) + +/-- What R asks for: every non-background cell becomes colour 2, background stays put. -/ +def goal (g : Grid) : Grid := g.map (fun r => r.map (fun v => if v == 0 then 0 else 2)) + +def cells (g : Grid) : List Nat := g.flatMap id + +def palette : List Nat := [0, 1, 2, 3, 4, 5, 6, 7, 8, 9] + +def histogram (g : Grid) : List (Nat × Nat) := + palette.map (fun v => (v, ((cells g).filter (fun c => c == v)).length)) + +/-! ## The PASS the checker reports for `Extract, Render2` -/ + +theorem recolor_meets_R : render2 (extract X) = goal X := by decide + +/-! ## The COUNTEREXAMPLE the checker reports for the empty series -/ + +theorem empty_series_fails : X ≠ goal X := by decide + +/-! ## The UNSAT: K asks the colour counts to be kept, R asks them to change -/ + +theorem histogram_contradicts_R : histogram X ≠ histogram (goal X) := by decide + +/-- Concretely: three cells change colour, so no series can satisfy both clauses. -/ +theorem histogram_witness : + histogram X = [(0, 5), (1, 0), (2, 0), (3, 1), (4, 2), (5, 1), + (6, 0), (7, 0), (8, 0), (9, 0)] := by decide + +theorem goal_histogram_witness : + histogram (goal X) = [(0, 5), (1, 0), (2, 4), (3, 0), (4, 0), (5, 0), + (6, 0), (7, 0), (8, 0), (9, 0)] := by decide + +/-! ## Facts reported back to `scripts/vv.py`, which compares them against the Python kernel. -/ + +def showHist (g : Grid) : String := + String.intercalate "," ((histogram g).map fun p => toString p.2) + +#eval IO.println s!"fact grid.recolor_meets_R={render2 (extract X) == goal X}" +#eval IO.println s!"fact grid.empty_series_meets_R={X == goal X}" +#eval IO.println s!"fact grid.hist_input={showHist X}" +#eval IO.println s!"fact grid.hist_goal={showHist (goal X)}" + +end Realize.Grid diff --git a/vv/lean/README.md b/vv/lean/README.md new file mode 100644 index 0000000..f9a2c2b --- /dev/null +++ b/vv/lean/README.md @@ -0,0 +1,54 @@ +# vv/lean — independent corroboration + +Four files. Each re-states the finite facts of one domain in Lean 4 and proves them with +kernel-checked `decide`. + +| File | Domain | What it settles | +|---|---|---| +| `Formula.lean` | `formula.bounded_coeff_template` | the template has 625 members; each phrase is realized by exactly one tuple; the affine sub-template is empty for `larger` | +| `Encoder.lean` | `encoder.finite_case_table` | the collapsing encoder's one fibre is obstructed while every pair still meets; the separating encoder is adequate and its decoder is sound | +| `Series.lean` | `term_series.guarded_integer_sequence` | 121 and 31 syntactic series; ten reach 7 and none in under three steps; the even repertoire and the above-cap target are both empty | +| `Grid.lean` | `term_series.typed_grid` | `Extract` then `Render2` meets `R`; the empty series does not; the histogram of the input and of the goal differ | + +## Ground rules + +Core Lean only. No Mathlib, no `lake`, no network at check time. + +**No `native_decide`, no `sorry`, no new `axiom`, no `@[implemented_by]` or `@[extern]`.** +`scripts/vv.py` greps for all of these and refuses the file before `lean` is invoked, because a +file that may assume things corroborates nothing. Lean also warns rather than fails on `sorry`, so +the runner treats any warning as a failure too. + +Rationals are carried as halves — every coefficient in `D = {-1, -1/2, 0, 1/2, 1}` is a whole number +of halves, so `h` stands for the value `h/2`. That keeps the arithmetic exact with no rational type. + +## Reported facts + +Proving something in Lean corroborates nothing on its own — two implementations drift apart quite +happily when nobody compares them. So each file ends with `#eval IO.println "fact ="` +lines reporting the quantities it settled. `scripts/vv.py` recomputes all 29 from the Python kernel +and compares them. A disagreement fails the run, and so does a fact that stops being reported. + +This is the check that bites when a frozen count in `tests/test_counts.py` is edited to match a +drifting kernel. The Python suite cannot catch that, because the suite is the thing that was edited. + +Facts are derived, not written down: `series.witness` asks Lean to enumerate and take the shortest +valid series rather than restating a known answer, so the two sides have to agree about the +enumeration as well as the result. + +## Run + +```bash +lean Formula.lean # one file; it checks on exit 0 with only its `fact` lines + # on stdout. Any other output is a failure. +python3 ../../scripts/vv.py --lean +``` + +Toolchain is pinned in `lean-toolchain`. Install with +[elan](https://github.com/leanprover/elan); the whole set checks in about seven seconds. + +## What this is not + +Lean does not verify the Python kernel, the CLI, the CI, or the papers' mathematics, and **a Lean +file cannot mint a verdict**. If Lean and Python disagree, the V&V job goes red and one of them is +wrong. The job does not say which. See [../../NONCLAIMS.md](../../NONCLAIMS.md) §10. diff --git a/vv/lean/Series.lean b/vv/lean/Series.lean new file mode 100644 index 0000000..7e2c2d5 --- /dev/null +++ b/vv/lean/Series.lean @@ -0,0 +1,88 @@ +/- + Cross-check for the `term_series.guarded_integer_sequence` domain (VCOS §8.3). + + Lean agrees or disagrees with the finite facts the Python kernel reports. + It does not certify the Python kernel, and it cannot mint a verdict. + + This is the grammar that shipped no spec before `vv/specs/series_seven.spec.json`. +-/ + +namespace Realize.Series + +set_option maxRecDepth 20000 + +inductive Op where + | add1 | add2 | add3 | double +deriving DecidableEq, Repr, BEq + +/-- One guarded step. The guard is the invariant `0 ≤ q ≤ cap`; `Nat` carries the lower half. -/ +def step (cap q : Nat) : Op → Option Nat + | .add1 => let r := q + 1; if r ≤ cap then some r else none + | .add2 => let r := q + 2; if r ≤ cap then some r else none + | .add3 => let r := q + 3; if r ≤ cap then some r else none + | .double => let r := 2 * q; if r ≤ cap then some r else none + +/-- Walk a series. A blocked step is a dead series, not a clamped one. -/ +def run (cap : Nat) : Nat → List Op → Option Nat + | q, [] => some q + | q, o :: rest => + match step cap q o with + | none => none + | some q' => run cap q' rest + +def ofLength (ops : List Op) : Nat → List (List Op) + | 0 => [[]] + | n + 1 => (ofLength ops n).flatMap (fun s => ops.map (fun o => s ++ [o])) + +/-- Every series the grammar can name up to the horizon, shortest first. -/ +def upTo (ops : List Op) (horizon : Nat) : List (List Op) := + (List.range (horizon + 1)).flatMap (ofLength ops) + +def repertoire : List Op := [.add1, .add3, .double] +def evenRepertoire : List Op := [.add2, .double] + +def valid (ops : List Op) (cap target horizon : Nat) : List (List Op) := + (upTo ops horizon).filter (fun s => run cap 0 s == some target) + +/-! ## Counts the Python side freezes in tests/test_counts.py -/ + +theorem syntactic_121 : (upTo repertoire 4).length = 121 := by decide +theorem syntactic_31 : (upTo evenRepertoire 4).length = 31 := by decide + +/-! ## The PASS and the COUNTEREXAMPLE the checker reports for `series_seven` -/ + +theorem witness_reaches_seven : run 8 0 [.add3, .double, .add1] = some 7 := by decide +theorem counterexample_is_blocked : run 8 0 [.add3, .double, .double] = none := by decide + +/-! ## Ten series reach 7, none shorter than three steps -/ + +theorem seven_has_ten : (valid repertoire 8 7 4).length = 10 := by decide +theorem seven_needs_three : + (valid repertoire 8 7 4).filter (fun s => s.length < 3) = [] := by decide + +/-! ## The two UNSATs: an even repertoire, and a target above the cap -/ + +theorem even_repertoire_empty : valid evenRepertoire 8 7 4 = [] := by decide +theorem target_nine_empty : valid repertoire 8 9 4 = [] := by decide + +/-! ## Facts reported back to `scripts/vv.py`, which compares them against the Python kernel. -/ + +def showSeq (s : List Op) : String := + String.intercalate "," (s.map fun o => match o with + | .add1 => "add1" | .add2 => "add2" | .add3 => "add3" | .double => "double") + +#eval IO.println s!"fact series.syntactic_121={(upTo repertoire 4).length}" +#eval IO.println s!"fact series.syntactic_31={(upTo evenRepertoire 4).length}" +#eval IO.println s!"fact series.seven_valid={(valid repertoire 8 7 4).length}" +#eval IO.println s!"fact series.even_valid={(valid evenRepertoire 8 7 4).length}" +#eval IO.println s!"fact series.nine_valid={(valid repertoire 8 9 4).length}" +#eval IO.println s!"fact series.seven_min_len={((valid repertoire 8 7 4).map List.length).min?.getD 0}" +/-- The shortest valid series, in enumeration order — derived here, not written down. -/ +def minValid : List (List Op) := + let vs := valid repertoire 8 7 4 + let m := (vs.map List.length).min?.getD 0 + vs.filter (fun s => s.length == m) + +#eval IO.println s!"fact series.witness={showSeq (minValid.headD [])}" + +end Realize.Series diff --git a/vv/lean/lean-toolchain b/vv/lean/lean-toolchain new file mode 100644 index 0000000..d0eb99f --- /dev/null +++ b/vv/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.15.0 diff --git a/vv/specs/encoder_separating.spec.json b/vv/specs/encoder_separating.spec.json new file mode 100644 index 0000000..bf4964f --- /dev/null +++ b/vv/specs/encoder_separating.spec.json @@ -0,0 +1,26 @@ +{ + "schema_version": "realize.v0", + "id": "vv.encoder.separating", + "problem_family": "encoder", + "context": { + "X": [0, 1, 2], + "Y": [0, 1, 2], + "semantics": "finite_relation" + }, + "specification": { + "R": {"0": [0, 1], "1": [1, 2], "2": [0, 2]}, + "K": null, + "preferences": [], + "evidence_mode": "exhaustive_finite", + "provenance": [{"clause": "R", "source": "VCMS Example 4.3 (separating encoder variant)"}] + }, + "library": { + "encoders": [ + {"id": "collapse_all", "map": {"0": "z", "1": "z", "2": "z"}}, + {"id": "separate_all", "map": {"0": "a", "1": "b", "2": "c"}} + ], + "primitives": [{"id": "case_table"}], + "grammar": "finite_case_table" + }, + "bound": {"budget": 100, "max_term_size": 8} +} diff --git a/vv/specs/encoder_zero_budget.spec.json b/vv/specs/encoder_zero_budget.spec.json new file mode 100644 index 0000000..1625dbc --- /dev/null +++ b/vv/specs/encoder_zero_budget.spec.json @@ -0,0 +1,25 @@ +{ + "schema_version": "realize.v0", + "id": "vv.encoder.zero_budget", + "problem_family": "encoder", + "context": { + "X": [0, 1, 2], + "Y": [0, 1, 2], + "semantics": "finite_relation" + }, + "specification": { + "R": {"0": [0, 1], "1": [1, 2], "2": [0, 2]}, + "K": null, + "preferences": [], + "evidence_mode": "exhaustive_finite", + "provenance": [{"clause": "R", "source": "VCMS Example 4.3 (separating encoder variant)"}] + }, + "library": { + "encoders": [ + {"id": "separate_all", "map": {"0": "a", "1": "b", "2": "c"}} + ], + "primitives": [{"id": "case_table"}], + "grammar": "finite_case_table" + }, + "bound": {"budget": 0, "max_term_size": 8} +} diff --git a/vv/specs/formula_affine_only.spec.json b/vv/specs/formula_affine_only.spec.json new file mode 100644 index 0000000..d090c54 --- /dev/null +++ b/vv/specs/formula_affine_only.spec.json @@ -0,0 +1,25 @@ +{ + "schema_version": "realize.v0", + "id": "vv.formula.larger.affine_only", + "problem_family": "formula", + "context": { + "semantics": "exact_rational" + }, + "specification": { + "R": {"phrase": "larger"}, + "K": null, + "preferences": [], + "evidence_mode": "exhaustive_finite", + "provenance": [{"clause": "R", "source": "VCOS §8.1 Table 2"}] + }, + "library": { + "encoders": [], + "primitives": [{"id": "add"}, {"id": "sub"}, {"id": "scale"}], + "grammar": "bounded_coeff_template" + }, + "bound": { + "affine_only": true, + "budget": 10000, + "max_term_size": 4 + } +} diff --git a/vv/specs/formula_unrecognized_phrase.spec.json b/vv/specs/formula_unrecognized_phrase.spec.json new file mode 100644 index 0000000..87e3aec --- /dev/null +++ b/vv/specs/formula_unrecognized_phrase.spec.json @@ -0,0 +1,25 @@ +{ + "schema_version": "realize.v0", + "id": "vv.formula.unrecognized_phrase", + "problem_family": "formula", + "context": { + "semantics": "exact_rational" + }, + "specification": { + "R": {"phrase": "mostly_bigger_ish"}, + "K": null, + "preferences": [], + "evidence_mode": "exhaustive_finite", + "provenance": [{"clause": "R", "source": "no source: the phrase is deliberately outside the declared set (NONCLAIMS.md §1)"}] + }, + "library": { + "encoders": [], + "primitives": [{"id": "add"}, {"id": "sub"}, {"id": "abs"}, {"id": "scale"}], + "grammar": "bounded_coeff_template" + }, + "bound": { + "affine_only": false, + "budget": 10000, + "max_term_size": 4 + } +} diff --git a/vv/specs/grid_preserve_histogram.spec.json b/vv/specs/grid_preserve_histogram.spec.json new file mode 100644 index 0000000..a2c09b9 --- /dev/null +++ b/vv/specs/grid_preserve_histogram.spec.json @@ -0,0 +1,79 @@ +{ + "schema_version": "realize.v0", + "id": "vv.grid.preserve_histogram", + "problem_family": "term_series", + "context": { + "X": [ + [ + 0, + 3, + 0 + ], + [ + 4, + 4, + 0 + ], + [ + 0, + 0, + 5 + ] + ], + "alphabet": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9 + ], + "semantics": "finite_integer" + }, + "specification": { + "R": { + "goal": "recolor_foreground_red" + }, + "K": { + "preserve_histogram": true + }, + "preferences": [ + "min_length" + ], + "evidence_mode": "exhaustive_finite", + "provenance": [ + { + "clause": "R", + "source": "IGVF-CTS §7.1" + }, + { + "clause": "K", + "source": "IGVF-CTS §7.1 — histogram preservation contradicts the recolor goal" + } + ] + }, + "library": { + "encoders": [], + "primitives": [ + { + "id": "Extract", + "in": "Grid", + "out": "Mask" + }, + { + "id": "Render2", + "in": "Mask", + "out": "Grid" + } + ], + "grammar": "typed_grid" + }, + "bound": { + "budget": 100, + "max_term_size": 4 + } +} diff --git a/vv/specs/grid_zero_budget.spec.json b/vv/specs/grid_zero_budget.spec.json new file mode 100644 index 0000000..33fedfe --- /dev/null +++ b/vv/specs/grid_zero_budget.spec.json @@ -0,0 +1,73 @@ +{ + "schema_version": "realize.v0", + "id": "vv.grid.zero_budget", + "problem_family": "term_series", + "context": { + "X": [ + [ + 0, + 3, + 0 + ], + [ + 4, + 4, + 0 + ], + [ + 0, + 0, + 5 + ] + ], + "alphabet": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9 + ], + "semantics": "finite_integer" + }, + "specification": { + "R": { + "goal": "recolor_foreground_red" + }, + "K": null, + "preferences": [ + "min_length" + ], + "evidence_mode": "exhaustive_finite", + "provenance": [ + { + "clause": "R", + "source": "IGVF-CTS §7.1" + } + ] + }, + "library": { + "encoders": [], + "primitives": [ + { + "id": "Extract", + "in": "Grid", + "out": "Mask" + }, + { + "id": "Render2", + "in": "Mask", + "out": "Grid" + } + ], + "grammar": "typed_grid" + }, + "bound": { + "budget": 0, + "max_term_size": 4 + } +} diff --git a/vv/specs/series_even_repertoire.spec.json b/vv/specs/series_even_repertoire.spec.json new file mode 100644 index 0000000..5cf3e67 --- /dev/null +++ b/vv/specs/series_even_repertoire.spec.json @@ -0,0 +1,27 @@ +{ + "schema_version": "realize.v0", + "id": "vcos.series.even_repertoire", + "problem_family": "term_series", + "context": { + "semantics": "finite_integer", + "q0": 0, + "cap": 8, + "Y_target": 7 + }, + "specification": { + "R": {"target": 7}, + "K": {"invariant": "in_S"}, + "preferences": ["min_length"], + "evidence_mode": "exhaustive_finite", + "provenance": [ + {"clause": "R", "source": "VCOS §8.3 — odd target under an even-only repertoire"}, + {"clause": "K", "source": "VCOS §8.3 — state stays in [0, cap] at every step"} + ] + }, + "library": { + "encoders": [], + "primitives": [{"id": "add2"}, {"id": "double"}], + "grammar": "guarded_integer_sequence" + }, + "bound": {"budget": 10000, "horizon": 4, "max_term_size": 4} +} diff --git a/vv/specs/series_seven.spec.json b/vv/specs/series_seven.spec.json new file mode 100644 index 0000000..9154808 --- /dev/null +++ b/vv/specs/series_seven.spec.json @@ -0,0 +1,27 @@ +{ + "schema_version": "realize.v0", + "id": "vcos.series.seven", + "problem_family": "term_series", + "context": { + "semantics": "finite_integer", + "q0": 0, + "cap": 8, + "Y_target": 7 + }, + "specification": { + "R": {"target": 7}, + "K": {"invariant": "in_S"}, + "preferences": ["min_length"], + "evidence_mode": "exhaustive_finite", + "provenance": [ + {"clause": "R", "source": "VCOS §8.3 — guarded integer term series"}, + {"clause": "K", "source": "VCOS §8.3 — state stays in [0, cap] at every step"} + ] + }, + "library": { + "encoders": [], + "primitives": [{"id": "add1"}, {"id": "add3"}, {"id": "double"}], + "grammar": "guarded_integer_sequence" + }, + "bound": {"budget": 10000, "horizon": 4, "max_term_size": 4} +} diff --git a/vv/specs/series_target_nine.spec.json b/vv/specs/series_target_nine.spec.json new file mode 100644 index 0000000..161e571 --- /dev/null +++ b/vv/specs/series_target_nine.spec.json @@ -0,0 +1,27 @@ +{ + "schema_version": "realize.v0", + "id": "vcos.series.target_nine", + "problem_family": "term_series", + "context": { + "semantics": "finite_integer", + "q0": 0, + "cap": 8, + "Y_target": 9 + }, + "specification": { + "R": {"target": 9}, + "K": {"invariant": "in_S"}, + "preferences": ["min_length"], + "evidence_mode": "exhaustive_finite", + "provenance": [ + {"clause": "R", "source": "VCOS §8.3 — target above the cap"}, + {"clause": "K", "source": "VCOS §8.3 — state stays in [0, cap] at every step"} + ] + }, + "library": { + "encoders": [], + "primitives": [{"id": "add1"}, {"id": "add3"}, {"id": "double"}], + "grammar": "guarded_integer_sequence" + }, + "bound": {"budget": 10000, "horizon": 4, "max_term_size": 4} +} diff --git a/vv/specs/series_zero_budget.spec.json b/vv/specs/series_zero_budget.spec.json new file mode 100644 index 0000000..a71790a --- /dev/null +++ b/vv/specs/series_zero_budget.spec.json @@ -0,0 +1,27 @@ +{ + "schema_version": "realize.v0", + "id": "vcos.series.zero_budget", + "problem_family": "term_series", + "context": { + "semantics": "finite_integer", + "q0": 0, + "cap": 8, + "Y_target": 7 + }, + "specification": { + "R": {"target": 7}, + "K": {"invariant": "in_S"}, + "preferences": ["min_length"], + "evidence_mode": "exhaustive_finite", + "provenance": [ + {"clause": "R", "source": "VCOS §8.3 — guarded integer term series"}, + {"clause": "K", "source": "VCOS §8.3 — state stays in [0, cap] at every step"} + ] + }, + "library": { + "encoders": [], + "primitives": [{"id": "add1"}, {"id": "add3"}, {"id": "double"}], + "grammar": "guarded_integer_sequence" + }, + "bound": {"budget": 0, "horizon": 4, "max_term_size": 4} +}