Skip to content

Commit 644119a

Browse files
spec: V17, demonstration and testing surfacing proof progress
(Rolled with v17 wips) V17 work-in-progress progression and the final staged closure into one canonical ENGI V17 demo-canon / operator cross-product pass since 18f5a2e. Promote V17 as the active ENGI canon focused on proving the V16 system through demonstrable operator workflows, executable tests, and browser-visible parity rather than by introducing new proof families. Advance ENGI_SPEC.txt to V17 and align the V17 specification, notes, and system parity matrix around demo-driven proof closure. Close the V17 acceptance shape around operator-facing cross-product coverage: eight canonical demo scenarios, two branch modes, and four projection principals, exercised as a 64-cell browser matrix. Treat that matrix as V17 canon, with the larger semantic proof-member and theorem-evidence cross-products explicitly deferred into V18 notes as generated/formal expansion work. Add the branch-mode operator seam to the demo UI and API flow. The browser now exposes patch and context branch modes, sends the selected branch mode into ENGI branch creation, renders the selected mode in the operator summary, and validates both modes across every scenario and projection principal. Tighten the public/reviewer/operator demonstration experience. The UI now renders exact projection-visible proof inventories, recovers the latest bundle summary for reviewer/public projections, surfaces raw projection visibility data for assertions, and preserves operator clarity across scenario selection, projection changes, branch-mode changes, reset, invalid deposit recovery, and no-survivor failure paths. Expand executable V17 coverage around the current specification surface: seeded HTTP/API scenario validation, source-backed and raw deposit flows, repo-auth provenance, mixed deposit normalization, restrictive unsafe patch behavior, prompt/inference synthesis, static and verification proof artifacts, selection and materialization, authorization and sensitive-flow boundaries, disclosure boundaries, settlement exactness, repeated runs, reset behavior, and no-survivor recovery. Update the canonical runtime coverage report so generated proof surfaces describe the V17 test posture directly: 112 total tests, full operator-facing browser matrix coverage, exact projection artifact inventory assertions, and continued proof-family contract coverage over the V16 proof system. Regenerate the V17 _PROVEN_ appendix as a generated-only canonical artifact: ENGI_SPEC_V17_PROVEN.md records the V17 proof inventory from the proof-bearing runtime surfaces, including 9 proof families, 45 members, 57 theorem entries, 16 scenario/branch runs, and 688 artifact digests. The file is not manually edited; it is regenerated for the canonical version commit and checked deterministically. Add ENGI_SPEC_V18_NOTES.md to preserve the intentionally deferred next work: generated semantic proof-member matrices, generated theorem-evidence matrices, state-machine/repeated-run expansion, broader visual/accessibility/runtime budgets, and deeper formal proof exhaustiveness beyond V17's accepted operator-facing canon. Verification: npm run typecheck npm test node scripts/generate-engi-proven.mjs --version V17 --commit d418ec9 --output ENGI_SPEC_V17_PROVEN.md --allow-dirty node scripts/generate-engi-proven.mjs --version V17 --commit d418ec9 --output ENGI_SPEC_V17_PROVEN.md --check --allow-dirty
1 parent d418ec9 commit 644119a

10 files changed

Lines changed: 2821 additions & 52 deletions

ENGI_SPEC.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
V16
1+
V17

ENGI_SPEC_V17.md

Lines changed: 36 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
- Prior canonical anchor: `/Users/garrettmaring/Developer/ENGI/ENGI_SPEC_V16.md`
99
- Current canonical/latest target: `V16`
1010
- Last fully realized canon preserved in source: `V16`
11-
- V17 state: advanced draft implementation/audit exhaustion; not yet the canonical pointer target
11+
- V17 state: implementation-complete demo-canon draft; pending canonical promotion and `_PROVEN_` regeneration
1212
- Current realization basis for this pass: `engi-demo`
1313

1414
## Version executive summary
@@ -64,24 +64,24 @@ but also:
6464
- do the sub-systems compose in realistic operator workflows,
6565
- and do tests fail at the same seams where demo truth breaks.
6666

67-
## Current V17 drafting scope
67+
## Current V17 implementation scope
6868

69-
This pass begins with:
69+
This pass is grounded in:
7070
- a canonical test-stack model for ENGI,
7171
- a demo-driven implementation posture for `engi-demo`,
7272
- explicit layering between subsystem unit tests, workflow integration tests, and fully interfaced browser E2E tests,
7373
- identification of the current gaps between V16 proof closure and V16 demonstrability,
74-
- and the first implementation ratchets needed to make that layered posture real in source.
74+
- and the implementation ratchets needed to make that layered posture real in source.
7575

