Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions CLAUDE.md
Original file line number Diff line number Diff line change
Expand Up @@ -124,8 +124,9 @@ Before finishing any package, run `dev.py test`, `dev.py lint` and `pytest`. If
- disable or weaken a CI job or gitleaks;
- commit directly to `main`.
- **Terraform and AWS.**
- Never run `terraform apply` or `terraform destroy`, and never use AWS credentials, unless the current prompt (P9 onward) says so and the user confirms.
- No provider blocks anywhere before P9. Resources only under `fixtures/`, as test data: `terraform init -backend=false` and `terraform validate` only; never plan, apply or use credentials there.
- AWS stays fully offline (C-71): no deployment, no AWS account, no calibration against live AWS. P9 and milestone M6 are removed; DAIL and the oracle are configuration-level only.
- Never run `terraform apply`, `terraform destroy` or `terraform plan`, and never use AWS credentials.
- No provider blocks anywhere. Resources only under `fixtures/`, as test data: `terraform init -backend=false` and `terraform validate` only.
- Terraform and AWS provider pins must match the TerraPreserve repository.
- **Secrets.**
- Never commit or print secrets. Secrets are referenced only as `env:NAME`.
Expand Down
7 changes: 4 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -137,13 +137,14 @@ cloudspartanx/
│ └── application/ # configuration + health (P0-close); scope policy (P4);
│ # EvaluationOrchestrator (P6b)
├── evidence/ # P2: evidence service, correlation context, structured logs, replay mode
├── llm/ # P7: adapter/, prompts/, schemas/, validation/
├── llm/ # P7a/P7b: adapter/ (fake and local Ollama), prompts/, schemas/,
│ # validation/; free open-weight models only (C-71)
├── experiments/ # P8: trial harness, conditions, metrics
├── fixtures/ # the 15 Doc 12 §7 canonical fixtures (Doc 04 §15 layout)
│ ├── canonical_regression/{baseline,patch_safe,patch_regression}/
│ ├── identity/ dependency/ impact/ verification/ adversarial/
├── infrastructure/terraform/ # P9: modules/, environments/{dev,test,experiment,staging}/,
│ # policies/, versions.tf (Doc 14 §18)
├── infrastructure/terraform/ # version pins only (versions.tf; validated by CI); no deployment:
│ # P9 and AWS deployment are removed (C-71)
├── requirements/ # dev.lock (hash-locked dev toolchain, generated by pip-compile)
├── tests/
│ ├── unit/ integration/ contract/ adversarial/ e2e/
Expand Down
1 change: 1 addition & 0 deletions config/base/llm.toml
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,5 @@
# generation_enabled is safety-critical (Doc 14 §37-38): it may be enabled only in a
# reviewed configuration file, never by an environment variable or runtime override.
generation_enabled = false
# provider: "fake" (CI and the default tests) or "ollama" (a local server only; C-71, C-182).
provider = "fake"
4 changes: 2 additions & 2 deletions core/application/config.py
Original file line number Diff line number Diff line change
Expand Up @@ -166,8 +166,8 @@ def dotted(self) -> str:
safety_critical=False,
conservative_value=None,
runtime_overridable=False,
allowed=("fake",),
spec_ref="Doc 01 FR-LLM-006; Doc 14 §12",
allowed=("fake", "ollama"),
spec_ref="Doc 01 FR-LLM-006; Doc 14 §12; C-71, C-182 (local Ollama only)",
),
ConfigKey(
area="llm",
Expand Down
8 changes: 7 additions & 1 deletion docs/DECISIONS_REGISTER.md
Original file line number Diff line number Diff line change
Expand Up @@ -192,4 +192,10 @@ This register records every conflict found between the 15 `CloudSpartanX_*` spec
| C-178 | P6d: registry v1.1 closes C-150; INV-SEC-001 and INV-SEC-002 version 2 | **Authors' decision (11 Nov 2026, C-150 amended): close the gap now, in registry v1.1, instead of stating it as a limitation.** `docs/specs/INVARIANT_REGISTRY_v1.1.md` (a new file, C-85; `INVARIANT_REGISTRY_v1.md` is unchanged) replaces the §3.3 clause by: `possible4(g) := exists indeterminate r in In(g) that could permit TCP/p (its protocol or ports unresolved, or they permit p) and (its IPv4 sources are unresolved or include a prefix list, or its resolved IPv4 sources, together with the union of v4(r') over r' in D(g), cover 0.0.0.0/0). possible6(g) is the same for IPv6 sources and ::/0.` A rule whose port is unresolved but whose source is the whole internet may open the port, and uncertainty is never a pass. INV-SEC-001 and INV-SEC-002 become version 2; their results change only for such rules. INV-SEC-003 and INV-FUNC-001 stay version 1. **C-155 is out of scope:** its conservative readings stay DAIL implementation choices for now and are not written into v1.1; the differences between DAIL and the oracle on those cases will be measured in P8. Evidence for SEC v1 does not satisfy v2 (C-62: equal `invariant_version` required). | Decided (authors, 11 Nov 2026) |
| C-179 | P6d: registry v1.1 §2.9 clarification (from the TerraPreserve oracle work, Open D5-D) | **Authors' decision (10 Nov 2026): wording only, no result changes, no `invariant_version` change.** Registry v1.1 §2.9 adds: "In the footprint comparison, an argument that neither configuration writes compares as absent on both sides and is not changed. The predicates still treat such a value as §2.2 says." and "The parent counterpart's inline-rule form (§3.5, §6.6) is compared through what it decides: whether the group is RETAINED-INLINE in that direction (§2.6). A baseline has no parent, so this is false for every group of a baseline." DAIL's impact analysis is resource-level (C-140) and is not changed by it. | Decided (authors, 10 Nov 2026) |
| C-180 | P6d: how DAIL stores registry 1.1, and the verifier version | The registry file says `invariant_registry_version = 1.1`, but the field is an integer ≥ 1 in `TrustedState`, `PromotionPolicy` and the schema (C-32). **User's decision (11 Nov 2026): keep the integer; DAIL stores registry v1.1 as `2`** (1 = the `registry-v1.0` tag, 2 = `registry-v1.1`; `core.domain.registry_v1_1.REGISTRY_VERSION_V1_1`). Definitions and evidence cite the tag `registry-v1.1`. **User's decision (11 Nov 2026): the verifier version of `dail.verify.public_ingress` stays `"1"`**: registry v1.1 changes exactly what the work package lists and §10 is not among them; v1 and v2 evidence are already told apart by `invariant_version` (C-62). Question for the reviewer: should a later registry bump §10 when a predicate changes? | Decided (user, 11 Nov 2026) |
| C-181 | P6d: implementation readings for registry v1.1 | (1) `core/domain/registry_v1_1.py` is a new module beside `registry_v1.py`, which keeps building the v1.0 definitions unchanged (they are what TerraPreserve v1.0's labels and the existing fixtures cite, and its tests read the v1.0 file). v1.1 takes INV-SEC-001/002 from v1.0, sets `version = 2`, cites `registry-v1.1` in `predicate.registry` and the description; INV-SEC-003 and INV-FUNC-001 are the v1.0 definitions object for object (same `definition_hash`, so a stored definition of the same id and version is not contradicted). (2) The public-ingress verifier reads `predicate.registry` of the definition: `registry-v1.0` evaluates the v1.0 clause, `registry-v1.1` the v1.1 clause, any other tag raises (VERIFIER_ERROR, fail closed). The direct function's default is v1.1 (the conservative one); baseline resource items use it. (3) C-146 (2) is kept: a rule whose direction is unresolved is `possible` for a family when it has any known source of that family (wider than v1.1). (4) The citation `registry-v1.0` that the verification engine and the impact work items wrote for every invariant now comes from the definition's `predicate.registry`. (5) The test pipeline (`tests/promotion_pipeline.py`) takes the definitions and the registry version as keywords; the default stays v1.0, so no passed test changes its inputs. | Proposed (P6d) |
| C-181 | P6d: implementation readings for registry v1.1 | (1) `core/domain/registry_v1_1.py` is a new module beside `registry_v1.py`, which keeps building the v1.0 definitions unchanged (they are what TerraPreserve v1.0's labels and the existing fixtures cite, and its tests read the v1.0 file). v1.1 takes INV-SEC-001/002 from v1.0, sets `version = 2`, cites `registry-v1.1` in `predicate.registry` and the description; INV-SEC-003 and INV-FUNC-001 are the v1.0 definitions object for object (same `definition_hash`, so a stored definition of the same id and version is not contradicted). (2) The public-ingress verifier reads `predicate.registry` of the definition: `registry-v1.0` evaluates the v1.0 clause, `registry-v1.1` the v1.1 clause, any other tag raises (VERIFIER_ERROR, fail closed). The direct function's default is v1.1 (the conservative one); baseline resource items use it. (3) C-146 (2) is kept: a rule whose direction is unresolved is `possible` for a family when it has any known source of that family (wider than v1.1). (4) The citation `registry-v1.0` that the verification engine and the impact work items wrote for every invariant now comes from the definition's `predicate.registry`. (5) The test pipeline (`tests/promotion_pipeline.py`) takes the definitions and the registry version as keywords; the default stays v1.0, so no passed test changes its inputs. **Authors' decision (11 Nov 2026): accepted as built after external review.** | Decided (authors, 11 Nov 2026) |
| C-182 | P7a: the only real LLM provider, and experiment models (C-71) | **Advisor's decision (11 Nov 2026; C-71):** the only real provider in this repository is a local Ollama server. Experiment models (P10) are free open-weight models pinned by exact digest, quantization, temperature and seed, each with its licence checked. No paid API, no API key, no account. CI and the default test run use the fake provider only. | Decided (advisor, 11 Nov 2026) |
| C-183 | P7a-1: standard library only in `llm/` | No LiteLLM, no Instructor, no Pydantic: the Ollama HTTP API is called with `urllib` (`llm/adapter/ollama.py`) and the response schema is checked by DAIL's own strict parser (`llm/validation/parser.py`). The project plan named LiteLLM and Instructor for paid providers; C-71 removed paid providers, so they add nothing. CLAUDE.md still says Pydantic is allowed in `llm/` from P7; nothing uses it. | Proposed (P7a) |
| C-184 | P7a-2: the patch format of an LLM response | The `patch` field of an `LLMRepairResponse` carries the format the P6c fixed-patch loop already accepts for `CandidateSource.FIXED_PATCH`: a `Patch` with `format = PatchFormat.TERRAFORM_HCL` and non-empty `content` (Doc 05 §9; `core/domain/enums.py` `PatchFormat`, `core/domain/patch.py` `Patch.create`, checked by `EvaluationRequest` in `core/application/orchestrator.py`). No second format. The parser checks only that a PATCH carries a non-empty string; what the HCL text means against the parent configuration (a whole-file replacement or a fragment) is not defined by P6c either (C-174: the patch text is not applied) and is P7b's to decide. | Proposed (P7a) |
| C-185 | P7a-3: Ollama structured output | The request sets Ollama's documented `format` parameter to the JSON schema of `LLMRepairResponse` (structured outputs), with `stream = false`; the source page and the installed Ollama version are recorded in `llm/adapter/ollama.py` and in the P7a report. The provider's JSON mode is never trusted as validation: every reply goes through the strict parser. | Proposed (P7a) |
| C-186 | P7a-4: the wiring model | For the local wiring check only, never for results: one small open-weight coder model that runs on CPU, licence Apache-2.0 or MIT, checked on its Ollama library page and with `ollama show --license` on the day. Name, tag, digest, quantization and licence are recorded in `docs/PHASE_GATES.md` (P7a). | Proposed (P7a) |
| C-187 | P7a: readings of Doc 10 made while building the LLM channel | (1) **Status to failure class.** A parsed NO_SOLUTION or UNCERTAIN is the model's inability signal (§10) and has failure class NO_SOLUTION; a model that answers INVALID is INVALID_OUTPUT. (2) **Ollama errors (§24).** Connection refused or reset, HTTP 5xx and an `error` object with status 200 are TRANSIENT_ERROR; a socket timeout is TIMEOUT; 429 is RATE_LIMIT; 400 and 404 (bad request, missing model) are UNSUPPORTED, not retried: the configured request cannot be served; a 200 reply without `done: true` and a string `message.content` is INVALID_OUTPUT. (3) **Boundaries (§22).** A PATCH must name at least one changed address (otherwise the boundaries are ambiguous); each must be a resource address; a type outside the supported model (registry §1.3) is UNSUPPORTED; an address outside `allowed_change_scope` is POLICY_VIOLATION. The scope is the neighbourhood, so a repair that adds a resource at a new address is refused in P7a; P7b decides whether to widen it. The patch text is not parsed as HCL in P7a (P7b). (4) **Neighbourhood (§6, §7).** The addresses an impact report names (its changed resources, the changed resources of each affected invariant and every node of their dependency paths) plus an explicit focus, restricted to the trusted state. (5) **Budget (§18, §19).** Estimate `ceil(characters / 4)` of the rendered prompt; items are dropped one at a time in the order 7, 6, 5, 4, 3, the last item of a priority first; priorities 1 and 2 are never dropped; the allowed types, the allowed scope and the patch format are the generation boundary (§8) and are always sent; what is dropped is recorded. CONTEXT_INSUFFICIENT is not retried even when the policy lists it, because the deterministic context would not change (`prompt_adjustment_policy` is `none`). (6) **Provider seam (ADR-006).** `generate(ProviderCall) -> ProviderReply`; the generator builds the `LLMResponse` record. (7) **No network (C-71).** The fake path is tested with every socket call blocked; only `llm/adapter/ollama.py` imports a network module; the Ollama unit tests talk to a stdlib fake server on 127.0.0.1 only; the real-server test is opt-in (`DAIL_OLLAMA_TEST=1`). (8) **Prompt versions (§9).** `PROMPT_HASHES` pins the template hash of each prompt version and `render` refuses templates that no longer match it. (9) `llm/` is added to mypy's `files`. The configuration key `llm.api_key_ref` stays in the schema, unused (C-71: no keys); removing it is a suggestion for a later package. | Proposed (P7a) |
55 changes: 53 additions & 2 deletions docs/PHASE_GATES.md
Original file line number Diff line number Diff line change
Expand Up @@ -249,7 +249,28 @@ Carry-forward: a second attempt on the same terminal candidate returns the first
deciding (MEDIUM; reject or document in P7/P8); C-173 Proposed until the authors confirm; C-169 Open;
C-170 to C-176 Proposed.

## P6d — Every move is a change, and invariant registry v1.1 (pending external review)
## P6d — Every move is a change, and invariant registry v1.1 — passed with limits (external review, 11 Nov 2026; merged as 1c3d72b, tagged registry-v1.1)

```text
Verdict (external review, 11 Nov 2026, PR #27 at 8c5ca0a): APPROVED WITH LIMITS. Merged as 1c3d72b,
tagged registry-v1.1. Limits carried forward (not blocking), from the verdict:
1. The pipeline still defaults to registry v1.0. The end-to-end tests run v1.0 definitions; v1.1 is
exercised in tests/unit/test_registry_v1_1.py. P8 must make v1.1 the default for every
experiment condition, so that DAIL is evaluated under the decided rules.
2. Version encoding (C-180). Registry 1.1 is stored as the integer 2, and the verifier version stays
"1" while its §3.3 behaviour depends on the definition's registry. The mapping "stored 2 =
registry 1.1" must be stated wherever evidence is reported (P8 reports, the paper).
3. C-181 (implementation readings) is Proposed; the authors must decide it. [Decided by the
authors on 11 Nov 2026, recorded in P7a.]
4. Equivalence evidence gap. In tp-v1-F3-0278 the oracle archive does not record the sources of 2
indeterminate rules; the conclusion relies on reading that scenario's .tf. Record in
TerraPreserve's v1.1 notes: the oracle evidence should record rule sources.
5. Stale mentions of P9 remain in CLAUDE.md and README.md; update them in P7a. [Done in P7a.]
6. C-155 readings stay DAIL implementation choices outside the registry; DAIL-oracle differences
on those cases are to be measured in P8.
```

The P6d author's input to the review, as written before the verdict:

```text
P6d mini-gate: NOT DECIDED. Status written by the P6d author as an input to the external review.
Expand Down Expand Up @@ -282,7 +303,37 @@ v1.1 by tests.unit.test_registry_v1_1. Carry-forward: C-181 Proposed; the user t
after the verdict and the merge.
```

## P7a–P10 — NOT STARTED
## P7a — The LLM channel (pending external review)

```text
P7a mini-gate: NOT DECIDED. Status written by the P7a author as an input to the external review.
What exists (llm/, standard library only, C-183; ADR-006 Proposed):
provider seam and failure classes (llm/adapter/provider.py, Doc 10 §24, §30); FakeProvider
(scripted, no network) and OllamaProvider (urllib, loopback only, digest pin; C-182, C-185);
context builder (§6-§8: impact neighbourhood only, secrets redacted before the prompt, unknown
values marked); budget (§18-§19: deterministic reduction 7..3, omissions recorded,
CONTEXT_INSUFFICIENT without a provider call); prompts dail-repair-prompt-1 (system and task
layers, infrastructure as data between <<<DAIL_DATA and DAIL_DATA>>>, template hash pinned);
strict parser dail-llm-parser-1 (§11, §22, §25; no tolerant parser); retries (§23, the four
classes, bounded); request and response records and observability (§16-§17, §20-§21, §32-§34);
the emergency switch llm.generation_enabled (off: no provider call); config llm.provider accepts
"ollama". Tests: tests.unit.test_llm_parser, test_llm_context, test_llm_generate, test_llm_ollama.
Wiring check (11 Nov 2026, the author's machine: Intel Core Ultra 5 125H, 15.7 GB RAM, CPU only):
Ollama 0.40.16 for Windows (official installer, signed by Ollama Inc.); model qwen2.5-coder:1.5b,
digest d7372fd828518a4d38b1eb196c673c31a85f2ed302b3d1e406c4c2d1b64a0668, Q4_K_M, 1.5B,
986 MB; licence Apache-2.0 (ollama.com/library/qwen2.5-coder:1.5b, licence blob 832dd9e00a68,
and `ollama show --license`). One run of the canonical objective (Doc 10 §36) with the
canonical regression context: status PATCH, parse errors none, latency 31.7 s, tokens in 2381 /
out 184, attempts 1. The patch was not turned into a candidate (P7b) and its quality was not
judged; this model is for wiring only, never for results (C-186).
Limits: patch validation beyond the parser (Doc 10 §13), HCL parsing of the patch and candidate
construction are P7b; a repair that adds a resource at a new address is refused by the scope check
(C-187 (3)); the token estimate is characters/4, not a tokenizer; the Ollama unit tests use a
loopback fake server, not the real one; the wiring check ran once on one machine.
Carry-forward: C-183 to C-187 Proposed; ADR-006 Proposed.
```

## P7b–P10 — NOT STARTED

P9 (AWS integration) and milestone M6 (AWS Demonstration) are removed (C-71, Decided by the advisor,
11 Nov 2026): AWS stays fully offline, with no deployment, no AWS account and no calibration against
Expand Down
Loading