wip v16

Author: geraldarthurdavis

ENGI_SPEC_TEMPLATEGUIDE.md

@@ -78,12 +78,14 @@ A full enriched ENGI release SHOULD normally include the following file family:
    The version-local drafting rationale, interpretation notes, numbering decisions, and clarification record.
 3. `ENGI_SPEC_VN_SYSTEM_PARITY_MATRIX.md`
    The primary parity/debt ledger between the system spec and current repository truth.
-4. `ENGI_SPEC_VN_INFORMATION_AUDIT.md`
+4. `ENGI_SPEC_VN_PROVEN.md`
+   The generated-only canonical proof appendix for the committed canonical version. This file MUST never be edited manually and MUST be regenerated as part of any canonical version commit.
+5. `ENGI_SPEC_VN_INFORMATION_AUDIT.md`
    Required when a version is materially recovering lost density, parity, or conceptual coverage from earlier canon.
-5. optional realization/demo family, for example:
+6. optional realization/demo family, for example:
    - `engi-demo/ENGI_DEMO_SPEC_VN.md`
    - `engi-demo/SPEC_VN_IMPLEMENTATION_MATRIX.md`
-6. optional parity-bearing adjunct files
+7. optional parity-bearing adjunct files
    Examples include host capability documents, architecture maps, or other structured reference artifacts that the canonical spec relies on directly.
 
 File-family rules:
@@ -95,6 +97,8 @@ File-family rules:
 6. If adjunct files are used as canonical parity surfaces, the spec or relevant matrix MUST name them explicitly and judge whether they are aligned.
 7. Notes and the system parity matrix MUST repeat the same pointer/latest-target vs last-fully-realized-canon interpretation as the main spec.
 8. When a realization/demo implementation matrix exists, its preferred filename under the realization root SHOULD be `SPEC_VN_IMPLEMENTATION_MATRIX.md`; longer demo-prefixed aliases MAY exist temporarily for compatibility but MUST NOT become the primary maintained path.
+9. When proof-family canon is part of the release, `ENGI_SPEC_VN_PROVEN.md` MUST be generated from proof-bearing runtime surfaces, not authored or edited as prose.
+10. A canonical version commit that advances `ENGI_SPEC.txt` or otherwise takes on canonical-version authority MUST include the regenerated `ENGI_SPEC_VN_PROVEN.md` file in that same commit.
 
 The system parity matrix is not optional bookkeeping for a serious release.
 It is the ledger that separates:

ENGI_SPEC_V15_PROVEN.md

@@ -60,15 +60,14 @@ This pass now covers:
 
 The following are still intentionally deferred:
 - theorem-family expansion beyond the current family-first pass,
-- proof appendix generation,
-- proof execution/audit orchestration,
-- and `_PROVEN_` file generation requirements.
+- and proof execution/audit orchestration beyond the now-implemented family appendix generation path.
 
 The correct reading is:
 - V15 remains active canon,
 - V16 is being drafted through proof-family-by-proof-family tightening,
 - `prompt-completeness` remains the most tightened family,
-- and the rest of the proof families are now opened deeply enough to support the next member and theorem passes.
+- the rest of the proof families are now opened deeply enough to support the next member and theorem passes,
+- and `_PROVEN_` generation is now part of the V16 canon contract with a realized generator path.
 
 ## Member-proof closure rule
 
@@ -3643,3 +3642,142 @@ What it now does have is:
 4. an initial witness-materialization and replay direction,
 5. an expected/realized/family-closure split,
 6. and a provisional member-coverage inventory.
