docs(verification): record post-merge DSL status

adr/verification/008-milestone-c3-productive-recursive-adts.md

@@ -1,6 +1,6 @@
 # ADR-008: Milestone C.3 — Productive Recursive ADTs
 
-- **Status:** Implemented on feature branch; pending manual review
+- **Status:** Implemented, manually reviewed, and integrated
 - **Date:** 2026-08-12
 - **Feature branch:** `feat/verification-c3-productive-recursion`
 - **Related:**

adr/verification/012-milestone-c6-stateful-spending-profile.md

@@ -1,6 +1,6 @@
 # ADR-012: Milestone C.6 Stateful Spending Profile v1
 
-- **Status:** Implemented; pending manual review
+- **Status:** Implemented, manually reviewed, and integrated
 - **Date:** 2026-08-13
 - **Related:**
   [ADR-007 — Java-Annotation Security Properties](007-java-annotation-security-properties-and-one-command-verification.md),

adr/verification/013-milestone-c7-controlled-minting-profile.md

@@ -1,6 +1,6 @@
 # ADR-013: Milestone C.7 Controlled Minting Profile v1
 
-- **Status:** Implemented; pending manual review
+- **Status:** Implemented, manually reviewed, and integrated
 - **Date:** 2026-08-13
 - **Related:**
   [ADR-007 — Java-Annotation Security Properties](007-java-annotation-security-properties-and-one-command-verification.md),

adr/verification/016-typed-verification-dsl-and-profile-catalog.md

@@ -707,7 +707,8 @@ See [ADR-026](026-milestone-e4k-typed-governance-transaction-data.md).
 ### E.4l: Reviewed raw-data adapters
 
 [ADR-027](027-milestone-e4l-reviewed-raw-data-adapters.md) implements this
-phase as opt-in property schema 10. It separates pinned-decoder from
+phase under the unreleased milestone property schema 10. It separates
+pinned-decoder from
 canonical validity-range semantics, models treasury optionals as the three
 distinct states present/absent/malformed, and permits only narrow
 duplicate-preserving views of changed-parameter IDs and structurally pinned
@@ -725,8 +726,10 @@ k-induction. It was rejected at the mandatory calibration gate: even an
 396-byte validator whose Java body returns true, with no ledger-domain premise,
 could not establish depth-1 target reachability within five minutes under the
 combined direct exact-artifact transition encoding. The product-facing
-prototype was removed, so schemas 1 through 10 and existing CLI/result meanings
-remain unchanged.
+prototype was removed, so the then-current milestone schemas 1 through 10 and
+CLI/result meanings remained unchanged. E.6 subsequently replaced those
+unreleased milestone gates with the public canonical
+`julc.verification.dsl` schema 1 contract.
 Any future temporal-verification attempt needs a materially different,
 separately reviewed execution-linkage strategy.
 
@@ -745,8 +748,10 @@ Stabilize the DSL only if the experiments demonstrate:
 Otherwise retain annotations/profiles as the product interface and the
 canonical IR or generated Lean workspace as the expert extension surface.
 
-Decision: the E.4 schema-10 construction surface is stable as verification DSL
-API version 1 under [ADR-029](029-milestone-e6-stable-verification-dsl-public-api.md).
+Decision: the complete reviewed E.4 construction surface is stable as
+verification DSL API version 1 and public canonical
+`julc.verification.dsl` schema 1 under
+[ADR-029](029-milestone-e6-stable-verification-dsl-public-api.md).
 Annotations are concise frontends over the same canonical DSL guarantee IR;
 profile-specific handwritten Lean predicates are not retained. E.5 is excluded.
 
@@ -818,6 +823,8 @@ entries and explicitly state whether equality is structural or extensional.
 ## Exit condition
 
 The E.4b compositional exit condition and the later purpose/type/value adapter
