evidence(ladder): 0.68.1 receipts re-measured at main a6f54e84c on both hosts — eight rungs with sha256, RED by construction on Qwen3.5 (#3510) - #3523
Merged
Conversation
… hosts — all eight rungs with sha256, RED by construction on the Qwen3.5 rungs (#3510, ONT-4c1 witness) Both receipts produced by scripts/model_ladder.sh at a6f54e8 (the first main with #3507's sha256 rows and #3511's four dense rungs), apr 0.68.1 (a6f54e8), lambda RTX 4090 cc 8.9 and gx10 GB10 cc 12.1. Every rung present, sha_ok, and carries the measured sha256 — the witness ONT-4c1's ladder-measured shape needs on day one. Green: qwen2-1.5b, qwen3-1.7b (both hosts), qwen3-8b (gx10; lambda optional rung: golden Empty output, #3486). Red by construction: qwen35-0.8b/2b fall back to CPU on main until #3517 merges; qwen35-4b/9b/27b exit 101 at forward_qwen35.rs:132 (GQA inside GDN, nk != nv — #3346 root cause). The T-2 judge is not a PR check; this changes no gate. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Contributor
Author
|
quorum-review (AD-04): three PASS — agreed (auto_merge: checked=true was_armed=false disarmed=false) {
"ticket": "PMAT-3524",
"head": "4e0d1c69339e73cde472fe26d5770d91cefe2abd",
"width": 3,
"executor": "agy",
"agreed": true,
"auto_merge": {
"checked": true,
"was_armed": false,
"disarmed": false,
"note": "auto-merge not armed"
},
"lanes": [
{
"lane": 1,
"verdict": "PASS",
"findings": 0
},
{
"lane": 2,
"verdict": "PASS",
"findings": 2
},
{
"lane": 3,
"verdict": "PASS",
"findings": 2
}
]
} |
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
noahgift
enabled auto-merge
September 19, 2026 09:54
|
§13.11 rung 1 — quorum shadow verdict Shadow mode: this records a verdict and merges nothing. A refusal |
This was referenced Sep 19, 2026
noahgift
pushed a commit
that referenced
this pull request
Sep 19, 2026
…tract::all, and the ladder receipts of #3523 as witnesses The reconciliation this branch carried on a scratch branch is now the rebase: extract::all is the ONE walk the shapes gate and pv extract share (pv_contract -> json per document -> gguf -> apr_model -> receipts::read_all -> resolve), ExtractFailure carries both a json declaration fault and a receipt schema fault, and ShapesOutcome::ExtractFailed maps both to exit 3. Measured on this head, with #3523 receipts on main: pv lint contracts --gate shapes Pass, shapes_n 3, focus_nodes_n 1741, violations 0, WITNESSES 16, armed [ladder-measured, ont-shapes-v1], reported [ladder-green], by_entity_type.gguf 8, pc_extract gguf+apr-model fired; pv extract contracts 9582 triples; aprender-contracts lib 1645/1645; ont4c1_model_receipts 12/12; ont_extract_json 7/7; ont4b_shapes_gate 11/11; check_ont_ratchet.sh PASS; clippy -D warnings clean. Pmat-Ticket: PMAT-3508 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
noahgift
pushed a commit
that referenced
this pull request
Sep 19, 2026
noahgift
pushed a commit
that referenced
this pull request
Sep 19, 2026
…ymbol/ and world/ roots), 16 vendored W3C SHACL-Core cases run by the gate, the pinned oracle differential out of gate
extract:code walks the BOUND symbols only — every module_path + function a binding.yaml declares — through a syn module-tree walk (inline mods, file mods, #[path], one re-export hop, impl methods, both [package] and [lib] crate names, a facade and the crate it re-exports tried in order). Fail-closed IN THE GRAPH: a symbol the walk cannot find is still an ont:Symbol with sym:resolved false and sym:unresolvedReason naming the file and the segment, so a ghost binding is a violation naming the symbol instead of a smaller graph. Measured on this tree: 270 bound symbols, 169 resolved, 101 genuinely absent.
extract:lean reads the in-tree theorems through ONT-2a's own scan and rule (a file carrying `sorry` grounds nothing), joins them to the contracts that cite them by ONT-2a's name forms, and counts references that name nothing (lean_refs_unresolved) rather than guessing. 410 statements on this tree.
The W3C arm is two-sided. 16 of ONT-0's 32-case table are translated into the contract dialect and RUN BY THE GATE every time (ontology::w3c); the other 16 are listed by name with the form that puts them outside the subset, so the count is over the cases the subset claims and a case refused by design is never scored as a failure. A failing case declines Unknown{Differential} — never a corpus verdict. tests/oracle/ is a scratch crate DETACHED from the workspace with shacl pinned =0.3.21 (ONT-0's verdict ORACLE, R-13 release gate only); `make oracle` validates the ORIGINAL case files and the real corpus through it and writes the tracked tests/oracle/differential.json (17 cases, 0 disagreements). A planted sh:minCount change in shapes.ttl makes it disagree — measured.
Four conformance fixes the cases and the oracle found in the in-house validator:
- sh:class and targetClass use the rdfs:subClassOf closure (SHACL 2.1.1; W3C class-001), through one index per validate() instead of a scan per node — the corpus gate went 27.2s -> 6.9s in the same commit.
- sh:datatype checks the lexical form is WELL FORMED for the type ("300"^^xsd:byte is a violation; W3C datatype-ill-formed).
- sh:node reports ONE result per failing value on the outer path, with the nested findings as its detail (W3C node-001/-002).
- sh:in is TERM equality: an entry carries the datatype its YAML scalar gives it and the export writes it typed. Before, `in: ["true"]` accepted "true"^^xsd:boolean, which the oracle refuses — 490 results of difference on the real corpus, which is how it was found.
Sigma: code and lean implemented: true, concepts Symbol and Statement. The shapes bound-symbols-resolve and lean-statements-grounded ship COMPUTED AND REPORTED, not armed (§3.9): 101 ghosts and three admitted theorem files exist on main today, and a gate red on its own target the day it merges trains bypass. Arming is one string in lint-baseline.json for the release that cleans them.
check_ont_ratchet.sh, two defects fixed with rows that go red without the fix: entity_types_registered and extractors_implemented grepped the Rust for `EntityType::` and `impl Extractor`, two forms this codebase has never used, so both measured 0 while the baseline carried 1 and 1 from an older tree — they now read Sigma; and `--write` DELETED formal_prose and legacy_unresolved_depends_on, two shrink-only ratchets the sigma and relations gates read from that same file, so updating one ratchet disarmed two others. Self-test 17 -> 23 rows.
Known red, all three the same inherited assertion and none of them this row's: lint_passes_on_real_contracts, ont4b_shapes_gate::the_repo_corpus_passes_..., ont4c1_model_receipts::the_repo_corpus_reports_... assert the real corpus PASSES, and the armed ladder-measured finds 0 witnesses until the re-measured receipts of #3523 are on main (#3526's waiting note). Proven by measurement: with ladder-measured unarmed for one run the same corpus is Pass, 0 violations, 113 reported.
Pmat-Ticket: PMAT-3509
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
noahgift
pushed a commit
that referenced
this pull request
Sep 19, 2026
…n) — ordinal 343, the sh:in message carries the path AND the terms, regenerated census / contracts.nt / tree-reader registry (Refs PMAT-3509) The branch was built on the reconciled 4c1 scratch base; only its two own commits were replayed (`git rebase --onto origin/main bd89c88`). One real conflict, shapes.rs check_lexical: #3530 put the property path at the front of the `in` message (`ont:study/scale: quadratic is not one of …`) and 4b2 renders the value and the list as TERMS (`sh:in` is term equality). Merged: `<path>: <term> is not one of [<terms>]` — #3530's CLI legs (contains path ∧ value ∧ "is not one of") and 4b2's still hold. The four generated files took main's copy and were regenerated with this tree's pv: `pv extract contracts --check` 0; sigma Pass, relations Pass, shapes Pass (shapes_n=5, focus_nodes_n=2318, symbols 169 resolved / 101 unresolved reported, W3C 16/16). Ordinal 340 was apr-cli-pixel-regression on main; 4b2 takes 343 (342 is 4c1's). Pmat-Ticket: PMAT-3509 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Replaces
evidence/dogfood/models/0.68.1/{lambda,gx10}.jsonwith receipts fromscripts/model_ladder.shat main a6f54e8 (the first main carrying #3507's per-rungsha256and #3511's four dense rungs),apr 0.68.1 (a6f54e84c), lambda RTX 4090 (cc 8.9) and gx10 GB10 (cc 12.1).forward_qwen35.rs:132assert 2048 ≠ 4096/4096/6144 (GQA inside GDN, #3346 root cause)Why commit a red receipt: every rung is
present,sha_ok, and carries the measuredsha256— the witness the ontology'sladder-measuredshape (ONT-4c1, #3508) needs tracked on main the day it is armed;ladder-greenstays unarmed until the bump (#3498) and will name exactly these rungs. The T-2 judge (check_model_ladder.sh) is not a PR check, so this changes no gate. Two cosmetic ladder defects seen in this run, filed separately: the "why" block prints a blank reason whenapr qacrashed (rc 101), and the optional 8B rung's Empty output on lambda persists.Closes #3524
keep-open: #3510 (closes when the five dense rungs are green), #3477 (epic closes at the tag), #3346 (dense-sizes branch), #3486
ont-delta: none — evidence files only
🤖 Generated with Claude Code