+
+## 15. Generated `_PROVEN_` Appendix
+
+### 15.1 Canonical artifact identity
+
+V16 introduces a generated canonical proof appendix artifact:
+
+1. `ENGI_SPEC_VN_PROVEN.md`
+
+Where:
+
+1. `VN` is the canonical spec version being committed,
+2. the file is versioned alongside the canonical spec,
+3. and the appendix is part of canon rather than an optional report.
+
+### 15.2 Generated-only rule
+
+`ENGI_SPEC_VN_PROVEN.md` is not a hand-authored notes file.
+
+It must:
+
+1. be generated from proof-bearing source surfaces,
+2. be reproducible from the canonical commit being designated,
+3. never be edited manually,
+4. fail validation if its content diverges from the generator output for that commit,
+5. and be treated as invalid canon if it is hand-mutated after generation.
+
+The canonical intent is:
+
+1. spec prose defines what `_PROVEN_` must contain,
+2. source-side proof execution produces the proof surfaces,
+3. the `_PROVEN_` generator renders those surfaces into markdown,
+4. and the committed file is only the generated rendering of that proof state.
+
+### 15.3 Canonical regeneration rule
+
+`ENGI_SPEC_VN_PROVEN.md` must only be regenerated on canonical version commits.
+
+A canonical version commit is any commit that:
+
+1. introduces a new canonical spec version artifact,
+2. advances the canonical pointer to a new version,
+3. or otherwise declares a new canonical version as depended-on ENGI truth.
+
+For such a commit:
+
+1. `_PROVEN_` must be regenerated from that commit's proof surfaces,
+2. the regenerated `_PROVEN_` file must be included in the same commit,
+3. and a canonical version commit lacking the regenerated `_PROVEN_` file is invalid.
+
+For non-canonical commits:
+
+1. `_PROVEN_` should not be manually refreshed for incidental edits,
+2. and partial or speculative `_PROVEN_` updates are forbidden.
+
+### 15.4 Minimum proof inputs
+
+The `_PROVEN_` generator must consume proof-bearing runtime surfaces rather than prose summaries.
+
+Its minimum proof inputs must include:
+
+1. proof-family proof objects,
+2. theorem verdict catalogs,
+3. member verdict catalogs,
+4. artifact bindings,
+5. replay steps,
+6. system proof bundle proof-family catalog,
+7. system proof bundle verifier entrypoint replay catalog,
+8. proof witness manifest artifact digests,
+9. proof witness manifest keyed artifact and family indexes,
+10. deliverables manifest,
+11. policy release artifact classifications,
+12. and any canonical scenario/run matrix required to state what was actually executed.
+
+At minimum, the generator must be able to read:
+
+1. `.engi/system-proof-bundle.json`,
+2. `.engi/proof-witness-manifest.json`,
+3. each family-specific proof artifact named by the proof-family catalog,
+4. and the canonical spec/version metadata for the commit being rendered.
+
+### 15.5 Minimum rendered contents
+
+`ENGI_SPEC_VN_PROVEN.md` must be singularly reliable as the stable proof appendix for the committed canonical version.
+
+It must render at least:
+
+1. canonical version and canonical commit id,
+2. generator identity and generation timestamp,
+3. proof-family inventory,
+4. per-family member inventory,
+5. per-family theorem inventory,
+6. per-family theorem verdicts,
+7. family witness artifact paths,
+8. family replay artifact paths and replay step ids,
+9. keyed artifact digest inventory,
+10. disclosure classification relevant to proof artifacts,
+11. any scenario/run matrix needed to interpret proof execution coverage,
+12. all failing or incomplete verdicts if any exist,
+13. and an aggregate statement of whether the canonical version is fully proven under the current V16 proof contract.
+
+The appendix must prefer exact ids, hashes, paths, counts, and verdicts over prose paraphrase.
+
+### 15.6 Reliability rule
+
+`_PROVEN_` is only reliable when:
+
+1. every carried proof family is represented directly from the runtime proof-family catalog,
+2. theorem verdicts are rendered from proof objects rather than re-inferred by the markdown renderer,
+3. witness and replay sections are rendered from the declared artifact/replay bindings,
+4. keyed artifact digest data comes from the witness manifest rather than from filesystem inference,
+5. and the canonical commit id in `_PROVEN_` matches the commit whose proof surfaces were rendered.
+
+The generator must fail closed when:
+
+1. a required proof artifact is missing,
+2. a named family in the bundle lacks a proof object,
+3. the witness manifest is missing a keyed digest for a required artifact,
+4. replay catalogs disagree about required artifact paths,
+5. or canonical version metadata and rendered proof state do not match.
+
+### 15.7 Commit and templateguide ratchet
+
+V16 requires templateguide and canonical release process language to ratchet this behavior.
+
+The release ratchet is:
+
+1. when creating a new canonical version commit, regenerate `ENGI_SPEC_VN_PROVEN.md`,
+2. include the regenerated file in that same canonical commit,
+3. reject canonical commits where `_PROVEN_` is stale, missing, or manually edited,
+4. and treat `_PROVEN_` regeneration as part of canonical version materialization rather than post-hoc documentation.
+
+Example canonical-version commits that would require regeneration include commits such as:
+
+1. `8b1ccbc2481f80bc63d31a33901a463f3ea7028a`
+2. `c021b9e48d6387f2aad9aab804c836736ef8437b`
+
+The relevant rule is not those specific hashes.
+The relevant rule is that any commit taking on canonical-version authority must also carry the regenerated `_PROVEN_` appendix for that version.

