Post-release maintenance: dependencies, onboarding, and examples

AGENTS.md

@@ -213,8 +213,8 @@ If that path is not inside this repository, prefix commands with `PYTHONPATH=src
 - `src/verifier/runtime/` — `public_cli.py` (every CLI entry point) and `demo.py`.
 - `src/verifier/specifications/` — byte-identical copies of normative spec files.
 - `receipts/schema/` — receipt JSON Schemas. `standard/schemas/` — strict non-receipt
-  mechanism schemas. `examples/` — runnable specimens.
-- `experiments/` — non-normative studies with profile manifests, explicit horizons,
+  mechanism schemas. `examples/` — supported runnable specimens.
+- `experiments/` — non-normative roadmap-steering studies with profile manifests, explicit horizons,
   and blockers.
 - `src/verifier/experimental_workflow/` — optional workflow/profile interchange; it
   records allocation but never grants a VSTD verdict from repository state.

CONTRIBUTING.md

@@ -17,7 +17,7 @@ are useful contributions.
 | Reference implementation | `src/verifier/` | Tests for the exact implemented proposition and failure boundary |
 | Command-line behavior | `src/verifier/runtime/public_cli.py` | Generated reference, installed-wheel smoke, and machine-readable output tests |
 | Ecosystem adapter or application profile | `src/verifier/interoperability/` or an explicitly experimental profile | Accepted upstream versions, native-verifier boundary, information-loss declaration, trust roots, and substitution/replay/scope-widening tests |
-| Non-normative research | `experiments/` | Experiment manifest, fixtures, unresolved horizons, and generated index |
+| Non-normative roadmap-steering research | `experiments/` | Experiment manifest, fixtures, unresolved horizons, and generated index |
 | Explanatory documentation | `docs/` | Local-link, acronym, presentation, and semantic-drift review |
 
 The authority order is:

examples/zizk_artifact_first/risc0/THREAT_MODEL.md

@@ -1,6 +1,8 @@
 # Threat model
 
-> **Acronyms:** Executable and Linkable Format (ELF); identifier (ID); JavaScript Object Notation (JSON);
+> **Acronyms:** American National Standards Institute (ANSI);
+> Common Vulnerabilities and Exposures (CVE); Executable and Linkable Format (ELF);
+> GitHub Security Advisory (GHSA); identifier (ID); JavaScript Object Notation (JSON);
 > reduced instruction set computer (RISC); Secure Hash Algorithm 256-bit (SHA-256);
 > scalable transparent argument of knowledge (STARK); zero-identity/zero-knowledge (ZIZK);
 > zero-knowledge virtual machine (zkVM).
@@ -90,6 +92,22 @@ audit every transitive crate, compiler binary, installer, or build host. Two cle
 under the same recorded Windows Subsystem for Linux 2 environment reproduced the image
 ID; a build on another trusted host and an independent implementation remain unavailable.
 
+The host pins `rand` 0.8.6, the first patched 0.8 release for
+[`GHSA-cq8v-f236-94qc`](https://github.com/advisories/GHSA-cq8v-f236-94qc).
+The locked RISC Zero 3.0.6 dependency graph also contains `tracing-subscriber` 0.2.25
+through `ark-relations`. That crate is affected by
+[`GHSA-xwfj-jgwm-7wp5` / `CVE-2025-58160`](https://github.com/advisories/GHSA-xwfj-jgwm-7wp5)
+only when its terminal-formatting path emits attacker-controlled ANSI escape sequences.
+Both committed lock files compile it without the formatting feature: its resolved package
+block depends only on `tracing-core`. The repository's host and guest sources do not
+initialize a formatting subscriber. The vulnerable terminal-output mechanism is therefore
+absent from this exact example even though the transitive package version remains present.
+
+This boundary expires if the dependency features, RISC Zero version, lock files, or Rust
+sources change. Enabling terminal formatting requires upgrading to a fixed dependency graph
+and regenerating or revalidating the recorded proof coordinate; a prior alert dismissal
+must not be carried forward by package name alone.
+
 ### Semantic overreach
 
 A prover selects the private bytes and candidate tag. The proof does not show that those

examples/zizk_artifact_first/risc0/host/Cargo.toml

@@ -6,7 +6,7 @@ publish = false
 
 [dependencies]
 hex = "=0.4.3"
-rand = "=0.8.5"
+rand = "=0.8.6"
 risc0-zkvm = { version = "=3.0.6", features = ["disable-dev-mode"] }
 rmp-serde = "=1.3.0"
 serde = { version = "=1.0.228", features = ["derive"] }

scripts/check_presentation.py

@@ -322,8 +322,11 @@ def maturity_table_violations(readme: str) -> list[str]:
     errors: list[str] = []
     if header not in section:
         errors.append("README.md maturity table does not expose all six required fields")
+        table = section
+    else:
+        table = section.split(header, 1)[1]
     rows: dict[str, list[str]] = {}
-    for line in section.splitlines():
+    for line in table.splitlines():
         if not line.startswith("|") or line.startswith("|---"):
             continue
         cells = [cell.strip() for cell in line.strip().strip("|").split("|")]
@@ -371,6 +374,7 @@ def check_claim_boundaries(errors: list[str]) -> None:
         "VSTD is a verification-domain language and Python reference implementation",
         "does **not**\nreplace native domain verifiers",
         "## 30–60 second demonstration",
+        "## The 90-second mental model",
         "## What a result means",
         "## Current maturity",
         "## Why VSTD exists",
@@ -395,6 +399,7 @@ def check_claim_boundaries(errors: list[str]) -> None:
     expected_order = (
         "VSTD is a verification-domain language",
         "## 30–60 second demonstration",
+        "## The 90-second mental model",
         "## What a result means",
         "## Current maturity",
         "## Why VSTD exists",

tests/test_experimental_workflow_profile.py

@@ -35,6 +35,11 @@
 )
 
 
+def test_non_normative_experiments_remain_outside_supported_examples() -> None:
+    assert (ROOT / "experiments" / "INDEX.md").is_file()
+    assert not (ROOT / "examples" / "experimental_profiles").exists()
+
+
 def _example_payload() -> dict[str, object]:
     return json.loads(EXPERIMENT_MANIFEST.read_text(encoding="utf-8"))
 

tests/test_presentation_surface.py

@@ -116,6 +116,11 @@ def test_maturity_table_requires_each_major_surface_and_explicit_conformance() -
 
     readme = (ROOT / "README.md").read_text(encoding="utf-8")
     assert module.maturity_table_violations(readme) == []
+    assert "## The 90-second mental model" in readme
+    assert "Exact surface-by-surface matrix for reviewers and integrators" in readme
+    assert readme.index("## The 90-second mental model") < readme.index(
+        "## Current maturity"
+    )
 
     combined = readme.replace("| VSTD-Graph-3 |", "| VSTD-Graph-2 |", 1)
     errors = module.maturity_table_violations(combined)

tests/test_zizk_artifact_first.py

@@ -5,6 +5,7 @@
 import hashlib
 import json
 from pathlib import Path
+import re
 import subprocess
 
 
@@ -23,11 +24,37 @@ def test_zero_knowledge_mechanism_is_optional_and_pinned() -> None:
 
     assert 'version = "=3.0.6"' in host_manifest
     assert 'features = ["disable-dev-mode"]' in host_manifest
+    assert 'rand = "=0.8.6"' in host_manifest
     assert 'version = "=3.0.6"' in guest_manifest
     assert 'version = "=3.0.6"' in methods_manifest
     assert "zizk" not in (ROOT / "pyproject.toml").read_text(encoding="utf-8").lower()
 
 
+def test_pinned_security_advisory_boundaries_are_current() -> None:
+    locks = (
+        MECHANISM / "Cargo.lock",
+        MECHANISM / "methods" / "guest" / "Cargo.lock",
+    )
+    workspace_lock = locks[0].read_text(encoding="utf-8")
+    assert 'name = "rand"\nversion = "0.8.5"' not in workspace_lock
+    assert 'name = "rand"\nversion = "0.8.6"' in workspace_lock
+
+    for path in locks:
+        text = path.read_text(encoding="utf-8")
+        match = re.search(
+            r'\[\[package\]\]\nname = "tracing-subscriber"\nversion = "0\.2\.25"'
+            r'.*?(?=\n\[\[package\]\]|\Z)',
+            text,
+            flags=re.DOTALL,
+        )
+        assert match is not None
+        assert 'dependencies = [\n "tracing-core",\n]' in match.group(0)
+
+    threat_model = (MECHANISM / "THREAT_MODEL.md").read_text(encoding="utf-8")
+    assert "vulnerable terminal-output mechanism is therefore" in threat_model
+    assert "absent from this exact example" in threat_model
+
+
 def test_zero_knowledge_claim_boundary_is_explicit() -> None:
     boundary = (MECHANISM / "CLAIM_BOUNDARY.md").read_text(encoding="utf-8")
     assert "does not prove" in boundary