-gates have been met. ADR-029 freezes the resulting schema-10 public API without
-claiming complete CardanoLedgerApi coverage. New semantic vocabulary requires a
-new reviewed property schema and must preserve schemas 1 through 10.
+gates have been met. ADR-029 freezes the resulting API version 1 and public
+canonical `julc.verification.dsl` schema 1 without claiming complete
+CardanoLedgerApi coverage. New semantic vocabulary requires a new reviewed
+public property schema; the unreleased milestone schemas 1 through 10 are
+historical evidence formats, not supported compatibility inputs.

adr/verification/017-purpose-indexed-multivalidator-blueprints.md

@@ -1,6 +1,6 @@
 # ADR-017: Purpose-Indexed CIP-57 Blueprints for `@MultiValidator`
 
-- **Status:** Implemented (pending manual review and commit)
+- **Status:** Implemented, manually reviewed, and merged through PR #84
 - **Date:** 2026-08-13
 - **Parent:**
   [ADR-005 — Compiler-Owned Blueprint Schemas](005-milestone-c1-compiler-owned-blueprint-schema.md)

adr/verification/019-milestone-e4b-compositional-property-promotion-core.md

@@ -1,6 +1,6 @@
 # ADR-019: Milestone E.4b Compositional Property Promotion Core
 
-- **Status:** Implemented experimentally; awaiting manual review
+- **Status:** Implemented experimentally, manually reviewed, and integrated
 - **Date:** 2026-08-20
 - **Feature branch:** `feat/typed-verification-dsl-e4b-composition`
 - **Parent:**

adr/verification/023-milestone-e4g-typed-non-value-transaction-context.md

@@ -1,6 +1,6 @@
 # ADR-023: Milestone E.4g — Typed Non-Value Transaction Context
 
-- **Status:** Implemented experimentally; awaiting manual review
+- **Status:** Implemented experimentally, manually reviewed, and integrated
 - **Date:** 2026-08-21
 - **Parent:**
   [ADR-016 — Typed Verification DSL and Foundational Profile Catalog](016-typed-verification-dsl-and-profile-catalog.md)

adr/verification/024-milestone-e4h-authorization-algebra.md

@@ -1,6 +1,6 @@
 # ADR-024: Milestone E.4h — Compositional Authorization Algebra
 
-- **Status:** Implemented experimentally; manual review pending
+- **Status:** Implemented experimentally, manually reviewed, and integrated
 - **Date:** 2026-08-21
 - **Parent:**
   [ADR-016 — Typed Verification DSL and Foundational Profile Catalog](016-typed-verification-dsl-and-profile-catalog.md)

adr/verification/025-milestones-e4i-e4j-certificate-payloads-and-value-algebra.md

@@ -1,6 +1,6 @@
 # ADR-025: Milestones E.4i–E.4j — Certificate Payloads and Value Algebra
 
-- **Status:** E.4i and E.4j implemented experimentally; E.4j manual review pending
+- **Status:** E.4i and E.4j implemented experimentally, manually reviewed, and integrated
 - **Date:** 2026-08-22
 - **Parent:**
   [ADR-016 — Typed Verification DSL and Foundational Profile Catalog](016-typed-verification-dsl-and-profile-catalog.md)

adr/verification/029-milestone-e6-stable-verification-dsl-public-api.md

@@ -1,6 +1,6 @@
 # ADR-029: E.6 stable verification DSL and annotation convergence
 
-- **Status:** Accepted; implemented on feature branch, awaiting review
+- **Status:** Accepted; implemented and merged through PRs #89 and #90
 - **Date:** 2026-08-23
 - **Integration branch:** `feat/typed-verification-dsl-e4`
 - **Schema-reset branch:** `feat/verification-dsl-schema-v1`
@@ -285,8 +285,9 @@ require separate ADRs and property-schema versions.
 
 ## Implementation outcome
 
-The pre-release schema reset is implemented on
-`feat/verification-dsl-schema-v1`.
+The pre-release schema reset was implemented on
+`feat/verification-dsl-schema-v1` and merged through PR #90 after the E.4/E.6
+integration branch landed through PR #89.
 
 - `VerificationDslApi` declares Java construction API version 1 and canonical
   property schema 1. No older canonical DSL schema is readable.

