diff --git a/design-docs/README.md b/design-docs/README.md index a324e8b3..da746259 100644 --- a/design-docs/README.md +++ b/design-docs/README.md @@ -20,10 +20,11 @@ This folder contains planning and design documents for NTNT features. | [dd-060-ai-native-developer-experience.md](dd-060-ai-native-developer-experience.md) | πŸ“‹ Draft | AI-native developer experience roadmap | | [dd-061-interpreter-performance-roadmap.md](dd-061-interpreter-performance-roadmap.md) | πŸ”Ά In Review | Current-use-case performance roadmap: template contract cleanup, benchmark harness, automatic template cache, template loop/scope cleanup, call/lookup fast paths | | [dd-062-secure-compiled-extension-libraries.md](dd-062-secure-compiled-extension-libraries.md) | πŸ“‹ Draft | Secure compiled extension libraries: stdlib-grade Rust modules, signed module universes, build provenance, and app-enforced trust requirements | +| [dd-078-intent-verification-runtime.md](dd-078-intent-verification-runtime.md) | πŸ“‹ Draft | Project-neutral truthful Intent evidence, pure-NTNT verification, hermetic resources/providers, and a reusable adoption protocol; Larrimon migration is tracked in a separate consumer plan | | [language_comparison.md](language_comparison.md) | βœ… Complete | NTNT vs other languages | | [INTENT_DRIVEN_DEVELOPMENT.md](INTENT_DRIVEN_DEVELOPMENT.md) | βœ… Complete | IDD philosophy and workflow | | [INTENT_ASSERTION_LANGUAGE.md](INTENT_ASSERTION_LANGUAGE.md) | βœ… Complete | IAL spec v1.0.0 | -| [ial_vision_v2.md](ial_vision_v2.md) | πŸ“‹ Planning | Future IAL capabilities | +| [ial_vision_v2.md](ial_vision_v2.md) | πŸ“¦ Superseded in part | Historical IAL vision; DD-078 now owns execution, evidence, resource, and delivery sequencing | | [dd-037-concurrency-and-jobs.md](dd-037-concurrency-and-jobs.md) | πŸ”Ά In Progress | Concurrency primitives + job system (master roadmap) | | [background_jobs.md](background_jobs.md) | πŸ“¦ Archived | Original job system design (superseded by DD-037) | | [http_updates.md](http_updates.md) | πŸ“‹ Planning | HTTP library improvements | diff --git a/design-docs/dd-078-intent-verification-runtime.md b/design-docs/dd-078-intent-verification-runtime.md new file mode 100644 index 00000000..8c21dad1 --- /dev/null +++ b/design-docs/dd-078-intent-verification-runtime.md @@ -0,0 +1,1182 @@ +# DD-078: Intent Verification Runtime and Pure-NTNT Project Testing + +**Status:** Draft / architecture decision +**Authors:** Larri + Josh +**Created:** 2026-07-28 +**Origin:** General-purpose application-verification architecture, pressure-tested by the Larrimon audit +**Related:** [IAL v1](INTENT_ASSERTION_LANGUAGE.md), [IAL vision v2](ial_vision_v2.md), [DD-037: Concurrency and Jobs](dd-037-concurrency-and-jobs.md), [DD-062: Secure Compiled Extensions](dd-062-secure-compiled-extension-libraries.md), [DD-063: Language Assessment](dd-063-language-assessment.md), DD-077: Correctness Primitives for Durable Applications + +--- + +## 1. Decision + +Ntnt will grow a first-class **Intent Verification Runtime** that makes a production ntnt application testable as a pure ntnt project. This is the v0.6.0-and-later verification track; it is not patch-release work and it may span multiple feature releases. + +A pure ntnt project may still contain production assets and migrations in their natural formats, and it may depend on PostgreSQL, Redis/Valkey, Chromium, OCI containers, Git, network devices, and other external systems. The purity claim is narrower and useful: + +- application behavior and durable requirements are declared in `.intent`; +- project-owned executable verification is written in `.tnt`; +- resources, profiles, capabilities, and suite composition are declared in `ntnt.toml`; +- one ntnt command plans, executes, reports, and cleans up the verification run; +- project-local Bash, Python, JavaScript, SQL-only test harnesses, and ad hoc CI orchestration are unnecessary; +- specialist engines may remain behind typed, bounded ntnt providers, but their evidence is incorporated without pretending that annotation coverage is behavioral proof. + +The target CI command is: + +```bash +ntnt intent check . --profile full +``` + +The command MUST fail closed when required obligations are unbound, unexecutable, blocked, skipped without an allowed reason, stale, or failed. `@implements` is traceability, not evidence. + +This DD supersedes the execution roadmap in `ial_vision_v2.md`. That document remains historical context for term rewriting and Studio, but execution trust, resource ownership, and project verification come before additional visual tooling. + +--- + +## 2. Why this is needed + +Production applications routinely need verification across HTTP state, databases, migrations, queues, browser behavior, external protocols, project policy, lifecycle, and failure recovery. Ntnt currently has useful pieces, but not a general runtime that can plan those resources, execute typed cases, preserve authority boundaries, and report current behavioral evidence truthfully. + +Larrimon is the first reference adoption and a deliberately demanding pressure test: authenticated multi-tenant HTTP, PostgreSQL RLS, immutable evidence, durable jobs, scheduler races, browser reconciliation, migrations, provenance, network protocols, alerts, AI inference, multi-node control planes, retention, and eventual HA/on-prem operation. It validates the generalized mechanisms; it does not define their public names, schemas, semantics, or release boundaries. + +The [immutable Larrimon audit baseline](../plans/dd-078-larrimon-baseline.md) binds these findings to repository `https://github.com/larimonious/larrimon.git` at commit `ceadfd992d1435ac27afb054968ff5569d697ce1`. At that commit: + +- the application had seven `.intent` files with 20 features, 27 scenarios, and 38 outcome/assertion lines; +- five domain intent files contained 11 features but no scenarios or assertions; +- `.tnt` source had 37 `@implements` annotations and no `@supports` annotations; +- `tests/intent.sh` had 18 direct `ntnt run tests/...` invocations and no `ntnt intent check` invocation; +- annotation coverage could report 100% while every scenario remained unexecuted; +- 27 project-owned shell, Python, and JavaScript/MJS support/test programs totaled 4,149 lines, and 3 SQL-only test inputs added 400 lines, for 30 replacement artifacts/4,549 lines; the audited `tests/` executable/spec set totaled 4,935 lines versus 4,827 lines of non-test production `.tnt`; +- most compensating code was lifecycle, fixture, assertion, polling, concurrency, database, browser, or policy plumbing rather than product-specific reasoning. + +The baseline records every path, full-file range, line count, Git blob, retained product-asset classification, and canonical inventory digest. Dirty-worktree bytes were excluded. A changed Larrimon base invalidates the counts and paths and requires a regenerated baseline plus protected contract before migration or deletion. Other projects adopt the same generalized inventory, protected-contract, parity, and deletion protocol with their own repository identities and pressure profiles. + +The compensation is rational. Current ntnt can parse and lint intent, resolve glossary terms, run simple HTTP checks, call simple functions, expand tabular data, and trace `@implements`. It cannot yet safely own an application verification run. + +Specific current defects reinforce the architectural gap: + +- live `intent check` and `src/ial/execute.rs` implement different execution paths; +- IAL request headers are modeled but ignored by one executor; +- live HTTP is hand-parsed, loses duplicate headers, assumes JSON request bodies, and has no cookie jar or capture; +- technical `setup` bindings are parsed but not executed; +- function arguments are reduced to strings/numbers and structured results are stringified; +- unsupported unit/code-quality assertions can pass as β€œnot applicable”; +- `intent check` always starts one server, inherits ambient environment, discards stdout/stderr, and has no resource graph; +- coverage fails only at zero and measures implementation annotations rather than execution; +- existing CLI/file primitives have more authority than an untrusted specification should possess. + +The answer is not an unrestricted shell primitive. That would preserve the same portability, authority, cleanup, and observability problems under friendlier prose. + +--- + +## 3. Product outcome + +A mature application should be able to organize verification as: + +```text +server.intent +lib/auth.intent +jobs/run_probe.intent +verification/ + auth_cases.tnt + database_cases.tnt + scheduler_cases.tnt + browser_cases.tnt + project_cases.tnt +ntnt.toml +migrations/*.sql # production artifact, not a test harness +public/*.js # production asset when the application needs it +``` + +There should be no requirement for: + +```text +tests/*.sh +tests/*.py +tests/*.mjs +tests/*_case.sql +Makefile test orchestration +curl/grep/psql polling loops +handwritten JUnit conversion +``` + +The runtime should support these general application-verification classes through project-neutral acceptance fixtures. Larrimon supplies a separate external consumer corpus: + +- auth, tenant isolation, CSRF/origin, sessions, role changes, and revocation; +- HTTP/HTMX/full-page/no-JavaScript/browser reconciliation behavior; +- PostgreSQL migrations, RLS, roles, security-definer functions, immutability, and checksums; +- durable jobs, idempotency, leases, recovery, restart, queue failure, and deterministic races; +- monitoring probes and local protocol fixtures, including HTTP, DNS, TCP, TLS, ICMP capability behavior, SNMP, and later NETCONF/gNMI; +- immutable observation envelopes, reducers, replay, late data, incidents, suppression, and alert outboxes; +- email/webhook capture, retry, signing, and ambiguous outcomes; +- multi-node enrollment, claim, heartbeat, completion, anti-replay, rotation, and wrong-node/tenant denial; +- deterministic AI-provider fixtures, schema validation, token/plan gates, evidence citations, and no-tool assertions; +- retention, partition pruning, legal holds, backpressure, overload priorities, restore/failover evidence, and upgrade compatibility; +- project architecture, migration inventory, CI/build configuration, OCI/runtime provenance, and deployable-artifact identity. + +--- + +## 4. Goals + +1. Make execution status truthful and machine-consumable. +2. Make `.intent` the durable obligation layer without turning natural-language files into scripts. +3. Make `.tnt` the project-owned executable verification language. +4. Share one action, observation, assertion, and evidence model across `ntnt test`, `ntnt intent check`, and Studio. +5. Provide hermetic process, fixture, database, HTTP, browser, local-protocol, and project-inspection capabilities. +6. Support multi-step state, captured values, named sessions, setup/teardown, eventual assertions, restarts, and deterministic coordination. +7. Keep authority explicit, capability-gated, root-confined, bounded, redacted, and reviewable before execution. +8. Preserve external specialist engines behind typed provider boundaries while keeping project test code in ntnt. +9. Produce stable JSON and JUnit evidence with source locations, timings, hashes, and diagnostics. +10. Let any adopting project delete compensating test harnesses incrementally, with each deletion gated by equivalent or stronger evidence; prove the protocol with project-neutral fixtures before any consumer migration. +11. Remain general-purpose: ntnt gains reusable verification mechanics, not application-, monitoring-, or Larrimon-specific syntax. +12. Work on Linux first without making unearned portability claims; define Windows/macOS behavior and explicit unsupported capabilities. + +## 5. Non-goals + +- No arbitrary shell evaluation from `.intent` or `.tnt`. +- No claim that every external system is deterministic. +- No container orchestrator, CI service, browser engine, database server, or network emulator reimplementation inside ntnt. +- No monitoring-, tenant-, incident-, or Larrimon-specific language keywords. +- No exactly-once network, queue, or alert-delivery claim. +- No automatic proof that implementation annotations are correct. +- No execution of repository code during `ntnt intent lint` or static plan inspection. +- No live production target, private network, cloud account, payment provider, or AI-provider access by default. +- No requirement to remove production SQL migrations, JavaScript assets, HTML, CSS, or other legitimate application artifacts. +- No plugin ABI that loads untrusted native libraries into the ntnt process. DD-062 governs compiled extension trust. + +--- + +## 6. Definitions + +### 6.1 Obligation + +A stable, source-located claim that must be proven. Scenario outcomes are obligations. A feature description with no outcomes is `unproven` unless it is explicitly and validly marked `verification: documentation-only`; it never passes behavioral coverage by default. + +### 6.2 Evidence + +A current, source-bound result produced by executing a verification case or approved provider operation. `@implements` and `@supports` are links, not evidence. + +### 6.3 Verification case + +A `.tnt` function discovered by stable test metadata, executed in `ExecutionMode::Verification`, and linked to one or more obligation IDs. + +### 6.4 Resource + +A lifecycle-owned capability such as a PostgreSQL database, disposable Redis instance, application process, worker, browser context, local mock server, temporary directory, or OCI container. + +### 6.5 Provider + +A built-in or separately trusted implementation that creates resources or observations behind a versioned protocol and host policy. + +### 6.6 Pure ntnt project + +A project whose verification specifications, test logic, suite orchestration, and project-owned development/support helpers are represented by `.intent`, `.tnt`, `ntnt.toml`, or direct ntnt/provider commands, even when the system under test depends on external resources or contains non-ntnt production assets. + +--- + +## 7. Architectural model + +```text +.intent files ───────┐ + β”œβ”€> obligation compiler ──┐ +@implements links β”€β”€β”€β”˜ β”‚ + β”œβ”€> verification planner +.tnt @test/@verifies ─> test discovery ───────── β”‚ + β”‚ β”œβ”€> capability plan +ntnt.toml ───────────> profiles/resources β”€β”€β”€β”€β”€β”˜ β”œβ”€> resource DAG + β”œβ”€> executable cases +host policy ─────────> grants and hard ceilings β”€β”€β”€β”€β”€β”€β”€β”˜ + +planner -> resource supervisor -> case interpreters -> typed actions/providers + -> observations -> assertions -> evidence ledger -> JSON/JUnit/human report + -> guaranteed teardown/reconciliation +``` + +The layers have deliberately different authority: + +1. **Intent parser and obligation compiler:** no execution authority. +2. **Planner:** reads project metadata and requests capabilities; it does not grant them. +3. **Host policy:** grants capability classes and hard ceilings. +4. **Supervisor:** owns processes, resources, deadlines, cancellation, and cleanup. +5. **Case interpreter:** receives only opaque handles for resources assigned to the case. +6. **Providers:** perform one bounded class of external work and return typed observations. +7. **Evidence ledger:** records results and provenance; it cannot manufacture a pass. + +--- + +## 8. Obligation identity and truth model + +### 8.1 Stable IDs + +Strict mode requires stable feature, scenario, and outcome IDs: + +```intent +Feature: Tenant-bound sessions + id: feature.auth.tenant-session + + Scenario: Disabled operators lose existing access + id: scenario.auth.disabled-session + Given an authenticated operator + When that identity is disabled + β†’ id: outcome.auth.disabled-session.denied; access is denied + β†’ id: outcome.auth.disabled-session.isolated; no cross-tenant state is exposed +``` + +Compatibility mode may derive IDs and warn. Derived IDs are not suitable for long-lived imported evidence because renaming or reordering changes identity. + +A descriptive feature that intentionally makes no behavioral claim may declare `verification: documentation-only` plus a rationale. It is excluded from behavioral denominators and remains visibly counted. This marker is invalid on an outcome and cannot be used to turn an unsupported promised behavior into a pass. Future/planned behavior remains unproven unless the selected profile explicitly excludes it by stable tag or ID. + +### 8.2 Orthogonal truth dimensions + +Do not compress truth into one status string. Every obligation reports: + +| Dimension | Values | +|---|---| +| specification | declared, documentation-only | +| implementation | linked, unlinked | +| binding | bound, unbound, ambiguous | +| executability | executable, unsupported, blocked | +| disposition | planned, running, passed, failed, flaky, skipped, cancelled, no-result | +| freshness | current, stale | + +An obligation is **verified** only when all required evidence bindings are current and passed. A feature is verified only when every required obligation is verified. A feature with no required obligations is `unproven`, not behaviorally passed, unless explicitly documentation-only. + +This is execution evidence, not a theorem prover. Project code can still contain a vacuous or incorrect assertion; review remains necessary. Ntnt records exactly which observation and assertion claimed each obligation, rejects zero-evidence success, and lints obvious tautologies such as literal `expect_true(true)`, but it does not claim to infer semantic correctness from arbitrary test code. + +Skipped tests do not satisfy obligations. A profile may allow a named skip reason, but the report must retain the unmet obligation and strict coverage remains below 100%. + +Case retries are never hidden. Strict profiles do not retry failed assertions by default. If a profile explicitly requests diagnostic reruns, every attempt is recorded and fail-then-pass is `flaky`, not verified, unless a separately reviewed policy permits that disposition. Provider-level transport retries are bounded action semantics and remain visible in evidence. + +### 8.3 Evidence binding + +Project-owned complex verification uses comment metadata on ordinary ntnt functions: + +```ntnt +// @test: test.auth.disabled-session +// @verifies: outcome.auth.disabled-session.denied +// @verifies: outcome.auth.disabled-session.isolated +// @uses: app, postgres, redis +// @tags: auth, http, full +fn verify_disabled_session(ctx) { + // std/test APIs consume the opaque verification context. +} +``` + +The first implementation uses annotations because it requires no new language syntax and matches current traceability. `@uses` assigns the minimum named resources to the case; undeclared resources remain unavailable even when the profile starts them for other cases. `@tags` supplies deterministic profile selection without conferring authority. The parser/discovery path must validate duplicate test IDs, unknown obligation IDs, unknown resources/tags, missing functions, and stale file references before resource startup. Strict profiles reject unlinked verification cases unless they are explicitly marked as diagnostic-only. + +Simple scenarios may compile directly into built-in actions. Complex scenarios bind to a test function. `@verifies` declares candidate evidence bindings; returning successfully is not enough to satisfy them. Every obligation must receive at least one current assertion/evidence atom. When a test names one obligation, its unlabelled assertions may default to that obligation. When it names several, each assertion must identify the obligation it proves. A zero-assertion successful function yields `no-result`. Provider assertions follow the same rule. + +Verification is profile-relative. For a selected profile, every selected non-advisory binding for an obligation must pass, at least one selected binding must produce a current assertion/evidence atom, and any selected failure fails the run. Known bindings excluded by profile tags remain visible in the report; their prior results do not become a global pass. Advisory/diagnostic bindings never satisfy an obligation. The `full` profile selects every applicable required binding, while narrower profiles can make only a profile-qualified verification claim. Manifest/profile policy, not a test's successful return, defines any required evidence classes. + +### 8.4 Imported evidence + +Imported JUnit/TAP/JSON may supplement provider-backed execution only when it includes: + +- schema and provider identity; +- obligation IDs; +- source, intent, manifest, and plan hashes; +- tool/provider versions; +- timestamps and execution identity; +- a supervisor-issued invocation record or canonical signed envelope. + +A strict imported envelope uses RFC 8785 JSON Canonicalization Scheme and Ed25519. The signature input is the domain-separated bytes `ntnt-evidence-v1\0 || JCS(envelope_without_signature)`; only `signature` is excluded, so `schema`, `algorithm`, and `key_id` are signed. `EvidenceEnvelopeV1` has one normative closed field set: + +| Signed field | Required binding | +|---|---| +| `schema`, `algorithm`, `key_id` | exact v1 schema, Ed25519 algorithm, authorized key | +| `issuer`, `audience`, `evidence_class` | supervisor/provider identity, intended verifier/workflow audience, allowed evidence class | +| `repository` | forge plus immutable repository ID and canonical owner/name/URL | +| `subject` | full immutable commit SHA plus requested ref kind/name and source-snapshot digest | +| `workflow` | CI system, workflow path/ref, run ID/attempt, and protected environment/runner trust class | +| `protected_scope` | protected-contract raw and canonical semantic digests, trusted base repository ID/ref/full commit/tree OIDs, and protected inventory digest | +| `run_id`, `operation_id`, `profile`, `plan_hash`, `policy_hash` | exact invocation and authority plan | +| `input_hashes` | source, Intent, verifier, fixture, manifest, lockfile, migration, and provider-input closures | +| `runtime_hash`, `provider_hashes`, `environment_hash` | exact ntnt/runtime, provider executables/images, and mutable environment identity | +| `obligations`, `result` | stable obligation/assertion IDs and per-atom dispositions, never one unstructured pass boolean | +| `artifact_digests`, `cleanup` | every retained artifact and resource cleanup disposition | +| `issued_at`, `started_at`, `finished_at`, `expires_at`, `nonce` | bounded freshness and replay identity | + +The schema fixture, report importer, key-authorization policy, and implementation tests use this exact field list rather than parallel aliases. A trusted supervisor-issued invocation record carries the same identity/result closure and is accepted only from the current authenticated supervisor channel; it is not a reduced-field bypass around the envelope. Host policy maps trusted keys to issuer/audience/evidence class, immutable repository IDs, allowed ref/workflow identities, protected-contract/base scopes, and validity/revocation windows. Unsigned evidence, legacy schemas missing mandatory fields, mutable-environment results without current environment identity, unknown fields, or user-authored `passed: true` files are display-only; they cannot satisfy strict mode. Import rejects tamper, duplicate claims, replay, key rotation/revocation failures, schema downgrade, and cross-repository, cross-ref/commit, cross-workflow/audience, cross-contract/base-ref, cross-profile/plan/policy, swapped-environment/provider, and swapped-artifact reuse. Import parsers are bounded and non-resolving: JUnit/XML disables DTDs, external entities, XInclude, and network/file resolution; TAP/JSON enforce depth, line, field, and byte limits. Artifact paths are treated as data and never followed outside the approved import bundle/root. + +### 8.5 Protected evidence contract + +Repository-authored specifications and tests are executable claims, not an adversarially stable requirement baseline. A pull request can otherwise delete outcomes, narrow globs, weaken a profile, or replace a meaningful assertion with a less obvious tautology while keeping every repository hash current. + +Protected CI therefore supplies an operator-owned evidence contract outside the repository. It fixes the required profile, obligation IDs or approved base-ref delta policy, minimum evidence classes/resources, deletion/rename rules, and minimum counts. Planning compares the candidate snapshot with the trusted contract and base ref before execution. Repository configuration may tighten this contract but cannot weaken it. The contract proves scope continuity, not arbitrary assertion semantics: changed verifier code still requires code review and the migration mutation/fault witnesses in Β§22. Without that external contract, the report is labeled `project-authored-claim`; even with it, ntnt reports `protected-contract-execution-claim`, not cryptographic proof that human-authored assertions are meaningful. + +Host policy and the protected evidence contract are one `TrustedInput` class. The trusted launcher opens each payload before repository code runs and passes inherited read-only handles, not repository-selected paths. Both require exact raw-byte digest, regular-file identity, trusted non-writable ownership/ancestor/ACL checks, hardlink/symlink rejection, pre/post-open identity validation, and approved signature/canonicalization algorithms where signed. The contract also has a canonical semantic digest. The launcher resolves its base repository/ref to an immutable repository ID plus full commit and tree OIDs; a mutable ref name is never the base identity. The raw contract bytes/digest, semantic digest, base repository/commit/tree, and protected inventory digest enter the snapshot, plan hash, report, replay checks, and strict evidence envelope. Rename swaps, hardlinks, mid-run replacement, base-ref retargeting, and cross-repository/ref/workflow/contract reuse fail closed. + +Signed trusted inputs use two closed, unknown-field-rejecting JCS envelopesβ€”`PolicyTrustedInputV1` and `ProtectedContractTrustedInputV1`β€”whose top-level fields are exactly `schema`, `algorithm`, `key_id`, `issuer`, `audience`, `repository`, `ref`, `workflow`, `not_before`, `expires_at`, `nonce`, `payload_sha256`, and `signature`. `schema` is the corresponding type name, `algorithm` is exactly `Ed25519`, identity/freshness fields are mandatory, and `payload_sha256` is lowercase SHA-256 of the exact already-open payload bytes before parsing. The envelope bytes themselves must be canonical RFC 8785 JCS with duplicate keys rejected. Signature input excludes only `signature` and is: + +```text +policy: "ntnt-policy-trusted-input-v1\0" || JCS(envelope_without_signature) +contract: "ntnt-protected-contract-trusted-input-v1\0" || JCS(envelope_without_signature) +``` + +Verification authenticates the envelope and key authorization, compares `payload_sha256` to the inherited payload handle, and only then parses the payload and derives its canonical semantic digest. The signature never authenticates semantics while leaving the raw-byte identity unsigned. Cross-type envelopes, unknown/duplicate fields, non-canonical envelope bytes, raw payload mutation, wrong repository/ref/workflow/audience, expired/not-yet-valid/revoked keys, and unsupported algorithms fail closed. Producer/consumer fixtures freeze both schemas and domains. + +--- + +## 9. Project manifest and profiles + +`ntnt.toml` gains a versioned `[verification]` section. The syntax below is normative in shape but may receive naming polish during implementation: + +```toml +[verification] +schema = 1 +authoring = "pure-ntnt" +clean_environment = true +default_profile = "fast" + +[verification.files] +application = ["server.tnt", "app/**/*.tnt"] +intent = ["**/*.intent"] +verification = ["verification/**/*.tnt"] +support = ["tools/**/*.tnt"] +product_assets = ["public/**", "views/**"] +migrations = ["migrations/**"] +project_metadata = ["*.md", "*.toml", ".github/**", "compose*.yaml"] + +[verification.profiles.fast] +mode = "strict" +include = ["unit", "project"] +required_coverage = 1.0 + +[verification.profiles.full] +mode = "strict" +include = ["unit", "db", "http", "browser", "project"] +resources = ["postgres", "redis", "mail", "app", "worker", "browser"] +required_coverage = 1.0 + +[verification.resources.postgres] +provider = "postgres" +mode = "external" +url_from = "TEST_DATABASE_URL" +isolation = "database-per-run" +migrations = "migrations" + +[verification.resources.redis] +provider = "redis" +mode = "managed" +isolation = "instance-per-run" + +[verification.resources.mail] +provider = "smtp.capture" +mode = "managed" + +[verification.resources.app] +provider = "process" +containment = "mediated-ntnt" +argv = ["ntnt", "run", "server.tnt"] +depends_on = ["postgres", "redis", "mail"] +readiness = { ntnt_child_http = "/readyz", status = 200, inherited_listener = true, timeout_ms = 30000 } +pass_environment = ["APP_NAME"] +environment = [ + { name = "DATABASE_URL", resource = "postgres", output = "url" }, + { name = "REDIS_URL", resource = "redis", output = "url" }, + { name = "SMTP_URL", resource = "mail", output = "url" } +] + +[verification.resources.browser] +provider = "browser.cdp" +containment = "sandboxed" +depends_on = ["app"] +executable_from_policy = "chromium" + +[verification.capabilities] +request = [ + "process:ntnt", + "network:loopback", + "database:postgres:test", + "browser:local", + "filesystem:project-read", + "git:project-read" +] +``` + +Rules: + +- secret values never appear in the manifest; +- `*_from` names refer to host-policy-approved inputs and are redacted; +- process environment receives only explicitly passed host values and typed outputs exported by declared dependency resources; arbitrary string interpolation is not performed. Secret resource outputs may be injected by the supervisor but are not made readable to test code or reports merely because the case has the resource handle; +- commands are exact executable plus argv; no shell parsing, interpolation, redirection, or command substitution; +- host policy constrains executable identity, provider/image digest, permitted argument templates, mounts, destinations, and exported outputs; a broad capability label is not permission to choose an arbitrary executable or container; +- `authoring = "pure-ntnt"` is mechanically enforced through an exhaustive project-file and executable-declaration classifier. Every tracked path must match exactly one protected class: ntnt application source, Intent/verification, ntnt support CLI, production asset, migration, or project metadata. Overlap, omission, an unclassified executable/support file, extensionless or renamed wrapper, executable shebang, relevant untracked executable, symlink/hardlink escape, or a project-owned non-ntnt helper fails planning. The classifier also parses every supported executable-bearing metadata format: CI workflow steps/actions, Compose/OCI command and entrypoint declarations, Docker build/run hooks, package/task-runner manifests, and generated-helper declarations. Support/orchestration contexts allow only closed typed ntnt/provider operations with immutable origins; inline shell/Python/Node, YAML block scripts, heredocs, shell operators/substitution, unpinned actions/images, arbitrary container commands, and unknown executable-bearing formats fail `proven`. Git mode `160000`, nested repositories, and generated executable closure fail by default; an operator-owned origin/digest lock must recursively pin and classify every committed object before any exception. Globs and classes are part of the protected contract, so a candidate cannot relabel or omit a helper. Product assets/migrations may contain JavaScript, SQL, templates, or data, but imports, build hooks, metadata declarations, provider origins, generated outputs, and process argv must prove they are not verification/support programs; +- verification/support may use only `.tnt` cases/CLI programs and approved typed built-in/host-installed providers. Planning rejects `Primitive::Cli`, legacy file/CLI actions, direct generic process/shell effects in those roots, Bash/Python/Node wrappers, SQL-only/browser test harnesses, generic command-taking providers, and provider executables/wrappers under the project root. Application source is also ntnt in a pure-ntnt project; a production capability such as DD-065 must use a typed native contract rather than becoming a wrapper loophole; +- third-party/generated exceptions come only from an operator-controlled lock outside the repository containing origin, immutable digest, non-project ownership, and proof the artifact is not verification/support. Project-generated support is never exempt. Violations and every excluded artifact are reported; fast/full require `authoring_purity = proven` before startup; +- project-wide `intent check` is strict by default. A verifying profile cannot weaken required-obligation truth, purity, protected-contract requirements, or host-clamped skip/advisory policy. Diagnostic execution is an explicit non-verifying CLI mode whose report/exit cannot be reused as verification evidence; +- reports include `authoring_purity = proven | not_checked | violated` plus the scanned source/provider closure; successful execution never implies purity; +- all paths are canonicalized under the project root unless host policy grants a named external path; +- profile inheritance is acyclic and deterministic; +- resource dependencies form an acyclic graph; +- a dry plan is available without executing project code; +- the same profile and policy produce a stable plan hash apart from explicitly recorded dynamic allocations. + +Privileged policy authority must originate outside repository-controlled argv and environment. A trusted launcher or CI control-plane step outside the checkout opens the policy/contract and then executes ntnt with a fixed profile: + +```bash +/usr/local/bin/ntnt-protected-verify full +``` + +The wrapper is operator-installed, accepts no policy path or capability arguments from the repository, clears untrusted policy environment, opens the fixed policy/contract as `TrustedInput` handles, resolves the contract base to immutable repository/commit/tree identity, and then invokes `ntnt intent check`. + +The repository requests authority. The host grants it. Ntnt's built-in default policy is unprivileged. Repository-controlled `--policy`, environment, workflow, symlink, or configuration may only reduce that default or an already provisioned host grant; it cannot create privilege. Privileged policy and protected-contract payloads always authenticate exact already-open bytes through the same `TrustedInput` machinery. Unsigned filesystem inputs require a regular non-hardlinked file, no symlink at any component, trusted owner, non-writable file and ancestor chain, platform ACL checks, and pre/post-open identity validation; same-CI-user ownership alone is insufficient. Signed inputs use the exact closed envelopes and domain strings in Β§8.5, verify the signed raw payload digest before payload parsing, and bind repository/ref/workflow/audience plus key validity/revocation. The trusted launcherβ€”not repository codeβ€”chooses both payload/envelope handle pairs. The plan/report records each non-secret raw/canonical digest and trust class. + +### 9.1 Immutable execution snapshot + +Planning and execution consume one immutable input closure. After safe discovery, the supervisor copies or opens the exact tracked/project-declared source, Intent, verifier, fixture, migration, manifest, lockfile, policy, and protected-contract raw bytes into a private content-addressed read-only snapshot. It records the contract's raw and canonical semantic digests, immutable base repository/commit/tree, and protected inventory digest. Test interpreters and managed ntnt children execute that snapshot, not the mutable checkout. Provider/browser/runtime executables and OCI images are opened or resolved by immutable digest at launch; a path or mutable tag is insufficient. The report hashes the bytes actually consumed. + +Strict mode fails if pre-snapshot discovery races, a required input cannot be captured safely, executable identity changes between validation and launch, or the source checkout drifts during the run. Generated outputs and external environment identity are recorded separately. This closes plan/use/report time-of-check/time-of-use gaps rather than attempting a hopeful post-hoc hash comparison. + +--- + +## 10. Verification runtime and `std/test` + +### 10.1 Execution isolation + +Each case receives: + +- a fresh interpreter by default; +- deterministic case seed; +- opaque `TestContext` bound to run, case, generation, and assigned resources; +- a clean environment containing only allowed values; +- a case deadline and cancellation token; +- a private artifact directory; +- assertion and diagnostic sinks with bounded output. + +A forged, serialized, copied across runs, or expired resource handle fails deterministically. Handles are runtime values, not maps containing provider IDs. + +DD-077 Design spike 0C/PR 4B's future `EffectKind` is descriptive static metadata; it is never authorization and is not a prerequisite for verification mediation. Runtime authority uses an opaque `VerificationGrant` bound to `{run_id, case_id, generation, resource_id, operation_set, scope, expiry, budget}`. Every authority-bearing sink validates the exact grant/handle at the final operation seam. A broad `database`, `network`, or `filesystem` effect classification cannot enable a constructor, another resource, another endpoint/path, or a wider operation. Grants are supervisor-minted and attenuating; test values, provider output, strings, environment, durable jobs, and imported evidence cannot mint or widen them. Constructors for external authority are unavailable in verification mode unless they consume the assigned resource grant. + +Each case uses a fresh interpreter/module environment, but a fresh interpreter alone is not an isolation proof. Verification authority and environment/cwd/args overlays are installed before interpreter initialization or module evaluation can observe host state. Every process-global auth, job, database, HTTP, cache, SQLite/KV, email, secret, time/random, and concurrency registry is inventoried and made run-scoped, reset/namespaced, or unreachable in verification mode. Only after those gates pass may module globals, imported singletons, deferred statements, and mutable values be claimed not to bleed across cases or concurrent runs. Suite fixtures share only serialized/typed fixture values or opaque supervisor handles under declared synchronization; they do not share an application interpreter. + +Suite/feature fixture sharing is opt-in. Shared resources must declare reset semantics. Cases are not parallelized across a shared mutable resource unless the profile explicitly allows it. + +Project fixtures are ordinary `.tnt` functions with discoverable metadata: + +```ntnt +// @fixture: fixture.auth.operator +// @scope: case +// @uses: postgres +// @teardown: cleanup_operator +fn create_operator(ctx) { + // Return typed fixture values; commit state needed by app processes. +} + +fn cleanup_operator(ctx, value) { + // Runs even when the dependent case fails, before resource teardown. +} + +// @test: test.auth.operator-dashboard +// @fixtures: fixture.auth.operator +// @uses: app +fn operator_dashboard(ctx) { + let operator = fixture(ctx, "fixture.auth.operator")? + // ... +} +``` + +Fixture dependencies form an acyclic DAG. Setup failure blocks dependent cases and does not satisfy their obligations. Teardown runs in reverse order after pass, failure, timeout, or cancellation; teardown failure is separately reported and fails strict mode. Case scope is the default. Suite/run sharing requires explicit reset semantics and scheduling constraints. Fixture return values preserve types and secret taint. + +### 10.2 Test API shape + +`std/test` and focused submodules expose free functions that require the context or an opaque child handle. Test modules are available only in `ExecutionMode::Verification`; importing them from production source or an ordinary `ntnt run` fails during validation. Verification files are loaded from configured test roots and cannot be imported by the application graph. + +Verification mode is not a blanket bypass for ordinary effectful stdlib. Direct network, database connection construction, secrets, environment, filesystem, jobs, or other I/O must consume an assigned opaque `VerificationGrant` for the exact resource and operation or be denied. A denied verification grant returns a structured failure; it never uses the current runtime convention of silently returning `Unit`. Until an existing production API can accept such scoped authority safely, it is tested through a managed process/provider boundary rather than enabled ambiently in the test interpreter. Pure production functions remain directly callable. + +```ntnt +import { + expect_equal, + expect_true, + expect_error, + expect_match, + expect_contains, + expect_path, + subcase, + resource +} from "std/test" + +// @test: test.reducer.golden-replay +// @verifies: outcome.reducer.replay-identical +fn reducer_golden_replay(ctx) { + let fixture = resource(ctx, "golden_observations")? + let first = reduce(fixture.observations, fixture.eval_time) + let second = reduce(fixture.observations, fixture.eval_time) + expect_equal(ctx, first, second, "semantic replay") +} +``` + +For a verifier bound to several obligations, assertion options carry the exact evidence identity: + +```ntnt +expect_equal(ctx, response.status, 403, map { + "obligation": "outcome.auth.disabled-session.denied", + "message": "disabled session is rejected" +}) +``` + +Assertions compare typed interpreter values, not debug strings. Required baseline assertions include: + +- equality/inequality with structural diffs; +- true/false, nil/some/ok/err and expected error class/message; +- type and shape; +- contains/not-contains for strings, arrays, maps, and sets where supported; +- key/path existence and typed path equality; +- regex, prefix, suffix, range, order, count, uniqueness, and approximate numeric comparison; +- redaction-aware snapshots/golden data; +- explicit failure and bounded diagnostic attachment. + +Ordinary verification is read-only with respect to committed golden files. An explicit update command may render a taint-checked candidate and generated patch into a private restrictive artifact directory, binding the source snapshot digest, target path, prior file identity/digest/mode, and proposed digest. Ntnt never replaces the committed target automatically: a human or VCS applies the patch, resolves concurrent edits, and reruns verification against the new immutable snapshot. CI never generates or applies acceptance updates. This deliberately avoids pretending that compare-then-rename is a cross-process compare-and-swap. + +Failed expectations are accumulated until the case deadline or a fatal assertion. Runtime errors, unsupported assertions, expired handles, provider failures, cleanup failures, zero-assertion cases, and candidate bindings without assertion evidence cannot pass as β€œnot applicable.” + +### 10.3 Table and property cases + +Existing Intent test data remains supported. `.tnt` tests can name subcases and deterministic seeds. Property tests require explicit generators, seed recording, bounded case counts, shrinking ceilings, and replay commands. Shrinking and reproducibility claims are limited to pure, case-local observations; resource/network/database/browser effects are rejected in shrinkable properties unless a future provider defines transactional reset semantics. Resource-backed matrices remain ordinary named subcases. β€œDeterministic” means the same inputs under the same declared runtime observations, not merely two calls made accidentally close together. + +--- + +## 11. One action and observation model + +`src/ial/execute.rs`, live `intent check`, Studio, and test commands must converge on one model: + +```text +Action + Capability + Deadline -> Observation | StructuredError +Observation + Assertion -> AssertionEvidence +``` + +Actions are typed and closed. Vocabulary rewrites terms into actions/assertions; it does not acquire authority. + +Intent may select only a planner-approved action/binding template and supply bounded non-authoritative data validated by that template. It cannot choose a provider, executable, resource, filesystem path, network destination, secret source/value, database connection, browser target, or capability. Auto-compiled HTTP is restricted to a relative path on an already planned application resource and a closed set of non-secret fields; authenticated or stateful flows bind to `.tnt` cases holding opaque clients. Legacy `Cli`, `ReadFile`/write, arbitrary URL, secret-header, and compatibility bindings are reported unsupported in strict/pure planning and fail before effects. + +Observations include: + +- provider/action kind and schema version; +- start/end monotonic timing; +- bounded typed values; +- structured error class; +- truncation/redaction metadata; +- resource and process identity without secrets; +- provenance needed to reproduce the check. + +Legacy IAL primitives become compatibility constructors over this model. `Primitive::Cli` is deprecated for project Intent and removed from default resolution; approved external programs run only through manifest resources/providers and host policy. + +--- + +## 12. HTTP and session verification + +Verification HTTP does not create a fourth transport/security stack. DD-077 Design spike 0B and PRs 2C–2E first land transport feasibility, trusted network configuration, one policy-bound HTTP transport, and `std/net` integration used by `src/stdlib/http.rs` and `src/stdlib/net/policy.rs`; DD-078 cannot start HTTP work before those exact merge commits are pinned. Production `std/http`, `std/net` target classification, IAL compatibility, and verification HTTP share all-address resolution, connect-time approved-address binding, proxy policy, TLS, per-hop redirect/reconnect validation, credential stripping, IPv4-mapped/private/metadata rules, body/time budgets, and error taxonomy. Verification adds session jars, captures, assertions, and evidence above that seam. Raw `TcpStream` test clients are retired rather than extended. + +The shared HTTP action uses one maintained client stack and supports: + +- arbitrary validated request headers; +- query parameters; +- JSON, form, raw bytes/text, and multipart bodies; +- named cookie jars and multiple simultaneous identities; +- duplicate response headers, especially `Set-Cookie`; +- redirect disabled by default, with bounded explicit policy and per-hop validation; +- response status, headers, body bytes/text, JSON, and timing; +- capture from headers, cookies, regex groups, JSON paths, HTML selectors, and URLs; +- substitution into later actions without logging secret captures; +- capture taint: cookies, authorization values, magic links, tokens, credentials, and values selected by policy become opaque secret values that may flow into approved later actions but cannot be stringified, snapshotted, or emitted; +- attach mode for an already running base URL; +- connection, request, response-size, redirect-count, and total-deadline bounds; +- exact origin, remote destination, and network-capability enforcement. + +Example `.tnt` verifier: + +```ntnt +import { client, request, expect_cookie_present } from "std/test/http" +import { expect_equal, resource } from "std/test" +import { latest_link } from "std/test/mail" + +// @test: test.auth.magic-link-session +// @verifies: outcome.auth.magic-link.single-use +// @uses: app, mail +fn magic_link_session(ctx) { + let browser = client(ctx, "operator")? + let issued = request(browser, map { + "method": "POST", + "path": "/auth/request", + "form": map { "email": "operator@example.test" } + })? + expect_equal(ctx, issued.status, 200) + + let mail = resource(ctx, "mail")? + let link = latest_link(mail, "operator@example.test")? + let signed_in = request(browser, map { "method": "GET", "url": link })? + expect_equal(ctx, signed_in.status, 303) + expect_cookie_present(ctx, browser, "__Host-session") +} +``` + +The API must support HTMX headers, form fallback, reconciliation polling, session revocation, redirects, and wrong-origin cases without shelling out to curl. + +--- + +## 13. Resource and fixture model + +### 13.1 Lifecycle + +Every resource follows: + +```text +declared -> planned -> reserved -> creating -> created -> finalized -> ready -> leased -> stopping -> stopped + \-> failed/recoverable +``` + +The supervisor starts dependencies in topological order and tears them down in reverse order. Teardown runs after pass, failure, interpreter error, timeout, cancellation, and ordinary signal handling. Cleanup failure is reported separately and fails strict CI only for a backend whose crash-safe ownership class was proven during planning. + +No system can guarantee cleanup after host power loss or an uncatchable kill, and a filesystem ledger cannot transact atomically with a process, database, or OCI daemon. Strict lifecycle ownership therefore uses an explicit `reserve β†’ create β†’ finalize β†’ expose` protocol through a durable host supervisor/broker: + +1. persist and fsync an authenticated reservation before creation, binding a high-entropy ownership token, deterministic backend-safe creation identity, run/resource/project/policy/provider identities, operation scope, expiry, and cleanup authority; +2. have the durable broker create the resource while retaining lifetime ownership or using a backend idempotency/recovery token; +3. obtain an exact object ID plus provider creation receipt, persist/finalize it atomically in the ledger, and revalidate the created object's token/identity; +4. only after finalization release readiness, credentials, endpoint, listener, or opaque handle to project code. + +A crash before creation leaves only an expirable reservation. A crash after creation but before finalization must be recoverable by exact reserved identity/token or by broker-owned lifetime cleanup; broad PID/name/prefix/port/container/database scans remain forbidden. The broker is an ntnt-installed, host-policy-pinned service or dedicated supervisor process started and authenticated outside repository control; project argv/env/config cannot select its endpoint, identity, state root, or cleanup authority. Clients connect over an inherited or mutually authenticated local handle, and protected profiles fail planning if no durable broker class is available. Broker binary/config/state identities enter the plan/report. Broker restart reconciles only its authenticated reservations/receipts. Processes are created suspended or inside a pre-owned cgroup/Job Object, recorded with pidfd/start time/executable/run token, then resumed only after finalization. Providers declare and prove their prepare/create/recover/finalize state machine, including controller and broker crash at every boundary. If the OS/backend cannot retain lifetime ownership or recover exact creation from the reservation token, cleanup is reported `best-effort`/non-verifying and strict/protected profiles reject that resource before startup. Partial/corrupt ledger writes and identity mismatches fail closed; leases have bounded TTLs and cleanup is idempotent. + +### 13.2 Fixture scopes + +- `case`: fresh for each test; default for mutable state; +- `suite`: shared with an explicit reset operation; +- `run`: shared infrastructure such as one PostgreSQL server, while each case/suite receives an isolated database/schema; +- `external`: lifecycle not owned by ntnt; health and namespace cleanup still apply. + +Fixtures return typed values or opaque handles. App-specific setup belongs in named `.tnt` fixtures, while providers own generic infrastructure lifecycle. Inline `setup` strings in `.intent` are deprecated and never interpreted as SQL or shell. + +### 13.3 PostgreSQL + +The PostgreSQL provider supports: + +- external server and managed OCI modes; +- database-per-run or schema-per-run isolation; +- committed canonical seeds visible to app/worker pools; +- explicit owner, migrator, app, worker, and tenant roles; +- migration application and checksum evidence through landed DD-077 PRs 1B–1C; +- bounded query/execute observations from `.tnt` tests; +- transaction and held-lock actors for SQL-only deterministic races; +- RLS context and privilege assertions; +- bounded database/schema cleanup on ordinary termination plus authenticated stale-run reconciliation; +- query, row, byte, statement-timeout, and lock-timeout ceilings; +- no credential or parameter value leakage. + +Destructive lifecycle operations are confined to identifiers generated for the current run and recorded in the supervisor ledger. External-server policy pins the approved endpoint identity, generated database/schema prefix, and allowed create/drop operations. A repository cannot point the provider at another server and inherit cleanup authority. SQL identifiers are constructed only by validated provider code, never interpolated from test values. + +Transaction-per-case alone is insufficient for app-backed tests because separate pooled connections cannot see uncommitted fixture data. It remains useful for direct SQL checks. + +### 13.4 Services and processes + +The process provider supports exact argv, clean environment, working directory under policy, readiness observations, expected-startup-failure mode, stdout/stderr ring buffers, process groups/job objects, restart, stop, liveness, exit assertions, and deadlines. + +A process group is lifecycle control, not a security sandbox. Every executable resource declares one containment class: + +- `mediated-ntnt`: a managed ntnt child executing the immutable snapshot with a run-scoped policy; all native/module-initializer/transitive effects are checked at the final runtime dispatch seam; +- `sandboxed`: OS/container enforcement provides a private writable root/HOME/tmp, constrained read-only inputs, dedicated identity, CPU/memory/PID/file-descriptor/disk limits, descendant containment, and brokered/allowlisted egress; +- `trusted-uncontained`: a pinned operator-approved binary whose direct syscalls are outside ntnt enforcement. This class is prohibited in untrusted-PR and hermetic profiles and receives no repository secret merely because its protocol is valid. + +Linux may satisfy `sandboxed` with user/mount/network namespaces or rootless OCI plus cgroups/seccomp; Windows requires Job Object/AppContainer or equivalent policy; macOS requires an approved sandbox boundary. If a platform cannot enforce a profile's declared guarantees, planning blocks it. Verification disables implicit dotenv loading and denies project `.env`/credential files unless named host policy grants them. Bare port probing is not authenticated readiness: ntnt children use inherited/reserved listeners or a run-nonce-bound readiness channel; other processes require provider/process identity evidence. + +Application, worker, scheduler, provider stubs, and external-agent processes are ordinary named resources. Tests may hold separate instances with isolated ports and resource namespaces. + +### 13.5 Local protocol fixtures + +Built-in local-only fixtures should cover common deterministic dependencies: + +- HTTP/HTTPS scripted server; +- SMTP/mail capture; +- webhook receiver; +- TCP and UDP scripted peers; +- DNS fixture/resolver where platform support permits; +- Redis disposable instance for verifying profiles; attached ACL mode is diagnostic/non-verifying; +- byte-oriented request/response scripts suitable for SNMP and later protocol fixtures; +- deterministic AI/payment/API stub responses; +- temporary workspace resources with root-confined read/write APIs and optional bounded copies of declared project fixtures. + +Fixtures must be finite, bounded, loopback by default, record requests with redaction, and fail on unexpected traffic when strict. Temporary workspaces expose opaque handles or supervisor-injected paths only to declared dependants; test code cannot turn them into arbitrary host filesystem authority. + +Redis key prefixes and logical database numbers are organization conventions, not isolation. Strict, hermetic, protected, and cleanup-claiming profiles require a disposable per-run instance whose process/container/volume follows Β§13.1's brokered lifecycle. Controller/provider crashes must be recoverable by exact reservation/object/token; reports remain cleanup-pending/non-passing until reconciliation completes, and only completed ordinary/recovery cleanup may claim zero residual keys plus revoked credentials. Host power loss retains Β§13.1's honest limitation. Attached Redis is explicitly trusted, non-hermetic, and non-verifying because Redis does not attribute dynamically created keys to the ACL user that created them, so exact cleanup cannot be proven when the application connects directly. An operator-created per-run ACL user with random key pattern, strict command allowlist, and mandatory bounded TTL may reduce attached-mode risk, but it cannot satisfy protected obligations or claim immediate cleanup. A future enforcing broker may strengthen that class only after it transactionally observes every mutation, records exact keys, enforces TTLs, and proves cleanup. Supervisor credentials never reach app/test code. + +--- + +## 14. Eventual behavior, lifecycle, and deterministic coordination + +### 14.1 Eventual assertions + +Polling is represented as a repeated observation under one deadline: + +```ntnt +import { eventually } from "std/test" + +eventually(ctx, map { + "within_ms": 5000, + "every_ms": 100, + "description": "queued run becomes terminal" +}, fn() { + return load_run_state(db, run_id) == "completed" +})? +``` + +The final syntax depends on DD-077 PR 0A's reusable native-callback bridge. This feature waits for that bridge; no bounded-provider or verification-only callback fallback is permitted. Reports include attempts, elapsed time, final observation, and whether cancellation interrupted the wait. No unbounded sleep loops. + +### 14.2 Expected failures and restart + +Tests can assert startup rejection, process exit, provider error class, transaction rollback, readiness loss, and recovery after restart. β€œFailed to start” is data only when the case explicitly expects it; otherwise it is a failed/blocked resource. + +### 14.3 Concurrency + +The runtime provides named actors, parallel groups, and barriers: + +- actor start/release/join; +- barrier wait/release with participant count; +- held PostgreSQL transaction/lock steps; +- mock-provider response holds; +- bounded cancellation and deadlock diagnostics; +- deterministic release order recorded in evidence. + +This controls test-visible interleavings. It does not claim to deterministically schedule arbitrary kernel, database, browser, or interpreter internals. Race tests must place barriers at observable seams. + +### 14.4 Time, randomness, and faults + +- property/table tests receive a deterministic generator seed; this does not virtualize wall time; +- DD-078 Slice 10P first inventories every direct wall-clock, monotonic-clock, sleep, auth/job expiry, UUID/random, retry, scheduler, and runtime-deadline site and proves one internal per-interpreter observation seam; DD-077 currently owns no such seam; +- only after that seam exists do in-process tests receive a test clock and managed ntnt processes opt into a local, run-token-bound control channel; +- the control channel is disabled outside `ExecutionMode::Verification`, never listens on a non-loopback interface, and cannot affect an unbound process; +- external systems use bounded real time unless their provider supports virtual time; +- dependency failures are injected through providers/proxies or named resources, not unrestricted monkey-patching of production code; +- every injected fault is named and reported. + +--- + +## 15. Browser verification from ntnt + +A pure ntnt project must not require a project-owned Playwright/Node test file. `std/test/browser` provides typed browser actions backed by a policy-approved local browser provider, initially Chromium DevTools Protocol: + +- launch/connect and isolated browser contexts; +- JavaScript-enabled and no-JavaScript modes; +- viewport, locale, timezone, and reduced-motion controls; +- navigation and redirect history; +- selectors/locators, count, text, HTML, attributes, visibility, focus, and accessibility snapshots; +- click, fill, select, submit, keyboard, and history actions; +- request interception, delay, abort, offline mode, and response observation; +- screenshots, traces, console errors, and failed requests as bounded artifacts; +- explicit script evaluation for behavior that cannot be observed otherwise, with output and deadline bounds; +- cookies, storage, and multiple contexts for separate users; +- deterministic cleanup of pages, contexts, and the browser process. + +Chromium remains an external resource. Ntnt owns the project-facing API, capability plan, lifecycle, evidence, and redaction. The provider reports browser executable/version/digest. Host policy pins acceptable executables or OCI images. + +CDP interception is observability, not an egress security boundary. Untrusted-PR browser profiles require a sandboxed browser with a private profile/home/filesystem and network enforcement beneath Chromiumβ€”an isolated network namespace/container or mandatory broker/proxy that denies undeclared DNS, loopback, private/metadata, WebSocket, WebRTC, service-worker, extension, and download paths. If the host cannot enforce that boundary, the profile blocks. A trusted-uncontained local browser profile is explicitly non-hermetic and cannot receive protected secrets or satisfy the protected CI contract. + +Browser navigation and subresource requests use the same network policy as other actions. `file:` URLs, local browser profile reuse, extension loading, arbitrary remote-debug targets, downloads outside the artifact directory, and access to undeclared loopback services are denied by default. + +Screenshots and traces can contain secret pixels or page content that generic string redaction cannot repair. They are sensitive artifacts: disabled unless the profile/policy permits them, written with restrictive permissions, masked with configured private selectors where possible, bounded, and labeled with retention/export policy. Ntnt MUST NOT claim arbitrary screenshot pixels are safely redacted. + +Consumer adoption plans can then express reconciliation, fragment behavior, responsive rendering, focus transfer, no-JavaScript fallback, and authenticated browser smoke in `.tnt`. The Larrimon plan is the first concrete consumer of that generalized capability. + +--- + +## 16. Project, architecture, migration, and provenance verification + +Not every obligation runs against a live app. `std/test/project` exposes typed, read-only facts: + +- canonical project file inventory and hashes; +- ntnt AST/import graph, function annotations, routes, effects when available, and ownership locations; +- UTF-8/text queries under the project root; +- parsed JSON, TOML, YAML, and lockfile data through bounded parsers; +- Git tracked/untracked/blob/ref facts without network access; +- migration inventory/checksums/status through landed DD-077 PRs 1B–1C; +- OCI image config, labels, layers, platform, and digest through a read-only provider; +- rendered Compose/project configuration through a pinned provider when required; +- generated-document drift and runtime/source identity. + +The default project view contains tracked source plus explicitly configured generated artifacts. VCS-ignored files, `.env*`, credentials, private keys, editor state, and host metadata are excluded unless trusted host policy grants a named path. Facts are read-only, root-confined, bounded, and cacheable by source hash. + +First-class Intent `Constraint` support should compile architecture obligations into these facts. Until then, `.tnt` tests linked by `@verifies` provide the executable form. + +The goal is not to replace Python regexes with Rust regexes. Ntnt source constraints should use AST/import/effect facts. Generic text checks remain available for artifacts without a stable parser, but reports identify them as textual evidence. + +Migration immutability, image provenance, CI policy, deployment shape, and asset integrity can therefore be authored in `.tnt`. Specialist tools may execute behind typed providers, but project-local Python and shell are unnecessary. + +### 16.1 Typed project state and environment lifecycle + +Pure-ntnt support includes ordinary development/staging operations, not only tests. Slices 14C–14D add a native project-state service plus typed environment lifecycle; they do not expose generic shell or arbitrary OCI commands. + +Slice 14C stores versioned state outside the checkout under an OS-appropriate user state root keyed by canonical project-root digest and environment name. Each record binds project/manifest digests, environment/generation, lifecycle state, pre-creation reservation identity/token, exact provider/object identities and creation receipts once available, finalization generation, allocation leases, opaque secret handles, timestamps, and cleanup disposition. Creation and transition use restrictive permissions, exclusive cross-process locking, temporary-file plus file/directory fsync and atomic replace, schema validation, and compare-and-swap generation. Corrupt, foreign-root, stale-generation, symlink/hardlink, writable-parent, or partially written state fails closed. Legacy schema upgrades are explicit and tested. This slice supplies provider-neutral lock/lease/CAS machinery; it neither inspects nor mutates OCI. + +Port allocation never probes and releases. Slice 14C gives managed processes inherited listeners and exposes a global allocation transaction. Slice 14D uses one realizable OCI handoff: a durable broker retains each host TCP listener for the environment lifetime and proxies it to an unpublished container port after the final service object is created; Compose does not publish or rebind that host port. Before exposure, the broker finalizes a route object binding `{listener ID, container object ID, network endpoint ID, generation, target port, ownership token}`. On every accept/reconnect it re-inspects and validates that exact object/endpoint/generation through the pinned daemon API, or consumes an authenticated daemon event stream that invalidates the route fail-closed; it never routes by service name, alias, or cached IP alone. Before forwarding any application or readiness byte, the target must also complete a broker-controlled generation-bound authentication handshake (for example an opaque sidecar nonce or ephemeral mTLS identity unavailable to peer containers). Container recreation, endpoint change, daemon restart, failed target authentication, or event-stream loss requires a newly finalized generation before traffic flows, and stale/wrong targets receive zero application bytes. UDP or a backend that cannot provide this lifetime route proof must instead let the daemon allocate the port on the final service object and persist/recover that exact object/port before exposure, or be rejected from strict profilesβ€”there is no placeholder-socket handoff. While holding the allocation transaction, 14D also creates the exact pre-created network/reservation, records immutable daemon object IDs plus ownership token/creation receipt, and only then releases the lock. Compose consumes that external network rather than recreating it by name. The user-state lock coordinates ntnt planners but is not a daemon-wide mutex; OS listener binding and daemon object creation are the authoritative conflict checks against other users and non-cooperating clients. Conflicts cause bounded re-inspection/replan, never overlap. Crash between backend creation and state finalization follows Β§13.1's exact reserved identity/token recovery. Worktree/project/image identities use the full canonical root digest plus collision handling; ambient environment cannot retarget them. Secret values are generated or obtained as opaque outputs, written only when an approved provider requires a restrictive compatibility file, and never printed or exposed to `.tnt` string APIs. + +Slice 14D defines `[project.environments.NAME]` with pinned provider, Compose/OCI manifests, profiles, services, build/create/up ordering, a migration action backed by landed DD-077 PRs 1B–1C, readiness, exported non-secret outputs, state schema, and cleanup policy. The normative shape is typed rather than an action/argv escape: + +```toml +[project.environments.staging] +schema = 1 +provider = "oci.compose" +manifest_files = ["compose.prod.yaml", "compose.staging.yaml"] +profiles = ["workers"] +allowed_services = ["postgres", "redis", "mail", "migrate", "app", "worker"] +build_services = ["app"] +create_services = ["app", "worker"] +start_dependencies = ["postgres", "redis", "mail"] +migration = "default" # landed DD-077 PRs 1B–1C ntnt db plan identity +start_services = ["app", "worker"] +readiness = { service = "app", path = "/readyz", status = 200, timeout_ms = 60000 } +state_scope = "canonical-worktree" +port_pools = ["staging-app", "staging-postgres", "staging-redis"] +subnet_pools = ["staging-private", "staging-edge", "staging-egress"] +cleanup = "exact-owned-objects" +``` + +`ntnt project env init|up|down|status NAME` parses and renders effective configuration through a typed OCI provider. Pure mode rejects shell interpreters/operators and project-owned shell/Python entrypoints or lifecycle hooks in that rendered configuration. `down` acts only on exact state-ledger object IDs after root/manifest/generation/ownership revalidation; it never trusts a project name, label prefix, or repository-supplied cleanup target. Crashes, concurrent worktrees, occupied ports/subnets, partial starts, migration failure, cancellation, stale state, and provider drift produce explicit recoverable dispositions. Host policy grants OCI/socket/build/network authority; untrusted PR profiles lacking that grant can plan but cannot execute the environment. + +These slices provide the generalized replacement surface for project-owned environment lifecycle and state programs. The standalone Larrimon adoption plan maps its concrete files and pure-project claim to these capabilities without making that migration a DD-078 release gate. + +--- + +## 17. Provider protocol + +Built-in providers are preferred for core HTTP, process, PostgreSQL, local fixtures, and project facts. Out-of-process providers, including CDP/OCI adapters when not built in, are allowed only through a versioned protocol and host policy. + +Protocol Slice 7P first proves this transport/framing adversarially on supported platforms without creating a public API. Only after that gate does v1 freeze inherited anonymous stdin/stdout pipes; each frame is a four-byte big-endian length followed by bounded UTF-8 JSON in a strict versioned schema. Stdout carries protocol only and stderr carries bounded redacted diagnostics. A later transport needs a protocol revision and conformance suite rather than silent substitution. + +Required protocol properties: + +- explicit handshake with protocol/provider versions and capability set; +- length-delimited messages with schema validation and message-size ceilings; +- request IDs, deadlines, cancellation, heartbeat, and terminal result exactly once; +- opaque resource handles scoped to run/provider/generation; +- no ambient inherited secrets or environment unless granted; +- structured errors and redaction metadata; +- bounded stdout/stderr separate from protocol transport; +- provider executable/digest provenance; +- crash, hang, malformed message, duplicate result, late result, and cancellation tests; +- an explicit containment class (`sandboxed` or `trusted-uncontained`) and permission manifest; protocol mediation alone is not described as syscall isolation; +- no in-process native plugin loading through this interface; +- denial of provider-requested capability escalation. + +A provider cannot declare its own result trusted merely because it emitted valid JSON. Host policy decides which provider identity may satisfy each evidence class. Pinned `trusted-uncontained` providers are fully trusted for their direct OS access and therefore forbidden in untrusted-PR/hermetic profiles; sandboxed providers receive only operation-specific handles and brokered destinations. Project-owned provider wrappers are executable repository code and fail `pure-ntnt` authoring. + +--- + +## 18. Capability and security model + +### 18.1 Trust zones + +| Input | Default trust | Authority | +|---|---|---| +| `.intent` | untrusted specification | none | +| ntnt source under test | project code | ordinary runtime capabilities | +| verification `.tnt` | executable test code | only assigned opaque test capabilities | +| repository `ntnt.toml` | authority request | cannot grant itself authority | +| host/CI policy | trusted operator configuration | grants capabilities and ceilings | +| provider binary/image | trusted only when pinned/approved | provider-specific | +| imported report | untrusted data by default | none without provenance validation | + +### 18.2 Mandatory rules + +- Static lint and plan inspection execute no project code. +- Network defaults to loopback and declared resource destinations. +- Public live-network smoke requires an explicit profile, host grant, destination policy, and visible report marker. +- Private/link-local/metadata destinations require stronger explicit grants; production credentials are never implied. +- Destination policy is enforced after resolution and on every redirect/reconnect; DNS rebinding or a later private address cannot inherit approval from an earlier public answer. +- Filesystem access is root-confined and symlink-safe; writes go only to assigned temp/artifact locations unless granted. +- Process execution uses exact argv and executable identity; no shell. +- Environment is empty by default apart from runtime essentials and allowed names. +- Secret inputs remain opaque and are redacted recursively from values, diffs, logs, URLs, headers, SQL diagnostics, artifact metadata, and textual artifacts. Binary/browser artifacts follow the separate sensitive-artifact policy because arbitrary pixels and opaque formats cannot be reliably redacted. +- Each provider/action has time, byte, row, process, request, redirect, and concurrency ceilings clamped by host policy. +- Cleanup authority is retained by the supervisor and cannot be discarded by test code. +- A timeout or cancellation never becomes a pass. +- Unsupported capability, platform, assertion, or evidence schema fails closed in strict profiles. +- JSON output never mixes banners or diagnostics on stdout. +- Providers capable of spend, public mutation, deployment, device configuration, or other irreversible side effects are denied in ordinary verification. A future explicit live-validation profile must expose estimated/hard budget, destination, idempotency/cleanup semantics, and separate host approval; it cannot be enabled merely by repository manifest changes. +- OCI/container authority is separate from ordinary process authority. Managed containers require pinned images and deny privileged mode, host networking, host PID/IPC, device access, arbitrary bind mounts, and Docker-socket mounting unless each is independently granted by host policy. +- CI for untrusted pull requests uses an unprivileged policy with no production secrets, private-network grants, host container socket, or deployment credentials. A repository change to `ntnt.toml` or verification code cannot modify the external policy that grants those capabilities. + +### 18.3 Baseline resource limits + +Defaults are conservative and host policy may lower them. Project configuration may request increases only up to host maxima. + +| Resource | Default | Suggested host maximum | +|---|---:|---:| +| case deadline | 30 s | 10 min | +| suite deadline | 15 min | 2 h | +| eventual wait | 5 s | 5 min | +| action output per stream | 1 MiB | 16 MiB | +| HTTP response body | 1 MiB | 16 MiB | +| database rows | 1,000 | 100,000 | +| database result bytes | 8 MiB | 64 MiB | +| managed processes | 16 | 64 | +| cumulative process launches | 64 | 512 | +| process tree PIDs/threads | 128 | host clamp | +| process CPU/memory | 2 cores / 2 GiB | host clamp | +| open files/sockets per process | 256 / 128 | host clamp | +| scratch + temp disk | 1 GiB | host clamp | +| aggregate network connections | 128 | host clamp | +| aggregate database connections | 64 | host clamp | +| concurrent actors | 32 | 256 | +| browser contexts/pages | 4/8 | 16/32 | +| artifacts per suite | 100 MiB | 1 GiB | + +One monotonic whole-run budget includes planning, startup, retries, readiness, actions, decoding, teardown, and report construction; nested budgets do not reset it. Bytes are charged at the read boundary, including malformed frames. CPU, memory, PIDs/threads, file descriptors, disk, descendants, and sockets require OS/container enforcement for any profile claiming containment. If those controls or descendant guarantees are unsupported, that profile blocks rather than merely printing a caveat. Exact numeric limits may be adjusted through implementation review, but unbounded or cooperative-only containment claims are not acceptable. + +--- + +## 19. Reports and CI contract + +JSON is a versioned public contract. A run report includes: + +- report schema and ntnt version/commit; +- run ID, profile, platform, start/end/duration; +- immutable repository identity, full subject commit/requested ref, and workflow/run/attempt/trust identity; +- claim level (`project-authored-claim` or `protected-contract-execution-claim`), protected-contract raw/canonical digests plus trusted base repository/ref/full commit/tree and protected-inventory identity, and authoring-purity disposition; +- immutable input-snapshot digest plus project root identity, exact consumed source/Intent/verifier/fixture/migration/manifest/lockfile/provider-input hashes, effective host-policy digest and trust class, plan hash, runtime/provider/environment identities, and source-drift result; +- requested, granted, and denied capabilities without secret values; +- resource lifecycle, containment class/guarantees, authenticated ledger IDs, and cleanup results; +- every feature/scenario/outcome obligation with all truth dimensions; +- test/evidence IDs, source locations, provider/tool versions, timings, attempts, seed, and disposition; +- bounded expected/actual structural diffs; +- redaction and truncation markers; +- artifacts by digest/path/media type; +- implementation, executable, and verified coverage as separate metrics. + +Exit behavior for strict profiles: + +| Condition | Exit | +|---|---:| +| all required obligations current and passed; authoring purity proven when required; cleanup succeeded | 0 | +| failed, flaky, unbound, unsupported, blocked, stale, disallowed skip, no-result, or cleanup failure | 1 | +| invalid spec/manifest/policy/plan, purity violation/not-checked, or protected-contract scope regression | 2 | +| internal ntnt/provider protocol defect | 3 | + +JUnit is derived from the same ledger. It must not recompute truth differently. Human output is a rendering of the same report. + +`ntnt intent coverage --json` reports at least: + +- implementation-linked feature/outcome coverage; +- executable obligation coverage; +- verified current obligation coverage; +- documentation-only counts; +- thresholds and unmet IDs. + +--- + +## 20. CLI surface + +Planned commands and compatibility: + +```bash +# Safe, static +ntnt intent lint . +ntnt intent plan . --profile full --json +ntnt intent coverage . --json + +# Execute +ntnt intent check . --profile full +ntnt intent check . --profile full --report-json report.json +ntnt intent check . --profile http --base-url http://127.0.0.1:8081 +ntnt test verification/reducer_cases.tnt + +# Reproduce +ntnt intent replay report.json --case test.reducer.golden-replay + +# Typed project environments +ntnt project env init staging +ntnt project env up dev +ntnt project env up staging +ntnt project env status staging --json +ntnt project env down staging + +# Resource diagnostics +ntnt intent doctor . --profile full +ntnt intent clean . --stale --dry-run +``` + +Existing `ntnt intent check server.tnt`, direct technical `test:` blocks, and `ntnt test server.tnt --get ...` remain compatibility surfaces during migration. They are implemented through the shared planner/executor and emit deprecation guidance only when a safer project form is available. + +Replay treats the report as untrusted selection data. It may recover a case ID, seed, and requested profile, but it re-discovers current project sources, rebuilds the plan, revalidates hashes, and reacquires authority from the current host policy. It never executes provider paths, environment values, or capability grants copied from a report. + +`intent clean` consults the supervisor-owned authenticated ledger for the canonical project and current operator policy. It can reconcile only exact recorded objects with valid ownership tokens; project files, report contents, names, prefixes, or glob scans cannot nominate cleanup targets. Dry-run output uses safe resource IDs only. + +`--json` prints JSON only. A file argument should be separated from output naming to avoid stdout ambiguity during implementation. + +--- + +## 21. Relationship to DD-077 and other systems + +DD-078 owns verification orchestration and evidence. The audited DD-077 candidate is in `https://github.com/ntntlang/ntnt.git` at commit `f0132afcff984bb43305be39122d7e74a6850396`, document `design-docs/dd-077-correctness-primitives-roadmap.md`, Git blob `31a6d82f79e6051a7f00bfb182c979e5e78f2c3f`, on a separate unmerged lineage; it is not an ancestor of this DD. It is design evidence only until its owning document and implementations merge. DD-078 uses that document's literal owning identifiers rather than inventing aliases: + +- DD-077 PR 0A owns the callback bridge; Design spike 0B and PRs 2C–2E own shared network policy/transport; PRs 1B–1C own migration lifecycle; Design spike 0C/PR 4B own static effects. DD-077 also owns scoped PostgreSQL transactions, leases/fencing, purity, and production runtime context. +- DD-078 owns isolated test databases/schemas, migration evidence, held test transactions, barriers, and resource cleanup. +- DD-062 owns trust for compiled extension libraries. DD-078's external provider protocol is out-of-process, does not authorize native in-process loading, and claims no sandbox beyond its separately reported containment class. +- DD-037 owns production job semantics. DD-078 owns observation, orchestration, failure injection, and evidence for those semantics. +- DD-047 owns network-monitoring primitives and catalogs. Its audited source is ntnt commit `5a24c0cd1ff2f4d58e77ef263346cf6828cd28d6`, path `design-docs/dd-047-std-netmon.md`, blob `41b644195e2aaa81997f76631daa8bae5e5cb53c`; source identity does not satisfy its unimplemented Slice 1C or PR 2. DD-078 owns bounded local fixtures and application verification around those APIs only after the plan ledger records their exact implementation merges. +- DD-065/`std/harness` would own production agent/tool execution, but this baseline contains no DD-065 design/owner artifact. DD-078 therefore excludes effect-transcript and tool-using production cases; deterministic protocol/AI fixtures and no-tool assertions do not substitute for that missing contract. + +DD-078 truth-accounting, project, policy, contract, purity, snapshot, and concrete-grant slices may proceed independently. Any externally dependent slice blocks until the implementation plan's generalized prerequisite ledger names the exact owner/source and records every required implementation merge. DD-077 PR 0A gates callback consumers; Design spike 0B plus PRs 2C–2E gate shared HTTP/network work; PRs 1B–1C gate migration consumers. DD-047 Slice 1C and PR 2 gate catalog/recognition acceptance Slice 18B. DD-078 Slices 10P/10B exclusively own the missing generic internal runtime observation/clock seam. DD-078 ships no temporary public traits, verification-only callback special cases, provider fallback, or duplicate network/migration seam. + +--- + +## 22. General adoption contract + +DD-078 defines a project-neutral adoption protocol: pin an immutable project inventory, classify every relevant path exactly once, bind a protected contract and execution snapshot to that identity, dual-run old and new checks, require semantic mutation/fault witnesses, and delete compensating code only after equivalent or stronger evidence passes on clean CI. + +The protocol itself is normative and is accepted with project-neutral fixture repositories. No particular application inventory, migration wave, helper deletion, or adoption completion date participates in the DD-078 core DAG, release sequence, or definition of done. Consumer projects maintain separate adoption plans that bind their own invariants to landed DD-078 capabilities. + +Larrimon is the first reference consumer. Its immutable baseline, Waves A–E, migration compatibility Slice 16M, deletion authority, and future pressure corpus are tracked in [`plans/dd-078-larrimon-adoption.md`](../plans/dd-078-larrimon-adoption.md). That plan may expose missing generalized capabilities, but cannot change ntnt APIs or block completion of the project-neutral runtime. + +--- + +## 23. Illustrative future-pressure matrix (non-normative) + +| Reference-consumer pressure | Generalized DD-078 mechanism | +|---|---| +| pure reducer, replay, backtest | typed values, golden fixtures, deterministic seed/time, property/subcase reports | +| signup/invite/Turnstile | stateful HTTP, independent identity/IP/purpose rate-limit actors, provider stub, verified-email membership fixture, transactional side-effect/rollback evidence | +| unified egress policy | shared production/verification transport policy, IPv4/IPv6 classification, metadata denial, scripted DNS rebinding, per-hop redirect/reconnect checks, credential stripping, private-node scope | +| tenant/RLS/security definer | isolated PostgreSQL roles/databases, direct SQL observations, app HTTP sessions | +| wrapped secrets/KMS release | typed KMS/secret-service fixture, AES-GCM nonce/AAD and envelope/rewrap vectors, purpose/run/node binding, expiry/write-only tests, KMS denial, proof agents never receive KEK/KMS authority | +| durable scheduler/probe workers | multi-process resources, eventual assertions, restart, queue observations | +| race-safe claims/projections/suppression | actors, barriers, held transactions, bounded deadlock diagnostics | +| alerts/email/webhooks | SMTP/webhook capture, stable-event assertions, fault/ambiguous outcome fixtures | +| SNMP/MIB/device inventory | UDP/binary scripted fixtures, counter wrap/reset/rate normalization vectors, gated real-network profile, secret redaction | +| NETCONF/gNMI/device onboarding | typed NETCONF plus gRPC/HTTP2 streaming/event-source providers with auth, ordering, reconnect, subscription flow-control/backpressure, bounded retention, and capability-scoped device smoke | +| syslog/inbound telemetry | TCP/UDP/TLS event-source fixtures, malformed/auth/order/reconnect/backpressure cases, bounded retention and immutable ingestion evidence | +| multi-node control plane | multiple app/agent processes, signed request fixtures, clocks, anti-replay concurrency, encrypted completion-spool failover replay | +| agent/tool harness | DD-065 effect-transcript provider, allow/deny capability assertions, bounded tool/network budgets, deterministic no-tool and tool-using cases; outside DD-078 and blocked because this baseline has no DD-065 design/owner artifact | +| AI hypotheses/discovery | deterministic provider stub, schema/evidence assertions, call/token counters, no-tool/network policy | +| plans/billing/usage | external API/webhook fixture, deterministic clock, idempotency and signature assertions | +| retention/partitions/legal hold | database resources, clock control, large bounded fixture generation | +| load/backpressure/priorities | bounded actor/load provider, resource metrics, starvation/deadline assertions | +| browser/HTMX/no-JS | CDP contexts, interception, focus/history/DOM/accessibility evidence | +| migrations/upgrades/rollback | DD-077 PRs 1B–1C migration integration, matrix resources, image/runtime pinning | +| HA/restore/failover | external topology provider proving independent failure domains, fenced one-writer promotion, tenant home-region/data residency, encrypted completion-spool replay, canonical queue/KMS outage behavior, PITR/RPO/RTO and immutable provenance | +| upgrades/overload/game day | expand/migrate/contract compatibility across app/worker/agent versions, exact heartbeat/completion/reducer/alert priority before probes/discovery/AI, clock/DNS/certificate/KMS failures and measurable recovery evidence | +| on-prem/private networks | host policy, scoped network capabilities, customer-managed/BYO KMS and private AI routing, proof of no hosted credential or evidence fallback, gated device smoke | +| build/OCI/CI provenance | project/Git/YAML/OCI providers and evidence hashes | + +The final HA, restore, live-network, and private-device profiles are environment-backed system verification. They can still be authored in `.tnt`, but reports must not call them hermetic. This matrix is not itself an implementation owner: plan Slices 18P/18A own streaming/event sources, 19A owns KMS/spool fixtures, 19B owns bounded load, and 20P/20A/20B own recovery/topology/fault feasibility and providers. Tasks 18B, 19C, and 20C cannot begin until those exact dependencies land. The agent/tool row remains a pressure requirement only and is excluded from those releases until DD-065 gains an immutable source design, exact owner/contract, and landed implementation identities. + +--- + +## 24. Compatibility and migration + +1. Existing `.intent` syntax remains parseable. +2. Strict IDs and evidence are opt-in initially, then become the default for project-wide `intent check` at the next feature boundary. +3. Existing coverage remains available as `implementation coverage`; its label changes before thresholds change. +4. Existing simple HTTP/function scenarios are translated into the new action model and must preserve behavior except where old behavior passed unsupported assertions. +5. Unsupported assertions change from pass-with-message to fail/unsupported. This is an intentional correctness fix. +6. Old `setup` technical bindings remain parsed but produce a warning and never gain arbitrary execution semantics. +7. Studio consumes the new report but is not an implementation prerequisite for the runner. +8. Provider/report schemas are versioned. Ntnt supports at least the current and previous report schema for reading/replay; execution uses the current provider protocol. +9. Platform-specific unsupported providers are blocked during planning, not skipped after expensive resource startup. + +--- + +## 25. Acceptance criteria + +### Truth and evidence + +- [ ] Every obligation has stable identity and source location in strict mode. +- [ ] Implementation, executable, and verified coverage are separate. +- [ ] Zero-executable, unbound, unsupported, stale, blocked, and disallowed-skipped obligations fail strict mode. +- [ ] Unsupported assertions can never pass. +- [ ] JSON, JUnit, human output, and exit code derive from one evidence ledger. +- [ ] `@implements` alone cannot satisfy an obligation. + +### Runtime and security + +- [ ] Static lint/plan runs no project code or provider. +- [ ] `.intent` cannot request or exercise CLI, filesystem, network, database, process, browser, or secret authority. +- [ ] Intent may supply only bounded data to a preplanned binding; negative tests reject destinations, providers, resources, paths, secret headers, and legacy CLI/file actions. +- [ ] `pure-ntnt` authoring requires `proven` and fails planning for project-owned wrappers/providers, executable shebangs, inline workflow/package/Compose/Docker execution, unpinned actions/images, gitlinks/nested repositories, unclassified generated helpers, non-`.tnt` verification/support, SQL-only/browser harnesses, or untrusted exclusions; violations and exclusions are reported. +- [ ] Project requests are intersected with external host policy. +- [ ] Privileged policy and protected evidence contracts originate outside repository-controlled argv, use the same inherited-handle `TrustedInput` loader, reject unknown/non-canonical/duplicate envelope fields, and use separate frozen domains that sign the exact raw-payload SHA-256 before parsing; immutable base repository/commit/tree and protected inventory remain bound. +- [ ] Effective policy identity is always digest-bound, and hardlink/symlink/writable-ancestor/TOCTOU/malformed-policy attacks fail closed. +- [ ] Plan, execution, and report consume one immutable content-addressed snapshot; launch identity and source drift are checked. +- [ ] Paths are project-confined and symlink-safe. +- [ ] Exact argv execution has no shell expansion. +- [ ] Handles are opaque, generation-bound, unforgeable, and invalid after scope. +- [ ] Semantic `EffectKind` never authorizes an operation; every effectful sink validates an exact run/case/generation/resource/operation `VerificationGrant`. +- [ ] Constructors, provider output, serialization, globals, and concurrent runs cannot widen or cross resource grants. +- [ ] Clean environment, recursive redaction, output bounds, deadlines, cancellation, and cleanup are adversarially tested. +- [ ] Provider crash/hang/malformed/late/duplicate messages fail closed and clean resources. +- [ ] Verification authority cannot be bypassed through direct or transitive imports, aliases, module initializers, or ordinary effectful stdlib calls. +- [ ] Untrusted executable/browser/provider profiles use enforceable OS containment and brokered egress; trusted-uncontained execution is visibly prohibited from protected PR lanes. +- [ ] CPU, memory, PIDs/threads, descriptors, disk, sockets, and descendants are bounded below project code. +- [ ] Stale cleanup uses authenticated exact host-ledger records rather than project labels or prefix scans. +- [ ] Strict resources prove a durable `reserve β†’ create β†’ finalize β†’ expose` broker/backend protocol and crash recovery at every boundary; unsupported backends are non-verifying and blocked from protected profiles. +- [ ] Strict/protected Redis uses the brokered disposable-instance lifecycle and proves zero residual keys/credentials after completed cleanup/reconciliation; pending cleanup cannot pass, and attached ACL mode is non-verifying. +- [ ] Imported strict evidence uses a supervisor invocation record or canonical signed, expiring, replay-resistant envelope. +- [ ] Project-wide execution is strict by default; diagnostic mode is explicitly non-verifying and cannot satisfy obligations. +- [ ] Uncatchable termination limitations are explicit; supervisor-crash and startup orphan-reaper paths are tested against authenticated ledger records. + +### Application verification + +- [ ] Structured function arguments/results and first-class assertions replace local assertion helpers. +- [ ] Stateful HTTP supports headers, forms, cookies, redirects, captures, multiple clients, and attach mode. +- [ ] PostgreSQL supports isolated committed fixtures, roles/RLS, migration evidence, direct observations, and cleanup. +- [ ] Managed processes support readiness, expected failure, logs, restart, exit, and process-tree cleanup. +- [ ] Local HTTP/SMTP/webhook/TCP/UDP fixtures support strict scripted behavior. +- [ ] Eventual assertions use one bounded deadline and report attempts/final observation. +- [ ] Named actors/barriers reproduce application-defined claim/scheduler/projection races without sleeps in project-neutral fixture applications. +- [ ] Browser cases cover authenticated, HTMX, no-JavaScript, focus/history, and reconciliation behavior from `.tnt`. +- [ ] Project/provider facts replace the audited Python provenance and architecture checks without granting arbitrary shell. + +### Adoption portability + +- [ ] A project-neutral fixture repository exercises the complete adoption protocol: immutable inventory, exact-once classification, protected contract/snapshot binding, old/new parity, mutation/fault witnesses, and evidence-backed deletion eligibility. +- [ ] The adoption protocol produces reusable machine-readable inputs and reports without project names or paths in public APIs, schemas, defaults, policies, fixture semantics, or privileged modes. +- [ ] A consumer adoption plan can bind its own inventory and migration waves to landed capabilities without joining or changing the DD-078 core DAG, releases, or completion criteria. +- [ ] The Larrimon reference-adoption checklist remains separately reviewable in [`plans/dd-078-larrimon-adoption.md`](../plans/dd-078-larrimon-adoption.md) and is not evidence that the project-neutral runtime itself passed. + +--- + +## 26. Open implementation questions + +These are implementation decisions, not permission to weaken the architecture: + +1. Whether project-wide execution remains under `ntnt intent check` alone or gains a future `ntnt verify` alias. The canonical first command is `ntnt intent check .`. +2. Whether a later language release introduces native `test fn` syntax. V1 comment metadata is fixed as `@test`, `@verifies`, `@uses`, `@tags`, `@fixture`, `@scope`, `@teardown`, and `@fixtures`. +3. Whether browser CDP ships in core or as an ntnt-maintained signed provider package. The project-facing API and evidence contract remain the same. +4. Exact resource-limit defaults after performance measurement. +5. How much virtual-time control can be safely exposed to managed app processes without creating a production footgun. +6. Which static project facts belong in core versus optional maintained providers. +7. Provider package discovery and lockfile format, coordinated with DD-062. + +--- + +## 27. Rejected alternatives + +### Run the existing scripts from Intent + +Rejected. It preserves ambient authority, shell portability problems, hidden setup, weak evidence, and unreliable cleanup. + +### Put SQL directly in `.intent` + +Rejected. Intent is an obligation layer, not a privileged database script. SQL may remain in migrations or bounded `.tnt` provider calls under explicit database authority. + +### Treat every skipped scenario as passing + +Rejected. A precondition mismatch is useful diagnostic data, not evidence that the promised behavior holds. + +### Build a universal YAML workflow engine + +Rejected. Ntnt needs a bounded verification planner and resource graph, not a second general-purpose CI language. + +### Keep specialist tests forever and only import JUnit + +Rejected as the target for ntnt application projects. Imported evidence is useful, but it does not achieve project-owned pure ntnt verification. Maintained providers should expose the specialist engine through `.tnt` where feasible. + +### Bundle a browser engine or database server into the ntnt binary + +Rejected. Ntnt owns lifecycle and evidence; external systems retain their own release and security boundaries. + +--- + +## 28. Delivery + +Implementation is split into reviewable, test-first PRs in the companion plan: + +[DD-078 implementation plan](../plans/dd-078-intent-verification-implementation.md) + +The design PR authorizes no production implementation by itself. Each runtime slice needs its own focused PR, security review proportional to new authority, full regression gates, generated-document truth sync, and a project-neutral acceptance corpus. Consumer migrations and their deletion gates land in separate adoption PRs against pinned runtime commits; Larrimon is the first such consumer, not a privileged runtime mode or core completion gate. diff --git a/design-docs/ial_vision_v2.md b/design-docs/ial_vision_v2.md index b2ac18f1..b90f78e2 100644 --- a/design-docs/ial_vision_v2.md +++ b/design-docs/ial_vision_v2.md @@ -1,9 +1,16 @@ # IAL Vision V2: Beyond Unit Testing -**Status:** Planning +**Status:** Historical planning; execution roadmap superseded by DD-078 **Date:** January 2026 **Prerequisites:** V1 Complete (Phases 0-5) +> **Supersession note (2026-07-28):** [DD-078](dd-078-intent-verification-runtime.md) +> now owns the obligation truth model, executable evidence, project verification +> runtime, capability/resource boundaries, provider model, and implementation +> sequence. This document remains useful historical context for glossary term +> rewriting, agent protocol ideas, and Intent Studio presentation, but its +> UI-first delivery order is no longer current. + --- ## Executive Summary diff --git a/plans/dd-078-intent-verification-implementation.md b/plans/dd-078-intent-verification-implementation.md new file mode 100644 index 00000000..f52398e2 --- /dev/null +++ b/plans/dd-078-intent-verification-implementation.md @@ -0,0 +1,1211 @@ +# DD-078 Intent Verification Runtime β€” Implementation Plan + +> **For Hermes and ntnt contributors:** Execute core slices in dependency order with RED β†’ GREEN β†’ REFACTOR. Keep generalized ntnt runtime changes and consumer-adoption migrations in separate PRs; consumer plans may use only pinned, reviewed runtime commits. + +**Goal:** Deliver the DD-078 Intent Verification Runtime so a production application can declare durable behavior in `.intent`, implement all project-owned tests in `.tnt`, declare resources/profiles in `ntnt.toml`, and run the complete suite through `ntnt intent check .` without project-local Bash, Python, JavaScript test, or SQL-only test harnesses. + +**Architecture:** Compile Intent into stable obligations; discover linked `.tnt` verification functions; plan an authority-checked resource DAG; execute cases in isolated interpreters through one action/observation model; supervise external resources; record one evidence ledger; render human, JSON, and JUnit outputs from that ledger. Specialist systems remain external resources behind typed, bounded providers. + +**Baseline:** `origin/main` at plan authoring was `79c61dd98b0f10e3f6c1bce4f1d6e4df2343a21f` (ntnt 0.5.3). Rebase each implementation branch onto current `origin/main` before work. The audited DD-077 candidate is in `https://github.com/ntntlang/ntnt.git` at commit `f0132afcff984bb43305be39122d7e74a6850396`, document `design-docs/dd-077-correctness-primitives-roadmap.md`, Git blob `31a6d82f79e6051a7f00bfb182c979e5e78f2c3f`, on a separate unmerged lineage; it is not an ancestor of this plan. Only DD-077's literal owning sections/PR identifiers below are dependencies. Their owning design and implementations must merge, and their exact merge commits must replace the candidate SHA in this ledger, before any dependent DD-078 branch starts. No DD-078 fallback contract is permitted. + +**Reference adoption / primary pressure test:** [`larimonious/larrimon`](https://github.com/larimonious/larrimon) at immutable commit `ceadfd992d1435ac27afb054968ff5569d697ce1`, recorded in [`dd-078-larrimon-baseline.md`](dd-078-larrimon-baseline.md) and governed by the standalone [`dd-078-larrimon-adoption.md`](dd-078-larrimon-adoption.md). Dirty-worktree bytes are not baseline evidence. Any changed base requires regenerating the canonical inventories and protected contract before deletion. + +**Generalization boundary:** The dependency table and Tracks A–G define reusable ntnt mechanisms. Application adoption plans are separate consumers: they may prove that the mechanisms are sufficient, but they do not participate in the core DAG, release sequence, or definition of done and may not introduce project-specific public APIs, schemas, keywords, defaults, fixture semantics, or privileged runtime modes. Every runtime slice lands with project-neutral fixtures and tests before an adoption plan consumes it. + +**Baseline gate note:** On the authoring host with Rust 1.94, `cargo nextest run` passed 1,962/1,962 tests (including the two-test DD-078 plan-consistency binary), but `cargo clippy --all-targets -- -D warnings` is already red on three unchanged `build.rs` lints (`collapsible_if` and two `manual_strip`). Before Task 1, either repair those baseline warnings in a separate narrow hygiene PR or pin/document the supported Rust toolchain that remains green. Do not bury baseline repair in the first verification feature diff. + +--- + +## Delivery rules + +1. Numbered tasks are portfolio epics. One focused ntnt PR lands per lettered slice in the dependency table below; no PR may silently combine slices. +2. Every behavior change starts with a failing Rust integration/unit test or fixture-app test. +3. Every new authority-bearing feature receives negative, timeout, cancellation, redaction, and cleanup tests in the same PR. +4. Existing compatibility paths remain green until their documented removal window. +5. No unrestricted shell execution, inline Intent SQL, ambient secret access, or unbounded provider output. +6. New public stdlib APIs require generated docs and examples. +7. New report/provider schemas carry explicit integer versions and committed fixtures. +8. Reference-adoption PRs consume pinned reviewed ntnt commits; they do not patch the runtime inside an app repository. Larrimon is the first such consumer. +9. Independent review uses immutable commits, not moving worktrees. +10. A PR is not complete because focused tests pass; run the appropriate full ntnt gate and record actual output. +11. Every project deletion gate inherits the generalized invariant-ledger and semantic mutation/fault-witness requirements from DD-078 Β§22; count/line parity alone is never sufficient. + +### External prerequisite ledger + +Every dependency beginning with `DD-` must name one exact row below. A design source is audit provenance, not a satisfied implementation prerequisite. Before a dependent branch starts, a docs truth-sync PR records the source design's merged commit/blob and every required implementation merge commit here; absent/unmerged rows remain hard blockers. A spike is a gate, never a production contract. + +DD-077 source identity: repository `https://github.com/ntntlang/ntnt.git`, candidate commit `f0132afcff984bb43305be39122d7e74a6850396`, path `design-docs/dd-077-correctness-primitives-roadmap.md`, blob `31a6d82f79e6051a7f00bfb182c979e5e78f2c3f`. DD-047 source identity: the same repository, design commit `5a24c0cd1ff2f4d58e77ef263346cf6828cd28d6`, path `design-docs/dd-047-std-netmon.md`, blob `41b644195e2aaa81997f76631daa8bae5e5cb53c`. + +| External owner | Required artifact | Depends on | Current status in this plan | +|---|---|---|---| +| DD-077 PR 0A | reusable native callback bridge with cleanup on every exit shape | merged DD-077 design | unmerged design only | +| DD-077 Design spike 0B | outbound transport binding feasibility note/fixtures; no production API | merged DD-077 design | unrun design gate | +| DD-077 PR 2C | trusted network configuration, internal capability core, shared target classification | DD-077 Design spike 0B | unimplemented | +| DD-077 PR 2D | policy-bound HTTP transport and public capability API | DD-077 PR 2C | unimplemented | +| DD-077 PR 2E | `std/net` integration with the same policy engine | DD-077 PR 2D | unimplemented | +| DD-077 PR 1B | `ntnt db status/plan/migrate/verify`, checksums, lock, lifecycle foundation | merged DD-077 design | unimplemented | +| DD-077 PR 1C | non-transactional migration hardening and dirty recovery | DD-077 PR 1B | unimplemented | +| DD-047 Slice 1C | canonical MIB catalog compiler/runtime registry, profiles, and finite plans from DD-047 Β§Implementation Plan | landed DD-047 design identity above | unimplemented; no implementation merge identity recorded | +| DD-047 PR 2 | device recognition and bounded inventory execution from DD-047 Β§Implementation Plan | DD-047 Slice 1C | unimplemented; no implementation merge identity recorded | + +DD-077 Design spike 0C and PR 4B own static effect-metadata coverage/transitive analysis. They do not own runtime authority and are not DD-078 prerequisites: Slice 2G independently inventories and mediates every verification-mode sink with concrete grants. DD-077 defines no runtime clock/observation seam, so this plan assigns that generic internal seam exactly once to DD-078 Slices 10P/10B. DD-065 has no source design artifact in this baseline; production agent/tool execution therefore remains explicitly outside this plan rather than appearing as a satisfiable dependency. + +### Dependency-closed DD-078 PR slices + +| Slice | Scope | Depends on | +|---|---|---| +| 1A | status algebra, stable IDs, false-pass fixes | Task 0 | +| 1B | JSON/human report schema and exit parity | 1A | +| 2A | canonical project root, manifest, deterministic discovery | 1B | +| 2B | privileged host-policy authentication and ceiling intersection | 2A | +| 2C | protected evidence contract and base-ref scope continuity | 2B | +| 2D | exhaustive pure-authoring project-file classification | 2C | +| 2E | immutable input snapshot and launch identity | 2D | +| 2F | resource/profile planner and deterministic dry plan | 2E | +| 2G | concrete resource-grant substrate and verification authority enforcement | 2F | +| 3A | adapt verification invocation to landed DD-077 PR 0A; no new bridge | DD-077 PR 0A, 2G | +| 3B | test metadata and binding discovery only | 3A | +| 3C | fresh verification interpreter, opaque context, environment/registry isolation | 3B | +| 3D | typed assertions, redaction, snapshots, assertion evidence | 3C | +| 3E | fixture DAG and bounded teardown | 3D | +| 4 | seeded table/property generation and replay; no virtual clock | 3D | +| 5A | adapt verification HTTP to landed DD-077 PRs 2C–2E | DD-077 PR 2E, 2G | +| 5B | stateful test sessions/captures/assertions | 5A, 3D | +| 6A | cross-platform containment/readiness feasibility spike | 2E | +| 6B | process supervisor, host ledger, cleanup, attach mode | 5A, 6A, 3D | +| 7P | provider-protocol feasibility/adversarial framing spike; no public API | 2G, 6B | +| 7A | frozen stdio provider protocol and adversarial conformance fixture | 7P | +| 7B | strict scripted HTTP/HTTPS and webhook fixture | 7A | +| 7C | SMTP/mail capture fixture | 7A | +| 7D | TCP/UDP/DNS and byte-script fixture | 7A | +| 7E | root-confined temporary workspace fixture | 7A | +| 7F | deterministic typed AI/payment/API stub fixture | 7A | +| 8 | PostgreSQL lifecycle/assertions and migration evidence | DD-077 PR 1C, 7A | +| 9 | Redis disposable lifecycle plus queue/mail/webhook observations | 3E, 7B, 7C | +| 10A | eventual observations on monotonic deadlines | DD-077 PR 0A, 3D | +| 10P | runtime clock/observation inventory and feasibility spike; no public API | 3C | +| 10B | verification clock controls over the DD-078-owned internal runtime observation seam | 2G, 10A, 10P | +| 10C | stop/restart/readiness/fault lifecycle controls | 6B, 10A–10B | +| 11A | deterministic actors/barriers/race observations | 6B, 8, 10A–10B | +| 12P | Chromium/CDP containment/egress feasibility spike; no public API | 5A, 6A, 7P | +| 12A | sandboxed browser provider, provenance, containment, egress | 6B, 7A, 12P | +| 12B | typed browser sessions, DOM/network/screenshot and reconciliation API | 3D, 12A | +| 13A | extract reusable project inspection from `src/main.rs`/Studio/interpreter scanners | 2A | +| 13B | core ntnt AST/import/route/effect/project facts | 2G, 3D, 13A | +| 13C | Git and bounded JSON/YAML/TOML/XML/text facts | 2G, 13A | +| 13D | OCI/migration/runtime provenance facts and reusable read-only OCI client | DD-077 PR 1C, 7A, 8, 13A | +| 13E | first-class `Constraint` parser/binding after a dedicated syntax decision | 13B | +| 14A | imported evidence and canonical signed envelope | 1B, 7A | +| 14B | JUnit renderer, Studio, docs, editor migration | 14A | +| 14C | typed project-state, locks/leases, allocation transaction substrate | 2G, 6B | +| 14D | typed `ntnt project env` init/up/down/status OCI lifecycle, brokered daemon allocation/ingress, and effective-config validation | DD-077 PR 1C, 7A, 13D, 14C | +| 18P | streaming/event-source feasibility spike: NETCONF, HTTP/2/gRPC, TLS/syslog, flow control | 7A, 7D | +| 18A | typed streaming/event-source fixture/provider contracts | 18P, 7A | +| 18B | monitoring protocol, catalog, and inventory acceptance profiles | 18A, 13A, DD-047 Slice 1C, DD-047 PR 2 | +| 19A | KMS/secret-service and encrypted completion-spool fixtures | 7A, 7E, 10C, 14C | +| 19B | bounded load/backpressure provider and evidence schema | 6B, 7A, 10B, 11A | +| 19C | multi-agent, AI, alerting, retention acceptance profiles | 7F, 9, 19A, 19B | +| 20P | backup/restore and multi-node fault/topology feasibility spike | 14D, 19A, 19B | +| 20A | backup/PITR/restore provider and immutable recovery evidence | 20P, 7A | +| 20B | multi-node topology, fencing, partition, and outage provider | 20P, 7A, 14D | +| 20C | upgrade, HA, on-prem, BYO-KMS/private-AI acceptance profiles | 7F, 19A, 20A, 20B | + +Each task below supplies the acceptance detail for exactly one slice. The table above is the sole dependency source of truth; every owner repeats its exact dependency cell as `Table dependencies`. Task 0's mechanical plan-consistency check rejects duplicate/unknown/cyclic dependencies, owner/table drift, external-ledger drift, release groups without transitive closure, production-bearing spikes, and missing/duplicate owners. + +--- + +## Planned module layout + +Create the new subsystem outside the current 7,500-line `src/intent.rs`: + +```text +src/verification/ + mod.rs + model.rs # obligation/evidence/report domain types + ids.rs # stable IDs and validation + discovery.rs # Intent/test/project discovery + manifest.rs # ntnt.toml verification schema + policy.rs # host grants and ceiling intersection + contract.rs # operator-owned protected obligation/evidence baseline + purity.rs # mechanically proven pure-ntnt authoring closure + snapshot.rs # immutable content-addressed execution inputs + planner.rs # resource DAG and executable plan + executor.rs # case orchestration + assertions.rs # typed comparisons/diffs + actions.rs # action/observation traits/enums + report.rs # ledger aggregation and exit decision + redact.rs # recursive redaction/truncation + supervisor.rs # processes/resources/deadlines/cleanup + provider/ + mod.rs + protocol.rs + process.rs + http.rs + postgres.rs + fixtures.rs + browser.rs + +src/project_inspection.rs # shared root-confined project facts; available before provider namespace +``` + +The exact split may be adjusted to keep files coherent. Shared operational support lives outside verification in `src/project_state.rs` and `src/project_env/`; it still consumes the same canonical project, policy, provider, grant, and lifecycle-ledger contracts. Do not add new execution behavior to `src/main.rs`; CLI code should parse arguments and call library functions. + +--- + +# Track A β€” Truth before power + +## Task 0: Land DD-078 design only + +**Files:** + +- Add: `design-docs/dd-078-intent-verification-runtime.md` +- Add: `plans/dd-078-intent-verification-implementation.md` +- Add: `plans/dd-078-larrimon-baseline.md` +- Add: `tests/dd078_plan_tests.rs` (documentation/DAG consistency only) +- Modify: `design-docs/README.md` +- Modify: `design-docs/ial_vision_v2.md` + +**Steps:** + +1. Add DD-078 and this plan. +2. Mark the execution phase order in `ial_vision_v2.md` as superseded by DD-078; retain historical term-rewriting/Studio material. +3. Register DD-078 in the design-document index. +4. Add tests that parse the table and every owner, expand ranges, and reject duplicate/unknown/cyclic dependencies, owner/table drift, generalized external-ledger or task-owner drift, incomplete core release closure, missing parent-module registration or transitive parent-creator dependency, production-bearing feasibility spikes, fictional aliases, identity loss, and missing/duplicate owners; include negative mutation fixtures for representative failures. +5. Run Markdown/link checks, the focused DAG test, and `cargo fmt --check`; the only Rust change is non-runtime plan validation. +6. Obtain architecture, security, and implementation-plan review against the exact staged diff. + +**Acceptance:** Design has explicit generalized pure-project scope and project-neutral runtime fixtures, authority model, provider boundary, a linked but non-gating consumer-adoption protocol, real DD-077 owner identifiers, report truth model, and mechanically valid implementation DAG. No runtime behavior changes. + +--- + +## Task 1A: Stable obligation identity and truth model + +**Table dependencies:** Task 0 + +**Create:** `src/verification/mod.rs`, `src/verification/model.rs`, `src/verification/ids.rs`, `tests/verification_truth_tests.rs`, and truth `.intent` fixtures. +**Modify:** `src/lib.rs` and `src/intent.rs` scenario/feature/outcome parsing. + +**RED:** Reject duplicate/malformed feature/scenario/outcome IDs with source locations; report zero-outcome behavioral features as `unproven`; distinguish justified feature-level documentation-only declarations without allowing outcome-level suppression; and prove linked-but-unexecuted obligations have implementation coverage but zero executable/verified coverage. + +**GREEN:** Add stable IDs and compatibility-derived IDs with warnings. Define `Obligation`, `EvidenceBinding`, orthogonal declaration/linkage/executability/disposition/freshness dimensions, source spans, and implementation/executable/verified coverage types. Unknown or unresolved assertions fail closed. No renderer, JSON schema, threshold, or exit-code behavior enters 1A. + +**Gate:** focused parser/ID/model tests, full Intent parser tests, fmt/clippy, and immutable review. + +--- + +## Task 1B: One evidence ledger, schema, rendering, and exit status + +**Table dependencies:** 1A + +**Create:** `src/verification/report.rs` and `tests/fixtures/verification/reports/schema-v1.json`. +**Modify:** `src/verification/mod.rs` registration, `src/main.rs` Intent check/coverage JSON and exit mapping, `docs/IAL_REFERENCE.md`, and `tests/intent_studio_tests.rs`. + +**RED:** Cover unbound, unsupported, blocked, skipped, stale, failed, flaky, cancelled, no-result, and current-passed evidence; fail strict exit for every unmet required binding; retain diagnostic fail-then-pass history; qualify results by profile; require one evidence atom for every selected binding; keep advisory/excluded bindings visible but non-satisfying; reject fast-profile evidence as global/full pass; require banner-free schema-valid JSON; and prove human totals and exit status consume the same ledger. JUnit remains deferred to 14B. + +**GREEN:** Define `EvidenceResult`, `CoverageSummary`, `RunReport`, schema/freshness/version fields, live-result compatibility conversion, centralized exit decisions, JSON/threshold flags, and one human renderer. Remove ad hoc summary arithmetic from `run_intent_check_command`. + +**Gate:** `cargo test verification_truth`, full Intent and Studio tests, committed schema validation, fmt/clippy, and immutable review. + + +--- + +## Task 2A: Canonical project root, manifest, and discovery + +**Table dependencies:** 1B + +**Create:** `src/project.rs`, `src/verification/discovery.rs`, `src/verification/manifest.rs`, `tests/verification_manifest_tests.rs`, canonical project fixtures, and `docs/verification-manifest.md`. +**Modify:** `src/lib.rs` and `src/verification/mod.rs` registrations, `src/config.rs`/shared manifest loading, and `src/stdlib/secrets.rs` only to reuse ancestor-root logic. + +**RED/GREEN:** Discover nested Intent and configured verification files deterministically; define the versioned exhaustive file-class manifest; reject unknown fields, overlapping/unclassified classes, traversal, duplicate resources, ambiguous roots, build-output ambiguity, and symlink/hardlink escape. Consolidate existing root lookup without changing secret behavior. No policy, contract, purity verdict, snapshot, resource DAG, profile execution, or CLI plan enters 2A. + +**Gate:** focused manifest/root/discovery tests, secret-root regression tests, schema docs, fmt/clippy, and immutable review. + +--- + +## Task 2B: Shared `TrustedInput` and host-policy authentication + +**Table dependencies:** 2A + +**Create:** `src/verification/trusted_input.rs`, `src/verification/policy.rs`, policy/envelope fixtures, producer/consumer interoperability fixtures, and focused trust tests. +**Modify:** `src/verification/mod.rs` registrations, the operator-launcher integration, and report trust fields; repository CLI/env may only reduce authority. + +**RED:** Prove requested capabilities cannot exceed external grants and broad labels cannot choose arbitrary executable/provider/image/argument/destination/mount/output. Default/untrusted PR policy cannot reach production secrets, private networks, OCI sockets, devices, privileged containers, arbitrary mounts, deployment credentials, spend, or public mutation. Repository files/argv/env/workflow/symlinks/same-CI-user paths cannot install privileged policy. Authenticate an inherited exact payload handle plus closed canonical `PolicyTrustedInputV1` envelope using domain `ntnt-policy-trusted-input-v1\0`: verify Ed25519/key/issuer/audience/repository/ref/workflow/validity/nonce and signed lowercase SHA-256 of exact raw payload before parsing. Reject duplicate/unknown fields, non-JCS envelope bytes, payload mutation, cross-type envelope, hardlink/non-regular/writable path or ancestor, owner/ACL failure, rename/TOCTOU swap, revoked key, wrong identity, and unknown algorithm. + +**GREEN:** Implement the shared inherited-handle loader, exact policy envelope producer/consumer contract, policy parser, ceiling intersection, and raw/canonical digest plus trust-class reporting. No protected-contract semantics enter 2B. + +**Gate:** trust interoperability/adversarial fixtures on supported platforms, focused policy tests, full security-sensitive review, fmt/clippy, and immutable review. + +--- + +## Task 2C: Authenticated protected contract and base continuity + +**Table dependencies:** 2B + +**Create:** `src/verification/contract.rs`, contract/envelope/base fixtures, and focused contract tests. +**Modify:** `src/verification/mod.rs` registration and report claim-scope/input-identity fields only; planner consumption begins in 2F after `planner.rs` exists. + +**RED:** Load the contract through the same inherited-handle `TrustedInput` machinery and closed `ProtectedContractTrustedInputV1` envelope using domain `ntnt-protected-contract-trusted-input-v1\0`; apply identical exact raw-digest, file identity, owner/ACL/ancestor, hardlink/symlink, pre/post-open, signature/key/validity/identity checks. Resolve base ref in the trusted launcher to immutable repository ID plus full commit/tree OIDs. Reject cross-type envelopes, raw/canonical digest swaps, mutable-ref substitution, wrong repository/ref/workflow, rename/hardlink/mid-run replacement, contract/base/inventory retargeting, deleted/renamed obligations, weakened globs/profiles/evidence/file classes, forbidden deltas, and count drops. + +**GREEN:** Parse the authenticated contract, derive canonical semantic digest only after raw signature verification, compare the immutable base, bind raw/canonical/base/inventory identity into the plan, and emit only `project-authored-claim` or `protected-contract-execution-claim`. No project purity scan or checkout snapshot enters 2C. + +**Gate:** producer/consumer and adversarial trust fixtures, base-continuity tests, report-schema checks, fmt/clippy, and immutable review. + +--- + +## Task 2D: Exhaustive pure-ntnt classification + +**Table dependencies:** 2C + +**Create:** `src/verification/purity.rs`, executable-bearing metadata parsers, operator exclusion-lock fixtures, and adversarial purity projects. +**Modify:** `src/verification/mod.rs` registration, discovery inventory, and report purity fields. + +**RED/GREEN:** Require every tracked path exactly once in the protected classes; reject omissions/overlap, relevant untracked executables, shebangs, extensionless/renamed wrappers, symlink/hardlink escape, non-ntnt helpers, legacy CLI/file and generic shell/process/provider routes, SQL/browser harnesses, inline workflow/package/Compose/Docker execution, YAML block scripts/heredocs/substitution/operators, unpinned actions/images, arbitrary containers, unknown executable-bearing formats, Git mode `160000`, nested repositories, and unclassified generated executable closure. Check import/build graphs, provider origins, generated outputs, argv, and file identity. External exceptions require an operator origin/digest lock recursively pinning every committed object; project-generated support is never exempt. Emit the complete inventory and `proven|not_checked|violated`. + +**Gate:** all adversarial purity fixtures, deterministic inventory schema, fmt/clippy, and immutable review. + +--- + +## Task 2E: Immutable execution snapshot + +**Table dependencies:** 2D + +**Create:** `src/verification/snapshot.rs`, concurrent-mutation fixtures, and focused snapshot tests. +**Modify:** `src/verification/mod.rs` registration, report input-identity fields, and launch/open-handle adapters. + +**RED/GREEN:** Capture source, Intent, verifier, fixture, migration, manifest, inventory, lockfile, provider inputs, policy, and raw contract bytes once into a private content-addressed read-only closure. Bind immutable repository/subject/ref/workflow/run/trust, policy raw/canonical digest, contract raw/canonical digest, base repository/ref/commit/tree, protected inventory, and every captured digest. Fail rename/hardlink/mid-run swaps, mutable base replacement, path/executable replacement, pre-capture races, checkout drift, wrong repository/ref/workflow, contract retargeting, and cross-identity replay. Execute only captured bytes and prove deterministic hashes under concurrent checkout mutation. + +**Gate:** focused snapshot/race/replay tests on supported filesystems, report-schema checks, fmt/clippy, and immutable review. + +--- + +## Task 2F: Resource/profile planner and non-authoritative Intent bindings + +**Table dependencies:** 2E + +**Create:** `src/verification/planner.rs`, planner fixtures, and `tests/verification_planner_tests.rs`. +**Modify:** `src/verification/mod.rs` registration, `src/main.rs` directory input/`intent plan`/profile arguments, and IAL/agent docs. + +**RED/GREEN:** Dry planning executes no project code/provider/process/network/secret lookup and has stable ordering/hash. Reject resource/profile cycles, unknown dependencies, unsupported platform/provider, and invalid limit/containment/readiness. Compute required/advisory/excluded bindings before startup; narrower profiles cannot claim broader verification. Intent cannot choose destinations/providers/resources/executables/paths/secrets/headers/arbitrary URLs or legacy CLI/file actions; auto HTTP is app-relative only. Strict fast/full cannot weaken truth, purity, contract, or host clamps; diagnostic mode is non-verifying. Implement the resource DAG and `ntnt intent plan . --profile NAME --json` without starting resources. + +**Gate:** planner/manifest/secret tests, no-execution proof, CLI schema/docs, fmt/clippy, and immutable review. + + +--- + +## Task 2G: Runtime effect inventory and concrete verification grants + +**Table dependencies:** 2F +**Boundary:** DD-077 Design spike 0C/PR 4B may later supply static `EffectKind` metadata, but it is not runtime authority or a prerequisite. DD-078 `VerificationGrant` is concrete runtime authorization and Slice 2G independently inventories every mediated sink. + +**Create:** + +- `src/verification/runtime_authority.rs` +- `src/verification/grant.rs` +- `tests/verification_runtime_authority_tests.rs` +- a committed machine-readable inventory fixture for native/server actions and effect classes + +**Modify:** + +- `src/interpreter.rs` (`Value::NativeFunction`, `RuntimeCapability`, server-action dispatch) +- every `src/stdlib/*.rs` native registration as required by the compile-enforced metadata field +- `src/stdlib/mod.rs` +- `src/verification/mod.rs` +- `src/verification/policy.rs`, `planner.rs`, `report.rs` + +**RED:** + +1. Inventory every native/server action plus direct environment/cwd/args/filesystem/clock/random/network read and mutable `OnceLock`/`LazyLock`/registry reached during interpreter construction, module loading, or execution. Classify semantic effects; fail the inventory test when a new entry lacks classification. +2. Preserve existing behavior in Normal/Worker/Job/HotReload/UnitTest modes. +3. In Verification mode, deny every unassigned authority-bearing effect with a structured error rather than silent `Unit`. +4. Prove pure calls remain available without authority; clock/random sinks require exact case grants and record real observations, while virtual controls remain unavailable until Slice 10B. +5. Prove imports, aliases, UFCS/method bridges, prelude exposure, and user-function indirection cannot bypass the check. +6. Prove direct/transitive imports and module initializers are checked before effects; importing `std/env`, `std/fs`, `std/http`, database, job, auth, process, or secret modules does not gain authority. +7. Overlay cwd/args/environment per interpreter; prove process environment mutation and dotenv loading cannot escape the case. +8. Inventory process-global auth/job/database/HTTP/cache/time/random registries; namespace/reset them or force process isolation before the first native-case release. +9. Prove dynamic/unknown native calls fail closed in Verification mode. +10. Record requested/denied effect class and source location without leaking arguments. +11. Prove a broad effect class never grants authority. Every sink requires an opaque `{run, case, generation, resource, operation, scope, expiry, budget}` grant; database grant A cannot construct/connect to B, network resource A cannot reach another endpoint, and read authority cannot write. +12. Prove strings, maps, environment, captures, provider output, durable jobs, serialization, aliases, callbacks, or imported evidence cannot forge or widen a grant. +13. Run concurrent cases and runs against constructors, handles, global registries, and stale generations; prove no cross-resource, cross-case, or cross-run escape. +14. Install verification mode, overlays, grant table, and registry namespace before interpreter initialization or module evaluation can read `NTNT_MAX_RECURSION` or any host state. + +**GREEN:** + +1. Add compile-enforced internal semantic effect metadata to native/server actions. +2. Add supervisor-minted attenuating `VerificationGrant`/opaque handles plus per-interpreter cwd/args/environment overlay; do not authorize by `EffectKind` or mode-wide booleans. +3. Validate exact resource/operation/scope/generation/budget at the final sink shared by every invocation form and module initializer. +4. Namespace/reset process-global registries or mark their APIs unavailable until process-isolated. +5. Keep public effect-system syntax in DD-077; expose only the pinned adapter and concrete grant/reporting contract needed by DD-078. + +**Verify:** full interpreter, stdlib, typechecker, language-feature, and verification policy tests; then full nextest because every native registration is touched mechanically. + + +--- + +# Track B β€” Native ntnt verification cases + +## Task 3A: Adapt verification invocation to DD-077 PR 0A + +**Table dependencies:** DD-077 PR 0A, 2G +**Invocation owner:** Adapt to the pinned callback/invocation bridge; do not extract, recreate, or special-case another bridge. + +**Create:** `src/verification/invocation.rs` and `tests/verification_invocation_tests.rs`. +**Modify:** `src/verification/mod.rs` registration, the landed callback adapter, `src/interpreter.rs`, and `src/types.rs` only at the published integration seam. + +**RED/GREEN:** Invoke an ordinary `fn(ctx)` through the shared native callback path with nested arrays/maps/options/results, structured errors, deadline, and cancellation; reject missing functions, invalid signatures, stale/forged invocation handles, duplicate terminal results, and stringification. Keep old function-call Intent tests through a compatibility adapter over this typed invocation. No metadata scanner, verification interpreter mode, assertion API, or fixture code enters 3A. + +**Gate:** Focused callback/interpreter/type tests, full callback conformance, fmt/clippy, and immutable review. + +--- + +## Task 3B: Discover and bind verification metadata + +**Table dependencies:** 3A + +**Create:** metadata fixtures and `tests/verification_discovery_tests.rs`. +**Modify:** Slice 2A's `src/verification/discovery.rs`, parser/AST comment metadata path or annotation scanner, plus planner/report schemas. + +**RED/GREEN:** Discover `@test`, `@verifies`, `@uses`, and `@tags` without executing project code. Reject duplicate IDs, unknown obligation/resource IDs, missing functions, invalid signatures, annotations on the wrong declaration, unlinked strict cases, ambiguous obligation defaults, and nondeterministic tag/profile selection. Produce immutable typed `CaseBinding` records only; no interpreter startup or assertions enter 3B. + +**Gate:** Focused discovery/planner/schema tests, static no-execution proof, fmt/clippy, and immutable review. + +--- + +## Task 3C: Execute isolated cases under concrete grants + +**Table dependencies:** 3B + +**Create:** `src/verification/executor.rs`, `src/verification/redact.rs`, `tests/verification_case_tests.rs`, and case fixtures. +**Modify:** `src/verification/mod.rs` registration, `src/interpreter.rs`, `src/types.rs`, stdlib registration, planner/report, and typechecker. + +**RED/GREEN:** Add `ExecutionMode::Verification` and an opaque generation-bound `TestContext`; install environment/cwd/args overlays and the case's concrete grants before interpreter/module initialization. Prove a fresh interpreter/module environment, deterministic seed, bounded output/artifacts, timeout/cancellation, recursive redaction, and reset on every exit. Module globals, imports, deferred state, mutable values, registries, and contexts cannot bleed across cases/runs. Source initializers pass through the same final authority seam and fail before unassigned effects; production source and ordinary `ntnt run` cannot import `std/test`, and application imports cannot reach verification files. Every effectful stdlib sink denies unassigned network/database/secret/environment/filesystem/job/process authority with a structured failure. No assertion vocabulary or fixture DAG enters 3C. + +**Gate:** Focused interpreter/isolation/authority tests, full nextest because registration changes mechanically, fmt/clippy, and immutable review. + +--- + +## Task 3D: Typed assertions and assertion-level evidence + +**Table dependencies:** 3C + +**Create:** `src/verification/assertions.rs`, `src/stdlib/test.rs`, `tests/verification_assertion_tests.rs`, and assertion fixtures. +**Modify:** `src/verification/mod.rs` and `src/stdlib/mod.rs` registrations, executor/report, `src/intent.rs` compatibility result path, generated stdlib docs, and typechecker. + +**RED/GREEN:** Record nested typed observations without stringification; implement structural diffs, error/exit expectations, approximate numbers, order/count/unique/path/contains/regex, subcase labels, and snapshots. Multiple failed expectations accumulate while fatal runtime errors stop the case. A successful zero-assertion function yields `no-result`; multi-obligation cases require assertion-level IDs and every candidate obligation needs an evidence atom. Reject unsupported assertions, stale contexts, obvious literal vacuity, secret/tainted snapshots, and bounds violations. Ordinary/CI runs cannot update goldens. An explicit update command writes only a restrictive private candidate plus generated patch bound to source snapshot, target/prior identity/digest/mode, and proposed digest; ntnt never overwrites the committed target. Human/VCS apply and a fresh verification run are mandatory. Delete pass-on-unsupported branches from `run_function_call_test` and render only the shared ledger. + +**Gate:** `cargo test verification_assertion`, case/function compatibility tests, docs validation, full applicable nextest, fmt/clippy, and immutable review. + + +--- + +## Task 3E: Typed project fixture DAG and teardown + +**Table dependencies:** 3D + +**Create:** + +- `src/verification/fixtures.rs` +- `tests/verification_project_fixture_tests.rs` +- `tests/fixtures/verification/fixtures/*.tnt` + +**Modify:** + +- `src/verification/discovery.rs`, `planner.rs`, `executor.rs`, `report.rs` +- `src/verification/mod.rs` registration +- `src/stdlib/test.rs` +- metadata/annotation discovery from Task 3 +- generated stdlib/verification docs + +**RED:** + +1. Discover `@fixture`, `@scope`, `@teardown`, and test `@fixtures` metadata. +2. Reject duplicate IDs, unknown fixtures/resources, fixture cycles, invalid signatures, and unsupported scopes before resource startup. +3. Return nested typed values and preserve opaque/secret taint. +4. Block dependent cases on setup failure without satisfying obligations. +5. Run teardown in reverse dependency order after pass, failed expectation, runtime error, timeout, and cancellation. +6. Report teardown failure separately and fail strict mode without hiding the original case failure. +7. Default to case scope; reject shared mutable fixture parallelism without explicit reset and scheduling semantics. +8. Prove stale fixture/context values cannot cross cases, generations, or runs. + +**GREEN:** + +1. Implement case-scoped project fixtures and `fixture(ctx, id)` lookup. +2. Add fixture DAG planning alongside resource DAG planning. +3. Invoke optional teardown functions under their own bounded deadline. +4. Add suite/run scope only after reset declarations and scheduler serialization are enforced. + +**Verify:** focused fixture tests, verification planner/case tests, docs generation, fmt, clippy. + +--- + +## Task 4 / Slice 4: Table/property execution and deterministic test observations + +**Table dependencies:** 3D + +**Create:** `src/stdlib/test/generators.rs` if module organization permits, `tests/verification_property_tests.rs`, and shrinking/replay fixtures under `tests/fixtures/verification/properties/`. + +**Modify:** `src/verification/mod.rs`, `executor.rs`, `assertions.rs`, and `report.rs`; `src/stdlib/mod.rs` and `src/stdlib/test.rs` submodule registration; and `src/intent.rs` test-data/corpus expansion. + +**RED:** + +1. Preserve nested typed table values instead of converting every input to string. +2. Record stable subcase IDs and source row/data labels. +3. Run bounded generated cases with a recorded seed. +4. Prove failure shrinking has case-count, time, depth, and output ceilings. +5. Prove exact seed/case replay. +6. Prove generator PRNG state is scoped to the case and reset afterward; do not claim wall-clock virtualization in this slice. +7. Reject shrinkable property cases that request resource/network/database/browser effects; allow such data sets only as ordinary named subcases until a provider defines transactional reset semantics. + +**GREEN:** + +1. Route existing Intent `test_data` and generated corpus through typed case parameters. +2. Add deterministic generator/replay infrastructure; do not imply broad QuickCheck semantics until implemented. +3. Add seeded test-generator APIs only in verification mode. Clock APIs wait for Slice 10B's runtime observation seam. +4. Report original and minimized failures. + +**Verify:** focused tests, full Intent tests, docs generation, clippy. + + +--- + +# Track C β€” Shared actions and application lifecycle + +## Task 5A: Shared HTTP action and policy-bound transport adaptation + +**Table dependencies:** DD-077 PR 2E, 2G + +**Create:** `src/verification/actions.rs`, `src/verification/provider/mod.rs`, `src/verification/provider/http.rs`, and focused shared-transport tests. +**Modify:** `src/verification/mod.rs` registration, IAL execute/primitives/mod, Intent `WhenAction`/compatibility execution, direct `ntnt test` compatibility, and the landed `src/stdlib/http.rs`/`src/stdlib/net/policy.rs` transport seam. + +**RED/GREEN:** Define `HttpAction`, `HttpObservation`, and structured transport errors; send custom headers plus JSON/form/raw/multipart/query payloads; preserve repeated headers and binary/chunked/compressed bodies; enforce connect/request/body/redirect/total limits and cancellation; prove production HTTP, net classification, IAL compatibility, and verification consume DD-077 PRs 2C–2E's identical all-address resolution/binding, proxy, mapped/private/metadata denial, rebinding, redirect/reconnect, TLS, credential-stripping, and deadline semantics. Auto-compiled Intent is app-relative and cannot select destination/provider/resource/secret headers. Adapt legacy IAL/live Intent to this one action and remove bespoke raw-TCP HTTP only after compatibility. No cookie jar, capture store, `std/test/http`, or assertion evidence enters 5A. + +**Gate:** shared transport/policy/IAL/Intent compatibility tests, network security review, fmt/clippy, and immutable review. + +--- + +## Task 5B: Stateful verification HTTP sessions, captures, and assertions + +**Table dependencies:** 3D, 5A + +**Create:** `src/stdlib/test/http.rs`, verification session/capture stores, `tests/verification_http_tests.rs`, and HTTP app fixtures. +**Modify:** `src/stdlib/test.rs` submodule registration plus executor/assertions/redaction/report and generated stdlib docs. + +**RED/GREEN:** Maintain independent named cookie jars; preserve multiple `Set-Cookie`; capture approved header/cookie/JSON/regex/URL values; support bounded redirect opt-in; prove no cross-session leakage; recursively redact Authorization/Cookie/Set-Cookie/query/body; turn token/magic-link captures into opaque tainted values usable by later approved actions but impossible to stringify/snapshot/attach/emit; and emit typed assertion-level HTTP evidence. Reuse only 5A transport and policyβ€”no parallel client or destination logic. + +**Gate:** focused session/capture/taint/assertion tests, full Intent HTTP and Studio compatibility tests, docs, fmt/clippy, and immutable review. + + +--- + +## Task 6A: Cross-platform containment and readiness feasibility spike + +**Table dependencies:** 2E +**Artifact:** `plans/dd078-process-containment-spike.md`; no public API or production supervisor + +Adversarially prove the implementable guarantees and unsupported-platform behavior for Linux namespace/rootless-OCI+cgroup/seccomp containment, Windows Job Object/AppContainer, and an approved macOS boundary. Include descendant escape, daemonization, stable process identity, CPU/memory/PID/file/socket/disk enforcement, private scratch/HOME, read-only inputs, egress brokerage, inherited listeners, authenticated readiness, and the exact suspended/pre-owned `reserve β†’ create β†’ finalize β†’ resume/expose` process protocol. Crash the controller and durable broker at every transition and identify which OS ownership primitive closes each gap. The note records exact kernel/API/dependency choices and a platform matrix. A failed spike revises 6B's containment/cleanup classes or blocks the platform; lifecycle primitives alone never become a sandbox or strict-cleanup claim. + +**Gate:** Independent review approves the immutable spike artifact before 6B begins. + +--- + +## Task 6B: Contained process supervisor, attach mode, and cleanup + +**Table dependencies:** 3D, 5A, 6A + +**Create:** + +- `src/verification/supervisor.rs` +- `src/verification/lifecycle_broker.rs` +- `src/bin/ntnt-verification-broker.rs` (ntnt-installed/internal; never repository-selected) +- `src/verification/provider/process.rs` +- `src/stdlib/test/process.rs` +- `tests/verification_process_tests.rs` +- helper binaries/fixtures under `tests/fixtures/verification/processes/` + +**Modify:** + +- `src/main.rs` current server spawn/readiness/kill code +- `src/verification/provider/mod.rs` and `src/stdlib/test.rs` submodule registrations +- `src/verification/mod.rs`, `planner.rs`, `executor.rs`, `report.rs` +- `Cargo.toml` for a small cross-platform process-group dependency only if necessary +- `docs/verification-manifest.md` + +**RED:** + +1. Start with clean env and prove undeclared ambient values are absent. +2. Capture bounded stdout/stderr and include the tail on readiness/exit failure. +3. Support TCP, HTTP, process-alive, and provider-defined readiness under one deadline. +4. Treat early exit as failure unless expected; support expected startup rejection and exact error assertions. +5. Stop/restart and observe generation changes. +6. Kill process trees on pass, assertion failure, interpreter error, timeout, Ctrl-C, and provider failure. +8. Persist and fsync an authenticated reservation before process creation; launch suspended or into a broker-owned cgroup/Job Object, record pidfd/start/executable/token creation receipt, finalize the ledger, and resume/expose only afterward. Crash at every boundary and recover only by exact reservation/object identity. +9. Prove cleanup failure changes strict exit status but does not hide the original test failure. +10. Prove `--base-url` attach mode starts no app process and never claims ownership of the external service. +11. Pass a run-scoped child policy to managed ntnt children and prove stdlib capabilities remain enforced; record containment level and prove plain process mode never claims OS sandboxing for arbitrary executables. +12. Prove untrusted-PR profiles pass no sensitive inputs to child processes and reject non-ntnt executables unless their identity/trust or sandbox boundary is explicitly granted. +13. Prove managed verification disables implicit dotenv loading and denies project `.env`/credential files unless host policy explicitly grants a named file; an empty process environment alone is not accepted as hermeticity. +14. Enforce CPU, memory, PID/thread, file-descriptor, disk/temp, socket, process-launch, and aggregate connection limits below project code; prove exact-limit and limit-plus-one behavior. +15. Prove daemonized/`setsid` descendants cannot escape a profile that claims process-tree cleanup; otherwise block that profile. +16. Use inherited/reserved listeners or a run-nonce-bound readiness channel; prove an unrelated process cannot win a port race and fabricate readiness. +17. Linux stale-process ownership uses pidfd and/or run-owned cgroup/subreaper plus PID start time, executable identity, and run token; Windows uses kill-on-close Job Objects/process identity; macOS either proves equivalent identity or refuses stale process cleanup. +18. Prove parent/broker crash, crash-before-create, crash-after-create-before-finalize, daemonized descendant, PID/PGID reuse, partial/corrupt ledger write, writable ledger path, concurrent runs, and identity mismatch never leak a strict resource or kill an unrelated process. Platforms without a closed crash window are reported non-verifying and rejected in protected profiles. +19. Authenticate broker binary/config/state and inherited or mutually authenticated local IPC outside repository control; reject repository-selected endpoints, state roots, policy, cleanup authority, or broker identity. Protected profiles fail before startup when no durable broker class exists. + +**GREEN:** + +1. Implement the durable `reserve β†’ create β†’ finalize β†’ expose` process lifecycle state machine, exact-receipt recovery, and reverse-order teardown. +2. Move current Intent app startup into a process resource. +3. Add exact argv, working directory, env allowlist, dynamic port allocation, readiness, expected exit, restart, and logs. +4. Add attach mode. +5. Add `intent doctor` diagnostics for executable, port, provider, and containment prerequisites. +6. Persist each reservation/finalization atomically with restrictive permissions outside the repository; implement exact OS-identity/token validation and bounded TTL recovery without PID/name/prefix scans. + +**REFACTOR:** Remove null stdout/stderr spawning and fixed-port assumptions from `run_intent_check_command`. + + +--- + +# Track D β€” Providers and stateful resources + +## Task 7P: Provider protocol feasibility spike + +**Table dependencies:** 2G, 6B +**Artifact:** throwaway branch or `spikes/dd078-provider-protocol/`; no public protocol/API + +Before Slice 7A, adversarially prove inherited stdin/stdout pipe handling on Linux/macOS/Windows; four-byte big-endian pre-allocation checks; strict UTF-8 JSON/schema/unknown-field behavior; one-request correlation or explicitly bounded multiplexing; EOF/trailing bytes; cancellation and heartbeat races; stdout protocol/stderr diagnostics separation; inherited handle closure; provider crash/hang/slow-drip/oversized frames; and child/process-tree cleanup. Record exact frame limits, state machine, and platform behavior. A failed spike changes the design before public implementation; it does not silently choose another transport. + +--- + +## Task 7A: Frozen out-of-process provider protocol + +**Table dependencies:** 7P + +**Create:** + +- `src/verification/provider/protocol.rs` +- `tests/verification_provider_protocol_tests.rs` +- malformed/crash/hang provider fixtures + +**Modify:** Slice 5A's `src/verification/provider/mod.rs`, plus `policy.rs`, `planner.rs`, `supervisor.rs`, `report.rs`, `docs/verification-provider-protocol.md`, and `docs/verification-manifest.md` + +**RED:** Handshake exact protocol/provider versions and capabilities; model `reserve/create/recover/finalize/expose/cleanup` with ownership token, deterministic creation identity, exact object ID, and signed/provider-authenticated creation receipt; reject expose before finalized ledger state. Crash the broker/provider/controller at every transition and require exact-token recovery or a non-verifying cleanup class. Reject oversize, malformed, unknown-field, duplicate/late/wrong-request-ID frames; cancel/kill hangs; reject capability escalation; bind handles to run/provider/generation; recursively redact diagnostics; enforce four-byte big-endian pre-allocation checks, strict UTF-8 JSON, protocol-only stdout, bounded stderr, deadlines, cancellation, heartbeat, inherited-handle closure, and process-tree cleanup on Linux/macOS/Windows. Classify providers as sandboxed or trusted-uncontained and prove protocol validation is not syscall confinement. + +**GREEN:** Implement only the frozen framing/state machine, conformance fixture, provenance, deadlines, cancellation, heartbeat, and structured errors. No built-in service fixture lands in 7A. + +--- + +## Task 7B: Strict scripted HTTP/HTTPS and webhook fixture + +**Table dependencies:** 7A +**Create:** `src/verification/provider/http_fixture.rs`, `src/stdlib/test/http_fixture.rs`, and focused HTTP/webhook fixture tests. +**Modify:** `src/verification/provider/mod.rs` and `src/stdlib/test.rs` submodule registrations. + +**RED/GREEN:** Add finite loopback-only request scripts, exact method/path/header/body matching, response/redirect/delay/disconnect scripts, generated ephemeral HTTPS identity, webhook signature/attempt capture, consumption counts, strict unexpected/unused-traffic failures, byte/deadline caps, taint/redaction, and bounded request evidence. No SMTP or generic TCP behavior enters this PR. + + +--- + +## Task 7C: SMTP/mail capture fixture + +**Table dependencies:** 7A +**Create:** `src/verification/provider/smtp_fixture.rs`, `src/stdlib/test/mail_fixture.rs`, and focused SMTP tests. +**Modify:** `src/verification/provider/mod.rs` and `src/stdlib/test.rs` submodule registrations. + +**RED/GREEN:** Implement a finite loopback SMTP script/capture with envelope/header/body/attachment assertions, delayed/rejected/disconnected replies, message/byte/deadline limits, required-message consumption, and recursive secret redaction. No queue observation or HTTP fixture code enters this PR. + + +--- + +## Task 7D: TCP/UDP/DNS and byte-script fixture + +**Table dependencies:** 7A +**Create:** `src/verification/provider/network_fixture.rs`, `src/stdlib/test/network_fixture.rs`, and focused packet/stream tests. +**Modify:** `src/verification/provider/mod.rs` and `src/stdlib/test.rs` submodule registrations. + +**RED/GREEN:** Implement finite loopback TCP/UDP request/response scripts, strict binary caps, source identity, delay/hold/disconnect/malformed behavior, deterministic DNS answers where platform support permits, exact consumption, and request recording. Keep protocol-domain semantics in DD-047 or later typed adapters; this slice is bounded transport scripting, not a raw-network escape. + +--- + +## Task 7E: Root-confined workspace fixture + +**Table dependencies:** 7A +**Create:** `src/verification/provider/workspace_fixture.rs`, `src/stdlib/test/workspace.rs`, and focused filesystem tests. +**Modify:** `src/verification/provider/mod.rs` and `src/stdlib/test.rs` submodule registrations. + +**RED/GREEN:** Return opaque workspace handles, copy only declared bounded fixture inputs, permit operations only beneath the private root, reject traversal/symlink/hardlink/device/FIFO escape, bound files/depth/bytes, and prove teardown on every exit path. Handles cannot become arbitrary host paths. + +--- + +## Task 7F: Deterministic typed AI/payment/API stubs + +**Table dependencies:** 7A +**Create:** `src/verification/provider/api_stub.rs`, `src/stdlib/test/api_stub.rs`, and focused typed-stub tests. +**Modify:** `src/verification/provider/mod.rs` and `src/stdlib/test.rs` submodule registrations. + +**RED/GREEN:** Support only registered typed request/response schemas, deterministic finite scripts, usage/cost ceilings, exact call counts, delay/rate-limit/error/disconnect cases, taint/redaction, and unused/unexpected-call failures. Reject arbitrary command, arbitrary destination, or real-spend/public-mutation behavior. + +--- + +## Task 8 / Slice 8: PostgreSQL verification provider and migration evidence + +**Table dependencies:** DD-077 PR 1C, 7A + +**Create:** + +- `src/verification/provider/postgres.rs` +- `src/stdlib/test/postgres.rs` +- `tests/verification_postgres_tests.rs` +- PostgreSQL fixtures under `tests/fixtures/verification/postgres/` + +**Modify:** + +- `src/verification/provider/mod.rs` and `src/stdlib/test.rs` submodule registrations +- `src/verification/manifest.rs`, `planner.rs`, `supervisor.rs`, `redact.rs` +- `Cargo.toml` only for disposable-test infrastructure not already available +- `docs/verification-manifest.md`, generated stdlib docs +- pinned DD-077 migration contract docs/adapter only; this task does not own another runner + +**RED:** + +1. External server mode creates an isolated database/schema with unique run identity and committed seed visible to another connection. +2. Managed OCI mode is capability/policy-gated and labeled for cleanup; skip only when profile explicitly does not require it. +3. Apply migrations as migrator and run app/worker observations under distinct least-privilege roles. +4. Prove FORCE RLS with no tenant context and cross-tenant access denial. +5. Prove fixed `search_path`, narrow grants, and security-definer caller behavior. +6. Bound query rows/bytes/time, lock waits, and diagnostics. +7. Hold a transaction/lock as an actor and release/rollback deterministically. +8. Clean database/schema after pass, failure, timeout, cancellation, and stale-run reconciliation. +9. Preserve credentials/parameters as redacted opaque values. +10. Produce migration inventory/checksum/applied-state evidence only through the landed DD-077 interface; there is no fallback trait or alternate runner. +11. Pin external endpoint identity and generated name prefixes; prove repository-controlled URLs/names cannot make cleanup drop or mutate a pre-existing database/schema. +12. Exercise fresh install, idempotent rerun, every supported legacy ledger, legacy checksum backfill, pre-package unverifiable rows, unknown-ledger rejection before mutation, malformed/missing manifests, missing or mutated applied files, database-enforced checksum policy, and role configuration. +13. Prove per-migration transactional rollback, dirty-state recovery, concurrent migrators/advisory locks, cancellation, and retry semantics with injected failures. + +**GREEN:** + +1. Implement external PostgreSQL provider first. +2. Add database-per-run and schema-per-run; default app-backed suites to database-per-run. +3. Add role-aware bounded query/execute and held transaction actors. +4. Integrate migrations through one versioned interface. +5. Add optional managed OCI mode after the external mode is green. + + +--- + +## Task 9 / Slice 9: Redis/queue/mail/resource observations and named fixtures + +**Table dependencies:** 3E, 7B, 7C + +**Create:** + +- `src/verification/provider/redis.rs`, `src/stdlib/test/redis.rs`, and `src/verification/resource_observations.rs` +- queue observation adapters plus typed consumers of 7B webhook and 7C mail captures; do not recreate those fixtures +- `tests/verification_resource_fixture_tests.rs` + +**Modify:** `src/verification/mod.rs`, `src/verification/provider/mod.rs`, `src/stdlib/test.rs`, `src/verification/manifest.rs`, `planner.rs`, `executor.rs`, `fixtures.rs`, `supervisor.rs`, and `report.rs` for submodule registration, exact lease ownership, reset, teardown, and cleanup dispositions; extend manifest/provider docs. + +**RED:** + +1. Require a disposable per-run Redis instance for strict, hermetic, protected, and cleanup-claiming profiles. It uses the durable reservation/creation-receipt/finalization protocol; crash at every transition is recoverable by exact object/token identity, and ordinary failure/cancellation leaves zero residual keys and revokes all credentials. +2. Permit attached Redis only in an explicitly trusted non-hermetic/non-verifying profile. An operator-created random-pattern ACL user, strict command allowlist, and mandatory bounded TTL reduce risk but do not imply exact key ownership or immediate cleanup; attached evidence cannot satisfy protected obligations. +3. Observe queue depth/job state through supported ntnt job APIs rather than Redis implementation strings where possible. +4. Consume 7B/7C typed webhook/mail captures and assert headers/body/signature/attempts without owning their lifecycle implementations. +5. Return named fixture values to test contexts with scope/reset semantics. +6. Reject mutable shared fixture parallelism without an explicit reset/serialization policy. +7. Prove secret-bearing payloads and supervisor/admin Redis credentials never enter app/test code or reports; stale cleanup acts on the exact disposable-instance ledger object, never keys discovered by logical DB or prefix scans. + +**GREEN:** Implement disposable Redis lifecycle plus project-neutral queue/mail/webhook observations; validate them with generic fixture applications before any consumer adoption. Attached Redis remains visibly non-verifying unless a future enforcing broker proves exact transactional key ownership and cleanup. + + +--- + +# Track E β€” Time, eventual behavior, and races + +## Task 10A: Bounded eventual observations on real monotonic deadlines + +**Table dependencies:** DD-077 PR 0A, 3D + +**Create:** `src/stdlib/test/eventually.rs` and `tests/verification_eventually_tests.rs`. +**Modify:** `src/stdlib/test.rs` submodule registration, executor/report, and generated docs. + +**RED/GREEN:** Re-run each observation under one monotonic deadline without reusing stale values; report attempts, elapsed time, final typed observation, and terminal reason; cancel promptly; reject zero/negative/unbounded intervals. Use the landed callback bridge only. No virtual clock/random or lifecycle faults enter 10A. + +**Gate:** focused eventual/cancellation/deadline tests, fmt/clippy, and immutable review. + +--- + +## Task 10P: Runtime clock/observation feasibility and inventory spike + +**Table dependencies:** 3C +**Artifact:** `plans/dd078-runtime-observation-spike.md`; no public API or production seam + +Inventory every wall/monotonic clock, sleep, auth/job expiry, UUID/random, retry, scheduler, and runtime deadline site. Prototype one per-interpreter internal seam without changing production behavior; prove thread/process ownership, callback re-entry, and reset on success/error/cancellation. Record unsupported sites/platform behavior. A failed spike revises 10B; it never creates a provider fallback. + +**Gate:** Independent review approves the immutable artifact before 10B. + +--- + +## Task 10B: Verification clock/random controls over the proven internal seam + +**Table dependencies:** 2G, 10A, 10P + +**Create:** `src/runtime_observation.rs`, `tests/verification_clock_tests.rs`, and build-enforced inventory fixtures. +**Modify:** `src/lib.rs` registration, interpreter, and every exact time/random/expiry owner identified by 10P. + +**RED/GREEN:** Route the approved inventory through one internal seam; fail coverage when a new owned site bypasses classification. Add verification-only clock/random controls over generation-bound concrete grants; prove case/run reset, no cross-interpreter or production influence, and monotonic-deadline safety. Managed-app control is separately token-bound, loopback-only, absent in production, and cannot alter an unbound process. + +**Gate:** focused inventory/clock/random/isolation tests, applicable full nextest, fmt/clippy, and immutable review. + +--- + +## Task 10C: Expected lifecycle failure and stop/restart observations + +**Table dependencies:** 6B, 10A, 10B + +**Create:** `tests/verification_lifecycle_tests.rs`. +**Modify:** executor, supervisor, report, and generated docs. + +**RED/GREEN:** Verify expected process/provider/startup failures without converting unexpected failures into data; stop/restart exact owned dependencies and prove generation, readiness loss/recovery, cancellation, cleanup, and fault disposition. + +**Gate:** focused lifecycle/crash/cleanup tests, full supervisor tests, fmt/clippy, and immutable review. + +--- + +## Task 11 / Slice 11A: Actors, barriers, and deterministic coordination + +**Table dependencies:** 6B, 8, 10A, 10B + +**Create:** + +- `src/verification/coordination.rs` +- `src/stdlib/test/concurrency.rs` +- `tests/verification_coordination_tests.rs` +- deadlock/race fixtures + +**Modify:** + +- `src/verification/mod.rs`, `executor.rs`, `report.rs` +- `src/stdlib/test.rs` submodule registration +- interpreter callback/suspension integration only through existing general mechanisms +- generated docs + +**RED:** + +1. Start named actors, wait at barriers, release in a recorded order, and join under deadlines. +2. Reject duplicate actor/barrier names, wrong participant counts, cross-case handles, and release after expiry. +3. Diagnose actor stacks/last steps on deadlock without leaking values. +4. Cancel remaining actors after one fatal failure. +5. Coordinate held PostgreSQL locks and held mock responses. +6. Reproduce duplicate scheduling, claim/revoke linearization, terminal-write fencing, projection serialization, enqueue failure/reconciliation, and alert/outbox idempotency patterns. +7. Prove the report describes controlled seams and does not claim deterministic kernel/database scheduling. + +**GREEN:** Implement bounded actor groups/barriers and provider hold/release integration. + + +--- + +# Track F β€” Browser and project evidence + +## Task 12P: Chromium/CDP feasibility spike + +**Table dependencies:** 5A, 6A, 7P +**Artifact:** throwaway branch or `spikes/dd078-browser-provider/`; no public API + +**Questions to prove:** + +1. Launch a policy-pinned Chromium with isolated profile and connect over CDP. +2. Navigate, query DOM, click/fill, inspect focus/history, disable JavaScript, intercept/hold/abort requests, capture console/network failures, screenshot, and clean process/profile. +3. Run on hosted Linux and determine macOS/Windows executable/job-object differences. +4. Bound CDP messages, artifacts, page count, time, and script evaluation output. +5. Decide core module versus maintained external provider using dependency size, release coupling, and sandbox boundaries. +6. Prove an enforcement point beneath CDP: isolated network namespace/container or mandatory brokered proxy covers DNS, redirects, subresources, WebSockets, WebRTC, service workers, loopback/private/metadata destinations, and downloads. If unavailable, untrusted-PR browser planning blocks. + +**Gate:** Do not start Slice 12A until the spike records exact dependency/API choice and cleanup/security review. A failed spike may choose a maintained external provider; it does not permit project-owned Playwright scripts as the final model. + +--- + +## Task 12A: Frozen browser provider contract and containment + +**Table dependencies:** 6B, 7A, 12P + +**Create:** + +- `src/verification/provider/browser.rs` or a separate pinned provider crate/repository +- `tests/verification_browser_provider_tests.rs` +- browser sandbox/network fixtures + +**Modify:** `src/verification/provider/mod.rs` registration when 12P selects the in-tree provider; an external provider instead records its pinned crate/repository registration in this slice. + +**RED:** + +1. Launch only policy-pinned Chromium/provider identities with isolated profiles, bounded CDP messages/pages/time/output, and explicit containment class. +2. Enforce navigation, DNS, redirects, subresources, WebSockets/WebRTC, service workers, downloads, loopback/private/metadata access, and reconnect below CDP through the approved broker/namespace. +3. Reject `file:` URLs, reused profiles, extensions, arbitrary remote-debug targets, undeclared services, unapproved downloads, missing/unsupported containment, and mutable executable identity. +4. Prove browser/provider crash, hang, cancellation, daemon descendants, and stale cleanup remove only exact owned processes/profiles/artifacts. +5. Record executable/version/digest, provider identity, sandbox/egress guarantees, sensitive-artifact disposition, and cleanup. `trusted-uncontained` is non-hermetic and cannot satisfy protected CI or receive protected secrets. + +**GREEN:** Land the supervised provider and security/provenance evidence only; no project-facing DOM API in this slice. + +--- + +## Task 12B: `std/test/browser` sessions and assertions + +**Table dependencies:** 3D, 12A + +**Create:** + +- `src/stdlib/test/browser.rs` +- `tests/verification_browser_tests.rs` +- fixture web app/pages +- `docs/verification-browser.md` + +**Modify:** `src/stdlib/test.rs` submodule registration and generated stdlib docs. + +**RED:** + +1. Context isolation for two users; cookie/storage cleanup. +2. JavaScript and no-JavaScript modes. +3. Locator text/HTML/attribute/count/visibility/focus/accessibility assertions. +4. Click/fill/select/submit/keyboard/history behavior. +5. Request interception, delay, abort, offline, replacement, and navigation races. +6. Console errors/failed requests as configurable failures. +7. Bounded screenshot/trace artifacts, sensitive-artifact policy, selector masking, restrictive permissions, and an explicit test proving arbitrary pixels are never described as generically redacted. +8. Browser crash/hang/cancel cleanup. +9. Executable/version/digest provenance and policy rejection. +10. Explicit script evaluation bounds and disabled-by-policy mode. +11. Apply network policy to navigation and every subresource; deny `file:` URLs, reused profiles, extensions, arbitrary remote-debug targets, undeclared loopback services, and downloads outside the artifact directory. +12. Prove CDP interception is treated as evidence, not containment; trusted-uncontained browser mode is non-hermetic and cannot receive protected secrets or satisfy protected CI. + +**GREEN:** Expose the typed API and evidence; keep provider internals unavailable to project code. + + +--- + +## Task 13A: Canonical root-confined project inspection + +**Table dependencies:** 2A + +**Create:** `src/project_inspection.rs`, canonical inspection tests, and tracked-file fixtures. +**Modify:** `src/lib.rs` registration plus current `src/main.rs`, Studio, and interpreter scanner consumers. + +**RED/GREEN:** Extract one reusable inspection library; enumerate tracked paths/blob hashes under the canonical root; exclude protected private classes by default; reject symlink/hardlink escape; and return stable bounded facts without executing project code. No AST constraint, data parser, OCI client, or new Intent syntax enters 13A. + +**Gate:** focused scanner parity/root-escape tests, existing inspector/Studio tests, fmt/clippy, and immutable review. + +--- + +## Task 13B: Structural ntnt facts and declarative constraint engine + +**Table dependencies:** 2G, 3D, 13A + +**Create:** `src/stdlib/test/project.rs`, `src/verification/constraints.rs`, structural fact/constraint tests, and AST/import/route fixtures. +**Modify:** `src/verification/mod.rs` and `src/stdlib/test.rs` submodule registrations, generated stdlib docs, and AST/inspect APIs to expose stable import/function/route/annotation/effect/ownership facts. + +**RED/GREEN:** Detect forbidden dependencies and architecture invariants structurally without implementation-string matching. Facts remain typed/bounded and consume concrete project-read grants. No Git/data/OCI provider or first-class Intent syntax enters 13B. + +**Gate:** focused structural-fact/constraint tests, AST/parser regressions, fmt/clippy, and immutable review. + +--- + +## Task 13C: Bounded Git and structured-data facts + +**Table dependencies:** 2G, 13A + +**Create:** `src/project_data.rs`, focused Git/data reader tests, and adversarial JSON/TOML/YAML/XML/text fixtures. +**Modify:** `src/lib.rs` registration, shared project-inspection facts, and docs. + +**RED/GREEN:** Read local tracked/blob/ref/dirty facts without network; parse bounded data with parser/version provenance; mark textual evidence; enforce root/depth/count/byte limits; reject traversal, entities/includes, aliases/expansion, and secret-class reads. No OCI daemon access or syntax changes enter 13C. + +**Gate:** focused parser/Git/root/bounds tests, dependency review, fmt/clippy, and immutable review. + +--- + +## Task 13D: Read-only OCI, migration, generated-doc, and runtime provenance facts + +**Table dependencies:** DD-077 PR 1C, 7A, 8, 13A + +**Create:** `src/oci_inspection.rs`, focused read-only OCI client tests, and provenance/migration fixtures. +**Modify:** `src/lib.rs` registration, shared project-inspection facts, provider policy, report, and docs. + +**RED/GREEN:** Inspect config/labels/platform/content digest through exact grants; integrate DD-077 migration inventory/checksums, generated-doc facts, and runtime/image provenance; reject mutation, untrusted daemon/network access, raw effective config, mutable identity, and secret output. No project environment lifecycle or first-class constraint syntax enters 13D. + +**Gate:** fake/adversarial OCI tests, migration/provenance parity, security review, fmt/clippy, and immutable review. + +--- + +## Task 13E: First-class Intent constraint syntax + +**Table dependencies:** 13B + +**Create:** failing parser/binding/diagnostic fixtures for a separately approved `Constraint` syntax. +**Modify:** parser/AST/Intent/Studio docs only after the syntax decision. + +**RED/GREEN:** Add the smallest declarative binding layer over 13B facts; no provider/fact implementation enters this PR. Generic `.tnt` project tests remain available where new syntax is unjustified. + +**Gate:** syntax decision, parser/binder diagnostics, docs, fmt/clippy, and immutable review. + + +--- + +## Task 14A: Bounded provenance-checked evidence import + +**Table dependencies:** 1B, 7A + +**Create:** `src/verification/import.rs`, `tests/verification_import_tests.rs`, and committed evidence-envelope/key-policy/JUnit/TAP/JSON adversarial fixtures. +**Modify:** `src/verification/mod.rs` registration, report schema, and evidence docs. + +**RED/GREEN:** Reject imported pass claims with missing/unknown schema, provider identity, obligation/assertion IDs, hashes, invocation provenance, or signatures; mark current-input mismatch stale. Preserve bounded/redacted failure diagnostics and reject XXE/DTD/XInclude/external resolution, oversized/deep input, traversal artifacts, duplicate claims, and archive expansion. Require either a current authenticated-supervisor record or exact closed `EvidenceEnvelopeV1` signed as `ntnt-evidence-v1\0 || JCS(envelope_without_signature)`; both carry repository/commit/ref/workflow/run/attempt/trust, contract raw/canonical/base/inventory, operation/profile/plan/policy, complete inputs/runtime/providers/environment, assertion results, artifacts/cleanup, timestamps/expiry/nonce. Reject unknown/missing/duplicate fields, tamper, artifact swaps, replay/skew, downgrade, revoked keys, mutable-environment mismatch, and every cross-repository/ref/workflow/contract/base/profile/plan/policy/environment/provider substitution. + +**Gate:** focused import/parser/signature/replay tests, committed schema interoperability, security review, fmt/clippy, and immutable review. + +--- + +## Task 14B: Deterministic JUnit, replay, and Studio ledger adapters + +**Table dependencies:** 14A + +**Create:** `src/verification/junit.rs`, `src/verification/replay.rs`, `tests/verification_replay_tests.rs`, and committed JUnit/report examples. +**Modify:** `src/verification/mod.rs` registrations, CLI replay/output arguments, and Studio server/UI. + +**RED/GREEN:** Generate deterministic JUnit from the ledger; replay one selected case by rebuilding current hashes, snapshot, grants, and authority rather than trusting prior pass; show implementation/executable/verified separately; never convert warning/pending/skip to pass. + +**Gate:** focused JUnit/replay/Studio schema tests, full report tests, fmt/clippy, and immutable review. + + +--- + +## Task 14C: Typed project-state, lock/lease, and allocation substrate + +**Table dependencies:** 2G, 6B + +**Create:** + +- `src/project_state.rs` +- `src/stdlib/project_environment.rs` +- `tests/project_state_tests.rs` +- committed state-schema and corruption fixtures + +**Modify:** `src/lib.rs` and `src/stdlib/mod.rs` registrations, shared canonical project loader, runtime authority/grants, and generated stdlib docs + +**RED:** + +1. Key state outside the checkout by canonical root digest plus environment; reject ambient root/project override, foreign-root state, stale generation, and identity collisions. +2. Require restrictive state/runtime directories, exclusive cross-process locks, atomic temporary write plus file/directory fsync and replace, schema validation, compare-and-swap transitions, and idempotent recovery. +3. Reject symlink/hardlink/non-regular/writable-parent paths, partial/corrupt files, unknown fields/schema, unsafe legacy upgrade, and concurrent lost updates. +4. Model exact `uninitialized β†’ reserved β†’ creating β†’ finalized β†’ starting β†’ ready|degraded β†’ stopping β†’ stopped|cleanup-failed` transitions with cancellation/crash dispositions. +5. Never probe-and-release managed-process ports: retain inherited listeners through binding. Expose provider-neutral global allocator locks, leases, compare-and-swap transitions, and opaque ownership records, but do not inspect or mutate OCI here. +6. Validate host-clamped port/subnet pool schemas, lock ordering, lease expiry, bounded retry state, overlap/exhaustion/IPv4/IPv6 rules, and concurrent-worktree serialization. A candidate lease is not reported as an external object until the provider's exact creation receipt is durably finalized; 14C itself never claims filesystem/provider atomicity. +7. Keep generated credentials/secret outputs opaque and restrictive; reports/status expose only safe names, allocation IDs, endpoints approved as non-secret, and dispositions. +8. Prove bounded stale-state reconciliation acts on exact ownership/object records, never root-derived names or prefixes. + +**GREEN:** Implement the versioned state service and opaque typed `std/project/environment` handle used by native project-environment commands; do not expose generic key/value storage, arbitrary paths, process execution, or OCI commands. + + +--- + +## Task 14D: Typed development/staging OCI environment lifecycle + +**Table dependencies:** DD-077 PR 1C, 7A, 13D, 14C + +**Create:** + +- `src/project_env/mod.rs` +- `src/project_env/manifest.rs` +- `src/project_env/oci.rs` +- `src/project_env/oci_allocation.rs` +- `src/project_env/report.rs` +- `tests/project_environment_tests.rs` +- fake/adversarial OCI provider fixtures +- `docs/project-environments.md` + +**Modify:** `src/lib.rs` registration, `src/main.rs`, `src/config.rs`/shared manifest model, provider policy, and generated CLI docs + +**RED:** + +1. Parse strict `[project.environments.NAME]` declarations for pinned provider, Compose/OCI files, profiles, allowed services, build/create/up order, migration action, readiness, non-secret outputs, allocation pools, and cleanup policy; reject generic argv/shell hooks. +2. Implement `ntnt project env init|up|down|status NAME`; JSON status is schema-versioned and contains no secret values. Effective rendered configuration is parsed in memory, recursively redacted/tainted, bounded, and never emitted raw. +3. Render effective Compose/OCI configuration through the pinned provider and reject undeclared files/services, privileged/host modes, arbitrary mounts/devices/socket forwarding, mutable images where policy requires digests, ambient environment overrides, shell interpreters/operators, and project-owned shell/Python entrypoints or lifecycle hooks. +4. Execute dev/staging lifecycle as typed actions. A durable broker binds and retains each host TCP listener for the environment lifetime and proxies it to an unpublished final container port; Compose never rebinds that host port. Before exposure finalize `{listener ID, container object ID, network endpoint ID, generation, target port, ownership token}`. Every accept/reconnect re-inspects that exact target or uses an authenticated daemon event stream that invalidates fail-closed; service names, aliases, and cached IPs never authorize routing. Before forwarding application/readiness bytes, require a broker-controlled generation-bound target handshake using an opaque sidecar nonce or ephemeral mTLS identity unavailable to peers. Recreation/restart, event loss, or failed target authentication requires a new finalized generation and wrong/stale targets receive zero application bytes. UDP/non-proxy backends must use daemon allocation on the final service object with exact pre-exposure receipt/recovery or be rejected. Under the allocator transaction, create the exact external network, persist/finalize daemon object IDs, ownership token, and receipts, then let Compose consume that network. Continue with validate, build, final service create, start dependencies, landed DD-077 migration, app/workers, authenticated readiness through the broker, and state commit. +5. Use `reserve β†’ create β†’ finalize β†’ expose` for network, service, and listener/proxy objects. On failure/cancellation/crash, retain truthful partial state and recover/clean only exact reserved identities, provider object IDs, and ownership tokens. `down` revalidates root, manifest, provider, generation, receipt, and object identity; names/labels/prefixes cannot nominate deletion. Unsupported crash windows are non-verifying and rejected in protected profiles. +6. Test concurrent worktrees, cross-user/shared-daemon runs, a non-cooperating daemon client, listener/network collisions, container recreation, bridge-IP reuse, alias collision/attachment, stale broker routes, stolen/stale target nonce and mTLS identity rejection, daemon restart, wrong-target zero-application-byte proof, crash before create/after create/before finalization/before exposure, repeated up/down, partial starts, migration failure/rollback, provider drift, occupied allocations, subnet overlap/exhaustion/IPv4/IPv6 mismatch, readiness spoof, stale state, and reboot recovery. The user-state lock is not treated as a daemon-wide mutex; OS binding and daemon object creation are authoritative. +7. Host policy separately grants OCI socket/build/network authority; untrusted PR execution without it is blocked before provider startup. + +**GREEN:** Implement one typed OCI/Compose lifecycle provider, durable ingress broker, exact creation receipts/recovery, and the CLI. Dev/staging behavior is data in the project manifest; no placeholder-socket handoff, shell-wrapper provider, or arbitrary command escape exists. + + +--- + +# Reference-adoption plans + +Application migrations do not participate in the DD-078 core DAG, release sequence, or definition of done. The first consumer profileβ€”including Larrimon Waves A–E, production-migration compatibility, deletion authority, immutable inventory, and future pressure casesβ€”is maintained separately in [`dd-078-larrimon-adoption.md`](dd-078-larrimon-adoption.md). Other projects define equivalent adoption plans without changing ntnt runtime slices. + +--- + +# Track G β€” Extended generalized verification capabilities + +These are acceptance applications for the runtime, not reasons to add product-specific primitives. + +## Task 18P: Streaming and event-source feasibility spike + +**Table dependencies:** 7A, 7D +**Artifact:** `plans/dd078-streaming-event-source-spike.md`; no public provider API + +Prove bounded cross-platform client/server fixtures for NETCONF framing, HTTP/2/gRPC streaming, TLS syslog/event sources, reconnect ordering, half-close/cancellation, flow-control, backpressure, slow-drip, certificate rotation, and byte/message/retention ceilings. Record library choices, containment/egress class, immutable endpoint identity, and unsupported-platform behavior. A failed spike revises 18A rather than exposing raw sockets or generic commands. + +## Task 18A: Typed streaming/event-source fixture providers + +**Table dependencies:** 7A, 18P + +Land separate typed NETCONF, gNMI/HTTP2-stream, and TLS syslog/event-source adapters over the provider protocol. Each contract has finite scripts, explicit auth/identity, deadlines, flow-control/backpressure, deterministic failure injection, bounded evidence, and cleanup. It grants no arbitrary network destination or raw protocol escape. + +## Task 18B: Monitoring protocol and inventory acceptance profiles + +**Table dependencies:** 13A, 18A, DD-047 Slice 1C, DD-047 PR 2 + +Add pure `.tnt` verification for: + +- SNMP GET/WALK strict BER, correlation, timeout, packet/result/byte bounds, opaque communities, counter wrap/reset/rate normalization, private/live gates; +- MIB compiler/catalog/profile/inventory expected-hash and rollback behavior; +- device recognition confidence/tie handling; +- finite inventory plans and normalized snapshots; +- NETCONF plus gRPC/HTTP2 gNMI and syslog/event-source auth, ordering, malformed input, reconnect, streaming subscription flow-control/backpressure, and bounded retention; +- gated real-device smoke with host policy and opaque secrets. + +## Task 19A: KMS/secret-service and encrypted completion-spool fixtures + +**Table dependencies:** 7A, 7E, 10C, 14C + +Define typed, finite KMS/secret-service fixtures with opaque handles, key version/rotation/revocation, deny/outage/timeout behavior, nonce/AAD/envelope vectors, purpose/run/node binding, and proof app/agent code never receives KEK authority. Add an encrypted completion-spool fixture whose exact files/claims/idempotency records live in a root-confined workspace, survive supervised restart/failover, and expose bounded replay evidence without secret material. + +## Task 19B: Bounded load/backpressure provider + +**Table dependencies:** 6B, 7A, 10B, 11A + +Define a contained provider with typed workload plans, fixed target handles, deterministic seeds, arrival/concurrency/byte/request ceilings, priority classes, cancellation, load-shed/fault controls, and bounded percentile/queue evidence. It cannot choose arbitrary destinations, execute project commands, or claim hermetic timing. Add exact-limit and limit-plus-one, overload ordering, backpressure, cleanup, and report-redaction tests. + +## Task 19C: Multi-agent, AI, alerting, and retention acceptance profiles + +**Table dependencies:** 7F, 9, 19A, 19B + +Add pure `.tnt` verification for: + +- signup/invite/Turnstile, independent identity/IP/purpose rate limits, verified-email membership creation, and transactional side-effect rollback; +- unified IPv4/IPv6 egress policy, metadata denial, DNS rebinding, per-hop redirect/reconnect validation, credential stripping, and private-node scope; +- AES-GCM nonce/AAD/envelope/rewrap vectors, write-only/expiry/purpose/run/node binding, KMS denial, and proof agents never receive KEK/KMS authority; +- multiple supervised application/agent protocol fixture processes, enrollment/signing/nonce/replay/rotation/revocation, wrong-node/cross-tenant denial, and encrypted completion-spool failover replay preserving run/claim/idempotency identity; these fixtures do not execute production tools; +- deterministic 7F AI responses with schema/citation/no-tool/token/plan assertions; +- 9/7B/7C email/webhook retries, signatures, deduplication, and ambiguous outcomes; +- clock-driven partition/retention/legal-hold cases and 19B bounded load/backpressure priorities. + +Production agent/tool execution, typed effect transcripts, and tool-using cases are not owned by 19C and are excluded from this release sequence. They remain blocked until DD-065 has a real design artifact, exact owner/contract, implementation merge identities, and a later plan truth-sync adds that dependency. + +## Task 20P: Backup/restore and multi-node topology/fault feasibility spike + +**Table dependencies:** 14D, 19A, 19B +**Artifact:** `plans/dd078-ha-recovery-provider-spike.md`; no public provider API + +Prove provider ownership/containment for disposable multi-node topologies, independent failure-domain representation, network partitions, clock/certificate/DNS/queue/KMS faults, fenced promotion, backup/PITR artifacts, and crash-safe teardown. Establish immutable environment/artifact identity, no production-target default, supported platform/OCI boundaries, measurable RPO/RTO semantics, and a non-hermetic report class. A failed spike blocks 20A/20B. + +## Task 20A: Backup/PITR/restore provider and recovery evidence + +**Table dependencies:** 7A, 20P + +Implement typed backup, restore, point-in-time target, integrity validation, and rollback actions against disposable resources only. Bind source database/image/runtime, backup object digest, encryption/KMS identity, target time, restored schema/data checks, cleanup, and measured recovery to one immutable evidence record. Reject arbitrary paths/buckets/credentials and unsupported recovery claims. + +## Task 20B: Multi-node topology, fencing, partition, and outage provider + +**Table dependencies:** 7A, 14D, 20P + +Implement an exact-owned disposable topology DAG with independent failure-domain labels, one-writer fencing, tenant home-region/data-residency assertions, network/queue/KMS/DNS/certificate/clock fault handles, encrypted completion-spool recovery, and bounded game-day timelines. Cleanup acts only on immutable provider object IDs; protected profiles block unless containment and topology claims are demonstrable. + +## Task 20C: Upgrade, restore, HA, and on-prem acceptance profiles + +**Table dependencies:** 7F, 19A, 20A, 20B + +Use explicit non-hermetic provider-backed profiles for: + +- old-to-new migration matrices, expand/migrate/contract compatibility, and rollback constraints across app/worker/agent versions; +- OCI/runtime/source provenance and signed artifacts; +- backup/PITR restore evidence; +- independent-failure-domain topology, fenced one-writer promotion, tenant home-region/data-residency, canonical queue/KMS outage behavior, and encrypted completion-spool recovery; +- overload ordering that preserves heartbeat/completion/reducer/alert work before probes and sheds discovery/AI first; +- measurable clock-skew, DNS, certificate, KMS, queue-loss, and partition recovery; +- private-network/device smoke under customer-controlled policy; +- customer-managed/BYO KMS and 7F private-AI matrices proving no hosted credential or private-evidence fallback; +- measured SLO/RPO/RTO/game-day evidence. + +Reports bind exact runtime/provider/environment/artifact identities and label these profiles non-hermetic. + +--- + +## Per-PR validation template + +Use the smallest focused commands first, then the full applicable gate. Exact test filters will evolve with modules. + +```bash +cargo fmt --check +cargo test +cargo test --test +cargo clippy --all-targets -- -D warnings +ntnt docs --validate +``` + +Before each ntnt runtime PR is considered ready: + +```bash +env -u NTNT_TYPE_MODE \ + -u NTNT_NETMON_ENABLE \ + -u NTNT_NET_ALLOW_PRIVATE \ + CARGO_TARGET_DIR=target \ + RUST_MIN_STACK=8388608 \ + cargo nextest run + +CARGO_TARGET_DIR=target RUST_MIN_STACK=8388608 cargo test --doc +``` + +If `cargo nextest` is unavailable, record that fact and run the complete `cargo test --all-targets` fallback. Never report a synthetic pass. + +Security-sensitive provider/process/network/browser PRs additionally require: + +- Linux hosted CI; +- macOS and Windows hosted CI where the capability claims support them; +- exact immutable diff review; +- secret canary scan of stdout, stderr, JSON, JUnit, textual artifacts, screenshots metadata, and failure messages, plus sensitive-artifact handling review for binary/browser artifacts; +- cancellation/timeout/cleanup test evidence; +- dependency/provenance review for new crates or provider binaries. + +--- + +## Release sequencing + +Do not put this portfolio into a patch release. Recommended feature sequence: + +| Candidate feature boundary | Minimum content | +|---|---| +| v0.6.0 foundation | Landed DD-077 PR 0A plus DD-078 Slices 1A–1B, 2A–2G, 3A–3E: truthful ledger/renderers, canonical project/policy/contract/purity/snapshot/planner, concrete runtime grants, bridge adaptation, metadata, isolated cases, assertions, and fixtures | +| next feature release | Landed DD-077 Design spike 0B and PRs 2C–2E plus DD-078 Slice 4, 5A–5B, 6A–6B: seeded data, shared production/verification HTTP policy, sessions, containment spike, and process supervisor/attach mode | +| following feature release | Landed DD-077 PRs 1B–1C plus DD-078 Slices 7P, 7A–7F, 8–9, 10P, 10A–10C, and 11A: provider protocol/fixtures, PostgreSQL/Redis/migration evidence, eventual/clock/lifecycle, and coordination | +| browser/project feature release | Slices 12P, 12A–12B, 13A–13E, and 14A–14B after their spikes and security review | +| project-environment feature release | Slices 14C–14D after process/provider foundations and DD-077 migration runner | +| future monitoring/reliability releases | Slices 18P, 18A–18B, then 19A–19C, then 20P, 20A–20C; 18B also waits for pinned landed DD-047 Slice 1C/PR 2 identities, and every public provider waits for its feasibility spike and exact dependency closure | + +Consumer adoption plans may begin their own evidence-backed migrations after each pinned release. Their deletion schedules and pure-project claims do not gate this core release sequence. + +--- + +## Definition of done + +DD-078 is implemented when: + +1. one evidence ledger truthfully represents every obligation and execution result; +2. project-wide static plan and strict execution are stable public CLI contracts bound to one immutable input snapshot; +3. protected CI enforces an operator-owned obligation/profile/evidence contract and pure-authoring disposition rather than trusting repository scope; +4. native `.tnt` verification covers typed unit, HTTP, database, process, fixture, eventual, concurrency, browser, and project-policy cases; +5. capabilities are externally granted, root-confined, bounded, redacted, and cleaned up through authenticated host-ledger ownership; +6. external providers are versioned, pinned, explicitly sandboxed or trusted-uncontained, and fail closed; protected PR lanes admit only allowed containment classes; +7. project-neutral fixture applications exercise every public mechanism without importing consumer code, names, data models, or policies; +8. the generalized adoption protocol binds an arbitrary immutable fixture repository, exact-once inventory, protected contract, and execution snapshot to one canonical identity; +9. old/new parity plus deliberate mutation/fault witnesses produce machine-readable deletion-eligibility evidence without automatically deleting consumer files; +10. fast, full, live-network, and environment-backed profiles state their evidence, claim level, containment, and hermeticity honestly; +11. full ntnt regression, docs, hosted-platform, and independent security/architecture reviews pass against immutable commits; +12. at least two project-neutral adoption fixtures with different identities and inventories complete the protocol without changing ntnt runtime APIs. Consumer-specific adoption completion remains outside DD-078. diff --git a/plans/dd-078-larrimon-adoption.md b/plans/dd-078-larrimon-adoption.md new file mode 100644 index 00000000..209fdacc --- /dev/null +++ b/plans/dd-078-larrimon-adoption.md @@ -0,0 +1,203 @@ +# DD-078 Larrimon Reference-Adoption Plan + +> **Status:** Consumer migration plan. This file does not participate in the DD-078 core dependency DAG, release sequence, or definition of done. + +**Consumer repository:** [`larimonious/larrimon`](https://github.com/larimonious/larrimon) + +**Immutable audit baseline:** commit `ceadfd992d1435ac27afb054968ff5569d697ce1`, recorded in [`dd-078-larrimon-baseline.md`](dd-078-larrimon-baseline.md) + +**Runtime architecture:** [`../design-docs/dd-078-intent-verification-runtime.md`](../design-docs/dd-078-intent-verification-runtime.md) + +**Core implementation plan:** [`dd-078-intent-verification-implementation.md`](dd-078-intent-verification-implementation.md) + +## 1. Boundary + +Larrimon is the first demanding consumer of DD-078's generalized verification runtime. It supplies application-specific inventories, invariant families, migration waves, deletion authority, and pressure cases. It does not define ntnt public APIs, schemas, keywords, defaults, fixture semantics, policies, privileged modes, or core release boundaries. + +This plan may begin only from pinned, reviewed ntnt commits. Larrimon migration PRs must not patch ntnt runtime behavior. Missing generalized capability returns to a separately reviewed ntnt slice; it is never implemented as project-owned shell, Python, or compensating JavaScript. + +Completion of this plan proves one reference adoption. Failure or delay here does not make the project-neutral DD-078 runtime incomplete, and completion here does not by itself prove the runtime generally correct. + +## 2. Adoption protocol + +Every deletion requires a checked-in old-to-new invariant ledger containing: + +1. old file and exact line/range; +2. stable invariant ID; +3. replacement obligation and case IDs; +4. environment and resources; +5. expected positive result; +6. deliberate violation, mutation, or fault witness; +7. retained versioned evidence digest; +8. exact candidate repository commit and canonical inventory digest. + +Deletion additionally requires: + +- old and new checks on the same clean immutable revision whenever technically runnable; +- a reviewer-approved alternative witness for every non-dual-runnable invariant; +- equivalent or stronger negative, race, cleanup, security, timing-boundary, and failure-injection coverage; +- no claim derived from annotation count, declaration count, filename count, or user-authored pass data; +- protected contract, execution snapshot, baseline inventory, and evidence bound to the same identity; +- narrowly scoped migration PRs that delete only the proven replacement slice. + +## 3. Core-capability consumption gates + +These are Larrimon gates against landed DD-078 capabilities. They are not core ntnt release gates. + +| Core owner | Larrimon consumer gate | +|---|---| +| 1A–1B | Run current Intent files through the static ledger and record declared, documentation-only, linked, unbound, executable, and verified obligations. Delete nothing. | +| 2A–2G | Add a non-executing draft `[verification]` section on a separate Larrimon branch and prove complete resource/test planning without startup. Merge only after the consuming runtime commit is pinned. | +| 3A–3C | No consumer execution until the authority floor is landed and externally granted. | +| 3D | Convert representative reducer, validation, probe-shape, and application-service files to discovered `.tnt` cases. After all 18 current direct `ntnt run` cases have same-revision parity, remove their manual print/pass conventions and the 18-run loop from `tests/intent.sh`. | +| 3E | Replace repeated scalar seed/setup builders in pure `.tnt` cases. Resource-backed database/auth fixtures wait for PostgreSQL and application-fixture owners. | +| 4 | Move validation matrices and reducer golden streams into typed data fixtures without growing hand-written assertion helpers. | +| 5A–5B | Migrate public health, headers, origin/HTMX, form fallback, auth request/consume, cookie, role, and multiple-identity cases. Keep server lifecycle in the old harness until process resources land. | +| 6A–6B | Move server/config/startup-failure and authenticated HTTP suites to manifest-managed application resources. Remove equivalent process, port, wait, and curl helpers only after parity. | +| 7B | Replace redirect/resend HTTP mocks and webhook receiver programs after mutation parity. | +| 7C | Replace the project-owned SMTP capture program after magic-link and alert-delivery mutation parity. | +| 8 | Migrate schema, migration, checksum, RLS, security-definer, immutability, tenant-isolation, rollback, and role cases. Application/schema SQL test files may be deleted after same-revision positive, negative, race, cleanup, and mutation parity; production migration programs remain until adoption Slice 16M. | +| 9 | Migrate magic-link email, queue wakeup/reconciliation, alert delivery, and resource-cleanup cases. | +| 10A–10C | Replace sleeps and poll loops for queued/running/terminal runs, readiness, session revocation, alert delivery, and scheduler recovery. | +| 11A | Port every background/FIFO/parallel race case. No sleep-based race is deleted until the replacement deterministically forces the intended interleaving. | +| 12A–12B | Rewrite reconciliation and staging browser smoke in `.tnt`; cover desktop/mobile, HTMX/full-page, no-JavaScript, focus, URL, abort/replacement, mutation ambiguity, and authentication. Remove project test `.js`/`.mjs` only after parity. | +| 13A–13D | Port architecture, CI policy, assets, runtime/image provenance, and Compose/project assertions. Dual-run migration-checksum facts but retain the migration-checksum program until Slice 16M. | +| 14A–14B | CI uploads one versioned JSON report and optional JUnit; no shell post-processing infers coverage or status. | +| 14C | Port every state/transition invariant and mutation from `scripts/staging-state.py` and `tests/staging_state_cases.py`; preserve worktree identity, legacy-state upgrade, restrictive permissions, and foreign-state rejection. Deletion also waits for 14D environment parity. | +| 14D | Replace `scripts/dev-up.sh`, `dev-down.sh`, `staging-up.sh`, and `staging-down.sh` only after same-revision positive, negative, partial-failure, cleanup, and mutation parity. `staging-smoke.sh` remains until its HTTP/browser evidence also migrates. | + +## 4. Wave A β€” Intent truth and native cases + +**Depends on landed ntnt owners:** 1A–1B, 2A–2G, 3A–3E, 4 + +1. Add stable scenario/outcome IDs and missing behavioral scenarios to all seven audited `.intent` files. +2. Add or convert `.tnt` cases under the project verification tree. +3. Add pinned profiles to `ntnt.toml`. +4. Run old and new tiers together temporarily. +5. Add the under-covered wrong-tenant session, readiness dependency failure, internal dispatch denial, request-path no-probe, persistence rollback, concurrent projection serialization, enqueue-failure reconciliation, and audit-immutability contracts. +6. Remove manual assertion/pass wrappers only after invariant-level parity. + +**Wave gate:** Every audited obligation is verified or explicitly documentation-only, corrected, or superseded with rationale. `@implements` coverage is never behavioral evidence. + +## 5. Waves B–D β€” HTTP, database/jobs, concurrency, and browser + +**Depends on landed ntnt owners:** 5A–12B plus the required landed DD-077 transport and migration owners + +Use separate focused Larrimon PRs: + +1. HTTP/auth/server conversion. +2. PostgreSQL/migration/RLS conversion. +3. Jobs/eventual/restart conversion. +4. Deterministic concurrency conversion. +5. Browser/reconciliation conversion. + +For each PR: + +1. inventory old cases with stable invariant IDs; +2. add failing `.tnt` equivalents; +3. run old and new checks on the same clean database, runtime, and image; +4. compare positive, negative, timing, cleanup, and race behavior; +5. inject representative semantic faults and prove both checks detect them with useful evidence; +6. delete only the replaced slice; +7. update Intent bindings and architecture/testing documentation. + +**Wave gate:** No project-owned Node/Playwright test files or non-migration SQL-only application test files remain after Wave D. Production JavaScript and SQL migrations remain. Production migration helpers remain until Slice 16M passes. + +## 6. Adoption Slice 16M β€” production migration compatibility + +**Consumer dependency only:** landed DD-077 PR 1C, landed DD-078 owner 8, and the Larrimon database-conversion wave. + +This slice is intentionally absent from the DD-078 core dependency table and releases. + +Run old migration checks and native `ntnt db`/`.tnt` evidence on one immutable Larrimon revision across: + +- fresh install and idempotent rerun; +- every supported legacy ledger and application/schema upgrade pair; +- checksum backfill and pre-package unverifiable rows; +- unknown-ledger rejection before mutation; +- malformed or missing manifests; +- missing or mutated applied files; +- database checksum enforcement; +- concurrent migrators and advisory locks; +- per-migration rollback and dirty recovery; +- cancellation and role configuration. + +Inject failures/mutations for every family and retain paired reports. + +**Exclusive deletion authority:** Only this consumer slice may authorize removal of: + +- `scripts/migrate.sh`; +- `scripts/migrate-prod.sh`; +- `scripts/check-migration-checksums.py`; +- `tests/migrate_prod_integration.sh`. + +DD-078 owner 8 may provide observations but cannot authorize these deletions. A later operational matrix may expand supported cases, but the currently supported production matrix cannot be deferred past deletion. + +## 7. Wave E β€” project policy and one-command CI + +**Depends on landed ntnt owners:** 13A–14D, adoption Slice 16M, and prior Larrimon waves + +1. Convert Python/static/provenance checks to `.tnt`. +2. Convert project-owned operational support outside the historical test tree to ordinary `.tnt` CLI programs or direct typed ntnt/provider commands. +3. Replace suite shell wrappers with `ntnt.toml` profiles. +4. Reduce CI to pinned setup/install/verify actions invoking named ntnt profiles through typed inputs; no project wrapper or inline script block. +5. Update `README.md`, `ARCHITECTURE.md`, and testing documentation. + +The immutable path/range/line/blob inventory remains [`dd-078-larrimon-baseline.md`](dd-078-larrimon-baseline.md). Regenerate it from the exact candidate base before deletion and require its digest, protected-contract base, and execution-snapshot base to match. + +## 8. Audited replacement destinations + +| Current Larrimon files | Required native destination | +|---|---| +| `tests/{all,fast,intent,db}.sh` | `ntnt.toml` profiles and pinned typed CI action entries for `ntnt intent check` | +| `tests/integration.sh`, `tests/server-smoke.sh`, `scripts/staging-smoke.sh` | linked `.tnt` HTTP/database/process/browser cases under the corresponding profile | +| `tests/migrate_prod_integration.sh` | adoption Slice 16M after the landed DD-077 migration owners | +| `scripts/{migrate,migrate-prod}.sh` | landed DD-077 `ntnt db` migration/apply/verify commands plus linked migration evidence | +| `scripts/{dev-up,dev-down,staging-up,staging-down}.sh` | landed 14C–14D typed `ntnt project env` state and OCI lifecycle | +| `scripts/staging-state.py`, `tests/staging_state_cases.py` | landed 14C state/lock/lease substrate, landed 14D OCI allocation, and `.tnt` cases | +| `scripts/check-migration-checksums.py` | owner 8 observations plus adoption Slice 16M compatibility; only 16M authorizes deletion | +| `tests/{architecture_cases,ci_cases,assets_provenance,runtime_provenance,runtime_image_provenance}.py` | `std/test/project`, Git/YAML/OCI/migration facts, and linked `.tnt` constraints | +| `tests/{smtp_mock,redirect_mock,resend_mock}.py` | landed typed SMTP and scripted HTTP fixture providers | +| `tests/reconciliation_cases.js`, `tests/staging-browser-smoke.mjs` | landed `std/test/browser` `.tnt` cases; production `public/larrimon.js` remains product code | +| `tests/{assertions,probe_run_state_fixture,security_definer_tenant_case}.sql` | typed PostgreSQL assertions/seed fixtures and role/RLS/security-definer `.tnt` cases; deleted before 16M | + +## 9. Consumer release sequence + +These are Larrimon milestones, not DD-078 releases: + +1. **Intent truth:** pinned owners 1A–4 plus Wave A. +2. **HTTP and process migration:** pinned owners 5A–7F plus Wave B. +3. **Database, jobs, and concurrency migration:** pinned owners 8–11A plus Wave C. +4. **Browser migration:** pinned owners 12A–12B plus Wave D. +5. **Project/environment migration:** pinned owners 13A–14D. +6. **Production migration compatibility:** adoption Slice 16M. +7. **Pure-project claim:** Wave E after every required prior milestone. + +A milestone starts only from exact landed ntnt commit identities. None of these milestones blocks a core DD-078 release. + +## 10. Larrimon definition of done + +This consumer adoption is complete when: + +- all 27 audited scenarios and 38 assertion/outcome lines are verified, corrected, superseded, or explicitly documentation-only; none vanish silently; +- every shell, Python, JavaScript test, and SQL-only application-test invariant has a destination and same-revision parity evidence; +- representative semantic mutations/faults prove detection before each old file is deleted; +- `tests/intent.sh` and suite wrappers are removed; +- project-owned `.sh` and `.py` support/orchestration files are zero, except operator-locked externally owned non-support artifacts; +- project-local browser/reconciliation test `.js`/`.mjs` and SQL-only application-test files are zero; +- typed project-state and `ntnt project env` replace dev/staging lifecycle programs with allocation, failure, cleanup, and mutation parity; +- the baseline inventory, protected contract, candidate base, execution snapshot, and evidence bind the same exact Larrimon commit and canonical digest; +- fast and full profiles run through ntnt with current verified coverage at the configured threshold; +- specialist external resources remain pinned, capability-scoped, and visible in reports; +- the complete old-to-new invariant ledger and mutation/fault witnesses remain in project history. + +Expected end-state commands: + +```bash +ntnt intent lint . +ntnt intent plan . --profile full --json +ntnt intent check . --profile fast +ntnt intent check . --profile full --report-json verification-report.json +``` + +Environment-backed protected profiles remain operator-selected outside the checkout. diff --git a/plans/dd-078-larrimon-baseline.md b/plans/dd-078-larrimon-baseline.md new file mode 100644 index 00000000..3f77769e --- /dev/null +++ b/plans/dd-078-larrimon-baseline.md @@ -0,0 +1,100 @@ +# DD-078 Larrimon audit baseline + +This appendix makes DD-078's first external reference-adoption facts reproducible. Larrimon is a demanding validation corpus for generalized ntnt mechanisms, not the scope or naming source for those mechanisms. This is an input baseline, not permission to delete files and not a substitute for the invariant/mutation ledger required before each migration deletion. Other adopters produce an equivalent appendix bound to their own repository, inventory, and invariants. + +- Repository: `https://github.com/larimonious/larrimon.git` +- Commit: `ceadfd992d1435ac27afb054968ff5569d697ce1` +- Audited branch label: `feat/host-check-management` +- Audit rule: committed bytes from the commit above only; concurrent dirty-worktree changes were excluded. +- Shell/Python/JavaScript/MJS extension inventory digest: `sha256:403ed54624a6d99cfe5b05a08f966ffaeb8d73eba20e05dfddff6aacbce3f253` +- SQL-only test inventory digest: `sha256:0e7bbaa9ddbd064a75eb4d55ff1dcee499c4564acb14a1fb8658ce835620f998` +- Intent inventory digest: `sha256:84dc5b6150950056bb3f56485f8dc7438b923d59ce140752e6630aaef3d015b7` + +Every digest is SHA-256 over UTF-8 rows in the exact form `pathline_countgit_blob_id`, sorted bytewise by Git tree path, with exactly one LF per row. `line_count` is LF count plus one only when non-empty content lacks a terminal LF. The extension digest includes every committed `.sh`, `.py`, `.js`, and `.mjs` path; the SQL-only digest includes committed `tests/*.sql`; the Intent digest includes every committed `*.intent`. Git tree paths and blob IDs are emitted by Git; duplicate paths are impossible in one tree and a non-UTF-8 path makes regeneration fail closed rather than substitute a lossy name. A rebase or changed Larrimon base invalidates all facts and requires a regenerated appendix and protected contract before a deletion gate. + +## Reproducible findings + +- 7 Intent files: 20 `Feature:` entries, 27 `Scenario:` entries, and 38 `β†’` outcome/assertion lines. +- 5 Intent files have no scenario: `jobs/run_probe.intent`, `jobs/schedule_due_checks.intent`, `lib/auth.intent`, `lib/settings.intent`, and `routes/users.intent`. +- Committed `.tnt` source contains 37 `@implements` and 0 `@supports` annotations. +- `tests/intent.sh` contains 18 direct `ntnt run tests/...` invocations and 0 `ntnt intent check` invocations. +- 14 shell files plus 11 Python files are project-owned migration, orchestration, fixture, policy, or test/support programs and must be replaced. +- 2 project-owned JavaScript/MJS test programs must be replaced. Product JavaScript and vendored HTMX remain product assets. +- 3 SQL-only test programs/fixtures contain 400 lines and are executable inputs to `tests/integration.sh`; Task 16 replaces them with typed PostgreSQL fixtures/assertions. +- Those 30 replacement files contain 4,549 committed lines. The audited `tests/` executable/spec set (`.sh`, `.py`, `.js`, `.mjs`, `.sql`, `.tnt`, `.intent`) contains 4,935 lines; non-test production `.tnt` contains 4,827 lines. + +## Intent files + +| Path | Lines | Git blob | +|---|---:|---| +| `jobs/run_probe.intent` | 26 | `73bcab32dadbfddfe80c001c185f47d12652e352` | +| `jobs/schedule_due_checks.intent` | 14 | `10dcb601c270ab03a708d6c328062a1018e61bf2` | +| `lib/auth.intent` | 13 | `67ff2100080c7e69c246298e3e1cbfc5883f9231` | +| `lib/settings.intent` | 13 | `519e6c189e636899072f891db4e7a9ab0e65beee` | +| `routes/users.intent` | 6 | `af85fdba78609986874af4b3e6b013b3fbe03748` | +| `server.intent` | 168 | `9c6b04ed72a364a052187091c9320de87b2df40f` | +| `tests/public_http.intent` | 46 | `8f34d8c53f28d3620a689ab21de64445e794cb67` | + +## Project-owned support/test replacement inventory + +`Range` is the full committed file range. The later invariant ledger must split these ranges into stable behavioral invariants, replacement obligation/case IDs, environment/resources, positive results, and mutation/fault witnesses. + +| Path | Range | Lines | Git blob | Required destination | +|---|---:|---:|---|---| +| `scripts/check-migration-checksums.py` | 1–59 | 59 | `02b9297b8b5e7f42229def5fdbc2f2bd3a6013d9` | DD-077 PRs 1B–1C, DD-078 Task 8 and Slice 16M | +| `scripts/dev-down.sh` | 1–5 | 5 | `aef22fa45c331529b583f0a2ab9c632c27b3ee70` | Slices 14C–14D typed project environment lifecycle | +| `scripts/dev-up.sh` | 1–8 | 8 | `eccf803b8cbb7eb91fad8d9d32b2ced54e3cc962` | Slices 14C–14D plus DD-077 migration runner | +| `scripts/migrate-prod.sh` | 1–136 | 136 | `fa46418cc580d64e18e4e3d3c4e3705510ee2e05` | DD-077 PRs 1B–1C and DD-078 Slice 16M | +| `scripts/migrate.sh` | 1–26 | 26 | `840f6c602c40e8625e63fa07e4f0157cede53051` | DD-077 PRs 1B–1C and DD-078 Slice 16M | +| `scripts/staging-down.sh` | 1–19 | 19 | `a5f58cde88dc13942c38cbc74a8df17bfdc48e32` | Slices 14C–14D ownership-safe teardown | +| `scripts/staging-smoke.sh` | 1–64 | 64 | `1a856607ceb913bc2d1949a6550b7cb17c830cbb` | Stateful HTTP/browser verification and environment profile | +| `scripts/staging-state.py` | 1–215 | 215 | `5f51983508bb622fc662f9341d28375cad1e4b9b` | Slice 14C typed project state/lease plus 14D OCI allocation API | +| `scripts/staging-up.sh` | 1–40 | 40 | `41202e958db829c10d18db2d7a0c5976b3bd7375` | Slices 14C–14D typed OCI environment lifecycle | +| `tests/all.sh` | 1–15 | 15 | `dbcae166b36185e8a3a314033c1cda40b115ea55` | `ntnt.toml` profiles and direct ntnt CI | +| `tests/architecture_cases.py` | 1–97 | 97 | `478eda515b93907909d08e4557a8863c7430c587` | `std/test/project` facts and `.tnt` constraints | +| `tests/assets_provenance.py` | 1–11 | 11 | `362f3d66aac906029d7bd3f09d728daa8f4e30cc` | Git/project provenance facts and `.tnt` constraints | +| `tests/ci_cases.py` | 1–9 | 9 | `f9e628e58351ba0505f1d79f0f610da0b7920f61` | Workflow/project facts and `.tnt` constraints | +| `tests/db.sh` | 1–6 | 6 | `517f1ac220ba0efacad4c3d3a3efbcb3d9bfc6d9` | Full database profile | +| `tests/fast.sh` | 1–17 | 17 | `8b83e0a1544310b0f1b6b4602a0ba1675dae6626` | Fast profile | +| `tests/integration.sh` | 1–1810 | 1810 | `7245afe663c8f4308169e0a22b857f6dbce4c0f0` | HTTP/process/DB/job/concurrency provider and `.tnt` slices | +| `tests/intent.sh` | 1–115 | 115 | `0965c489f91f320269be4ebf11fb34a2f4be44fb` | Native Intent planner/executor and linked `.tnt` cases | +| `tests/migrate_prod_integration.sh` | 1–207 | 207 | `613216620b748778b0b4e3b523eff2c374712cc6` | DD-077 PRs 1B–1C and DD-078 Slice 16M | +| `tests/reconciliation_cases.js` | 1–503 | 503 | `98d342df7105e3e13ad7f017c4a564e3440e61e4` | Sandboxed browser `.tnt` cases | +| `tests/redirect_mock.py` | 1–48 | 48 | `65c5ed780489904fe543796a760b449b5bfbeb97` | Built-in scripted HTTP fixture | +| `tests/resend_mock.py` | 1–40 | 40 | `47b2aabc34fa035482f7d4e9d9e791f4dc2af42b` | Built-in scripted HTTP fixture | +| `tests/runtime_image_provenance.py` | 1–50 | 50 | `7c23146f2ce68199d0b092d44881c24c8030a6f0` | OCI/image provenance facts and `.tnt` constraints | +| `tests/runtime_provenance.py` | 1–62 | 62 | `077a6af4ae4acccf626c9720485f687d4099dc1d` | Runtime/Git provenance facts and `.tnt` constraints | +| `tests/server-smoke.sh` | 1–6 | 6 | `fb8141ccaca69799e9ae13e901c5b3736b70c46e` | Managed app readiness/HTTP case | +| `tests/smtp_mock.py` | 1–72 | 72 | `da90d8c0cf1e779b1ee7183bc0d4b52dc7a5d031` | Built-in SMTP capture fixture | +| `tests/staging-browser-smoke.mjs` | 1–289 | 289 | `2eaa9db6c0e2fb6597d5a00e27ba25f74af5e276` | Sandboxed browser `.tnt` cases | +| `tests/staging_state_cases.py` | 1–220 | 220 | `81132144b791cca3b2a8927543c547989cef4410` | Slices 14C–14D state/allocation conformance plus `.tnt` cases | + +## SQL-only test replacement inventory + +These are application/schema verification inputs, not production migration-runner fixtures. Task 16 deletes them after same-revision positive, negative, race, cleanup, and mutation parity; Slice 16M does not hold them. + +| Path | Range | Lines | Git blob | Required destination | +|---|---:|---:|---|---| +| `tests/assertions.sql` | 1–96 | 96 | `a5959ce6a090b8c6f4f85f7f5add903a41cb98a0` | Task 16 typed PostgreSQL assertions | +| `tests/probe_run_state_fixture.sql` | 1–206 | 206 | `cfc691bbb28f9a7be3d3d8193caec1c3bce82b8e` | Task 16 typed committed seed/fixture API | +| `tests/security_definer_tenant_case.sql` | 1–98 | 98 | `a7934134fec0244143322c069291d23f4a56dda4` | Task 16 role/RLS/security-definer `.tnt` cases | + +## Retained product assets + +These files are in the extension inventory but are not verification/support programs and are not deletion targets. + +| Path | Range | Lines | Git blob | Classification | +|---|---:|---:|---|---| +| `public/larrimon.js` | 1–733 | 733 | `f96088c41f6f2d84905c303456ea2621d42612ec` | project-owned production asset | +| `public/vendor/htmx-2.0.10.min.js` | 1–1 | 1 | `3b7ac1aceb211ca716c7a9c5774c649f74331ee1` | vendored production asset; immutable origin/digest classification required | + +## Regeneration gate + +Before any Larrimon migration/deletion branch: + +1. resolve and record the exact candidate base commit; +2. regenerate the extension, SQL-only test, and Intent canonical inventories from committed bytes; +3. update every changed full-file range and Git blob ID; +4. regenerate the protected contract from the same base; +5. expand affected files into invariant-level rows before deletion; +6. fail closed if the worktree, contract base, inventory base, or report base differ. diff --git a/tests/dd078_plan_tests.rs b/tests/dd078_plan_tests.rs new file mode 100644 index 00000000..11af54e0 --- /dev/null +++ b/tests/dd078_plan_tests.rs @@ -0,0 +1,958 @@ +use sha2::{Digest, Sha256}; +use std::collections::{BTreeMap, BTreeSet}; + +const PLAN: &str = include_str!("../plans/dd-078-intent-verification-implementation.md"); +const LARRIMON_ADOPTION: &str = include_str!("../plans/dd-078-larrimon-adoption.md"); +const DESIGN: &str = include_str!("../design-docs/dd-078-intent-verification-runtime.md"); +const CORE_PLAN_SHA256: &str = include_str!("fixtures/dd078/core-plan.sha256"); +const CORE_DESIGN_SHA256: &str = include_str!("fixtures/dd078/core-design.sha256"); +const LARRIMON_ADOPTION_SHA256: &str = include_str!("fixtures/dd078/larrimon-adoption.sha256"); +const CORE_ACCEPTANCE_SNAPSHOT: &str = include_str!("fixtures/dd078/core-acceptance-criteria.md"); +const CORE_DOD_SNAPSHOT: &str = include_str!("fixtures/dd078/core-definition-of-done.md"); +const LARRIMON_16M_SNAPSHOT: &str = include_str!("fixtures/dd078/larrimon-slice-16m.md"); +const LARRIMON_DOD_SNAPSHOT: &str = include_str!("fixtures/dd078/larrimon-definition-of-done.md"); + +#[derive(Debug)] +struct SliceGraph { + dependencies: BTreeMap>, + scopes: BTreeMap, +} + +fn expand_id(value: &str) -> Result, String> { + let value = value.trim(); + let Some((start, end)) = value.split_once('–') else { + return Ok(vec![value.to_string()]); + }; + + let prefix_len = start + .char_indices() + .find_map(|(index, ch)| ch.is_ascii_alphabetic().then_some(index)) + .unwrap_or(start.len()); + let (prefix, start_suffix) = start.split_at(prefix_len); + let end_suffix = end.strip_prefix(prefix).unwrap_or(end); + + if start_suffix.len() == 1 + && end_suffix.len() == 1 + && start_suffix.as_bytes()[0].is_ascii_alphabetic() + && end_suffix.as_bytes()[0].is_ascii_alphabetic() + { + let start_byte = start_suffix.as_bytes()[0]; + let end_byte = end_suffix.as_bytes()[0]; + if start_byte > end_byte { + return Err(format!("reversed slice range {value}")); + } + return Ok((start_byte..=end_byte) + .map(|suffix| format!("{prefix}{}", suffix as char)) + .collect()); + } + + Ok(vec![start.to_string(), end.to_string()]) +} + +fn dependency_tokens(value: &str) -> Result, String> { + let mut tokens = BTreeSet::new(); + for item in value + .split(',') + .map(str::trim) + .filter(|item| !item.is_empty()) + { + if item.starts_with("DD-") || item.starts_with("Task ") { + tokens.insert(item.to_string()); + } else { + tokens.extend(expand_id(item)?); + } + } + Ok(tokens) +} + +fn internal_dependencies(value: &BTreeSet) -> Vec { + value + .iter() + .filter(|item| !item.starts_with("DD-") && !item.starts_with("Task ")) + .cloned() + .collect() +} + +fn depends_transitively(graph: &SliceGraph, slice: &str, target: &str) -> bool { + let mut pending = vec![slice.to_string()]; + let mut seen = BTreeSet::new(); + while let Some(current) = pending.pop() { + if !seen.insert(current.clone()) { + continue; + } + for dependency in internal_dependencies(&graph.dependencies[¤t]) { + if dependency == target { + return true; + } + pending.push(dependency); + } + } + false +} + +fn parse_graph(plan: &str) -> Result { + let block = plan + .split_once("### Dependency-closed DD-078 PR slices") + .ok_or("missing DD-078 slice table marker")? + .1 + .split_once("Each task below supplies") + .ok_or("missing DD-078 slice table terminator")? + .0; + + let mut dependencies = BTreeMap::new(); + let mut scopes = BTreeMap::new(); + for line in block.lines().filter(|line| line.starts_with("| ")) { + if line.starts_with("| Slice") || line.starts_with("|---") { + continue; + } + let columns: Vec<_> = line.trim_matches('|').split('|').map(str::trim).collect(); + if columns.len() != 3 { + return Err(format!("malformed slice row: {line}")); + } + let row_dependencies = dependency_tokens(columns[2])?; + for id in expand_id(columns[0])? { + if dependencies + .insert(id.clone(), row_dependencies.clone()) + .is_some() + { + return Err(format!("duplicate slice ID {id}")); + } + scopes.insert(id, columns[1].to_string()); + } + } + if dependencies.is_empty() { + return Err("slice table must not be empty".to_string()); + } + Ok(SliceGraph { + dependencies, + scopes, + }) +} + +fn visit( + id: &str, + graph: &SliceGraph, + visiting: &mut BTreeSet, + visited: &mut BTreeSet, +) -> Result<(), String> { + if visited.contains(id) { + return Ok(()); + } + if !visiting.insert(id.to_string()) { + return Err(format!("dependency cycle at {id}")); + } + for dependency in internal_dependencies(&graph.dependencies[id]) { + if !graph.dependencies.contains_key(&dependency) { + return Err(format!( + "slice {id} has unknown internal dependency {dependency}" + )); + } + visit(&dependency, graph, visiting, visited)?; + } + visiting.remove(id); + visited.insert(id.to_string()); + Ok(()) +} + +fn heading_ids(line: &str) -> Result>, String> { + let declaration = if let Some(rest) = line.strip_prefix("## Task ") { + if let Some((_, slice)) = rest.split_once(" / Slice ") { + slice.split_once(':').ok_or("slice heading colon")?.0 + } else if let Some((_, slices)) = rest.split_once(" / Slices ") { + slices.split_once(':').ok_or("slices heading colon")?.0 + } else { + rest.split_once(':').ok_or("task heading colon")?.0 + } + } else if let Some(rest) = line.strip_prefix("### Slice ") { + rest.split_once(':').ok_or("slice heading colon")?.0 + } else { + return Ok(None); + }; + + let mut ids = Vec::new(); + for part in declaration.replace(" and ", ",").split(',') { + ids.extend(expand_id(part.trim())?); + } + Ok(Some(ids)) +} + +fn validate_owners(plan: &str, graph: &SliceGraph) -> Result<(), String> { + let lines: Vec<_> = plan.lines().collect(); + let mut owners = BTreeMap::::new(); + let allowed_non_slice_tasks = ["0", "15", "16", "17"]; + + for (index, line) in lines.iter().enumerate() { + let Some(ids) = heading_ids(line)? else { + continue; + }; + let known_ids: Vec<_> = ids + .iter() + .filter(|id| graph.dependencies.contains_key(*id)) + .collect(); + for id in &ids { + if id.chars().any(|ch| ch.is_ascii_alphabetic()) && !graph.dependencies.contains_key(id) + { + return Err(format!("unknown slice owner heading {id}")); + } + if !graph.dependencies.contains_key(id) + && !allowed_non_slice_tasks.contains(&id.as_str()) + { + return Err(format!("unknown task owner heading {id}")); + } + } + if known_ids.is_empty() { + continue; + } + let end = lines[index + 1..] + .iter() + .position(|candidate| { + candidate.starts_with("## Task ") || candidate.starts_with("### Slice ") + }) + .map(|offset| index + 1 + offset) + .unwrap_or(lines.len()); + let dependency_lines: Vec<_> = lines[index + 1..end] + .iter() + .filter_map(|candidate| candidate.strip_prefix("**Table dependencies:** ")) + .collect(); + if dependency_lines.len() != 1 { + return Err(format!( + "owner heading {line} must have exactly one Table dependencies line" + )); + } + let owner_dependencies = dependency_tokens(dependency_lines[0])?; + for id in known_ids { + *owners.entry(id.clone()).or_default() += 1; + if owner_dependencies != graph.dependencies[id] { + return Err(format!( + "slice {id} owner dependencies {owner_dependencies:?} do not match table {:?}", + graph.dependencies[id] + )); + } + } + } + + for id in graph.dependencies.keys() { + if owners.get(id) != Some(&1) { + return Err(format!( + "slice {id} must have exactly one owning task/section heading" + )); + } + } + Ok(()) +} + +fn validate_created_module_registration(plan: &str, graph: &SliceGraph) -> Result<(), String> { + let lines: Vec<_> = plan.lines().collect(); + for (index, heading) in lines + .iter() + .enumerate() + .filter(|(_, line)| line.starts_with("## Task ") || line.starts_with("### Slice ")) + { + let owner = heading_ids(heading)? + .unwrap_or_default() + .into_iter() + .find(|id| graph.dependencies.contains_key(id)); + let end = lines[index + 1..] + .iter() + .position(|candidate| { + candidate.starts_with("## Task ") || candidate.starts_with("### Slice ") + }) + .map(|offset| index + 1 + offset) + .unwrap_or(lines.len()); + let section = lines[index..end].join("\n"); + let mut remainder = section.as_str(); + while let Some(create_start) = remainder.find("**Create") { + let after_create = &remainder[create_start..]; + let create_end = [ + "\n**Create", + "\n**Modify", + "\n**RED", + "\n**GREEN", + "\n**REFACTOR", + "\n**Gate", + "\n**Verify", + "\n**Acceptance", + ] + .iter() + .filter_map(|marker| after_create.find(marker)) + .min() + .unwrap_or(after_create.len()); + let create_block = &after_create[..create_end]; + for path in create_block + .split('`') + .filter(|part| part.starts_with("src/") && part.ends_with(".rs")) + { + let required = if path.starts_with("src/verification/provider/") + && path != "src/verification/provider/mod.rs" + { + Some("src/verification/provider/mod.rs") + } else if path.starts_with("src/verification/") && path != "src/verification/mod.rs" + { + Some("src/verification/mod.rs") + } else if path.starts_with("src/stdlib/test/") { + Some("src/stdlib/test.rs") + } else if path.starts_with("src/stdlib/") && path != "src/stdlib/mod.rs" { + Some("src/stdlib/mod.rs") + } else if path.starts_with("src/project_env/") && path != "src/project_env/mod.rs" { + Some("src/project_env/mod.rs") + } else if path.matches('/').count() == 1 + && path != "src/main.rs" + && !path.starts_with("src/bin/") + { + Some("src/lib.rs") + } else { + None + }; + if let Some(required) = required { + if !section.contains(required) { + return Err(format!( + "owner {heading} creates {path} without parent registration {required}" + )); + } + let creator = match required { + "src/verification/mod.rs" => Some("1A"), + "src/stdlib/test.rs" => Some("3D"), + "src/verification/provider/mod.rs" => Some("5A"), + "src/project_env/mod.rs" => Some("14D"), + _ => None, + }; + if let (Some(owner), Some(creator)) = (owner.as_deref(), creator) { + if owner != creator && !depends_transitively(graph, owner, creator) { + return Err(format!( + "owner {heading} creates {path}, but parent {required} is owned by non-dependency {creator}" + )); + } + } + } + } + if create_end == after_create.len() { + break; + } + remainder = &after_create[create_end..]; + } + } + Ok(()) +} + +fn validate_external_prerequisites(plan: &str, graph: &SliceGraph) -> Result<(), String> { + let ledger = plan + .split_once("### External prerequisite ledger") + .ok_or("missing external prerequisite ledger")? + .1 + .split_once("### Dependency-closed DD-078 PR slices") + .ok_or("missing external prerequisite ledger terminator")? + .0; + let owners: BTreeSet<_> = ledger + .lines() + .filter(|line| { + line.starts_with("| ") + && !line.starts_with("| External owner") + && !line.starts_with("|---") + }) + .filter_map(|line| line.trim_matches('|').split('|').next()) + .map(str::trim) + .map(str::to_string) + .collect(); + + for dependency in graph.dependencies.values().flatten() { + if dependency.starts_with("DD-") && !owners.contains(dependency) { + return Err(format!("unknown external prerequisite {dependency}")); + } + } + for required in [ + "DD-077 PR 0A", + "DD-077 Design spike 0B", + "DD-077 PR 2C", + "DD-077 PR 2D", + "DD-077 PR 2E", + "DD-077 PR 1B", + "DD-077 PR 1C", + "DD-047 Slice 1C", + "DD-047 PR 2", + ] { + if !owners.contains(required) { + return Err(format!("missing external ledger owner {required}")); + } + } + for identity in [ + "f0132afcff984bb43305be39122d7e74a6850396", + "31a6d82f79e6051a7f00bfb182c979e5e78f2c3f", + "5a24c0cd1ff2f4d58e77ef263346cf6828cd28d6", + "41b644195e2aaa81997f76631daa8bae5e5cb53c", + ] { + if !ledger.contains(identity) { + return Err(format!("missing external source identity {identity}")); + } + } + Ok(()) +} + +fn validate_task_dependencies(plan: &str, graph: &SliceGraph) -> Result<(), String> { + let allowed = BTreeMap::from([("Task 0", "## Task 0:")]); + for dependency in graph.dependencies.values().flatten() { + if !dependency.starts_with("Task ") { + continue; + } + let heading = allowed + .get(dependency.as_str()) + .ok_or_else(|| format!("unknown task dependency {dependency}"))?; + if !plan.contains(heading) { + return Err(format!( + "task dependency {dependency} has no exact owner {heading}" + )); + } + } + Ok(()) +} + +fn assert_release_closed( + name: &str, + members: &[&str], + available: &mut BTreeSet, + graph: &SliceGraph, +) -> Result<(), String> { + let group: BTreeSet<_> = members.iter().map(|id| id.to_string()).collect(); + for id in &group { + if !graph.dependencies.contains_key(id) { + return Err(format!("release {name} names unknown slice {id}")); + } + for dependency in internal_dependencies(&graph.dependencies[id]) { + if !available.contains(&dependency) && !group.contains(&dependency) { + return Err(format!( + "release {name} omits dependency {dependency} required by {id}" + )); + } + } + } + available.extend(group); + Ok(()) +} + +fn validate_releases(plan: &str, graph: &SliceGraph) -> Result<(), String> { + let block = plan + .split_once("## Release sequencing") + .ok_or("missing release sequencing")? + .1; + let mut rows = BTreeMap::new(); + for line in block.lines().filter(|line| line.starts_with("| ")) { + if line.starts_with("| Candidate feature boundary") || line.starts_with("|---") { + continue; + } + let columns: Vec<_> = line.trim_matches('|').split('|').map(str::trim).collect(); + if columns.len() != 2 { + return Err(format!("malformed release row: {line}")); + } + if rows.insert(columns[0], columns[1]).is_some() { + return Err(format!("duplicate release row {}", columns[0])); + } + } + let expected_rows = [ + "v0.6.0 foundation", + "next feature release", + "following feature release", + "browser/project feature release", + "project-environment feature release", + "future monitoring/reliability releases", + ]; + if rows.keys().copied().collect::>() + != expected_rows.into_iter().collect::>() + { + return Err(format!("release row set drifted: {:?}", rows.keys())); + } + for (name, required) in [ + ("v0.6.0 foundation", "Slices 1A–1B, 2A–2G, 3A–3E"), + ("next feature release", "Slice 4, 5A–5B, 6A–6B"), + ( + "following feature release", + "Slices 7P, 7A–7F, 8–9, 10P, 10A–10C, and 11A", + ), + ( + "browser/project feature release", + "Slices 12P, 12A–12B, 13A–13E, and 14A–14B", + ), + ("project-environment feature release", "Slices 14C–14D"), + ( + "future monitoring/reliability releases", + "Slices 18P, 18A–18B, then 19A–19C, then 20P, 20A–20C", + ), + ] { + if !rows[name].contains(required) { + return Err(format!( + "release {name} omits canonical membership {required}" + )); + } + } + + let mut available = BTreeSet::new(); + assert_release_closed( + "foundation", + &[ + "1A", "1B", "2A", "2B", "2C", "2D", "2E", "2F", "2G", "3A", "3B", "3C", "3D", "3E", + ], + &mut available, + graph, + )?; + assert_release_closed( + "next", + &["4", "5A", "5B", "6A", "6B"], + &mut available, + graph, + )?; + assert_release_closed( + "providers", + &[ + "7P", "7A", "7B", "7C", "7D", "7E", "7F", "8", "9", "10P", "10A", "10B", "10C", "11A", + ], + &mut available, + graph, + )?; + assert_release_closed( + "browser-project", + &[ + "12P", "12A", "12B", "13A", "13B", "13C", "13D", "13E", "14A", "14B", + ], + &mut available, + graph, + )?; + assert_release_closed( + "project-environment", + &["14C", "14D"], + &mut available, + graph, + )?; + assert_release_closed("monitoring", &["18P", "18A", "18B"], &mut available, graph)?; + assert_release_closed("reliability", &["19A", "19B", "19C"], &mut available, graph)?; + assert_release_closed("ha", &["20P", "20A", "20B", "20C"], &mut available, graph)?; + let all_slices: BTreeSet<_> = graph.dependencies.keys().cloned().collect(); + if available != all_slices { + let unreleased: Vec<_> = all_slices.difference(&available).cloned().collect(); + let unknown: Vec<_> = available.difference(&all_slices).cloned().collect(); + return Err(format!( + "release groups must cover every core slice exactly: unreleased={unreleased:?}, unknown={unknown:?}" + )); + } + Ok(()) +} + +fn validate_spikes(plan: &str, graph: &SliceGraph) -> Result<(), String> { + for (spike, implementation) in [ + ("6A", "6B"), + ("7P", "7A"), + ("10P", "10B"), + ("12P", "12A"), + ("18P", "18A"), + ("20P", "20A"), + ] { + if !graph.scopes[spike].contains("spike") { + return Err(format!("{spike} is not table-classified as a spike")); + } + if !graph.dependencies[implementation].contains(spike) { + return Err(format!("{implementation} does not depend on spike {spike}")); + } + let marker = format!("## Task {spike}:"); + let body = plan + .split_once(&marker) + .ok_or_else(|| format!("missing spike owner {spike}"))? + .1; + let end = [body.find("\n## Task "), body.find("\n### Slice ")] + .into_iter() + .flatten() + .min() + .unwrap_or(body.len()); + let section = &body[..end]; + if !section.contains("**Artifact:**") + || !(section.contains("no public") || section.contains("no production")) + || section.contains("**Create:** `src/") + { + return Err(format!( + "spike {spike} must remain artifact-only with no public/production API" + )); + } + } + if !graph.dependencies["20B"].contains("20P") { + return Err("20B does not depend on spike 20P".to_string()); + } + Ok(()) +} + +fn canonical_lf(document: &str) -> String { + document.replace("\r\n", "\n") +} + +fn reviewed_section(document: &str, start: &str, end: Option<&str>) -> Result { + let document = canonical_lf(document); + let start_count = document.matches(start).count(); + if start_count != 1 { + return Err(format!( + "reviewed section heading {start:?} must occur exactly once, found {start_count}" + )); + } + let start_offset = document + .find(start) + .ok_or_else(|| format!("missing reviewed section heading {start:?}"))?; + let tail = &document[start_offset..]; + let section = if let Some(end) = end { + let end_count = tail.matches(end).count(); + if end_count != 1 { + return Err(format!( + "reviewed section terminator {end:?} must occur exactly once after {start:?}, found {end_count}" + )); + } + let end_offset = tail + .find(end) + .ok_or_else(|| format!("missing reviewed section terminator {end:?}"))?; + &tail[..end_offset] + } else { + tail + }; + Ok(section.trim().to_string()) +} + +fn require_reviewed_snapshot(name: &str, actual: &str, expected: &str) -> Result<(), String> { + let actual = canonical_lf(actual); + let expected = canonical_lf(expected); + if actual.trim() != expected.trim() { + return Err(format!( + "reviewed DD-078 safety snapshot drifted: {name}; inspect the source/fixture diff before updating" + )); + } + Ok(()) +} + +fn require_reviewed_envelope_digest( + name: &str, + document: &str, + expected_hex: &str, +) -> Result<(), String> { + let canonical = canonical_lf(document); + let actual = format!("{:x}", Sha256::digest(canonical.as_bytes())); + if actual != expected_hex.trim() { + return Err(format!( + "reviewed DD-078 normative envelope drifted: {name}; inspect the complete source and digest fixture diff before updating" + )); + } + Ok(()) +} + +fn validate_adoption_boundary( + plan: &str, + adoption: &str, + design: &str, + graph: &SliceGraph, +) -> Result<(), String> { + if graph.dependencies.contains_key("16M") { + return Err("consumer Slice 16M entered the core DD-078 DAG".to_string()); + } + for forbidden in [ + "## Task 15: Larrimon", + "## Task 16: Larrimon", + "## Task 17: Larrimon", + "### Slice 16M:", + "| Larrimon pure-project deletion |", + "**Larrimon gate", + "**Reference-adoption gate (Larrimon)", + "**Reference-adoption deletion gate (Larrimon)", + ] { + if plan.contains(forbidden) { + return Err(format!( + "consumer-specific adoption requirement remained in core plan: {forbidden}" + )); + } + } + for required in [ + "does not participate in the DD-078 core dependency DAG, release sequence, or definition of done", + "## 6. Adoption Slice 16M β€” production migration compatibility", + "**Exclusive deletion authority:**", + "scripts/migrate.sh", + "scripts/migrate-prod.sh", + "scripts/check-migration-checksums.py", + "tests/migrate_prod_integration.sh", + "## 10. Larrimon definition of done", + ] { + if !adoption.contains(required) { + return Err(format!( + "standalone Larrimon adoption plan lost required boundary or gate: {required}" + )); + } + } + if !plan.contains("[`dd-078-larrimon-adoption.md`](dd-078-larrimon-adoption.md)") { + return Err("core plan does not link the standalone adoption plan".to_string()); + } + for forbidden in [ + "### Reference-adoption proof: Larrimon", + "Task 17 cannot claim pure-ntnt", + ] { + if design.contains(forbidden) { + return Err(format!( + "consumer-specific completion requirement remained in core design: {forbidden}" + )); + } + } + for required in [ + "No particular application inventory, migration wave, helper deletion, or adoption completion date participates in the DD-078 core DAG, release sequence, or definition of done.", + "plans/dd-078-larrimon-adoption.md", + "### Adoption portability", + ] { + if !design.contains(required) { + return Err(format!( + "core design lost its generalized adoption boundary: {required}" + )); + } + } + require_reviewed_snapshot( + "core acceptance criteria", + &reviewed_section( + design, + "## 25. Acceptance criteria\n", + Some("## 26. Open implementation questions\n"), + )?, + CORE_ACCEPTANCE_SNAPSHOT, + )?; + require_reviewed_snapshot( + "core definition of done", + &reviewed_section(plan, "## Definition of done\n", None)?, + CORE_DOD_SNAPSHOT, + )?; + require_reviewed_snapshot( + "Larrimon Slice 16M", + &reviewed_section( + adoption, + "## 6. Adoption Slice 16M β€” production migration compatibility\n", + Some("## 7. Wave E β€” project policy and one-command CI\n"), + )?, + LARRIMON_16M_SNAPSHOT, + )?; + require_reviewed_snapshot( + "Larrimon definition of done", + &reviewed_section(adoption, "## 10. Larrimon definition of done\n", None)?, + LARRIMON_DOD_SNAPSHOT, + )?; + require_reviewed_envelope_digest("core design", design, CORE_DESIGN_SHA256)?; + require_reviewed_envelope_digest("core implementation plan", plan, CORE_PLAN_SHA256)?; + require_reviewed_envelope_digest( + "standalone Larrimon adoption plan", + adoption, + LARRIMON_ADOPTION_SHA256, + )?; + Ok(()) +} + +fn validate_plan(plan: &str) -> Result<(), String> { + let graph = parse_graph(plan)?; + for (id, dependencies) in &graph.dependencies { + for dependency in internal_dependencies(dependencies) { + if !graph.dependencies.contains_key(&dependency) { + return Err(format!( + "slice {id} has unknown internal dependency {dependency}" + )); + } + } + } + let mut visiting = BTreeSet::new(); + let mut visited = BTreeSet::new(); + for id in graph.dependencies.keys() { + visit(id, &graph, &mut visiting, &mut visited)?; + } + validate_owners(plan, &graph)?; + validate_created_module_registration(plan, &graph)?; + validate_external_prerequisites(plan, &graph)?; + validate_task_dependencies(plan, &graph)?; + validate_releases(plan, &graph)?; + validate_spikes(plan, &graph)?; + validate_adoption_boundary(plan, LARRIMON_ADOPTION, DESIGN, &graph)?; + if !plan.contains("f0132afcff984bb43305be39122d7e74a6850396") || plan.contains("DD-077 Slice 0") + { + return Err("DD-077 immutable identity/owner naming drift".to_string()); + } + Ok(()) +} + +#[test] +fn dd078_plan_is_dependency_closed_and_owner_consistent() { + validate_plan(PLAN).unwrap(); + + let plan_crlf = PLAN.replace("\r\n", "\n").replace('\n', "\r\n"); + let adoption_crlf = LARRIMON_ADOPTION + .replace("\r\n", "\n") + .replace('\n', "\r\n"); + let design_crlf = DESIGN.replace("\r\n", "\n").replace('\n', "\r\n"); + let graph = parse_graph(&plan_crlf).unwrap(); + validate_adoption_boundary(&plan_crlf, &adoption_crlf, &design_crlf, &graph).unwrap(); +} + +#[test] +fn dd078_plan_validator_rejects_representative_drift() { + let owner_drift = PLAN.replacen( + "**Table dependencies:** 1A", + "**Table dependencies:** 2A", + 1, + ); + assert!(validate_plan(&owner_drift).is_err()); + + let unknown_dependency = PLAN.replacen( + "| 1B | JSON/human report schema and exit parity | 1A |", + "| 1B | JSON/human report schema and exit parity | ZZ |", + 1, + ); + assert!(validate_plan(&unknown_dependency).is_err()); + + let duplicate_id = PLAN.replacen( + "| 1A | status algebra, stable IDs, false-pass fixes | Task 0 |", + "| 1A | status algebra, stable IDs, false-pass fixes | Task 0 |\n| 1A | duplicate | Task 0 |", + 1, + ); + assert!(validate_plan(&duplicate_id).is_err()); + + let production_spike = PLAN.replacen( + "no public API or production supervisor", + "production supervisor", + 1, + ); + assert!(validate_plan(&production_spike).is_err()); + + let release_drift = PLAN.replacen( + "| project-environment feature release | Slices 14C–14D", + "| project-environment feature release | Slice 14D", + 1, + ); + assert!(validate_plan(&release_drift).is_err()); + + let unreleased_slice = PLAN + .replacen( + "| 1B | JSON/human report schema and exit parity | 1A |", + "| 1B | JSON/human report schema and exit parity | 1A |\n| 21 | synthetic unreleased slice | 1A |", + 1, + ) + .replace( + "# Reference-adoption plans", + "## Task 21: Synthetic unreleased slice\n\n**Table dependencies:** 1A\n\n**Modify:** documentation only.\n\n---\n\n# Reference-adoption plans", + ); + assert!(validate_plan(&unreleased_slice) + .unwrap_err() + .contains("unreleased=[\"21\"]")); + + let external_owner_drift = PLAN + .replace( + "| 18B | monitoring protocol, catalog, and inventory acceptance profiles | 18A, 13A, DD-047 Slice 1C, DD-047 PR 2 |", + "| 18B | monitoring protocol, catalog, and inventory acceptance profiles | 18A, 13A, DD-999 Slice 1C, DD-047 PR 2 |", + ) + .replace( + "**Table dependencies:** 13A, 18A, DD-047 Slice 1C, DD-047 PR 2", + "**Table dependencies:** 13A, 18A, DD-999 Slice 1C, DD-047 PR 2", + ); + assert!(validate_plan(&external_owner_drift).is_err()); + + let plan_lf = PLAN.replace("\r\n", "\n"); + let adoption_lf = LARRIMON_ADOPTION.replace("\r\n", "\n"); + let design_lf = DESIGN.replace("\r\n", "\n"); + let adoption_boundary_drift = adoption_lf.replace( + "does not participate in the DD-078 core dependency DAG, release sequence, or definition of done", + "participates in the DD-078 release sequence", + ); + let graph = parse_graph(&plan_lf).unwrap(); + assert!( + validate_adoption_boundary(&plan_lf, &adoption_boundary_drift, &design_lf, &graph).is_err() + ); + + let core_scope_drift = plan_lf.replace( + "DD-078 is implemented when:\n", + "DD-078 is implemented when:\n\n0. Larrimon has completed Wave E;\n", + ); + assert!( + validate_adoption_boundary(&core_scope_drift, &adoption_lf, &design_lf, &graph) + .unwrap_err() + .contains("core definition of done") + ); + + let acceptance_scope_drift = design_lf.replace( + "## 25. Acceptance criteria\n", + "## 25. Acceptance criteria\n\n- [ ] Larrimon has completed Wave E.\n", + ); + assert!( + validate_adoption_boundary(&plan_lf, &adoption_lf, &acceptance_scope_drift, &graph) + .unwrap_err() + .contains("core acceptance criteria") + ); + + let migration_matrix_drift = adoption_lf.replace( + "Run old migration checks and native `ntnt db`/`.tnt` evidence on one immutable Larrimon revision across:", + "Run whichever migration examples are convenient.", + ); + assert!( + validate_adoption_boundary(&plan_lf, &migration_matrix_drift, &design_lf, &graph) + .unwrap_err() + .contains("Larrimon Slice 16M") + ); + + let (before_consumer_dod, _) = adoption_lf + .split_once("## 10. Larrimon definition of done\n") + .unwrap(); + let collapsed_consumer_dod = format!( + "{before_consumer_dod}## 10. Larrimon definition of done\n\nThe migration is declared complete.\n" + ); + assert!( + validate_adoption_boundary(&plan_lf, &collapsed_consumer_dod, &design_lf, &graph) + .unwrap_err() + .contains("Larrimon definition of done") + ); + + let completion_bypass_before_dod = plan_lf.replace( + "\n## Definition of done\n", + "\nDD-078 remains incomplete until Larrimon finishes Wave E.\n\n## Definition of done\n", + ); + assert!(validate_adoption_boundary( + &completion_bypass_before_dod, + &adoption_lf, + &design_lf, + &graph, + ) + .unwrap_err() + .contains("core implementation plan")); + + let deletion_bypass_before_16m = adoption_lf.replace( + "## 6. Adoption Slice 16M β€” production migration compatibility\n", + "DD-078 owner 8 may delete all four protected migration files before the compatibility matrix or consumer definition of done passes.\n\n## 6. Adoption Slice 16M β€” production migration compatibility\n", + ); + assert!( + validate_adoption_boundary(&plan_lf, &deletion_bypass_before_16m, &design_lf, &graph,) + .unwrap_err() + .contains("standalone Larrimon adoption plan") + ); + + let module_registration_drift = PLAN.replace( + "**Modify:** `src/verification/mod.rs` registration and report claim-scope/input-identity fields only;", + "**Modify:** report claim-scope/input-identity fields only;", + ); + assert!(validate_plan(&module_registration_drift).is_err()); + + let parent_creator_dependency_drift = PLAN + .replace( + "| 13B | core ntnt AST/import/route/effect/project facts | 2G, 3D, 13A |", + "| 13B | core ntnt AST/import/route/effect/project facts | 2G, 13A |", + ) + .replace( + "**Table dependencies:** 2G, 3D, 13A", + "**Table dependencies:** 2G, 13A", + ); + assert!(validate_plan(&parent_creator_dependency_drift).is_err()); + + let reversed_range = PLAN.replacen("6B, 8, 10A–10B", "6B, 8, 10B–10A", 1); + assert!(validate_plan(&reversed_range) + .unwrap_err() + .contains("reversed slice range 10B–10A")); + + let nested_slice_after_spike = PLAN.replace( + "## Task 7A: Frozen out-of-process provider protocol", + "### Slice 16M: synthetic spike-boundary fixture\n\n**Create:** `src/not-part-of-spike.rs`\n\n## Task 7A: Frozen out-of-process provider protocol", + ); + let nested_graph = parse_graph(&nested_slice_after_spike).unwrap(); + assert!(validate_spikes(&nested_slice_after_spike, &nested_graph).is_ok()); + + let second_create_block = PLAN.replace( + "**Gate:** focused scanner parity/root-escape tests, existing inspector/Studio tests, fmt/clippy, and immutable review.", + "**Create:** `src/verification/provider/late.rs`\n\n**Gate:** focused scanner parity/root-escape tests, existing inspector/Studio tests, fmt/clippy, and immutable review.", + ); + assert!(validate_plan(&second_create_block) + .unwrap_err() + .contains("without parent registration src/verification/provider/mod.rs")); +} diff --git a/tests/fixtures/dd078/README.md b/tests/fixtures/dd078/README.md new file mode 100644 index 00000000..ef38cf54 --- /dev/null +++ b/tests/fixtures/dd078/README.md @@ -0,0 +1,12 @@ +# DD-078 reviewed section snapshots + +These fixtures apply two review locks: + +1. Exact section snapshots preserve DD-078's highest-risk scope and deletion-safety contracts: + - project-neutral core acceptance criteria; + - project-neutral core definition of done; + - Larrimon adoption Slice 16M migration compatibility and exclusive deletion authority; + - Larrimon consumer definition of done. +2. Canonical SHA-256 fixtures lock the complete normative envelopes of the core design, core implementation plan, and standalone Larrimon adoption plan. This prevents equivalent requirements or authority exceptions from being inserted immediately outside the named sections. + +`tests/dd078_plan_tests.rs` compares section source byte-for-byte after normalizing line endings and verifies each complete document's SHA-256 over canonical LF bytes. A source edit therefore fails until the matching fixture is deliberately updated in the same review. Do not regenerate snapshots or digests merely to make a test green: inspect the source and fixture diffs and confirm that core scope remains project-neutral and consumer migration/deletion safeguards remain equivalent or stronger. diff --git a/tests/fixtures/dd078/core-acceptance-criteria.md b/tests/fixtures/dd078/core-acceptance-criteria.md new file mode 100644 index 00000000..3e6a95e7 --- /dev/null +++ b/tests/fixtures/dd078/core-acceptance-criteria.md @@ -0,0 +1,58 @@ +## 25. Acceptance criteria + +### Truth and evidence + +- [ ] Every obligation has stable identity and source location in strict mode. +- [ ] Implementation, executable, and verified coverage are separate. +- [ ] Zero-executable, unbound, unsupported, stale, blocked, and disallowed-skipped obligations fail strict mode. +- [ ] Unsupported assertions can never pass. +- [ ] JSON, JUnit, human output, and exit code derive from one evidence ledger. +- [ ] `@implements` alone cannot satisfy an obligation. + +### Runtime and security + +- [ ] Static lint/plan runs no project code or provider. +- [ ] `.intent` cannot request or exercise CLI, filesystem, network, database, process, browser, or secret authority. +- [ ] Intent may supply only bounded data to a preplanned binding; negative tests reject destinations, providers, resources, paths, secret headers, and legacy CLI/file actions. +- [ ] `pure-ntnt` authoring requires `proven` and fails planning for project-owned wrappers/providers, executable shebangs, inline workflow/package/Compose/Docker execution, unpinned actions/images, gitlinks/nested repositories, unclassified generated helpers, non-`.tnt` verification/support, SQL-only/browser harnesses, or untrusted exclusions; violations and exclusions are reported. +- [ ] Project requests are intersected with external host policy. +- [ ] Privileged policy and protected evidence contracts originate outside repository-controlled argv, use the same inherited-handle `TrustedInput` loader, reject unknown/non-canonical/duplicate envelope fields, and use separate frozen domains that sign the exact raw-payload SHA-256 before parsing; immutable base repository/commit/tree and protected inventory remain bound. +- [ ] Effective policy identity is always digest-bound, and hardlink/symlink/writable-ancestor/TOCTOU/malformed-policy attacks fail closed. +- [ ] Plan, execution, and report consume one immutable content-addressed snapshot; launch identity and source drift are checked. +- [ ] Paths are project-confined and symlink-safe. +- [ ] Exact argv execution has no shell expansion. +- [ ] Handles are opaque, generation-bound, unforgeable, and invalid after scope. +- [ ] Semantic `EffectKind` never authorizes an operation; every effectful sink validates an exact run/case/generation/resource/operation `VerificationGrant`. +- [ ] Constructors, provider output, serialization, globals, and concurrent runs cannot widen or cross resource grants. +- [ ] Clean environment, recursive redaction, output bounds, deadlines, cancellation, and cleanup are adversarially tested. +- [ ] Provider crash/hang/malformed/late/duplicate messages fail closed and clean resources. +- [ ] Verification authority cannot be bypassed through direct or transitive imports, aliases, module initializers, or ordinary effectful stdlib calls. +- [ ] Untrusted executable/browser/provider profiles use enforceable OS containment and brokered egress; trusted-uncontained execution is visibly prohibited from protected PR lanes. +- [ ] CPU, memory, PIDs/threads, descriptors, disk, sockets, and descendants are bounded below project code. +- [ ] Stale cleanup uses authenticated exact host-ledger records rather than project labels or prefix scans. +- [ ] Strict resources prove a durable `reserve β†’ create β†’ finalize β†’ expose` broker/backend protocol and crash recovery at every boundary; unsupported backends are non-verifying and blocked from protected profiles. +- [ ] Strict/protected Redis uses the brokered disposable-instance lifecycle and proves zero residual keys/credentials after completed cleanup/reconciliation; pending cleanup cannot pass, and attached ACL mode is non-verifying. +- [ ] Imported strict evidence uses a supervisor invocation record or canonical signed, expiring, replay-resistant envelope. +- [ ] Project-wide execution is strict by default; diagnostic mode is explicitly non-verifying and cannot satisfy obligations. +- [ ] Uncatchable termination limitations are explicit; supervisor-crash and startup orphan-reaper paths are tested against authenticated ledger records. + +### Application verification + +- [ ] Structured function arguments/results and first-class assertions replace local assertion helpers. +- [ ] Stateful HTTP supports headers, forms, cookies, redirects, captures, multiple clients, and attach mode. +- [ ] PostgreSQL supports isolated committed fixtures, roles/RLS, migration evidence, direct observations, and cleanup. +- [ ] Managed processes support readiness, expected failure, logs, restart, exit, and process-tree cleanup. +- [ ] Local HTTP/SMTP/webhook/TCP/UDP fixtures support strict scripted behavior. +- [ ] Eventual assertions use one bounded deadline and report attempts/final observation. +- [ ] Named actors/barriers reproduce application-defined claim/scheduler/projection races without sleeps in project-neutral fixture applications. +- [ ] Browser cases cover authenticated, HTMX, no-JavaScript, focus/history, and reconciliation behavior from `.tnt`. +- [ ] Project/provider facts replace the audited Python provenance and architecture checks without granting arbitrary shell. + +### Adoption portability + +- [ ] A project-neutral fixture repository exercises the complete adoption protocol: immutable inventory, exact-once classification, protected contract/snapshot binding, old/new parity, mutation/fault witnesses, and evidence-backed deletion eligibility. +- [ ] The adoption protocol produces reusable machine-readable inputs and reports without project names or paths in public APIs, schemas, defaults, policies, fixture semantics, or privileged modes. +- [ ] A consumer adoption plan can bind its own inventory and migration waves to landed capabilities without joining or changing the DD-078 core DAG, releases, or completion criteria. +- [ ] The Larrimon reference-adoption checklist remains separately reviewable in [`plans/dd-078-larrimon-adoption.md`](../plans/dd-078-larrimon-adoption.md) and is not evidence that the project-neutral runtime itself passed. + +--- diff --git a/tests/fixtures/dd078/core-definition-of-done.md b/tests/fixtures/dd078/core-definition-of-done.md new file mode 100644 index 00000000..025bc8d8 --- /dev/null +++ b/tests/fixtures/dd078/core-definition-of-done.md @@ -0,0 +1,16 @@ +## Definition of done + +DD-078 is implemented when: + +1. one evidence ledger truthfully represents every obligation and execution result; +2. project-wide static plan and strict execution are stable public CLI contracts bound to one immutable input snapshot; +3. protected CI enforces an operator-owned obligation/profile/evidence contract and pure-authoring disposition rather than trusting repository scope; +4. native `.tnt` verification covers typed unit, HTTP, database, process, fixture, eventual, concurrency, browser, and project-policy cases; +5. capabilities are externally granted, root-confined, bounded, redacted, and cleaned up through authenticated host-ledger ownership; +6. external providers are versioned, pinned, explicitly sandboxed or trusted-uncontained, and fail closed; protected PR lanes admit only allowed containment classes; +7. project-neutral fixture applications exercise every public mechanism without importing consumer code, names, data models, or policies; +8. the generalized adoption protocol binds an arbitrary immutable fixture repository, exact-once inventory, protected contract, and execution snapshot to one canonical identity; +9. old/new parity plus deliberate mutation/fault witnesses produce machine-readable deletion-eligibility evidence without automatically deleting consumer files; +10. fast, full, live-network, and environment-backed profiles state their evidence, claim level, containment, and hermeticity honestly; +11. full ntnt regression, docs, hosted-platform, and independent security/architecture reviews pass against immutable commits; +12. at least two project-neutral adoption fixtures with different identities and inventories complete the protocol without changing ntnt runtime APIs. Consumer-specific adoption completion remains outside DD-078. diff --git a/tests/fixtures/dd078/core-design.sha256 b/tests/fixtures/dd078/core-design.sha256 new file mode 100644 index 00000000..bc68d691 --- /dev/null +++ b/tests/fixtures/dd078/core-design.sha256 @@ -0,0 +1 @@ +fed29b1da15b5a5536a7a81f4f939e5390417510d1b8a5cd56bfacd67ee2965e diff --git a/tests/fixtures/dd078/core-plan.sha256 b/tests/fixtures/dd078/core-plan.sha256 new file mode 100644 index 00000000..99f81353 --- /dev/null +++ b/tests/fixtures/dd078/core-plan.sha256 @@ -0,0 +1 @@ +4b084fed51f3d7995174c470dd8f8e351ceac4259e9738492ddeddd00889af0f diff --git a/tests/fixtures/dd078/larrimon-adoption.sha256 b/tests/fixtures/dd078/larrimon-adoption.sha256 new file mode 100644 index 00000000..39eab247 --- /dev/null +++ b/tests/fixtures/dd078/larrimon-adoption.sha256 @@ -0,0 +1 @@ +0968597f6d722acacef564d495df55be45750d32f4453c3cdd9ecb5eea9dc63d diff --git a/tests/fixtures/dd078/larrimon-definition-of-done.md b/tests/fixtures/dd078/larrimon-definition-of-done.md new file mode 100644 index 00000000..956adba0 --- /dev/null +++ b/tests/fixtures/dd078/larrimon-definition-of-done.md @@ -0,0 +1,26 @@ +## 10. Larrimon definition of done + +This consumer adoption is complete when: + +- all 27 audited scenarios and 38 assertion/outcome lines are verified, corrected, superseded, or explicitly documentation-only; none vanish silently; +- every shell, Python, JavaScript test, and SQL-only application-test invariant has a destination and same-revision parity evidence; +- representative semantic mutations/faults prove detection before each old file is deleted; +- `tests/intent.sh` and suite wrappers are removed; +- project-owned `.sh` and `.py` support/orchestration files are zero, except operator-locked externally owned non-support artifacts; +- project-local browser/reconciliation test `.js`/`.mjs` and SQL-only application-test files are zero; +- typed project-state and `ntnt project env` replace dev/staging lifecycle programs with allocation, failure, cleanup, and mutation parity; +- the baseline inventory, protected contract, candidate base, execution snapshot, and evidence bind the same exact Larrimon commit and canonical digest; +- fast and full profiles run through ntnt with current verified coverage at the configured threshold; +- specialist external resources remain pinned, capability-scoped, and visible in reports; +- the complete old-to-new invariant ledger and mutation/fault witnesses remain in project history. + +Expected end-state commands: + +```bash +ntnt intent lint . +ntnt intent plan . --profile full --json +ntnt intent check . --profile fast +ntnt intent check . --profile full --report-json verification-report.json +``` + +Environment-backed protected profiles remain operator-selected outside the checkout. diff --git a/tests/fixtures/dd078/larrimon-slice-16m.md b/tests/fixtures/dd078/larrimon-slice-16m.md new file mode 100644 index 00000000..6f948bee --- /dev/null +++ b/tests/fixtures/dd078/larrimon-slice-16m.md @@ -0,0 +1,29 @@ +## 6. Adoption Slice 16M β€” production migration compatibility + +**Consumer dependency only:** landed DD-077 PR 1C, landed DD-078 owner 8, and the Larrimon database-conversion wave. + +This slice is intentionally absent from the DD-078 core dependency table and releases. + +Run old migration checks and native `ntnt db`/`.tnt` evidence on one immutable Larrimon revision across: + +- fresh install and idempotent rerun; +- every supported legacy ledger and application/schema upgrade pair; +- checksum backfill and pre-package unverifiable rows; +- unknown-ledger rejection before mutation; +- malformed or missing manifests; +- missing or mutated applied files; +- database checksum enforcement; +- concurrent migrators and advisory locks; +- per-migration rollback and dirty recovery; +- cancellation and role configuration. + +Inject failures/mutations for every family and retain paired reports. + +**Exclusive deletion authority:** Only this consumer slice may authorize removal of: + +- `scripts/migrate.sh`; +- `scripts/migrate-prod.sh`; +- `scripts/check-migration-checksums.py`; +- `tests/migrate_prod_integration.sh`. + +DD-078 owner 8 may provide observations but cannot authorize these deletions. A later operational matrix may expand supported cases, but the currently supported production matrix cannot be deferred past deletion.