superJ PR-v1: TRUE

# PR-v1 — the SuperJ Readiness Contract (spec page) > Contract: `PR-v1 = C1 ∧ C2 ∧ C3`. Version: PR-v1 (2026-10-11). > Source: [READINESS-CERTIFICATION-PLAN.md](READINESS-CERTIFICATION-PLAN.md) (ticket #53), > [READINESS-CONTRACT-V3.md](READINESS-CONTRACT-V3.md). Evidence binding: the > provenance stamp (#37) — every cited run is stamped {plan_rev, sdk_version, > corpus_hash, git_rev}. > > Standing rule: the certificate is a claim, not a payload. Gates run in > `the certification repository`; the release embeds only the pointer. Refutation is local — > every command below is copy-paste runnable from the public tree. > > Status: APPROVED — owner approval recorded 2026-10-11 (superj > #5917 spec-authority rule; ticket the certification repository #63). This page is > normative: PR-v1 = C1 ∧ C2 ∧ C3 is the standing readiness contract. --- ## C1 — Spec conformance Claim: the implementation matches the spec as operationalized by the claims ledger — every normative manual claim has covering evidence, every test cites its contract, and the conformance kit passes. ### Checker commands python3 tools/spec-lint.py --strict # exit 0: 100% of language tests cite # a contract AND claims-ledger coverage # is complete python3 tools/jck-batch.py # exit 0: conformance kit, fails=0 python3 tools/metamorphic.py # exit 0: 60 programs, 4-way agreement ### Pass criterion - All three commands exit 0 on the release commit. - Every red conformance cell carries an open-or-closed ticket reference (the #39/#44 trail discipline); an untrailed red fails C1 outright. ### Evidence tier | Sub-item | Tier | |---|---| | claims-ledger coverage (92 claims) | TEST + ledger | | JCK-style conformance kit | TEST | | metamorphic differential | TEST | ### Boundary — what C1 does NOT prove - Tier-B/C ledger claims (manual prose without a mechanical oracle) are ledger-verified, not re-proved per release. - The JCK kit covers the Java-shared subset + documented divergences; it is not an exhaustive language-difference proof. - Metamorphic generation covers the Java-shared subset only (the #52 searcher gap). --- ## C2 — Soundness / no undefined behaviour Claim: safe SuperJ cannot reach undefined behaviour — every hazard class is closed by a named proof or a two-channel (static + runtime) instrument, and no finding has silently reopened. ### Checker commands python3 tools/formal-core.py # full-domain SMT laws + numeric model python3 tools/bounds-guard-formal.py # B1-B5: the emitted guard is exact python3 tools/stack-escape-formal.py # L1-L6: placement safety laws python3 tools/arena-lifetime-formal.py # A1-A7: reclamation + strictness laws python3 tools/partial-escape-formal.py # guarded-store semantics python3 tools/stop-protocol-formal.py # T1-T3: dispatch/lifetime law python3 tools/da-formal.py # definite assignment (JLS 16) python3 tools/utf8-formal.py # full-domain string round-trip python3 tools/wide-formal.py # i128/i256/i512 laws python3 tools/fp-formal.py # float semantics python3 tools/conservation-formal.py # builder/bitwriter conservation python3 tools/tv-core.py && python3 tools/tv-refine.py # translation # validation of emitted IR python3 tools/ub-inventory.py && python3 tools/ub-parity.py \ && python3 tools/ub-profile-matrix.py && python3 tools/ub-local-band.py python3 tools/diff-java.py # differential vs javac-11 python3 tools/sigsegv-audit.py # null-deref proof + residual ratchet python3 tools/exit-sweep.py # zero signal deaths, all binaries ### Pass criterion - Every command exits 0. - Ratchets hold: sigsegv residual ≤ its pinned bound (`docs/sigsegv-audit.json`); zero unclassified UB verdict flips (crater-diff classification); zero new-rare IR opcodes. - Monotone findings: every UB/parity/sanitizer finding is a ledger row (`docs/ub-findings-ledger.md`, ticket #69); a closed row that reopens fails C2. - Checker-P0 rule (normative): a defect in any checker invalidates every clause citing it — the audit defect class. A self-check failure (diag-grid, diag-silence, warn-grid, exit-sweep self-tests) renders C2 FALSE regardless of other evidence. ### Evidence tier | Sub-item | Tier | |---|---| | full-domain SMT laws (int32 etc.) | PROOF (z3, exhaustive) | | safety-law kernels (bounds/escape/arena/stop/DA) | PROOF (z3 + differential) | | translation validation (tv-core/tv-refine) | MEASUREMENT (per-function) | | UB matrix / parity / hostile-source | MEASUREMENT | | sigsegv residual | PROOF + audited residual | ### Boundary — what C2 does NOT prove - Translation validation checks emitted output, not the compiler itself. - Escape-analysis flow-completeness stays empirical (the EA ticket set); what is proved is verdict SOUNDNESS, not that every escape is caught. - Hostile-source fuzzing is sampled, not exhaustive. - `unsafe`-family access (SPEC 4.13, #5474) is out of scope for safe SuperJ. --- ## C3 — Garbage-freedom Claim: memory behavior is as documented — arena reclamation is exact and O(1), stack placement is safe (witness two-sidedness), and every SDK surface has a flatness verdict with zero UNMEASURED. ### Checker commands python3 tools/sdk-leak-cert.py && python3 tools/sdk-leak-gate.py # the SDK flatness ledger + gate python3 tools/mem-sweep.py # every suite binary under --mem-track python3 escape-grid/tools/escape-grid.py # 18+ shape grid python3 escape-grid/tools/store-grid.py # 37 cells, two-legged pins python3 escape-grid/tools/arena-grid.py # block grammar python3 escape-grid/tools/grade-audit.py # L5a ratchet (no witness-less # definite anywhere) python3 escape-grid/tools/corpus-grade-audit.py # corpus-wide L5a python3 escape-grid/tools/widening-ledger.py # every widening ranked, >2x # ratchet python3 escape-grid/tools/benchmark-trap-audit.py # ctor-buffer / trap audit ### Pass criterion - Every command exits 0 (pinned-red cells report PIN-RED + exit 0 per the ESC-PIN-RED convention; a pinned cell that PASSES means the fix landed — flip it). - Zero UNMEASURED SDK surfaces: the reconciliation (ticket #70) fails C3 if any ledger row lacks a verdict. - Every CARVEOUT row and every pinned-red cell is listed in the certificate boundary digest (never silently carried). ### Evidence tier | Sub-item | Tier | |---|---| | arena reclamation theorem | PROOF (A3) | | stack-placement safety + witness two-sidedness | PROOF (L-series) | | flatness verdict algebra | MEASUREMENT (N + 10N, touched-bytes gauge) | | grade-soundness audit | PROOF-shaped ratchet (L5a) | ### Boundary — what C3 does NOT prove - Shape-space completeness is empirical: the placement/arena oracles compose from verified-safe grammars; unknown-unknowns beyond the grammar are the #52 funnel's territory. - String bodies are site-invisible to the memlog (sj_str_alloc from C — the documented uncovered kind). - Exception objects are global by design (A6); documented rates (INTENTIONAL class) are not leaks. - Documented carve-outs (e.g. #4790) are permanent, listed in the boundary. --- ## Certificate semantics (normative, applies to all clauses) 1. An unrun gate renders FALSE, not unknown ("instrument absent" ≠ "passed"). 2. Every gate has a failing exit code; a check without one is a dashboard. 3. Ratchets over percentages; every "all X" denominator is cross-checked by a second mechanical means. 4. Pins flip when their tickets close; a pinned cell that passes means the fix landed — flip it the same day. 5. Evidence older than the expiry window, or built from a non-release commit, renders FALSE (schema: tickets #64/#65). 6. The boundary sections above ship VERBATIM in every certificate page; a page without them is marketing, not a certificate. ## Phasing - PR-v1 = C1 ∧ C2 ∧ C3 (this page). - PR-v2 ∧= C4 determinism (tail-shape gate, #71) ∧ C5 perf envelope (#72 — needs the canonical machine-class decision). - PR-v3 ∧= C6 round-trip replay (#73) ∧ full C7 standing machinery (#74/#75/#76). --- ## Pointer artifact format (version 1) The release embeds `readiness-cert.json` — a few hundred bytes, emitted by `tools/readiness-cert.py` (source of truth for this schema). Field order is normative; consumers must ignore unknown fields (forward compatibility): { "contract": "PR-v1", "status": "TRUE | FALSE", "clauses": {"C1": true, "C2": true, "C3": true, "C4": "not-gating | true | false", "...": "..."}, "failing_clauses": ["C2"], "problems": ["evidence: 91 days old (limit 90) - EXPIRED"], "evidence": { "generated": "YYYY-MM-DD HH:MM:SS", "age_days": 0, "sdk_version": "1.3.6514.d0ca143273 (enterprise)", "corpus_hash": "29f1cba3b6f2b8a5", "git_rev": "4db924c3..." }, "link": "https://superj.dev/readiness/PR-v1.html" } Consumer contract (superj release side): 1. `status != "TRUE"` ⇒ the release holds NO certificate claim; the pointer may still be embedded for transparency but must not be advertised. 2. `age_days` beyond the contract's expiry rule ⇒ treat as FALSE even if `status == "TRUE"` (defense in depth; the emitter already expires). 3. The `link` resolves to the full evidence page — the claim and its evidence stay one hop apart. Refutation is local: re-run the checkers from the public tree. 4. No test code, validators, or corpora ship in the toolchain. Upstream handoff: the consuming-side ticket in `superj` is filed ONLY after owner approval of this page (#63/#5917).

