ONT-4b2: extract:code + extract:lean as focus nodes; 16 of the ONT-0 table's 32 W3C SHACL-Core cases vendored in the gate, 16 accounted for by excluding form; the pinned oracle differential out of it (Refs PMAT-3509)

Makefile

@@ -1361,3 +1361,23 @@ ont-ratchet:
 
 ont-ratchet-check:
 	@bash scripts/check_ont_ratchet.sh --check
+
+# ONT-001 §5 ONT-4b2 / R-13 — the out-of-gate SHACL differential oracle.
+#
+# NOT a PR check, by the rule that puts it here: `shacl` is 316 crates and pinned at ONE version (ONT-0's
+# ledger), so it lives in tests/oracle/ — a crate DETACHED from the workspace — and runs in the release gate
+# only. It validates the same graph twice (the pinned processor and the in-house validator) and writes
+# tests/oracle/differential.json, which is TRACKED: the row's probe reads `cases>0 and disagreements==0`, and
+# a tracked file nobody regenerated is caught by `oracle-check` diffing it.
+.PHONY: oracle oracle-check
+oracle:
+	@echo "== W3C cases + the real corpus through the pinned oracle (shacl 0.3.21, out of gate) =="
+	@. scripts/pv_bin.sh && "$$PV" lint contracts --gate shapes --format json > "$${TMPDIR:-/tmp}/pv-shapes.json" 2>/dev/null || true
+	@# No `cd`: this Makefile is .ONESHELL, so a cd on one line moves every line after it (the first form of
+	@# this target built in tests/oracle/ and then ran `$(cd tests/oracle …)` from inside it — "No such file").
+	@cargo build --release --quiet --manifest-path tests/oracle/Cargo.toml
+	@"$$(cargo metadata --no-deps --format-version 1 --manifest-path tests/oracle/Cargo.toml | sed -n 's/.*"target_directory":"\([^"]*\)".*/\1/p')/release/ont-oracle" . "$${TMPDIR:-/tmp}/pv-shapes.json"
+
+oracle-check: oracle
+	@git diff --exit-code tests/oracle/differential.json \
+	  || { echo "FAIL: tests/oracle/differential.json differs from a fresh run — commit it"; exit 1; }

README.md

@@ -41,7 +41,7 @@ publishing — all backed by YAML provable contracts that fail CI on drift.
 | Metric | Count | Source of truth |
 |-------:|------:|---|
 | Workspace crates | **79** workspace crates | `cargo metadata --no-deps` (NOT `ls crates/` — 4 are `exclude`d, 1 has no Cargo.toml) |
-| Provable contracts | **<!-- CONTRACT_COUNT_START -->1798<!-- CONTRACT_COUNT_END -->** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) |
+| Provable contracts | **<!-- CONTRACT_COUNT_START -->1799<!-- CONTRACT_COUNT_END -->** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) |
 | CLI commands | **110** CLI commands | `apr --help` |
 | Book CLI chapters | **112** chapters | `ls book/src/cli/*.md` |
 | Book lib chapters | **71** chapters | `ls book/src/lib/*.md` (parity with `pub mod`) |