76-
The following are intentionally out of scope for the opening V17 pass:
76+
The following remain intentionally out of scope for V17:
7777
- introducing a new proof-family canon distinct from V16,
7878
- replacing the V16 proof appendix model,
7979
- or broadly rewriting the root system model before demonstration gaps are surfaced by tests.
8080

8181
The correct reading is:
8282
- V16 remains active canon,
83-
- V17 starts as the next canon draft,
84-
- and the first V17 job is to make V16 demonstrable and test-ratcheted enough that new gaps appear through real execution rather than speculation.
83+
- V17 is the next canon draft,
84+
- and the V17 job is to make V16 demonstrable and test-ratcheted enough that new gaps appear through real execution rather than speculation.
8585

8686
## V17 test-stack rule
8787

@@ -209,6 +209,7 @@ The current source state now includes:
209209
- runtime `testCoverageReport` taxonomy updated to `unit` / `integration` / `e2e`,
210210
- a dedicated `engi-demo/test/workflow.integration.test.js` suite,
211211
- a browser shell aligned to the canonical V16 operator posture rather than the older V15-facing labeling,
212+
- a browser branch-mode selector so operator runs can exercise both `patch` and `context`,
212213
- projection visibility and proof-family catalog surfaces in the demo UI,
213214
- direct browser-visible audit surfaces for prompt-family registry, prompt contracts, inference moment contracts, inference proofs, parsed completion envelopes, prompt/inference family proofs, static reports, verification/selection/auth/disclosure family proofs, and settlement source-to-shares proof,
214215
- public suppression of hidden private source-material path enumeration while retaining bounded visibility counts,
@@ -245,6 +246,8 @@ The current source state now includes:
245246
- browser-visible no-survivor conflict recovery,
246247
- browser-visible reset after a realized run,
247248
- browser-visible repeated scenario runs without reset,
249+
- full browser operator-facing cross-product coverage across `8` scenarios, `2` branch modes, and `4` projection principals,
250+
- exact browser-visible projection artifact inventory checks from `projectionPolicy` across that `64`-cell matrix,
248251
- and deeper unit replay-catalog closure over proof families, witness paths, and emitted branch artifacts.
249252

250253
The current V17 audit also exposed and fixed a source-side documentation/runtime seam: `ENGI_NEED.md` was still returning an older markdown body before the V16 prompt-completeness additions. It now renders failure modes, constraints, target artifact kinds, and closure criteria from the same prompt/inference surfaces that prove those fields.
@@ -261,18 +264,39 @@ The V16-generated appendix remains the canonical model for proof appendix produc
261264

262265
This pass therefore specifies the V17 `_PROVEN_` rule but intentionally does not create a draft generated appendix.
263266

267+
## V17 cross-product exhaustion rule
268+
269+
V17 should make its remaining exhaustiveness explicit through named assertion matrices rather than through open-ended "more coverage" language.
270+
271+
The accepted V17 source/runtime and operator-facing finish line is:
272+
- `8` seeded scenarios x `2` branch modes = `16` source branchability cells,
273+
- `8` seeded scenarios x `2` branch modes x `4` principals = `64` HTTP projection cells,
274+
- `9` proof families x `8` seeded scenarios x `2` branch modes = `144` proof-family structural cells,
275+
- `45` proof-family members x `8` seeded scenarios x `2` branch modes = `720` member identity/passing cells,
276+
- `57` proof-family theorems x `8` seeded scenarios x `2` branch modes = `912` theorem identity/passing cells,
277+
- `57` projection-policy artifact paths x `8` seeded scenarios x `2` branch modes = `912` public projection exactness cells,
278+
- and `8` seeded scenarios x `2` branch modes x `4` principals = `64` browser operator cells with exact visible artifact inventory assertions.
279+
280+
The remaining generated/formal cross-products are deferred to V18:
281+
- `720` member semantic payload cells,
282+
- `912` theorem-specific evidence cells,
283+
- generated non-public projection source/integration matrices beyond the accepted browser exactness,
284+
- and stateful workflow cross-products for repeated-run pairs, reset-after-run scenarios, mixed-deposit cells, and no-survivor conflict cells.
285+
286+
The system parity matrix is the canonical location for the detailed arithmetic and the concrete remaining permutation list.
287+
264288
Current verification state for this pass is:
265289
- `npm run typecheck`
266290
- `npm run test:unit`
267291
- `npm run test:integration`
268292
- `npm run test:e2e`
269293
- `npm test`
270294

271-
All are green in the current worktree, with `111/111` tests passing in the full suite after the latest audit ratchets.
295+
All are green in the current worktree, with `112/112` tests passing in the full suite after the latest audit ratchets.
272296