# C3 carve-out digest (generated by tools/c3-reconcile.py)

Totals: 3598 FLAT / 414 BOUNDED / 1054 CARVEOUT across 15 package ledgers (3126 declared surfaces, 0 unmeasured).

## Carve-outs per package

- crypto: 19 CARVEOUT (of 208 declared)
- http: 144 CARVEOUT (of 468 declared)
- io: 14 CARVEOUT (of 134 declared)
- json: 38 CARVEOUT (of 129 declared)
- lang: 18 CARVEOUT (of 287 declared)
- sci: 2 CARVEOUT (of 4 declared)
- sql: 5 CARVEOUT (of 22 declared)
- test: 11 CARVEOUT (of 79 declared)
- time: 6 CARVEOUT (of 52 declared)
- util: 270 CARVEOUT (of 1395 declared)
- all: 527 CARVEOUT (of None declared)

## Ticketed carve-outs and pinned cells (must travel with the certificate boundary)

- #4790: SDK-arena carve-out: precompiled callees route block-destined stores global (list-fresh-global ~80 B/iter)
- #5315: witness-less definite (L5a pinned row, corpus-grade-audit)
- #4960: cross-hashCode lookup flake (concurrent; FLAKE-LEDGER)
- #5383: --warn-retained never fires (warn-grid PIN-RED)
- #5384: println false positive under --warn-retained