ENGI_SPEC_V16.md

@@ -64,15 +64,15 @@ The current state after the member-tightening and theorem-catalog pass is:
 - every V15 proof family is open in V16 drafting,
 - every family now has member inventory plus member-closure criteria,
 - every family now has a current realization-basis theorem catalog and theorem-by-theorem closure reading,
-- and the next pass is no longer enumeration but theorem tightening, proof execution, and later appendix generation.
+- and the next pass is no longer enumeration but theorem tightening, proof execution, and then generated appendix formalization.
 
 That theorem-by-theorem pass is now present across the family layer.
 The current theorem-binding reading is:
 - every family now has realized theorem identifiers in source,
 - the spec now binds each family to its current realization-basis theorem catalog,
 - the parity matrix now carries theorem-by-theorem closure readings rather than theorem debt only,
 - every family now has realized proof-object field and artifact/replay-binding direction,
-- and `_PROVEN_` generation remains intentionally deferred until the rest of V16 proving work is finished.
+- and `_PROVEN_` generation is now ready to be formalized because the rest of the V16 proving layer has been tightened far enough to support it.
 
 ## Prompt-completeness parity debt collection method
 
@@ -314,14 +314,12 @@ It is a proof-family drafting wedge into V16, with some families tighter than ot
 
 ## What remains out of scope for now
 
-This pass still does not yet draft:
-- the cross-family theorem catalog beyond the now-realized family theorem sets,
-- `_PROVEN_` appendix generation,
+This pass still does not yet complete:
 - proof-program inventory beyond the family-first closure pass,
 - or the full V16 system spec rewrite.
 
-Those are still deferred on purpose.
-The proof families now come first so the same drafting and parity pattern can be pushed through every family before theorem and appendix work begins.
+The cross-family family theorem layer is now materially in place.
+That is why `_PROVEN_` is no longer deferred as a concept and is now backed by a realized generator path.
 
 ## Why static-code-analysis is the next family
 
@@ -925,12 +923,29 @@ All nine V15 proof families are now opened in V16 drafting at the same broad clo
 - and theorem-by-theorem closure reading tied to realized source theorem ids.
 
 The next work after this family pass is not to open more families.
-It is to translate this audited family layer into source-side implementation completion and proof execution, then only after that move into `_PROVEN_` appendix generation and broader proof-program inventory.
+It is to translate this audited family layer into source-side implementation completion and proof execution, and then use that tightened runtime surface to implement `_PROVEN_` appendix generation and broader proof-program inventory.
 
 The current audit conclusion is:
 
 1. every V15 proof family now has an explicit member inventory in the spec and parity matrix,
 2. every family member now also has explicit closure criteria and ratchetable debt language,
 3. every family now has a realized theorem catalog and theorem-by-theorem closure reading aligned to current source,