273-
## V17 opening success condition
297+
## V17 completion condition
274298

275-
The current V17 pass is in good shape when:
299+
The current V17 pass is complete when:
276300

277301
1. the root V17 draft states the demo-driven and test-layered posture explicitly,
278302
2. the notes explain why V17 starts from demonstration instead of more proof-family invention,
@@ -282,4 +306,5 @@ The current V17 pass is in good shape when:
282306
6. the seeded scenario corpus is exercised through realistic HTTP workflows across both `patch` and `context`,
283307
7. exact proof-family names, proof artifact paths, member ids, and theorem ids stay stable through that workflow layer,
284308
8. the browser shell truthfully demonstrates canonical V16 proof, projection, and settlement surfaces,
285-
9. and V16 proof closure remains the base system contract while V17 keeps surfacing bugs through actual workflows rather than speculative review alone.
309+
9. the browser operator matrix covers all `64` scenario/branch/principal cells with exact projection visibility checks,
310+
10. and V16 proof closure remains the base system contract while V17 keeps surfacing bugs through actual workflows rather than speculative review alone.

ENGI_SPEC_V17_NOTES.md

Lines changed: 40 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -65,13 +65,13 @@ Practically, V17 should use them to ask:
6565
- which proof/artifact/operator seams are still only lightly tested,
6666
- and where a bug would currently hide because there is no integration or e2e ratchet on the seam.
6767

68-
## Current V17 observations after the opening pass
68+
## Current V17 observations after completion pass
6969

7070
The current audit pass shows:
7171

7272
1. There is now strong subsystem coverage in `engi-demo/test/core.test.js`, and it is materially operating as the canonical unit layer.
7373
2. `engi-demo/test/api.test.js` is better separated from workflow integration than it was at the opening pass, though it still carries some workflow-adjacent coverage.
74-
3. `engi-demo/test/e2e.test.js` now covers a materially broader set of operator flows, including projection visibility, raw proof inspection, failure feedback, and reset behavior.
74+
3. `engi-demo/test/e2e.test.js` now covers a materially broader set of operator flows, including projection visibility, raw proof inspection, failure feedback, reset behavior, branch-mode switching, and the full `64`-cell operator matrix.
7575
4. Runtime `testCoverageReport` now encodes the explicit V17 `unit` / `integration` / `e2e` stack honestly.
7676
5. The demo already has realistic ingredients for integration and E2E testing:
7777
- authenticated repo artifact selection,
@@ -83,7 +83,7 @@ The current audit pass shows:
8383
- and bounded-public versus replay-capable proof visibility.
8484
6. The V16 spec and parity matrix already identify strong candidate audit areas, and V17 is now materially converting those guided seams into executable ratchets rather than leaving them as review-only guidance.
8585

86-
This means V17 is no longer only “ready to start source-side.” It is already in the stage where the remaining work is to keep exhausting the inherited V16 audit surface through more scenario/principal/workflow depth.
86+
This means V17 is no longer only “ready to start source-side.” It is implementation-complete as a demo-canon draft, with generated/formal and state-machine exhaustiveness intentionally deferred to V18.
8787

8888
## V17 drafting posture
8989

@@ -110,14 +110,14 @@ V17 starts from:
110110

111111
## Initial V17 debts in view
112112

113-
The current debts after this pass are:
113+
The current debts after this pass are deferred to V18:
114114

115-
1. V16 audit inheritance is materially executable, but not yet generated as every possible family/member/scenario/principal/operator cross-product assertion.
116-
2. Integration workflows are first-class now, but `api.test.js` still carries limited workflow smoke checks that can migrate if a pure endpoint-boundary suite becomes required.
117-
3. Runtime-emitted coverage metadata is honest again after the latest ratchets, but it must continue changing whenever the suite taxonomy changes.
118-
4. E2E flows cover the highest-risk happy, projection, proof-inspection, failure, recovery, and repeated-run paths, but not every seeded scenario and proof/artifact surface.
119-
5. Projection differences are exercised across the full seeded HTTP corpus and representative browser surfaces, but not every proof/artifact UI surface has been demonstrated across every principal.
120-
6. V17 `_PROVEN_` generation remains deferred until canonical promotion; draft edits should only specify and test the generation rule.
115+
1. Generated proof-member semantic payload assertions.
116+
2. Generated theorem-specific evidence assertions.
117+
3. Full state-machine cross-products for repeated runs, reset, mixed deposits, and no-survivor conflicts.
118+
4. Optional endpoint/API suite purity cleanup.
119+
5. Optional visual regression, accessibility, and browser performance budgets.
120+
6. V17 `_PROVEN_` generation, which remains deferred until canonical promotion.
121121