@@ -262,7 +262,7 @@ falsification_tests:
   prediction: apr validate bad-model.apr exits non-zero
 ```
 
-The tree carries <!-- CONTRACT_COUNT_START -->1798<!-- CONTRACT_COUNT_END --> contracts across inference, training, quantization, attention, FFN,
+The tree carries <!-- CONTRACT_COUNT_START -->1799<!-- CONTRACT_COUNT_END --> contracts across inference, training, quantization, attention, FFN,
 tokenization, model formats, CLI safety — and this README itself.
 
 ## Migration from old crates

ci/explicit-test-commands.d/343-aprender-contracts-cli-ont4b2-code-lean-w3c.cmd

@@ -0,0 +1 @@
+cargo test -p aprender-contracts-cli --test ont4b2_code_lean_w3c

contracts/census.json

@@ -1,8 +1,8 @@
 {
   "schema": "ont.paiml.dev/census/v1alpha1",
   "git_sha": null,
-  "n_files": 1798,
-  "n_parsed": 1798,
+  "n_files": 1799,
+  "n_parsed": 1799,
   "n_parse_errors": 0,
   "parse_errors": [],
   "quarantined_n": 0,
@@ -12,7 +12,7 @@
     "kernel": 362,
     "model-family": 28,
     "model-family-variant": 1,
-    "pattern": 85,
+    "pattern": 86,
     "pretraining-corpus": 2,
     "registry": 519,
     "schema": 766,
@@ -25,11 +25,11 @@
     "pv-contract": 1
   },
   "by_anchoring": {
-    "unanchored": 1795,
+    "unanchored": 1796,
     "class": 2,
     "instance": 1
   },
-  "id_set_sha256": "a5a5d6518fff519dee2cae9ffd1a00d74c404da02d5ed3d85b5814d0027773d9",
+  "id_set_sha256": "a547cd5527caeffade2d8260d25421f26506df1c1d8f00f5eb7b9cde12e8107e",
   "declared_external": [
     {
       "name": "provable-contracts",

contracts/lint-baseline.json

@@ -4,14 +4,14 @@
   "armed_shapes": ["ont-shapes-v1", "ladder-measured"],
   "ont": {
     "consumer_present": false,
-    "contracts_total": 1837,
-    "entity_types_registered": 1,
-    "extractors_implemented": 1,
+    "contracts_total": 1852,
+    "entity_types_registered": 9,
+    "extractors_implemented": 6,
     "contracts_anchored": 3,
-    "contracts_shaped": 2,
+    "contracts_shaped": 3,
     "unanchored_but_bindable": 297,
     "formal_prose": 1464,
     "legacy_unresolved_depends_on": 8,
-    "shapes_unarmed": 1
+    "shapes_unarmed": 3
   }
 }

contracts/ont-code-symbols-v1.yaml

@@ -0,0 +1,156 @@
+# ─────────────────────────────────────────────────────────────────────────────
+# ont-code-symbols-v1 — `extract:code` + `extract:lean`: the bound Rust symbols and the in-tree Lean theorems
+# as focus nodes (ONT-001 §3.7, §5 ONT-4b2; aprender#3509, PMAT-3509)
+#
+# WHAT IT GOVERNS
+#   provable_contracts::ontology::extract::code   — every `module_path` + `function` a binding.yaml declares,
+#                                                   resolved by a `syn` module-tree walk → ont:Symbol.
+#   provable_contracts::ontology::extract::lean   — every `theorem` under ProvableContracts/Theorems → ont:Statement.
+#   provable_contracts::ontology::w3c             — the vendored W3C SHACL-Core cases, run by the gate.
+#   tests/oracle/                                 — the pinned out-of-gate differential (R-13, release gate only).
+#
+# WHY THE BOUND SYMBOLS AND NOT THE WORKSPACE. 3.9 M lines of Rust would be a second copy of the tree in RDF,
+# and no contract constrains a symbol nothing binds. The bindings are the corpus's OWN claim about which code
+# its equations name — ONT-3a already makes that claim falsifiable one binding at a time; this row puts the
+# claim in the graph, where a SHAPE says it, and where `sym:attribute "kernel"` is what ONT-4c3 will type.
+#
+# WHY AN UNRESOLVED SYMBOL IS STILL A NODE. A walker that silently dropped what it could not find would shrink
+# the graph exactly where the defect is: the corpus would conform because the ghost was never a focus node.
+# `sym:resolved false` + `sym:unresolvedReason` is the fail-closed form — measured on this tree: 169 of 270
+# bound symbols resolve, and the 101 that do not name modules and functions that are genuinely absent.
+#
+# WHY THE SHAPES SHIP UNARMED. §3.9: a gate red on its own target the day it merges trains bypass. 101 ghosts
+# exist on main today; `bound-symbols-resolve` is COMPUTED AND REPORTED at this row (under `not_armed_shapes`)
+# and the release that cleans the bindings arms it by adding one string to lint-baseline.json's `armed_shapes`.
+# Same for `lean-statements-grounded`: three theorem files carry `sorry`.
+#
+# KIND: pattern. Two extractors, their vocabularies, and the shapes they feed.
+# ─────────────────────────────────────────────────────────────────────────────
+name: ont-code-symbols
+version: "1.0.0"
+scope: >
+  How a bound Rust symbol and an in-tree Lean theorem become RDF, what `sym:*` and `lean:*` carry, and what the
+  two shapes over them assert. Out of scope: symbols no binding names (not focus nodes at v1alpha1), Lean
+  `formalization.yaml` (PVL EV-8b's file, not in this tree), and proof CHECKING — `lean:sorryFree` is a
+  property of the file's text, never a claim that `lake` succeeded.
+status: active
+
+metadata:
+  version: "1.0.0"
+  kind: pattern
+  created: '2026-09-19'
+  last_modified: '2026-09-19'
+  author: PAIML Engineering
+  description: >
+    extract:code — the bound symbols by a syn module-tree walk (inline mods, file mods, #[path], one re-export
+    hop, impl methods), fail-closed with the reason in the graph; extract:lean — theorems from the in-tree
+    Theorems tree, sorry-free files only grounding, joined to the contracts that cite them by ONT-2a's name
+    forms; 16 vendored W3C SHACL-Core cases run every gate run; the oracle differential in the release gate.
+  references:
+    - 'paiml/infra docs/specifications/paiml-ontology.md §3.6 (the subset), §3.7 (extractors), §5 ONT-4b2, R-13, R-15, R-18'
+    - 'paiml/infra docs/specifications/ont-oracle-ledger.md (ONT-0: the 32-case table and the pinned oracle)'
+    - 'crates/aprender-contracts/src/ontology/extract/{code,lean}.rs, ontology/w3c.rs, tests/oracle/'
+    - 'ONT-2a: crates/aprender-contracts/src/proof_status.rs — the same theorem scan this extractor reuses'
+
+relations:
+  depends_on: [ont-shapes-v1, ont-sigma-v1]
+
+equations:
+  resolve_symbol:
+    formula: "resolve(module_path, function) = walk(crate_root(head), tail) ▷ (fn function ∨ impl::function ∨ use → resolve(target))"
+    domain: "every (module_path, function) a binding.yaml under contracts/ declares with a function"
+    codomain: "Resolved{file, visibility, kind, attributes} or Unresolved{reason naming the file and the segment}"
+    invariants:
+      - "only the files on the walk are parsed: cost is bindings × depth, never the workspace"
+      - "a symbol that does not resolve is still a focus node, with sym:resolved false"
+      - "a re-export is followed at most 8 hops, so a cycle terminates with a reason"
+    preconditions:
+      - "the workspace's Cargo.toml files name their crates ([package] name and [lib] name, both indexed)"
+    postconditions:
+      - "two extractions of the same tree are byte-identical (R-15)"
+    lean_theorem: none — L4 not declared
+  ground_theorem:
+    formula: "grounded(t) ⇔ ¬contains(file(t), \"sorry\") ; modelOf(t) = { c | ref ∈ refs(c) ∧ ref ∈ acceptedNames(t) }"
+    domain: "every `theorem` declaration under <lean base>/ProvableContracts/Theorems/<Domain>/*.lean"
+    codomain: "an ont:Statement node with lean:sorryFree, lean:discharge and one lean:modelOf edge per citing contract"
+    invariants:
+      - "a file carrying `sorry` grounds nothing — the same rule ONT-2a's L4 credit uses, from the same scan"
+      - "a contract reference that names no theorem, file or domain is counted (lean_refs_unresolved), never guessed"
+    preconditions:
+      - "the Lean tree is the first of proof_status::LEAN_THEOREM_BASES that exists under the repo root"
+    postconditions:
+      - "what the graph says about a theorem and what `pv proof-status` credits agree by construction"
+    lean_theorem: none — L4 not declared
+
+invariants:
+  - id: SYM-INV-001
+    property: deterministic, no blank nodes
+    formal: '∀ tree: extract(tree) = extract(tree) ∧ ∀ t ∈ extract(tree): subject(t) ∈ IRI'
+    prose: false
+  - id: SYM-INV-002
+    property: fail-closed — an unresolved binding is a node with a reason, never an absence
+    formal: '¬resolves(b) ⇒ (b, sym:resolved, false) ∈ graph ∧ (b, sym:unresolvedReason, r) ∈ graph'
+    prose: false
+  - id: SYM-INV-003
+    property: an admitted proof grounds nothing
+    formal: 'sorry ∈ file(t) ⇒ (t, lean:sorryFree, false) ∧ discharge(t) = admitted'
+    prose: false
+  - id: SYM-INV-004
+    property: the validator agrees with the standard on every form it claims
+    formal: '∀ c ∈ vendored W3C cases: results(c) = expected(c) ∨ verdict = Unknown{Differential}'
+    prose: false
+  - id: SYM-INV-005
+    property: no third-party SHACL crate is reachable from the gate path
+    formal: 'shacl ∉ deps(aprender-contracts, {normal, build, dev})'
+    prose: false
+
+falsification_tests:
+  - id: FALSIFY-SYM-001
+    rule: the module-tree walk
+    prediction: the walk resolves a file module, an inline module, an impl method and one `pub use … as` hop, and refuses a ghost naming the file it looked in and the segment it wanted
+    test: cargo test -p aprender-contracts --lib ontology::extract::code
+    if_fails: a binding that names nothing is dropped from the graph instead of reported, and a ghost passes because it was never a focus node
+  - id: FALSIFY-SYM-002
+    rule: an admitted proof grounds nothing
+    prediction: a theorem file carrying `sorry` yields lean:sorryFree false and discharge "admitted"; a contract reference naming no theorem, file or domain is counted in lean_refs_unresolved, never guessed
+    test: cargo test -p aprender-contracts --lib ontology::extract::lean
+    if_fails: an admitted theorem grounds an L4 claim, or a dangling lean_theorem is silently ignored
+  - id: FALSIFY-SYM-003
+    rule: the vendored W3C cases
+    prediction: all 16 vendored cases pass, the 32 of ONT-0's table are accounted for case by case (vendored or excused by name), and a mistranslated expectation fails naming the difference
+    test: cargo test -p aprender-contracts --lib ontology::w3c
+    if_fails: the subset claims a component the standard's own case refutes, or a case is quietly dropped from the count
+  - id: FALSIFY-SYM-004
+    rule: the gate's answers on the CLI
+    prediction: the bound symbols are focus nodes with the counts reported; the SAME ghost is a Fail naming the symbol under an armed shape and a reported unarmed_violation under an unarmed one; a failing vendored case declines Unknown{Differential} naming it; no shacl crate is in the workspace lock
+    test: cargo test -p aprender-contracts-cli --test ont4b2_code_lean_w3c
+    if_fails: arming is ignored, a differential is graded as a corpus verdict, or the oracle leaks into the gate path
+  - id: FALSIFY-SYM-005
+    rule: the out-of-gate differential
+    prediction: the pinned shacl 0.3.21 agrees with the in-house validator on all 16 cases and on the real corpus's violation set; a planted `sh:minCount` change in shapes.ttl makes it disagree, measured
+    test: make oracle
+    if_fails: the in-house subset has drifted from the standard and nobody outside it noticed
+
+qa_gate:
+  required_checks:
+    - "cargo test -p aprender-contracts --lib ontology::"
+    - "cargo test -p aprender-contracts-cli --test ont4b2_code_lean_w3c"
+
+shapes:
+  # REPORTED, not armed (see the header): 101 of 270 bound symbols on this tree name code that is not there.
+  - id: bound-symbols-resolve
+    targetClass: ont:Symbol
+    properties:
+      - {path: sym:crate, minCount: 1, maxCount: 1}
+      - {path: sym:module, minCount: 1, maxCount: 1}
+      - {path: sym:name, minCount: 1, maxCount: 1}
+      - {path: sym:implements, minCount: 1, nodeKind: IRI, class: ont:Contract}
+      - {path: sym:resolved, minCount: 1, maxCount: 1, in: [true]}
+  # REPORTED, not armed: three theorem files carry `sorry`.
+  - id: lean-statements-grounded
+    targetClass: ont:Statement
+    properties:
+      - {path: lean:name, minCount: 1, maxCount: 1}
+      - {path: lean:file, minCount: 1, maxCount: 1}
+      - {path: lean:discharge, minCount: 1, maxCount: 1, in: [grounded, admitted]}
+      - {path: lean:sorryFree, minCount: 1, maxCount: 1, in: [true]}

contracts/ontology.yaml

@@ -23,6 +23,8 @@ concepts:
   Test: {doc: "a test function a contract cites as its falsifier"}
   Proof: {doc: "a Kani harness or Lean theorem discharging an obligation"}
   Doc: {doc: "a prose document under contract (README.md, CLAUDE.md)"}
+  Symbol: {doc: "a Rust symbol a binding names — a free fn or an impl method; the focus node of extract:code (ONT-4b2: ont:Symbol with sym:crate, sym:module, sym:resolved)"}
+  Statement: {doc: "a Lean theorem in the in-tree Theorems tree; the focus node of extract:lean (ONT-4b2: ont:Statement with lean:sorryFree, lean:modelOf)"}
   Model: {doc: "a model file — an .apr container or a GGUF; the ladder's rungs are the ones the release measures (ONT-4c1: model:Model, model:RequiredModel, model:Receipt)"}
   Dataset: {doc: "a CSV or corpus file"}
 
@@ -131,8 +133,8 @@ agents:
 entity_types:
   - {name: pv-contract, extractor: pv_contract, implemented: true}
   - {name: json, extractor: json, implemented: true}
-  - {name: code, extractor: code, implemented: false}
-  - {name: lean, extractor: lean, implemented: false}
+  - {name: code, extractor: code, implemented: true}
+  - {name: lean, extractor: lean, implemented: true}
   - {name: readme, extractor: readme, implemented: false}
   - {name: llm-context, extractor: llm_context, implemented: false}
   - {name: apr-model, extractor: apr_model, implemented: true}
@@ -142,8 +144,8 @@ entity_types:
 extractors:
   - {name: pv_contract, reader: ontology/extract/pv_contract.rs, implemented: true}
   - {name: json, reader: ontology/extract/json.rs, implemented: true}
-  - {name: code, reader: ontology/extract/code.rs, implemented: false}
-  - {name: lean, reader: ontology/extract/lean.rs, implemented: false}
+  - {name: code, reader: ontology/extract/code.rs, implemented: true}
+  - {name: lean, reader: ontology/extract/lean.rs, implemented: true}
   - {name: readme, reader: ontology/extract/readme.rs, implemented: false}
   - {name: llm_context, reader: ontology/extract/llm_context.rs, implemented: false}
   - {name: apr_model, reader: ontology/extract/apr_model.rs, implemented: true}

contracts/shapes.ttl

@@ -2,6 +2,63 @@
 @prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
 @prefix ont: <https://ont.paiml.dev/v1alpha1/> .
 
+<https://ont.paiml.dev/v1alpha1/shape/bound-symbols-resolve> a sh:NodeShape ;
+    sh:targetClass <https://ont.paiml.dev/v1alpha1/Symbol> ;
+    sh:property [
+        sh:path <https://ont.paiml.dev/v1alpha1/sym/crate> ;
+        sh:minCount 1 ;
+        sh:maxCount 1 ;
+    ] ;
+    sh:property [
+        sh:path <https://ont.paiml.dev/v1alpha1/sym/module> ;
+        sh:minCount 1 ;
+        sh:maxCount 1 ;
+    ] ;
+    sh:property [
+        sh:path <https://ont.paiml.dev/v1alpha1/sym/name> ;
+        sh:minCount 1 ;
+        sh:maxCount 1 ;
+    ] ;
+    sh:property [
+        sh:path <https://ont.paiml.dev/v1alpha1/sym/implements> ;
+        sh:minCount 1 ;
+        sh:class <https://ont.paiml.dev/v1alpha1/Contract> ;
+        sh:nodeKind sh:IRI ;
+    ] ;
+    sh:property [
+        sh:path <https://ont.paiml.dev/v1alpha1/sym/resolved> ;
+        sh:minCount 1 ;
+        sh:maxCount 1 ;
+        sh:in ( "true"^^<http://www.w3.org/2001/XMLSchema#boolean> ) ;
+    ] ;
+.
+
+<https://ont.paiml.dev/v1alpha1/shape/lean-statements-grounded> a sh:NodeShape ;
+    sh:targetClass <https://ont.paiml.dev/v1alpha1/Statement> ;
+    sh:property [
+        sh:path <https://ont.paiml.dev/v1alpha1/lean/name> ;
+        sh:minCount 1 ;
+        sh:maxCount 1 ;
+    ] ;
+    sh:property [
+        sh:path <https://ont.paiml.dev/v1alpha1/lean/file> ;
+        sh:minCount 1 ;
+        sh:maxCount 1 ;
+    ] ;
+    sh:property [
+        sh:path <https://ont.paiml.dev/v1alpha1/lean/discharge> ;
+        sh:minCount 1 ;
+        sh:maxCount 1 ;
+        sh:in ( "grounded" "admitted" ) ;
+    ] ;
+    sh:property [
+        sh:path <https://ont.paiml.dev/v1alpha1/lean/sorryFree> ;
+        sh:minCount 1 ;
+        sh:maxCount 1 ;
+        sh:in ( "true"^^<http://www.w3.org/2001/XMLSchema#boolean> ) ;
+    ] ;
+.
+
 <https://ont.paiml.dev/v1alpha1/shape/ladder-measured> a sh:NodeShape ;
     sh:targetClass <https://ont.paiml.dev/v1alpha1/model/Model> ;
     sh:property [