-4. the spec, matrix, and notes now consistently defer `_PROVEN_` until the rest of proving closure is finished,
-5. and the next productive move is source-side implementation completion rather than further family-level drafting.
+4. source-side theorem/proof execution tightening is now strong enough to support generated appendix work,
+5. `_PROVEN_` can now be specified as a generated-only canonical artifact rather than a deferred concept,
+6. and the generator plus canonical-commit regeneration ratchet can now be treated as realized source/process behavior rather than as a next-step note.
+
+## `_PROVEN_` interpretation
+
+The correct V16 reading for `_PROVEN_` is now:
+
+1. `_PROVEN_` is a canonical generated appendix, not a hand-maintained markdown note,
+2. it must render directly from proof-bearing runtime surfaces,
+3. it must never be edited manually,
+4. it must be regenerated when a commit takes on canonical-version authority,
+5. and the regenerated file must be committed in the same canonical version commit.
+
+The important operational consequence is:
+
+1. `_PROVEN_` is not part of everyday drift churn,
+2. `_PROVEN_` is part of canonical version materialization,
+3. and a canonical version commit without regenerated `_PROVEN_` should be treated as incomplete.

ENGI_SPEC_V16_NOTES.md

@@ -36,6 +36,8 @@ The opening V16 focus is:
 - family-member coverage within each proof family,
 - and the first family-specific closure tests required to support later V16 proof execution.
 
+That family-tightening and theorem-execution work is now far enough along that `_PROVEN_` generation can be treated as a concrete parity target rather than a deferred placeholder.
+
 ## Interpretation rule
 
 The correct V16 reading is:
@@ -51,7 +53,8 @@ For this drafting pass:
 - `inference-synthesis` is opened and theorem-shaped,
 - `static-code-analysis`, `verification-decisions`, and `selection-and-materialization` are now carried through theorem-by-theorem closure drafting,
 - `authorization-and-sensitive-flow`, `settlement-source-to-shares`, `disclosure-boundary`, and `proof-contract` are now also carried through theorem-by-theorem closure drafting,
-- and all nine V15 proof families are now inside the active V16 family pass.
+- all nine V15 proof families are now inside the active V16 family pass,
+- and `_PROVEN_` is now a valid implementation target for the next V16 canonical-output step.
 
 ## Member-tightening interpretation rule
 
@@ -4902,3 +4905,47 @@ Proof-contract is now complete enough in V16 drafting terms to continue later fa
 4. replay/witness direction exists,
 5. expected versus realized versus family closure ownership is now named,
 6. and family-member coverage is now enumerated.
+
+## `_PROVEN_` parity target
+
+### Canonical-output rule
+
+V16 now treats `ENGI_SPEC_VN_PROVEN.md` as a generated canonical-output target.
+
+Its parity requirement is:
+
+1. the appendix must be renderable from source-realized proof surfaces,
+2. it must not require hand-maintained family or theorem interpretation,
+3. and it must be strict enough that canonical commits can regenerate it deterministically.
+
+### Minimum source-side prerequisites
+
+The matrix now considers the following prerequisites materially required for `_PROVEN_` generation:
+
+1. every proof family emits theorem-bearing proof objects,
+2. every proof family exposes witness artifact paths and replay artifact paths,
+3. every proof family exposes replay steps with required artifact paths,
+4. the system proof bundle exposes a normalized proof-family catalog,
+5. the system proof bundle exposes a normalized verifier replay catalog and required-artifact set,
+6. the proof witness manifest exposes keyed artifact digests by path,
+7. the proof witness manifest exposes keyed proof families by family name,
+8. and proof-contract closure remains strong enough to summarize bundle and witness coherence rather than only naming them.
+
+### Canonical-commit regeneration rule
+
+The parity target for release process is:
+
+1. `_PROVEN_` is never edited manually,
+2. `_PROVEN_` is regenerated only when a commit takes on canonical-version authority,
+3. the regenerated `_PROVEN_` file is included in that same canonical commit,
+4. and a canonical version commit without regenerated `_PROVEN_` is parity-incomplete.
+
+### Current implementation reading
+
+The current implementation now satisfies the minimum proof-surface preconditions for that next step:
+
+1. proof-family theorem verdicts are no longer carried by unconditional `passed: true` placeholders,
+2. witness/replay closure is derived from artifact bindings and replay-step coverage,
+3. proof-contract is finalized against bundle and witness summaries,
+4. the system proof bundle carries a proof-family catalog plus verifier replay catalog,
+5. and the proof witness manifest carries keyed artifact and family indexes.