adr/verification/INTEGRATION-BRANCHES.md

@@ -7,16 +7,18 @@ decisions in the linked ADRs.
 ## Shared foundation
 
 - **Branch:** `main`
-- **Recorded point:** `bcfc3c7` (PR #86), superseded normally by later `main`
-  commits.
+- **Recorded point:** `5d67f04` (PR #90 merge), superseded normally by later
+  `main` commits.
 - **Included foundation:** C.1–C.7, managed local/Docker execution, strict
   `strict-data-v1` compiler boundaries, purpose-indexed CIP-57 blueprints, and
-  line-oriented verification progress. ADR-016 E.1 capability inventory, E.2
-  typed AST prototype, and E.3 seller-payment vertical slice are also landed.
+  line-oriented verification progress. ADR-016 E.1 through E.4l and E.6 are
+  landed; E.5 remains a rejected calibration rather than a product API. The
+  public verification construction contract is API version 1 with canonical
+  `julc.verification.dsl` schema 1.
 - **Rule:** new verification milestone branches start from current `main`
   after their prerequisite integration PR has landed.
 
-## Active integration branches
+## Completed integration branches
 
 ### Typed verification DSL E.4
 
@@ -31,16 +33,18 @@ decisions in the linked ADRs.
   `feat/typed-verification-dsl-e6-public-api`
 - **Completed final milestone ADR:**
   [ADR-029](029-milestone-e6-stable-verification-dsl-public-api.md)
-- **Current scope:** integration review and landing through PR #89.
-- **Current state:** E.4a through E.4l are merged into this integration branch.
+- **Landing:** PR #89 merged the E.4/E.6 integration branch; PR #90 merged the
+  public schema-1 reset and documentation.
+- **Final state:** E.4a through E.4l were merged into this integration branch.
   E.5 retained only its exact-artifact calibration result and did not promote a
   temporal product API; its scoped merge is `823f4e3`. E.6 was manually
   reviewed, committed as `4ba114f`, and merged into this integration branch as
-  `fbe2619`. Schema 10 is the stable API-v1 default and every annotation profile
-  lowers through canonical DSL IR before Lean generation.
-- **Next scope:** merge PR #89 into `main` after its integration checks and
-  review are complete. Further DSL semantics require a new property-schema ADR
-  rather than changing schema 10.
+  `fbe2619`. The complete reviewed surface is now stable as construction API
+  version 1 with public canonical `julc.verification.dsl` schema 1, and every
+  annotation profile lowers through canonical DSL IR before Lean generation.
+- **Next scope:** new verification work starts from current `main`. Further DSL
+  semantics require a new public property-schema ADR rather than changing
+  canonical schema 1 in place.
 
 Milestone work is developed on a dedicated feature branch and merged with a
 non-fast-forward merge into this integration branch. Existing examples are:
@@ -132,15 +136,16 @@ main (C.1-C.7 + strict boundaries + purpose-indexed blueprints + E.1-E.3)
           -> merged to E.4 integration after completed evidence and manual review
 ```
 
-Preferred landing sequence:
+Completed landing sequence:
 
-1. Keep completed E.4a–E.4l commits scoped and merged non-fast-forward into
+1. E.4a–E.4l were merged as scoped milestone commits into
    `feat/typed-verification-dsl-e4`.
-2. Keep E.5 outside the stable API until a later exact temporal calibration
-   passes a separately accepted ADR gate.
-3. Land the completed integration branch through PR #89.
-4. Keep compiler and blueprint work independent of the verification DSL unless
-   a separate accepted ADR changes that module boundary.
+2. E.5 stayed outside the stable API after its exact temporal calibration
+   failed the accepted gate.
+3. PR #89 landed the completed integration branch on `main`.
+4. PR #90 landed the canonical public schema-1 reset and documentation.
+5. Compiler and blueprint work remain independent of the verification DSL
+   unless a separate accepted ADR changes that module boundary.
 
 ## Maintenance rules