122122
## Initial V17 target
123123

@@ -127,7 +127,28 @@ The first clean V17 move was:
127127
- reflect that taxonomy in source-side test scripts and runtime coverage reporting,
128128
- and add explicit closer-to-real workflow integration paths so the integration layer is not only a naming change.
129129

130-
That target is now satisfied for the opening V17 posture. The remaining question is whether V17 acceptance requires cross-product generation beyond the current high-risk exhaustive surfaces.
130+
That target is now satisfied for V17. V17 accepts full operator-facing cross-product coverage as canon and defers generated/formal proof/state-machine expansion to V18.
131+
132+
## Cross-product matrix notes
133+
134+
The parity matrix now details the exact V17 exhaustion arithmetic.
135+
136+
The important distinction is:
137+
- source/runtime matrices are closed for V17,
138+
- browser matrices are now full cross-product for V17 operator canon,
139+
- stateful matrices are representative and intentionally not every scenario pair,
140+
- and proof-family matrices are structurally closed while full member/theorem semantic payload equality is deferred as a generated-expansion target.
141+
142+
The main remaining permutation groups are:
143+
- `720` proof-member semantic payload cells,
144+
- `912` theorem-specific evidence cells,
145+
- generated source/integration duplication of non-public projection artifact visibility cells if V18 wants them outside browser,
146+
- `63` repeated-run ordered scenario pairs,
147+
- `7` reset-after-run scenario cells,
148+
- `63` mixed-deposit scenario/branch/principal cells,
149+
- and `62` no-survivor scenario/branch/principal cells.
150+
151+
Those are not V17 blockers. They are listed so V18 can make a deliberate acceptance decision rather than treating "exhaustion" as unbounded.
131152

132153
## Current implemented V17 state
133154

@@ -139,7 +160,10 @@ The repo now has:
139160
- a dedicated `workflow.integration.test.js` suite,
140161
- a demo shell aligned to canonical V16 rather than older V15-facing operator labeling,
141162
- a browser-visible projection visibility summary and proof-family catalog,
163+
- a browser-visible branch-mode selector for `patch` and `context`,
142164
- browser-visible first-class audit surfaces for prompt-family registry, prompt contracts, inference moment contracts, inference proofs, parsed completion envelopes, prompt/inference family proofs, static measurement report/proof, verification decisions proof, selection/materialization proofs, authorization/sensitive-flow proof, projection policy, redaction/disclosure proofs, and settlement/disclosure family proofs,
165+
- a full `8 x 2 x 4 = 64` browser operator matrix over every seeded scenario, branch mode, and projection principal,
166+
- exact browser-visible projection artifact inventory assertions from the active projection policy across that matrix,
143167
- public suppression of hidden source-material path enumeration while still surfacing bounded counts,
144168
- reviewer-visible replay/proof artifacts without raw source-material exposure,
145169
- a full seeded scenario-corpus HTTP workflow audit across both `patch` and `context` branch modes,
@@ -177,7 +201,9 @@ The repo now has:
177201
- browser-visible invalid-to-valid deposit recovery,
178202
- browser-visible no-survivor conflict recovery,
179203
- browser-visible reset-after-run behavior,
180-
- browser-visible repeated scenario runs without reset,
204+
- browser-visible repeated scenario runs without reset,
205+
- browser-visible branch-mode switching,
206+
- browser-visible all-scenario/all-branch/all-principal operator matrix coverage,
181207
- and unit replay-catalog closure across proof families, witness artifacts, and verifier-required artifact paths.
182208

183209
This is the right shape for the beginning of V17 because it is already doing what the version is supposed to do:
@@ -192,8 +218,8 @@ The current verification state is also materially stronger than the opening pass
192218
- `npm run test:unit` is green,
193219
- `npm run test:integration` is green,
194220
- `npm run test:e2e` is green,
195-
- and `npm test` is green at `111/111`.
221+
- and `npm test` is green at `112/112`.
196222

197223
V17 `_PROVEN_` generation is intentionally not performed in this draft state. The V16 generated appendix remains the model, and V17 should regenerate `ENGI_SPEC_V17_PROVEN.md` only on the eventual canonical version-promotion commit after implementation/parity closure is accepted.
198224

199-
That does not mean V17 is finished. It means the version has moved from “opening posture established” to “advanced, demonstrable, and now ready to decide whether the remaining work is cross-product exhaustiveness, browser-level proof-surface completeness, or canonical promotion preparation.”
225+
V17 is implementation-complete as a demo-canon draft. The remaining work is canonical promotion mechanics, including regenerated `_PROVEN_`; V18 carries the next generated/formal exhaustiveness ideas.

0 commit comments

Comments
 (0)