From afb4526eb64fefba64dca742f01bbdd8e1ef903c Mon Sep 17 00:00:00 2001 From: Dimitri Kennedy <344842+roodboi@users.noreply.github.com> Date: Fri, 6 Nov 2026 21:08:03 -0500 Subject: [PATCH 1/3] fix(native): reconcile edited graphs that have a dependency cache An env-only Compose edit stranded a retained run whose graph has a `hack.dependencies.*` cache: plan reconciliation skipped every cache graph, so the edit fell through to the hostname-change proof and `up`/`restart` refused with a misleading `graph_hostname_change`. - Cache graphs are now eligible for reconciliation. A cache whose freshly resolved identity equals the recorded one is kept with its provenance; a changed identity selects that identity's shared cache exactly as a fresh admission does (adopt by labels or create, then the initializer runs) from a freshly published source snapshot, and only this run's reference to the old shared cache is released. Run-owned data is never reselected as a cache: declaring one refuses with `graph_plan_reconcile` and names the service and the `hack.dependencies.cache-volume` field. - A cache identity now binds the initializer's own reviewed definition and its cache volume declaration instead of the whole Compose digest, so an edit to another service keeps the cache, as Compose keeps a named volume. Receipts recorded under the earlier whole-document identity keep their cache while the review still resolves to it, and move to the new identity on the first edit. - Graphs that reconciliation still does not select (live source, a carried cache scope, a pending source-device rebind or initializer cache release) refuse a non-hostname edit with `graph_plan_change_unsupported` instead of `graph_hostname_change`; a hostname change mixed with other edits names the routed service. Errors carry a value-free `plan_change` diagnostic and the CLI prints closed guidance: revert, or `hack down --remove-data` then `up`. - Adds the native-cache-reconcile TLA+ model (54 states) with negative controls for whole-document identities, stale cache reattachment and run data reused as a cache. Refs HACK-1937 Co-Authored-By: Claude Opus 5.5 --- docs/guides/native-candidate.md | 28 +- docs/reference/v5-model-coverage.md | 3 +- packages/runtime-core/README.md | 19 +- packages/runtime-core/src/error.rs | 34 ++ .../src/provider/graph/cache_provenance.rs | 9 + .../runtime-core/src/provider/graph/config.rs | 55 ++- .../src/provider/graph/dependency_cache.rs | 119 ++++- .../src/provider/graph/foreground.rs | 6 +- .../src/provider/graph/hostname_change.rs | 82 +++- .../src/provider/graph/plan_reconcile.rs | 429 ++++++++++++++++-- .../src/provider/graph/restore.rs | 17 +- scripts/lib/tla-runtime-models.ts | 22 + src/backends/native-plan-change.ts | 70 +++ src/backends/native-project-restore.ts | 11 +- src/backends/native-project-retained.ts | 34 +- src/backends/native-runtime-client.ts | 13 +- tests/models/tla/README.md | 37 +- .../native-cache-reconcile/CacheReconcile.tla | 103 +++++ .../native-cache-reconcile/data-as-cache.cfg | 4 + .../tla/native-cache-reconcile/negative.cfg | 4 + .../tla/native-cache-reconcile/positive.cfg | 4 + .../tla/native-cache-reconcile/stale.cfg | 4 + tests/native-plan-change.test.ts | 39 ++ tests/native-project-restore.test.ts | 52 +++ tests/native-project-retained-images.test.ts | 40 ++ tests/native-runtime-client.test.ts | 31 ++ 26 files changed, 1167 insertions(+), 102 deletions(-) create mode 100644 src/backends/native-plan-change.ts create mode 100644 tests/models/tla/native-cache-reconcile/CacheReconcile.tla create mode 100644 tests/models/tla/native-cache-reconcile/data-as-cache.cfg create mode 100644 tests/models/tla/native-cache-reconcile/negative.cfg create mode 100644 tests/models/tla/native-cache-reconcile/positive.cfg create mode 100644 tests/models/tla/native-cache-reconcile/stale.cfg create mode 100644 tests/native-plan-change.test.ts diff --git a/docs/guides/native-candidate.md b/docs/guides/native-candidate.md index 6d3263668..a0a7230d6 100644 --- a/docs/guides/native-candidate.md +++ b/docs/guides/native-candidate.md @@ -713,10 +713,30 @@ is reattached under its recorded name after the same label and identity checks; newly declared volume is created fresh; a retained volume the new file no longer declares stays owned and unmounted until `hack down --remove-data` (Compose also keeps project volumes). Retained data is only ever reattached to the run and -namespace that created it. Graphs with dependency caches, live source or a pending -source-device rebind keep the narrower rules below. `hack restart` of a stopped -graph refuses and points to `hack up`. -For a shared-source graph admitted with a retained compatibility contract, ordinary +namespace that created it. + +Graphs with `hack.dependencies.*` caches reconcile the same way. A cache's identity +covers only its own inputs: the initializer's service definition and resolved +command, entrypoint, environment and user, the cache declaration, its image, the +declared lockfile and runtime-file contents, and the cache volume layout. An edit +to another service, such as an environment value on the app, keeps the cache. An +edit to one of those inputs, including a lockfile, selects the cache for the new +identity as a fresh `up` would, so the initializer installs into it; the old cache +is shared and is only released by this run. Each such `up` publishes the current +source snapshot. A retained named volume is never reused as a dependency cache: +declaring one refuses and names the service and the `hack.dependencies.cache-volume` +field. Caches recorded by earlier builds, whose identity also covered the whole +Compose file, are kept while that file is unchanged and replaced once on the first +edit. Live source, a cache scope carried across a source-device rebind or a pending +initializer cache release keep the narrower rules below: a Compose edit other than +a routed hostname change refuses there with `graph_plan_change_unsupported`, and a +hostname change mixed with other edits refuses with `graph_hostname_change` and the +service name. Every refusal says to revert the edit, or to run +`hack down --remove-data` and then `hack up`. `hack restart` of a stopped graph +refuses and points to `hack up`. +For a shared-source graph that reconciliation does not select (live source, a +carried cache scope, a pending source-device rebind or initializer cache release) +and that was admitted with a retained compatibility contract, ordinary source-content edits may change the reviewed plan ID: restart checks the stable execution, exclusion, mount and dependency-cache inputs before cleanup and again under the provider lease. The original installer publication and graph ownership diff --git a/docs/reference/v5-model-coverage.md b/docs/reference/v5-model-coverage.md index 2e4438c36..386fec859 100644 --- a/docs/reference/v5-model-coverage.md +++ b/docs/reference/v5-model-coverage.md @@ -40,7 +40,7 @@ must be attached to the eventual exact integration revision. | Foreground Compose startup failing after resources started; unconfirmed cleanup; unauthenticated final inspection | native-startup-owner | `recordFailedStartupOwner` in [native-project-start](../../src/backends/native-project-start.ts) publishes the authenticated failed run with a finalization lifetime; [start regressions](../../tests/native-project-start.test.ts) cover recording, an unauthenticated receipt and a retained mapping | A refused final inspection still leaves only the runtime journal; crash between finalization registration and mapping publication; physical guest acceptance. | | Canceled/expired startup; reader cancellation versus EOF; producer/group uncertainty | pre-ready-retirement, authority-lifetime, native-file-material | Native graph finalizer/onSettled, exact Removed, hard-signal freshness, host stop/close; local pre-Ready retained/removed regressions, including separate live/foreign/hard-canceled fresh-teardown-admission assertions (HACK-1801) | Physical guest acceptance; current root aggregate; explicit executable unknown host-close control; async proof-to-stop and partial binding-retirement crash windows; post-stop source/session replacement or hard cancellation before Retire (Retire does not recheck these inputs; Safe has no post-stop interference predicate). | | Crash between reserve, publish, sync and release; stale recovery | native-frontend-recovery, publication, publication-journal, native-storage-witness | Durable intent/enrolled/released records, fresh lease and expected binding; recovery and sync-failure tests | Fsync guarantees, process-kill windows, real restarted provider observations. No missing-path authority. | -| Data lifetime independent of compute; replaced/aliased metadata; retained-data handoff across Compose plan changes | native-persistent-enrollment, native-storage-witness, native-file-material, native-plan-reconcile | Existing-only enrollment, exact birth/witness and reference fencing; copied-label/replacement tests; `provider/graph/plan_reconcile.rs` projection tests | Real SQL/content retention, external writer assumptions, allocated-byte evidence. | +| Data lifetime independent of compute; replaced/aliased metadata; retained-data handoff across Compose plan changes, including dependency caches | native-persistent-enrollment, native-storage-witness, native-file-material, native-plan-reconcile, native-cache-reconcile | Existing-only enrollment, exact birth/witness and reference fencing; copied-label/replacement tests; `provider/graph/plan_reconcile.rs` projection and cache-selection tests | Real SQL/content retention, external writer assumptions, allocated-byte evidence. | | Settled retained Compose route-attempt retirement; pinned references; interrupted deletion | **Coverage gap:** filesystem journal compaction is not modeled; native-route-stop covers a different stop protocol | Instance mutation lock and exact surviving claim witnesses in [journal compaction](../../src/lib/native-compose-route-claims.ts); [claim regressions](../../tests/native-compose-route-claims.test.ts) and [retained lifecycle integration](../../tests/native-compose-adoption-routing-generation.test.ts) | 24 successful operations keep two attempt directories and constant Linux descriptors; four integrated lifecycle operations check directory counts. Injected unlink failures cover same-store and fresh-store cleanup retries. Assumes cooperative same-user writers, the caller's mutation lock and working filesystem synchronization. No process-kill/power-loss durability proof or bound on unresolved/over-budget histories. | | Graph cleanup container stop batch: bounded in-flight stops, shared worker queue, connect-stage retry, batch-wide unreachable state, deadline expiry, worker panic | **Coverage gap:** no maintained model covers scheduling inside the stop batch; native-route-stop covers a different stop protocol | `dispatch` and `attempt` in [the stop batch](../../packages/runtime-core/src/provider/engine/stop.rs): at most 4 stops in flight, every worker joined; only `connect`/`connect_timeout` failures retry (25 ms doubling to 500 ms, within the batch deadline and 30 s of a stop's first connect failure); once one stop exhausts its window, later connect failures return at once; a deadline reached during backoff keeps the connect stage; `response`, `timeout` and `transport` never retry. Regressions in the same file's `provider::engine::stop` tests (bounded in-flight socket server, late socket, missing socket, 14-stop retry counts, persistent connect failures, oversleeping backoff, non-retried stages, worker panic) and `fourteen_service_connect_failures_keep_resumable_progress_and_retry_only_unstopped` | Tests cover exact attempt counts and the in-flight bound for fixed interleavings; no model explores all worker schedules or proves at most one delivered request per stop. Assumes a failed connect sent no request bytes and that the stop budget covers fully serialized grace periods. Graph-level resume after a partial batch is covered by tests only. Host qualification of the descriptor-pressure root cause (HACK-1302) remains open. | | Concurrent stop/publication; route claim and relay lifetime | native-route-stop, shared-https-lifetime, previous-boot-shared-https, relay-lifecycle-barrier, relay-authorization, relay-staging, relay-fence | Fenced route removal, relay owner, ready/removed protocol, authenticated observations | Native DNS/TLS/browser behavior; old-boot uncertainty and external routing. | @@ -67,6 +67,7 @@ liveness/reachability controls have their own documented assumptions. | Model | Positive distinct states | Configurations | | --- | ---: | ---: | | [native-plan-reconcile](../../tests/models/tla/native-plan-reconcile/Reconcile.tla) | 747,656 | 4 | +| [native-cache-reconcile](../../tests/models/tla/native-cache-reconcile/CacheReconcile.tla) | 54 | 4 | | [pre-ready-retirement](../../tests/models/tla/pre-ready-retirement/Retirement.tla) | 10,965 | 8 | | [native-persistent-enrollment](../../tests/models/tla/native-persistent-enrollment/Enrollment.tla) | 38 | 6 | | [native-frontend-recovery](../../tests/models/tla/native-frontend-recovery/Recovery.tla) | 602 | 10 | diff --git a/packages/runtime-core/README.md b/packages/runtime-core/README.md index e7abf4bcd..35c2d007b 100644 --- a/packages/runtime-core/README.md +++ b/packages/runtime-core/README.md @@ -1451,10 +1451,21 @@ admission would, retained volumes are projected by logical key onto their record names, newly declared volumes receive unused `reserved` names in this run and are created exclusively, and retained volumes the plan no longer declares stay in the receipt. Run, owner, namespace and the ownership plan on every label are unchanged. -`graph source-compatibility` reports `"reconcile": true` for this path. Receipts -with dependency caches, live source or a pending source-device rebind keep the -hostname/shared-source proofs. A volume still `reserved` in a stopped receipt was -never created; selection requires it absent and restore creates it. +`graph source-compatibility` reports `"reconcile": true` for this path. Dependency +caches reconcile too: a cache whose freshly resolved identity (the initializer's own +definition and inputs, not the whole Compose digest) equals the recorded binding is +kept with its provenance; a changed identity is selected like a fresh admission +(adopted by labels or created) with a freshly published source revision, and the old +shared cache is only released. A retained run-owned volume newly declared as a cache +refuses with `graph_plan_reconcile` and a `plan_change` diagnostic naming the service +and field. A receipt recorded under the earlier whole-document identity keeps that +cache while the review still resolves to it (`config::retain_recorded_legacy_caches`). +Receipts with live source, a carried cache scope, pending initializer cache release +or a pending source-device rebind keep the hostname/shared-source proofs; a +non-hostname edit there refuses with `graph_plan_change_unsupported`. A volume still +`reserved` in a stopped receipt was never created; selection requires it absent and +restore creates it, except a reserved dependency cache, which may already exist as a +shared cache. Selection binds the receipt, current VM boot and verified current volume observations. Restoration rechecks these before effects, requires the old owner diff --git a/packages/runtime-core/src/error.rs b/packages/runtime-core/src/error.rs index 2e9f3132b..784244fdb 100644 --- a/packages/runtime-core/src/error.rs +++ b/packages/runtime-core/src/error.rs @@ -53,6 +53,27 @@ pub struct StartupLogsDiagnostic { pub services: Vec, } +/// Closed vocabulary for the Compose field of a retained-run edit that cannot be +/// applied in place. +#[derive(Clone, Copy, Debug, Deserialize, Eq, PartialEq, Serialize)] +#[serde(rename_all = "snake_case")] +pub enum PlanChangeField { + /// A retained run-owned named volume is now declared as a dependency cache. + DependencyCacheVolume, + /// Routed hostnames changed together with something only reconciliation applies. + Hostnames, +} + +/// Value-free location of a refused retained-run edit. The service is an +/// admitted Compose identifier, never a value, path or engine ID. +#[derive(Clone, Debug, Deserialize, Eq, PartialEq, Serialize)] +#[serde(deny_unknown_fields)] +pub struct PlanChangeDiagnostic { + pub version: u8, + pub service: String, + pub field: PlanChangeField, +} + #[derive(Debug, Serialize)] pub struct CandidateError { pub code: &'static str, @@ -66,6 +87,8 @@ pub struct CandidateError { /// [`StartupLogTail`]. Never persist an error carrying it. #[serde(skip_serializing_if = "Option::is_none")] pub startup_logs: Option>, + #[serde(skip_serializing_if = "Option::is_none")] + pub plan_change: Option>, } impl CandidateError { @@ -76,9 +99,20 @@ impl CandidateError { cause_code: None, stop_failures: None, startup_logs: None, + plan_change: None, } } + /// Name the service and field of a refused retained-run edit. + pub fn with_plan_change(mut self, service: &str, field: PlanChangeField) -> Self { + self.plan_change = Some(Box::new(PlanChangeDiagnostic { + version: 1, + service: service.to_owned(), + field, + })); + self + } + pub fn with_cause_code(mut self, code: String) -> Self { self.cause_code = Some(code); self diff --git a/packages/runtime-core/src/provider/graph/cache_provenance.rs b/packages/runtime-core/src/provider/graph/cache_provenance.rs index 5dc6cc873..9f243449b 100644 --- a/packages/runtime-core/src/provider/graph/cache_provenance.rs +++ b/packages/runtime-core/src/provider/graph/cache_provenance.rs @@ -63,6 +63,15 @@ impl CacheProvenance { && bounded(&c.finished_at) }) } + /// Keep only initializers the reconciled graph still declares. The volume + /// identity fence is unchanged; removed services' history is dropped so the + /// receipt never names a container it no longer records. + pub(super) fn retain_initializers(&mut self, mut present: impl FnMut(&str) -> bool) { + self.initializers.retain(|service| present(service)); + let initializers = &self.initializers; + self.completed + .retain(|service, _| initializers.contains(service)); + } pub(super) fn needs_completion(&self, service: &str) -> bool { self.origin == Origin::CreatedHere && self.initializers.contains(service) diff --git a/packages/runtime-core/src/provider/graph/config.rs b/packages/runtime-core/src/provider/graph/config.rs index 8cadf64d4..f9411278a 100644 --- a/packages/runtime-core/src/provider/graph/config.rs +++ b/packages/runtime-core/src/provider/graph/config.rs @@ -16,12 +16,53 @@ pub(super) fn container_base(image: &str, labels: Value) -> Value { pub(super) struct Prepared { pub graph: Graph, pub cache_initializers: BTreeMap, + /// Earlier whole-document identities of this review's cache volumes, keyed by + /// logical volume. Only [`retain_recorded_legacy_caches`] may select one. + pub legacy_caches: BTreeMap, pub configs: BTreeMap, pub probes: BTreeMap, pub resources: BTreeMap, pub namespace: String, pub plan_id: String, } +/// A receipt recorded before cache identities bound only the initializer's own +/// definition keeps its exact cache volume while the review still resolves to +/// that recorded identity under the earlier formula. Nothing else is projected: +/// a changed input yields a different legacy identity and the current one stays. +pub(super) fn retain_recorded_legacy_caches(prepared: &mut Prepared, receipt: &Receipt) { + let mut renamed = BTreeMap::new(); + for (volume, legacy) in &prepared.legacy_caches { + let key = format!("volume:{volume}"); + let Some(resource) = prepared.resources.get_mut(&key) else { + continue; + }; + if resource.cache.as_ref() == Some(legacy) + || receipt + .resources + .get(&key) + .and_then(|old| old.cache.as_ref()) + != Some(legacy) + { + continue; + } + renamed.insert(resource.name.clone(), legacy.name()); + resource.name = legacy.name(); + resource.cache = Some(legacy.clone()); + } + if renamed.is_empty() { + return; + } + for config in prepared.configs.values_mut() { + if let Some(mounts) = config["HostConfig"]["Mounts"].as_array_mut() { + for mount in mounts.iter_mut().filter(|m| m["Type"] == "volume") { + if let Some(name) = mount["Source"].as_str().and_then(|s| renamed.get(s)) { + mount["Source"] = json!(name); + } + } + } + } +} + /// After source replay admission, preserve the original graph ownership identity /// on restored requests. Never change resource names, images, routes or cache keys. pub(super) fn retain_replay_ownership( @@ -44,6 +85,7 @@ fn retain_ownership( receipt: &Receipt, change: Option<&hostname_change::Verified>, ) -> Result<(), CandidateError> { + retain_recorded_legacy_caches(prepared, receipt); let same = change.map_or_else( || same_resource_bindings(&prepared.resources, &receipt.resources), |change| change.matches_resources(&prepared.resources, receipt), @@ -229,7 +271,10 @@ pub(super) fn prepare_delivery( "At most 32 services fit this driver profile; aggregate resource limits also apply.", )); } - let caches = if plan + let dependency_cache::Resolved { + current: caches, + legacy: legacy_caches, + } = if plan .services .values() .any(|service| service.active && service.dependency_cache.is_some()) @@ -244,14 +289,17 @@ pub(super) fn prepare_delivery( || dependency_cache::scope(&plan.source), |scope| scope.scope(&plan.source), )?; - dependency_cache::resolve( + dependency_cache::resolve_with_legacy( plan, source.current_manifest.as_ref().unwrap_or(&source.manifest), &scope, &inputs.services, )? } else { - BTreeMap::new() + dependency_cache::Resolved { + current: BTreeMap::new(), + legacy: BTreeMap::new(), + } }; let publications = loopback_publications(plan, loopback_ports)?; let mut networks = BTreeSet::new(); @@ -651,6 +699,7 @@ pub(super) fn prepare_delivery( .collect(); Ok(Prepared { cache_initializers, + legacy_caches, graph, configs, probes, diff --git a/packages/runtime-core/src/provider/graph/dependency_cache.rs b/packages/runtime-core/src/provider/graph/dependency_cache.rs index ca6a44b63..ae7cdc624 100644 --- a/packages/runtime-core/src/provider/graph/dependency_cache.rs +++ b/packages/runtime-core/src/provider/graph/dependency_cache.rs @@ -82,12 +82,49 @@ fn selected(manifest: &ContentRevision, path: &str) -> Result, Can _ => Err(refused()), } } +/// Cache identities for one review: `current` names the volumes a fresh +/// admission selects; `legacy` recomputes the earlier whole-document identity for +/// the same inputs, so a retained receipt recorded under it can still be matched +/// exactly. Neither map grants volume creation, adoption or deletion authority. +pub struct Resolved { + pub current: BTreeMap, + pub legacy: BTreeMap, +} + +#[cfg(test)] pub fn resolve( plan: &PlanData, manifest: &ContentRevision, scope: &str, executable: &BTreeMap, ) -> Result, CandidateError> { + Ok(resolve_with_legacy(plan, manifest, scope, executable)?.current) +} + +fn insert_binding( + result: &mut BTreeMap, + volume: &str, + binding: CacheBinding, +) -> Result<(), CandidateError> { + if result + .get(volume) + .is_some_and(|existing| existing != &binding) + { + return Err(refused()); + } + result.insert(volume.to_owned(), binding); + Ok(()) +} + +/// The current identity binds the initializer's own reviewed service definition +/// and its cache volume declaration instead of the whole Compose document, so an +/// edit to an unrelated service keeps the cache, as Compose keeps a named volume. +pub fn resolve_with_legacy( + plan: &PlanData, + manifest: &ContentRevision, + scope: &str, + executable: &BTreeMap, +) -> Result { manifest.validate().map_err(|_| refused())?; if !hex(scope) || !hex(&plan.compose_sha256) @@ -95,7 +132,8 @@ pub fn resolve( { return Err(refused()); } - let mut result = BTreeMap::new(); + let mut current = BTreeMap::new(); + let mut legacy = BTreeMap::new(); for (name, service) in plan.services.iter().filter(|(_, s)| s.active) { let Some(declaration) = &service.dependency_cache else { continue; @@ -141,10 +179,29 @@ pub fn resolve( return Err(refused()); } } - // Compose digest binds actual argv text (the plan's argv representation is redacted). - // Script content belongs in explicitly declared runtime files; whole source revisions - // would prevent compatible branches with unrelated source changes from sharing. + // The plan's argv and literal values are redacted, so the resolved public + // command, entrypoint, environment, user and hosts are bound explicitly. + // Script content belongs in explicitly declared runtime files; whole source + // revisions would prevent compatible branches with unrelated source changes + // from sharing. The legacy identity also bound the whole Compose digest. let base_fingerprint = hash(&( + "hack-dependency-cache-v2", + scope, + &declaration.volume, + image, + service, + &plan.volumes[&declaration.volume], + &plan.registry, + declaration, + &inputs, + &public.command, + &public.entrypoint, + &public.environment, + &public.user, + &public.extra_hosts, + &service.working_dir, + ))?; + let legacy_fingerprint = hash(&( "hack-dependency-cache-v1", scope, &declaration.volume, @@ -173,25 +230,31 @@ pub fn resolve( .map(move |m| (name, &m.target, &m.subpath, m.read_only)) }) .collect::>(); - let fingerprint = if layout.iter().any(|(_, _, subpath, _)| subpath.is_some()) { - hash(&("hack-cache-volume-subpaths-v1", base_fingerprint, layout))? - } else { - base_fingerprint + let subpaths = layout.iter().any(|(_, _, subpath, _)| subpath.is_some()); + let with_layout = |fingerprint: String| -> Result { + if subpaths { + hash(&("hack-cache-volume-subpaths-v1", fingerprint, &layout)) + } else { + Ok(fingerprint) + } }; - let binding = CacheBinding { + let binding = |fingerprint| CacheBinding { scope: scope.into(), fingerprint, image: image.clone(), }; - if result - .get(&declaration.volume) - .is_some_and(|existing| existing != &binding) - { - return Err(refused()); - } - result.insert(declaration.volume.clone(), binding); + insert_binding( + &mut current, + &declaration.volume, + binding(with_layout(base_fingerprint)?), + )?; + insert_binding( + &mut legacy, + &declaration.volume, + binding(with_layout(legacy_fingerprint)?), + )?; } - Ok(result) + Ok(Resolved { current, legacy }) } fn owned_directory(path: &Path) -> Result { @@ -694,7 +757,9 @@ mod tests { .arguments[0] .environment_references .push("INSTALLER".into()); - assert_eq!(baseline, resolve(&dynamic, &manifest, &scope).unwrap()); + // The redacted plan form is part of the initializer's own definition. + let dynamic_baseline = resolve(&dynamic, &manifest, &scope).unwrap(); + assert_ne!(baseline, dynamic_baseline); for field in [ "command", "entrypoint", @@ -716,7 +781,7 @@ mod tests { } } assert_ne!( - baseline, + dynamic_baseline, super::resolve(&dynamic, &manifest, &scope, &values).unwrap() ); } @@ -725,9 +790,23 @@ mod tests { changed.services.get_mut("deps").unwrap().image = Some(format!("sha256:{}", "e".repeat(64))); assert_ne!(baseline, resolve(&changed, &manifest, &scope).unwrap()); + // Only the earlier whole-document identity follows unrelated Compose edits. changed = plan.clone(); changed.compose_sha256 = "f".repeat(64); - assert_ne!(baseline, resolve(&changed, &manifest, &scope).unwrap()); + assert_eq!(baseline, resolve(&changed, &manifest, &scope).unwrap()); + let legacy = |plan: &PlanData| { + super::resolve_with_legacy(plan, &manifest, &scope, &executable(plan)) + .unwrap() + .legacy + }; + assert_ne!(legacy(&plan), legacy(&changed)); + assert_ne!(legacy(&plan), baseline); + // Another service, with its own environment, is not a cache input. + let mut app = plan.services["deps"].clone(); + app.dependency_cache = None; + app.mounts.clear(); + changed.services.insert("app".into(), app); + assert_eq!(baseline, resolve(&changed, &manifest, &scope).unwrap()); changed = plan.clone(); let mut other = changed.services["deps"].clone(); other.dependency_cache.as_mut().unwrap().bootstrap = false; diff --git a/packages/runtime-core/src/provider/graph/foreground.rs b/packages/runtime-core/src/provider/graph/foreground.rs index 033bd4a85..79fb9e648 100644 --- a/packages/runtime-core/src/provider/graph/foreground.rs +++ b/packages/runtime-core/src/provider/graph/foreground.rs @@ -163,7 +163,11 @@ pub fn restore_selection(candidate: &Candidate, run: &str) -> Result CandidateError { error( @@ -9,6 +10,22 @@ fn refused() -> CandidateError { ) } +/// A hostname change of `service` that is refused, named so the caller can say +/// which routed service and field the edit touched. +fn refused_for(service: &str) -> CandidateError { + refused().with_plan_change(service, PlanChangeField::Hostnames) +} + +/// The review changed, but no routed hostname did. Only receipts that plan +/// reconciliation cannot select reach this proof, so the edit is not applicable +/// in place; reporting it as a hostname change would name the wrong field. +pub(super) fn not_hostname_change() -> CandidateError { + error( + "graph_plan_change_unsupported", + "This retained graph uses live source, a carried cache scope, a pending source-device rebind or a pending initializer cache release; only a routed hostname change can be applied to it in place. Values omitted.", + ) +} + pub(super) struct Verified { pub source: source::Inputs, previous: NormalizedInputIdentity, @@ -23,7 +40,7 @@ pub(super) struct Verified { fn selected_routes( plan: &project::PlanData, receipt: &Receipt, -) -> Result, CandidateError> { +) -> Result<(BTreeMap, String), CandidateError> { let mut names = BTreeSet::new(); let routes = plan .services @@ -46,6 +63,17 @@ fn selected_routes( .map(|route| (resource.key.clone(), route)) }) .collect::>(); + let changed = routes + .iter() + .find(|(service, route)| prior.get(*service) != Some(route)) + .map(|(service, _)| service.clone()) + .or_else(|| { + prior + .keys() + .find(|service| !routes.contains_key(*service)) + .cloned() + }) + .ok_or_else(not_hostname_change)?; if routes.is_empty() || routes.len() != prior.len() || !routes.iter().all(|(service, route)| { @@ -56,13 +84,10 @@ fn selected_routes( .iter() .all(|name| names.insert(name.clone())) }) - || routes - .iter() - .all(|(service, route)| prior.get(service).is_some_and(|old| *old == route)) { - return Err(refused()); + return Err(refused_for(&changed)); } - Ok(routes) + Ok((routes, changed)) } /// Identical normalized input remains on the ordinary strict replay path. @@ -81,18 +106,29 @@ pub(super) fn prepare( if previous == next { return Ok(None); } - let routes = selected_routes(plan, receipt)?; - let binding = receipt.source.as_ref().ok_or_else(refused)?; + let (routes, changed) = selected_routes(plan, receipt)?; + let binding = receipt + .source + .as_ref() + .ok_or_else(|| refused_for(&changed))?; let cached = plan .services .values() .any(|service| service.active && service.dependency_cache.is_some()); + // Anything besides the hostnames changed too: name the routed service. let source = source::prepare_shared_hostnames( engine, plan, receipt, cached.then_some(binding.revision.as_str()), - )?; + ) + .map_err(|failure| { + if failure.code == "live_source_contract" { + refused_for(&changed) + } else { + failure + } + })?; super::super::publication::check_hostname_change( engine.guest().candidate(), &receipt.owner, @@ -355,4 +391,32 @@ pub(super) mod tests { assert!(proof.apply(&mut stale).is_err()); } } + + #[test] + fn a_review_without_a_hostname_change_is_not_reported_as_one() { + let (fixture, mut receipt, _) = transition(); + let plan = project::plan( + &Candidate::discover(&fixture.0).unwrap(), + project::PlanOptions { + branch: None, + project: &fixture.0.join("project"), + compose_file: Path::new("compose.yaml"), + profiles: &[], + }, + ) + .unwrap() + .plan; + // The routed service lost its route: a real hostname change, named. + let failure = selected_routes(&plan, &receipt).unwrap_err(); + assert_eq!(failure.code, "graph_hostname_change"); + let change = failure.plan_change.unwrap(); + assert_eq!(change.service, "web"); + assert_eq!(change.field, PlanChangeField::Hostnames); + // No route before or after: some other edit, which only reconciliation + // applies. The accurate code says so instead of naming hostnames. + receipt.resources.get_mut("container:web").unwrap().routing = None; + let failure = selected_routes(&plan, &receipt).unwrap_err(); + assert_eq!(failure.code, "graph_plan_change_unsupported"); + assert!(failure.plan_change.is_none()); + } } diff --git a/packages/runtime-core/src/provider/graph/plan_reconcile.rs b/packages/runtime-core/src/provider/graph/plan_reconcile.rs index 526151433..f05b72997 100644 --- a/packages/runtime-core/src/provider/graph/plan_reconcile.rs +++ b/packages/runtime-core/src/provider/graph/plan_reconcile.rs @@ -13,18 +13,36 @@ //! (Compose also keeps project volumes of removed declarations); explicit //! data removal still reaches it; //! * containers and networks of removed services are dropped from the receipt only -//! because their absence was confirmed before this projection. +//! because their absence was confirmed before this projection; +//! * a dependency cache whose freshly resolved identity equals the recorded one is +//! kept with its provenance. Its identity binds only the initializer's own +//! definition, cache declaration, image and input files, so edits to other +//! services keep it. A changed identity selects that identity's shared cache +//! exactly as a fresh admission would (adopt by labels or create, then the +//! initializer runs); the old cache is shared, never run-owned data, so only +//! this run's reference to it is released. A retained run-owned volume is never +//! reselected as a cache. //! //! Ownership never moves: run, owner, namespace and the ownership plan recorded on //! every label are unchanged, so another instance's data cannot be selected. -//! Dependency caches, live source and source-device rebinding keep their narrower -//! dedicated proofs and are not eligible here. +//! Live source, a cache scope carried across a source-device rebind and pending +//! initializer cache-release effects keep their narrower dedicated proofs and are +//! not eligible here. use super::*; +use crate::error::PlanChangeField; fn refused(message: &str) -> CandidateError { error("graph_plan_reconcile", message) } +/// Run-owned data is never reselected as a shared, content-addressed cache. +fn cache_over_retained_data(service: &str) -> CandidateError { + refused( + "A retained named volume is now declared as a dependency cache; its data was not reselected as a shared cache.", + ) + .with_plan_change(service, PlanChangeField::DependencyCacheVolume) +} + /// Retained named data is any recorded volume that may have been created. A /// volume still `reserved` never received a create intent, so it holds no data. pub(super) fn retained_volume(resource: &Resource) -> bool { @@ -45,25 +63,18 @@ fn active_volume_keys(plan: &project::PlanData) -> BTreeSet { .collect() } -/// Whether the plan or receipt uses machinery that has its own narrower proof. -fn eligible(receipt: &Receipt, plan: &project::PlanData) -> bool { +/// Whether the receipt uses machinery that has its own narrower proof. +fn eligible(receipt: &Receipt) -> bool { receipt.normalized_input.is_some() && receipt.initializer_cache_release.is_empty() - && receipt - .resources - .values() - .all(|resource| resource.cache.is_none() && resource.cache_provenance.is_none()) && receipt .source .as_ref() .is_none_or(|binding| binding.cache_scope.is_none() && binding.live.is_none()) - && plan - .services - .values() - .all(|service| !service.active || service.dependency_cache.is_none()) } -/// The ordinary strict replay derives volume names from the sorted declared set. +/// The ordinary strict replay derives run-owned volume names from the sorted +/// declared set (a dependency cache takes an index but keeps its content name). /// Once a reconciliation reattached data out of that order, or retains data no /// longer declared, only this projection can restore the graph again. fn ordinary_layout(receipt: &Receipt, plan: &project::PlanData) -> bool { @@ -72,18 +83,21 @@ fn ordinary_layout(receipt: &Receipt, plan: &project::PlanData) -> bool { .resources .values() .filter(|resource| resource.kind == Kind::Volume) - .map(|resource| (resource.key.clone(), resource.name.clone())) + .map(|resource| (resource.key.clone(), resource)) .collect::>(); recorded.len() == declared.len() && declared.iter().enumerate().all(|(index, key)| { - recorded.get(key) == Some(&format!("{}{index}", volume_prefix(&receipt.run))) + recorded.get(key).is_some_and(|resource| { + resource.cache.is_some() + || resource.name == format!("{}{index}", volume_prefix(&receipt.run)) + }) }) } /// Selects reconciliation for a reviewed plan that the strict replay path cannot -/// restore. Unchanged reviews with the ordinary layout keep strict replay; -/// graphs with dependency caches, live source or a pending source-device rebind -/// keep their dedicated hostname/shared-source proofs. +/// restore. Unchanged reviews with the ordinary layout keep strict replay; live +/// source, a carried cache scope or a pending source-device rebind keep their +/// dedicated hostname/shared-source proofs. pub(super) fn applies( receipt: &Receipt, plan_id: &str, @@ -92,7 +106,7 @@ pub(super) fn applies( source_rebind: bool, ) -> bool { !source_rebind - && eligible(receipt, plan) + && eligible(receipt) && !(receipt.plan_id == plan_id && receipt.normalized_input.as_ref() == Some(next) && ordinary_layout(receipt, plan)) @@ -126,9 +140,9 @@ pub(super) fn prepare( .normalized_input .clone() .ok_or_else(|| refused("Only normalized graphs can be reconciled."))?; - if !eligible(receipt, plan) { + if !eligible(receipt) { return Err(refused( - "Dependency caches, live source and cache-scoped source use their dedicated restore proofs.", + "Live source, a carried cache scope and pending initializer cache release use their dedicated restore proofs.", )); } if !next.matches_plan(plan) @@ -156,17 +170,31 @@ pub(super) fn prepare( if resource.kind != Kind::Volume { continue; } - if !resource - .name - .strip_prefix(&prefix) - .is_some_and(|index| index.parse::().is_ok_and(|n| n < 64)) - || !matches!(resource.phase.as_str(), "created" | "reserved") - { + let owned_name = resource.cache.as_ref().map_or_else( + || { + resource + .name + .strip_prefix(&prefix) + .is_some_and(|index| index.parse::().is_ok_and(|n| n < 64)) + }, + |cache| cache.valid() && resource.name == cache.name(), + ); + if !owned_name || !matches!(resource.phase.as_str(), "created" | "reserved") { return Err(refused( "Retained data is not this run's settled owned volume; it was not reattached.", )); } } + for (service, declared) in plan.services.iter().filter(|(_, service)| service.active) { + if let Some(cache) = &declared.dependency_cache + && receipt + .resources + .get(&format!("volume:{}", cache.volume)) + .is_some_and(|old| old.cache.is_none() && retained_volume(old)) + { + return Err(cache_over_retained_data(service)); + } + } Ok(Verified { run: receipt.run.clone(), owner: receipt.owner.clone(), @@ -219,11 +247,14 @@ impl Verified { if !self.matches_receipt(receipt) || prepared.namespace != receipt.namespace { return Err(refused("Reconciliation ownership changed.")); } + config::retain_recorded_legacy_caches(prepared, receipt); let prefix = volume_prefix(&receipt.run); + // Run-owned retained data. Dependency caches are shared, content-addressed + // volumes selected separately below; they are never reattached as data. let retained = receipt .resources .iter() - .filter(|(_, resource)| retained_volume(resource)) + .filter(|(_, resource)| retained_volume(resource) && resource.cache.is_none()) .collect::>(); let mut used = retained .values() @@ -236,12 +267,42 @@ impl Verified { resources.insert(key.clone(), resource.clone()); continue; } - if resource.cache.is_some() { - return Err(refused( - "Dependency cache volumes use their dedicated restore proof.", - )); - } - let selected = if let Some(old) = retained.get(key) { + let selected = if let Some(cache) = &resource.cache { + if retained.contains_key(key) { + let service = prepared + .cache_initializers + .iter() + .find(|(_, volume)| *volume == &resource.key) + .map_or(resource.key.as_str(), |(service, _)| service.as_str()); + return Err(cache_over_retained_data(service)); + } + match receipt.resources.get(key) { + // Same identity: keep the cache and its provenance fence. + Some(old) + if old.cache.as_ref() == Some(cache) + && old.name == resource.name + && matches!(old.phase.as_str(), "created" | "reserved") => + { + let mut kept = old.clone(); + if let Some(provenance) = kept.cache_provenance.as_mut() { + provenance.retain_initializers(|service| { + prepared + .resources + .contains_key(&format!("container:{service}")) + }); + } + kept + } + // New or changed identity: fresh-admission selection of the + // shared cache; the recorded reference (if any) is released. + _ => Resource { + id: None, + cache_provenance: None, + phase: "reserved".into(), + ..resource.clone() + }, + } + } else if let Some(old) = retained.get(key) { if old.key != resource.key || old.disposable_caches != resource.disposable_caches { return Err(refused( "A retained volume's disposable-cache declaration changed; it was not reattached.", @@ -270,6 +331,7 @@ impl Verified { resources.insert(key.clone(), selected); } // Retained data a changed plan no longer declares stays owned and recorded. + // A dependency cache is not run-owned data: an undeclared one is released. for (key, resource) in &retained { resources .entry((*key).clone()) @@ -342,7 +404,7 @@ impl Verified { #[cfg(test)] mod tests { use super::*; - use std::path::Path; + use std::{os::unix::fs::DirBuilderExt, path::Path}; const RUN: &str = "abababababababababababababababab"; @@ -397,6 +459,20 @@ mod tests { project::PlanReport, NormalizedInputIdentity, config::Prepared, + ) { + self.prepared_with(document, false) + } + + /// Dependency-cache graphs resolve their identities from a reviewed + /// source snapshot, as a fresh admission's publication supplies it. + fn prepared_with( + &self, + document: Value, + cached: bool, + ) -> ( + project::PlanReport, + NormalizedInputIdentity, + config::Prepared, ) { let (report, identity) = self.review(document); let inputs = project::inputs::compile( @@ -416,9 +492,35 @@ mod tests { .services .iter() .filter(|(_, service)| service.active) - .map(|(name, _)| (name.clone(), Condition::Started)) + .map(|(name, service)| { + let goal = if service.dependency_cache.is_some() { + Condition::Completed + } else { + Condition::Started + }; + (name.clone(), goal) + }) .collect(); - let prepared = config::prepare(inputs, &readiness, RUN, &"b".repeat(32), None).unwrap(); + let source = cached.then(|| { + let snapshot = project::snapshot::capture_plan(&report.plan).unwrap(); + let manifest = snapshot.receipt().clone(); + source::Inputs { + current_manifest: None, + binding: SourceBinding { + cache_scope: None, + shared: None, + shared_contract: None, + live: None, + revision: manifest.revision.clone(), + archive_sha256: "6".repeat(64), + selection_sha256: manifest.selection_sha256.clone(), + }, + manifest, + paths: BTreeMap::new(), + } + }); + let prepared = + config::prepare(inputs, &readiness, RUN, &"b".repeat(32), source.as_ref()).unwrap(); (report, identity, prepared) } } @@ -802,4 +904,255 @@ mod tests { super::super::restore::observed_volumes_with(&next, |_| Ok(None)).unwrap_err(); assert_eq!(missing.code, "graph_data_missing"); } + + /// An initializer populating a shared dependency cache, beside an app that + /// mounts the cache and its own run-owned data. + fn cached(marker: &str, installer: &str) -> Value { + json!({ + "services": { + "deps": { + "image": image('a'), + "network_mode": "none", + "entrypoint": [installer], + "volumes": ["deps:/deps"], + "labels": { + "hack.dependencies.bootstrap": "true", + "hack.dependencies.cache-volume": "deps", + "hack.dependencies.lockfiles": "lock.txt", + }, + }, + "app": { + "image": image('a'), + "network_mode": "none", + "entrypoint": ["/bin/app"], + "environment": {"MARKER": marker}, + "volumes": ["deps:/deps", "data:/data"], + }, + }, + "volumes": {"deps": {}, "data": {}}, + }) + } + + fn cached_project() -> (Project, Receipt, config::Prepared) { + let project = Project::new(); + fs::write(project.root.join("lock.txt"), "v1").unwrap(); + let (report, identity, prepared) = + project.prepared_with(cached("one", "/bin/install"), true); + let mut receipt = stopped(&prepared, &identity); + // A completed first admission recorded the cache's provenance fence. + let provenance: cache_provenance::CacheProvenance = serde_json::from_value(json!({ + "version": 1, "origin": "created_here", "boot": "boot", + "identity": {"created_at": "2026-11-06T00:00:00Z", "directory": "1:2"}, + "initializers": ["deps"], "completed": {}, + })) + .unwrap(); + receipt + .resources + .get_mut("volume:deps") + .unwrap() + .cache_provenance = Some(provenance); + assert!(receipt.resources["volume:deps"].cache.is_some()); + assert!(!applies( + &receipt, + &report.plan_id, + &report.plan, + &identity, + false + )); + (project, receipt, prepared) + } + + fn reconcile_cached( + project: &Project, + receipt: &Receipt, + next: Value, + ) -> (config::Prepared, Projection) { + let (report, identity, mut prepared) = project.prepared_with(next, true); + assert!(applies( + receipt, + &report.plan_id, + &report.plan, + &identity, + false + )); + let proof = prepare(&report.plan, receipt, &identity).unwrap(); + let projection = proof.project(&mut prepared, receipt).unwrap(); + let mut applied = receipt.clone(); + let snapshot = Projection { + resources: projection.resources.clone(), + }; + let readiness = projection + .resources + .values() + .filter(|resource| resource.kind == Kind::Container) + .map(|resource| (resource.key.clone(), Condition::Started)) + .collect(); + proof + .apply(&mut applied, snapshot, &readiness, None) + .unwrap(); + // The reconciled receipt still loads: every cache name and provenance is valid. + let fixture = super::super::tests::Fixture::new(); + let root = fixture.0.join(RUN); + fs::DirBuilder::new().mode(0o700).create(&root).unwrap(); + state::write(&root.join("state.json"), &applied).unwrap(); + super::super::load_at(root, RUN, &applied.owner).unwrap(); + (prepared, projection) + } + + #[test] + fn env_edit_to_another_service_reconciles_and_keeps_the_dependency_cache() { + let (project, receipt, original) = cached_project(); + let cache = receipt.resources["volume:deps"].clone(); + let (prepared, projection) = + reconcile_cached(&project, &receipt, cached("two", "/bin/install")); + // The same shared cache, with its provenance, and the same run-owned data. + assert!(same(&projection.resources["volume:deps"], &cache)); + assert!(same( + &projection.resources["volume:data"], + &receipt.resources["volume:data"] + )); + assert!(added(&projection).is_empty()); + assert_eq!(mounts(&prepared, "deps"), mounts(&original, "deps")); + assert_eq!(mounts(&prepared, "app"), mounts(&original, "app")); + assert_eq!(projection.resources["container:app"].phase, "reserved"); + } + + #[test] + fn changed_cache_inputs_select_a_fresh_cache_and_keep_run_data() { + let (project, receipt, _) = cached_project(); + let old = receipt.resources["volume:deps"].clone(); + // The initializer's own definition is a cache input. + let (prepared, projection) = + reconcile_cached(&project, &receipt, cached("one", "/bin/install-v2")); + let fresh = &projection.resources["volume:deps"]; + assert_ne!(fresh.cache, old.cache); + assert_ne!(fresh.name, old.name); + assert_eq!(fresh.name, fresh.cache.as_ref().unwrap().name()); + assert_eq!(fresh.phase, "reserved"); + assert!(fresh.cache_provenance.is_none()); + assert!(mounts(&prepared, "app").contains(&fresh.name)); + assert!(!mounts(&prepared, "app").contains(&old.name)); + assert!(same( + &projection.resources["volume:data"], + &receipt.resources["volume:data"] + )); + // So is a lockfile's content. + fs::write(project.root.join("lock.txt"), "v2").unwrap(); + let (_, projection) = reconcile_cached(&project, &receipt, cached("two", "/bin/install")); + let rebuilt = &projection.resources["volume:deps"]; + assert_ne!(rebuilt.cache, old.cache); + assert_eq!(rebuilt.phase, "reserved"); + } + + #[test] + fn retained_run_data_is_never_reselected_as_a_dependency_cache() { + let project = Project::new(); + fs::write(project.root.join("lock.txt"), "v1").unwrap(); + let mut plain = cached("one", "/bin/install"); + plain["services"]["deps"] + .as_object_mut() + .unwrap() + .remove("labels"); + let (_, identity, prepared) = project.prepared(plain); + let receipt = stopped(&prepared, &identity); + assert!(receipt.resources["volume:deps"].cache.is_none()); + let (report, identity, mut next) = + project.prepared_with(cached("one", "/bin/install"), true); + let failure = prepare(&report.plan, &receipt, &identity).err().unwrap(); + assert_eq!(failure.code, "graph_plan_reconcile"); + let change = failure.plan_change.as_deref().unwrap(); + assert_eq!(change.service, "deps"); + assert_eq!(change.field, PlanChangeField::DependencyCacheVolume); + // Admission repeats the check on the projection itself. + let proof = Verified { + run: receipt.run.clone(), + owner: receipt.owner.clone(), + namespace: receipt.namespace.clone(), + ownership_plan: receipt.plan_id.clone(), + previous: receipt.normalized_input.clone().unwrap(), + next: identity, + }; + let failure = proof.project(&mut next, &receipt).err().unwrap(); + assert_eq!(failure.plan_change.unwrap().service, "deps"); + } + + #[test] + fn dropping_a_cache_declaration_releases_the_reference_and_creates_run_data() { + let (project, receipt, _) = cached_project(); + let mut plain = cached("one", "/bin/install"); + plain["services"]["deps"] + .as_object_mut() + .unwrap() + .remove("labels"); + let (report, identity, mut prepared) = project.prepared(plain); + let proof = prepare(&report.plan, &receipt, &identity).unwrap(); + let projection = proof.project(&mut prepared, &receipt).unwrap(); + let deps = &projection.resources["volume:deps"]; + assert!(deps.cache.is_none()); + assert_eq!(deps.phase, "reserved"); + assert!(deps.name.starts_with(&volume_prefix(RUN))); + assert_ne!(deps.name, receipt.resources["volume:data"].name); + } + + #[test] + fn legacy_cache_identity_is_kept_only_while_its_inputs_still_match() { + let (project, mut receipt, original) = cached_project(); + let legacy = original.legacy_caches["deps"].clone(); + assert_ne!( + Some(&legacy), + original.resources["volume:deps"].cache.as_ref() + ); + let deps = receipt.resources.get_mut("volume:deps").unwrap(); + deps.cache = Some(legacy.clone()); + deps.name = legacy.name(); + // Unchanged review: strict replay keeps the recorded legacy cache. + let (report, identity, mut prepared) = + project.prepared_with(cached("one", "/bin/install"), true); + // The review's source metadata is fresh; the receipt is that admission's. + receipt.plan_id = report.plan_id.clone(); + assert!(!applies( + &receipt, + &report.plan_id, + &report.plan, + &identity, + false + )); + config::retain_replay_ownership(&mut prepared, &receipt).unwrap(); + assert_eq!(prepared.resources["volume:deps"].name, legacy.name()); + assert!(mounts(&prepared, "app").contains(&legacy.name())); + // An edit changes the legacy whole-document identity: the current one is + // selected once, after which edits elsewhere keep it. + let (_, projection) = reconcile_cached(&project, &receipt, cached("two", "/bin/install")); + let fresh = &projection.resources["volume:deps"]; + assert_ne!(fresh.name, legacy.name()); + assert_eq!(fresh.cache, original.resources["volume:deps"].cache); + assert_eq!(fresh.phase, "reserved"); + } + + #[test] + fn reserved_shared_caches_may_exist_but_reserved_run_names_may_not() { + let (project, receipt, _) = cached_project(); + let (_, projection) = + reconcile_cached(&project, &receipt, cached("one", "/bin/install-v2")); + let mut next = receipt.clone(); + next.resources = projection.resources; + let present = |_: &Resource| { + Ok(Some( + json!({"inspected": {"Name": "x"}, "directory": "1:2"}), + )) + }; + // The fresh cache may already exist as another graph's shared cache. + let selected = super::super::restore::observed_volumes_with(&next, present).unwrap(); + assert!(!selected.contains_key("volume:deps")); + assert!(selected.contains_key("volume:data")); + let mut owned = next.clone(); + let data = owned.resources.get_mut("volume:data").unwrap(); + data.phase = "reserved".into(); + assert_eq!( + super::super::restore::observed_volumes_with(&owned, present) + .unwrap_err() + .code, + "graph_resource_exists" + ); + } } diff --git a/packages/runtime-core/src/provider/graph/restore.rs b/packages/runtime-core/src/provider/graph/restore.rs index 756427a92..435016a7b 100644 --- a/packages/runtime-core/src/provider/graph/restore.rs +++ b/packages/runtime-core/src/provider/graph/restore.rs @@ -176,7 +176,9 @@ pub(super) fn observed_volumes_with( } if !plan_reconcile::retained_volume(resource) { // Never created: it holds no data, and an existing name is not adopted. - if observe(resource)?.is_some() { + // A not-yet-selected dependency cache is shared and content-addressed: + // admission adopts it by labels or creates it, as a fresh graph does. + if resource.cache.is_none() && observe(resource)?.is_some() { return Err(error( "graph_resource_exists", "A never-created volume name already resolves; it will not be adopted.", @@ -366,19 +368,20 @@ fn restore_inputs( #[cfg(not(target_os = "macos"))] let source_receipt = &receipt; let ordinary_source = if reconcile.is_some() { - // Exactly what a fresh admission of this review would select. Caches are - // not eligible here, so no retained cache publication may be named. - if options.source_revision.is_some() || options.live_source { + // Exactly what a fresh admission of this review would select: dependency + // caches name a publication that must match the current project contents + // (verified by the same mode checks); other graphs name none. + if options.live_source { return Err(error( "graph_plan_reconcile", - "Reconciliation selects no retained cache publication or live source.", + "Reconciliation selects no live source.", )); } source::prepare_mode( candidate, &engine, &inputs.review.plan, - None, + options.source_revision, false, options.shared_source, )? @@ -494,7 +497,7 @@ fn restore_inputs( "Retained volume is missing; restore will not recreate it.", )); } - if !plan_reconcile::retained_volume(resource) && present { + if !plan_reconcile::retained_volume(resource) && resource.cache.is_none() && present { return Err(error( "graph_resource_exists", "A never-created volume name already resolves; it will not be adopted.", diff --git a/scripts/lib/tla-runtime-models.ts b/scripts/lib/tla-runtime-models.ts index dd00652b7..ebbc0f737 100644 --- a/scripts/lib/tla-runtime-models.ts +++ b/scripts/lib/tla-runtime-models.ts @@ -149,6 +149,28 @@ const contracts: readonly ModelContract[] = [ }, ], }, + { + name: "native-cache-reconcile", + module: "CacheReconcile", + states: 54, + invariant: "UnrelatedEditKeepsCache", + action: "UpCache", + fields: ["needlessRebuild = TRUE", "staleMounted = FALSE"], + additionalControls: [ + { + name: "stale", + negative: true, + invariant: "CacheMatchesInputs", + fields: ["staleMounted = TRUE", "needlessRebuild = FALSE"], + }, + { + name: "data-as-cache", + negative: true, + invariant: "NoDataAsCache", + fields: ["dataMounted = TRUE", "staleMounted = FALSE"], + }, + ], + }, { name: "pre-ready-retirement", module: "Retirement", diff --git a/src/backends/native-plan-change.ts b/src/backends/native-plan-change.ts new file mode 100644 index 000000000..fb331e8d7 --- /dev/null +++ b/src/backends/native-plan-change.ts @@ -0,0 +1,70 @@ +import { isRecord } from "../lib/guards.ts"; + +/** + * Where a Compose edit that a retained native run cannot apply in place was + * made. The service is an admitted Compose identifier and the field a closed + * vocabulary, so both are safe to print; native messages never are. + */ +export interface NativePlanChange { + readonly service: string; + readonly field: NativePlanChangeField; +} + +const FIELDS = { + dependency_cache_volume: "`hack.dependencies.cache-volume`", + hostnames: "routed hostnames", +} as const; +type NativePlanChangeField = keyof typeof FIELDS; + +const SERVICE = /^[A-Za-z0-9_.-]{1,128}$/; + +/** Accept only the exact versioned diagnostic; anything else is dropped. */ +export function readNativePlanChange( + value: unknown +): NativePlanChange | undefined { + if ( + !isRecord(value) || + Object.keys(value).sort().join(",") !== "field,service,version" || + value.version !== 1 || + typeof value.service !== "string" || + !SERVICE.test(value.service) || + typeof value.field !== "string" || + !Object.hasOwn(FIELDS, value.field) + ) { + return; + } + return { + service: value.service, + field: value.field as NativePlanChangeField, + }; +} + +const APPLY = + "Revert the edit to keep the retained run as admitted, or run `hack down --remove-data` and then `hack up` to apply it with fresh data."; + +/** + * Closed guidance for native refusals of a Compose edit to a retained run. + * Returns undefined for every other code, which keeps the generic text. + */ +export function nativePlanChangeGuidance( + code: string, + change: NativePlanChange | undefined +): string | undefined { + const where = change + ? ` (service \`${change.service}\`, ${FIELDS[change.field]})` + : ""; + switch (code) { + case "graph_plan_reconcile": + return `this Compose edit${where} cannot be applied to the retained run. ${ + change?.field === "dependency_cache_volume" + ? "A retained named volume holds run data and is never reused as a shared dependency cache. " + : "" + }${APPLY}`; + case "graph_plan_change_unsupported": + return `this Compose edit cannot be applied in place: the retained run uses live source, a carried cache scope, a pending source-device rebind or a pending initializer cache release, so only routed hostname changes apply to it. ${APPLY}`; + case "graph_hostname_change": + return `the hostname change${where} cannot be applied to the retained run together with the other changes. Apply the hostname change on its own, or ${APPLY.charAt(0).toLowerCase()}${APPLY.slice(1)}`; + default: + return; + } +} diff --git a/src/backends/native-project-restore.ts b/src/backends/native-project-restore.ts index 42d532b70..db77b873a 100644 --- a/src/backends/native-project-restore.ts +++ b/src/backends/native-project-restore.ts @@ -88,8 +88,15 @@ export async function verifyNativeSourceCompatibility(opts: { `Native shared-source compatibility changed; ${NOT_ADOPTED}` ); } - const cached = nativeCacheInitializers(opts.review.report.plan).size > 0; - if ((result.source_revision === null) !== !cached) { + // Reconciliation recreates compute exactly as a fresh admission: it never + // names a retained cache publication, so a cached review publishes afresh. + const cached = + result.reconcile !== true && + nativeCacheInitializers(opts.review.report.plan).size > 0; + if ( + (result.reconcile !== undefined && result.reconcile !== true) || + (result.source_revision === null) !== !cached + ) { throw new ClosedCliError( `Native shared-source compatibility changed; ${NOT_ADOPTED}` ); diff --git a/src/backends/native-project-retained.ts b/src/backends/native-project-retained.ts index 577d49d29..91a50d8ff 100644 --- a/src/backends/native-project-retained.ts +++ b/src/backends/native-project-retained.ts @@ -44,15 +44,7 @@ export function confirmedNativeRetainedGraph( return false; } expected.add(key); - const observed = observations[key]; - // A `reserved` volume never received a create intent: it holds no data and - // must be absent. Every other volume is settled retained data. - const settledData = - resource.kind === "volume" && resource.phase !== "reserved"; - if ( - !isRecord(observed) || - observed.state !== (settledData ? "present" : "absent") - ) { + if (!observedAsRecorded(resource, observations[key])) { return false; } } @@ -61,3 +53,27 @@ export function confirmedNativeRetainedGraph( Object.keys(observations).every((key) => expected.has(key)) ); } + +/** + * Compute must be absent and settled data present. A `reserved` volume never + * received a create intent: it holds no data and must be absent. A reserved + * dependency cache is shared and content-addressed: admission adopts an + * existing one by labels or creates it, so either observation is valid. + */ +function observedAsRecorded( + resource: Record, + observed: unknown +): boolean { + if (!isRecord(observed)) { + return false; + } + if (resource.kind !== "volume") { + return observed.state === "absent"; + } + if (resource.phase !== "reserved") { + return observed.state === "present"; + } + return isRecord(resource.cache) + ? observed.state === "present" || observed.state === "absent" + : observed.state === "absent"; +} diff --git a/src/backends/native-runtime-client.ts b/src/backends/native-runtime-client.ts index 67d52f89d..fbf337bf1 100644 --- a/src/backends/native-runtime-client.ts +++ b/src/backends/native-runtime-client.ts @@ -2,6 +2,11 @@ import { isAbsolute } from "node:path"; import { ClosedCliError, HackCliError } from "../lib/cli-result.ts"; import { isRecord } from "../lib/guards.ts"; import { nativeAuthoredExecOptions } from "./native-authored-exec-options.ts"; +import { + type NativePlanChange, + nativePlanChangeGuidance, + readNativePlanChange, +} from "./native-plan-change.ts"; import { NATIVE_STARTUP_FAILURE_REPLY_BYTES, type NativeStartupLogTail, @@ -23,6 +28,7 @@ interface NativeFailure { readonly causeCode?: string; readonly stopFailures?: readonly NativeStopFailure[]; readonly startupLogs?: readonly NativeStartupLogTail[]; + readonly planChange?: NativePlanChange; } /** @@ -481,7 +487,10 @@ function nativeFailureMessage(failure: NativeFailure | undefined): string { const code = failure ? ` (${failure.code}${failure.causeCode ? `: ${failure.causeCode}` : ""})` : ""; - return `Native runtime request failed${code}; inspect owned state before retrying.${nativeStopFailureSummary(failure?.stopFailures)}`; + const guidance = failure + ? nativePlanChangeGuidance(failure.code, failure.planChange) + : undefined; + return `Native runtime request failed${code}; ${guidance ?? "inspect owned state before retrying."}${nativeStopFailureSummary(failure?.stopFailures)}`; } function completionResponse( @@ -628,9 +637,11 @@ function nativeFailureFromReply( code: value.code, cause: value.cause_code, }); + const planChange = readNativePlanChange(value.plan_change); return { code: value.code, ...(causeCode ? { causeCode } : {}), + ...(planChange ? { planChange } : {}), ...(["engine_protocol", "engine_rejected", "engine_not_found"].includes( value.code === "graph_owner_recovery" && typeof value.cause_code === "string" diff --git a/tests/models/tla/README.md b/tests/models/tla/README.md index 269822194..19a8dfce7 100644 --- a/tests/models/tla/README.md +++ b/tests/models/tla/README.md @@ -735,9 +735,40 @@ Assumptions: admission through startup holds the provider mutation lease, so no replacement happens inside it. A replacement with copied ownership labels before selection is indistinguishable from the recorded volume by name and labels, as in the implementation; the generation fence protects only the selection-to-admission -window. Dependency caches, live source and source-device rebinding keep their own -proofs and are outside this model. It does not prove engine mount behavior, crash -durability of the receipt, image resolution or application data contents. +window. Dependency caches are checked by the next model; live source and +source-device rebinding keep their own proofs and are outside this model. It does +not prove engine mount behavior, crash durability of the receipt, image resolution +or application data contents. + +## Dependency caches across plan changes + +`native-cache-reconcile/CacheReconcile.tla` checks which volume backs a dependency +cache key when a stopped graph is reconciled after a Compose edit. A cache is a +shared volume named by an identity of its inputs; run-owned data uses the run's own +names. Edits change the cache's own inputs (initializer definition, declaration, +image, lockfiles), anything else in the Compose file, or whether the key is declared +as a cache. Two values for each explore 54 distinct states. + +| Model action | Implementation boundary | +| --- | --- | +| `EditInputs` / `EditOther` / `EditDeclaration` | Compose or lockfile edit between ups; `dependency_cache::resolve_with_legacy` computes the current identity | +| `UpCache` | `plan_reconcile::prepare` refuses run data declared as a cache; `Verified::project` keeps a cache of the same identity or selects the new identity's shared cache, then `Session::create_resources` adopts it by labels or creates it | +| `UpData` | A key that is no longer a cache gets a fresh run-owned volume; the cache reference is released, never deleted | +| `Stop` | Ctrl-C or `down` keeps every recorded volume | + +The `negative` control binds the whole Compose document into the identity (the +earlier formula) and must fail `UnrelatedEditKeepsCache` in an `UpCache` state with +`needlessRebuild = TRUE`. The `stale` control reattaches the recorded cache whatever +its identity and must fail `CacheMatchesInputs` with `staleMounted = TRUE`. The +`data-as-cache` control mounts retained run data newly declared as a cache and must +fail `NoDataAsCache` with `dataMounted = TRUE`. + +Assumptions: identities are exact (no collisions), the initializer populates a newly +selected cache before dependents start, and admission holds the provider lease. The +compatibility path that keeps a receipt recorded under the earlier identity while +its inputs still match is covered by `plan_reconcile.rs` tests, not this model. It +does not prove initializer idempotence, cache content, capacity limits or cache-wide +collection. ## Graph admission diff --git a/tests/models/tla/native-cache-reconcile/CacheReconcile.tla b/tests/models/tla/native-cache-reconcile/CacheReconcile.tla new file mode 100644 index 000000000..0b03c7e04 --- /dev/null +++ b/tests/models/tla/native-cache-reconcile/CacheReconcile.tla @@ -0,0 +1,103 @@ +------------------------- MODULE CacheReconcile ------------------------- +(* Dependency-cache selection when a stopped native graph is reconciled after a + Compose edit. A cache is a shared volume named by an identity of its inputs; + run-owned data lives under the run's own names. Compute is always recreated, + so only which volume backs the cache key is modeled. `inputs` are the cache's + own inputs (initializer definition, declaration, image, lockfiles); `other` is + every other part of the Compose file. Broken constants are negative controls. *) +EXTENDS Naturals, TLC +CONSTANTS Values, + WholeDocument, \* identity also binds `other` (the earlier formula) + KeepStale, \* reattach the recorded cache whatever its identity + DataAsCache \* reselect retained run data newly declared as a cache +None == [kind |-> "none", id |-> <<0, 0>>, rin |-> 0] +Id(i, o) == IF WholeDocument THEN <> ELSE <> +VARIABLES phase, inputs, other, declared, recorded, caches, mounted, + staleMounted, dataMounted, needlessRebuild +vars == <> + +\* A first admission populated the cache for the initial inputs. +Init == /\ phase = "stopped" + /\ inputs = 1 /\ other = 1 /\ declared = "cache" + /\ recorded = [kind |-> "cache", id |-> Id(1, 1), rin |-> 1] + /\ caches = {Id(1, 1)} + /\ mounted = None + /\ staleMounted = FALSE /\ dataMounted = FALSE /\ needlessRebuild = FALSE + +\* Edits between ups: the cache's own inputs, anything else, or whether the key +\* is declared as a cache at all. +EditInputs(v) == /\ phase = "stopped" /\ v # inputs /\ inputs' = v + /\ UNCHANGED <> +EditOther(v) == /\ phase = "stopped" /\ v # other /\ other' = v + /\ UNCHANGED <> +EditDeclaration == /\ phase = "stopped" + /\ declared' = IF declared = "cache" THEN "data" ELSE "cache" + /\ UNCHANGED <> + +\* plan_reconcile::Verified::project then Session::create_resources: keep a +\* recorded cache of the same identity; otherwise select that identity's shared +\* cache (adopt or create; the initializer populates it) and release the old +\* reference. Retained run data declared as a cache is refused. +UpCache == + LET want == Id(inputs, other) + entry == [kind |-> "cache", id |-> want, rin |-> inputs] IN + /\ phase = "stopped" /\ declared = "cache" + /\ IF recorded.kind = "data" + THEN IF DataAsCache + THEN /\ phase' = "running" /\ mounted' = recorded + /\ dataMounted' = TRUE + /\ UNCHANGED <> + ELSE UNCHANGED <> + ELSE IF recorded.kind = "cache" /\ (recorded.id = want \/ KeepStale) + THEN /\ phase' = "running" /\ mounted' = recorded + /\ staleMounted' = (staleMounted \/ recorded.rin # inputs) + /\ UNCHANGED <> + ELSE /\ phase' = "running" /\ mounted' = entry + /\ recorded' = entry + /\ caches' = caches \cup {want} + /\ needlessRebuild' = (needlessRebuild \/ + (recorded.kind = "cache" /\ recorded.rin = inputs + /\ want \notin caches)) + /\ UNCHANGED <> + /\ UNCHANGED <> + +\* The key is ordinary run data: reattach recorded data, or create fresh run data +\* when it was a cache (whose shared volume is only released, never deleted). +UpData == + /\ phase = "stopped" /\ declared = "data" + /\ phase' = "running" + /\ recorded' = IF recorded.kind = "data" THEN recorded + ELSE [kind |-> "data", id |-> <<0, 0>>, rin |-> 0] + /\ mounted' = recorded' + /\ UNCHANGED <> + +Stop == /\ phase = "running" /\ phase' = "stopped" /\ mounted' = None + /\ UNCHANGED <> + +Next == \/ \E v \in Values : EditInputs(v) \/ EditOther(v) + \/ EditDeclaration \/ UpCache \/ UpData \/ Stop +Spec == Init /\ [][Next]_vars + +TypeOK == /\ phase \in {"stopped", "running"} + /\ inputs \in Values /\ other \in Values + /\ declared \in {"cache", "data"} + /\ recorded.kind \in {"none", "cache", "data"} + /\ mounted.kind \in {"none", "cache", "data"} + +\* A running graph's cache was populated for exactly its current inputs. +CacheMatchesInputs == /\ ~staleMounted + /\ (phase = "running" /\ mounted.kind = "cache") => + mounted.rin = inputs +\* Run-owned data is never mounted as a shared cache. +NoDataAsCache == ~dataMounted +\* An edit that leaves the cache's own inputs unchanged keeps the cache: it never +\* selects a not-yet-populated cache for the same inputs. +UnrelatedEditKeepsCache == ~needlessRebuild +============================================================================= diff --git a/tests/models/tla/native-cache-reconcile/data-as-cache.cfg b/tests/models/tla/native-cache-reconcile/data-as-cache.cfg new file mode 100644 index 000000000..2c5f19a6f --- /dev/null +++ b/tests/models/tla/native-cache-reconcile/data-as-cache.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANTS Values = {1, 2} + WholeDocument = FALSE KeepStale = FALSE DataAsCache = TRUE +INVARIANTS TypeOK CacheMatchesInputs NoDataAsCache UnrelatedEditKeepsCache diff --git a/tests/models/tla/native-cache-reconcile/negative.cfg b/tests/models/tla/native-cache-reconcile/negative.cfg new file mode 100644 index 000000000..d8c5edf62 --- /dev/null +++ b/tests/models/tla/native-cache-reconcile/negative.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANTS Values = {1, 2} + WholeDocument = TRUE KeepStale = FALSE DataAsCache = FALSE +INVARIANTS TypeOK CacheMatchesInputs NoDataAsCache UnrelatedEditKeepsCache diff --git a/tests/models/tla/native-cache-reconcile/positive.cfg b/tests/models/tla/native-cache-reconcile/positive.cfg new file mode 100644 index 000000000..cbcf0c537 --- /dev/null +++ b/tests/models/tla/native-cache-reconcile/positive.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANTS Values = {1, 2} + WholeDocument = FALSE KeepStale = FALSE DataAsCache = FALSE +INVARIANTS TypeOK CacheMatchesInputs NoDataAsCache UnrelatedEditKeepsCache diff --git a/tests/models/tla/native-cache-reconcile/stale.cfg b/tests/models/tla/native-cache-reconcile/stale.cfg new file mode 100644 index 000000000..cc68f47cd --- /dev/null +++ b/tests/models/tla/native-cache-reconcile/stale.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANTS Values = {1, 2} + WholeDocument = FALSE KeepStale = TRUE DataAsCache = FALSE +INVARIANTS TypeOK CacheMatchesInputs NoDataAsCache UnrelatedEditKeepsCache diff --git a/tests/native-plan-change.test.ts b/tests/native-plan-change.test.ts new file mode 100644 index 000000000..72deecda6 --- /dev/null +++ b/tests/native-plan-change.test.ts @@ -0,0 +1,39 @@ +import { expect, test } from "bun:test"; +import { + nativePlanChangeGuidance, + readNativePlanChange, +} from "../src/backends/native-plan-change.ts"; + +test("only the exact versioned plan-change diagnostic is read", () => { + const valid = { version: 1, service: "deps", field: "hostnames" }; + expect(readNativePlanChange(valid)).toEqual({ + service: "deps", + field: "hostnames", + }); + for (const value of [ + undefined, + { ...valid, version: 2 }, + { ...valid, field: "environment" }, + { ...valid, field: "toString" }, + { ...valid, service: "two words" }, + { ...valid, extra: true }, + ]) { + expect(readNativePlanChange(value)).toBeUndefined(); + } +}); + +test("retained-run edit refusals get closed, accurate guidance", () => { + expect( + nativePlanChangeGuidance("graph_plan_change_unsupported", undefined) + ).toContain("only routed hostname changes apply to it"); + expect( + nativePlanChangeGuidance("graph_hostname_change", { + service: "web", + field: "hostnames", + }) + ).toContain("the hostname change (service `web`, routed hostnames)"); + expect(nativePlanChangeGuidance("graph_plan_reconcile", undefined)).toBe( + "this Compose edit cannot be applied to the retained run. Revert the edit to keep the retained run as admitted, or run `hack down --remove-data` and then `hack up` to apply it with fresh data." + ); + expect(nativePlanChangeGuidance("graph_budget", undefined)).toBeUndefined(); +}); diff --git a/tests/native-project-restore.test.ts b/tests/native-project-restore.test.ts index 4eb41a5dd..6eed50433 100644 --- a/tests/native-project-restore.test.ts +++ b/tests/native-project-restore.test.ts @@ -223,3 +223,55 @@ test("an edited Compose plan restores the same run after the native reconcile pr flags: ["--expect-generation", selected.generation], }); }); + +test("a reconciled dependency-cache graph publishes fresh source instead of the retained revision", async () => { + const review = { + ...options.review, + planId: "f".repeat(64), + report: { + plan: { + services: { + deps: { active: true, dependency_cache: { volume: "deps" } }, + app: { active: true }, + }, + }, + }, + }; + const compatibility = { + run: saved.run, + owner: saved.owner, + namespace: saved.namespace, + plan: saved.planId, + reviewed_plan: review.planId, + source_revision: null, + reconcile: true, + }; + const restore = (reply: Record) => + selectNativeProjectRestore({ + ...options, + review, + restore: saved, + invoke: async ({ args }) => + args[1] === "restore-selection" ? selected : reply, + }); + // No retained revision: the start path publishes the current snapshot. + expect(await restore(compatibility)).toEqual({ + run: saved.run, + restoring: true, + flags: ["--expect-generation", selected.generation], + }); + // A reconciliation never names a retained cache publication. + await expectClosedRefusal( + restore({ ...compatibility, source_revision: "1".repeat(64) }), + "compatibility changed" + ); + // Without reconciliation the retained revision stays mandatory. + await expectClosedRefusal( + restore({ ...compatibility, reconcile: undefined }), + "compatibility changed" + ); + await expectClosedRefusal( + restore({ ...compatibility, reconcile: "true" }), + "compatibility changed" + ); +}); diff --git a/tests/native-project-retained-images.test.ts b/tests/native-project-retained-images.test.ts index 816bc0359..27f8a2c31 100644 --- a/tests/native-project-retained-images.test.ts +++ b/tests/native-project-retained-images.test.ts @@ -459,3 +459,43 @@ test("restart of a stopped graph points at up instead of reporting image drift", "stopped with data retained. Run hack up" ); }); + +test("a reconciled graph's reserved shared cache may already exist; reserved run data may not", () => { + const baseline = observation(); + const withCache = (state: string, cache: boolean) => ({ + ...baseline, + receipt: { + ...baseline.receipt, + resources: { + ...baseline.receipt.resources, + "volume:deps": { + kind: "volume", + key: "deps", + phase: "reserved", + ...(cache + ? { + cache: { + scope: "1".repeat(64), + fingerprint: "2".repeat(64), + image, + }, + } + : {}), + }, + }, + }, + observations: { ...baseline.observations, "volume:deps": { state } }, + }); + expect(confirmedNativeRetainedGraph(withCache("present", true), saved)).toBe( + true + ); + expect(confirmedNativeRetainedGraph(withCache("absent", true), saved)).toBe( + true + ); + expect(confirmedNativeRetainedGraph(withCache("unknown", true), saved)).toBe( + false + ); + expect(confirmedNativeRetainedGraph(withCache("present", false), saved)).toBe( + false + ); +}); diff --git a/tests/native-runtime-client.test.ts b/tests/native-runtime-client.test.ts index 75d8afd01..64d8e3e45 100644 --- a/tests/native-runtime-client.test.ts +++ b/tests/native-runtime-client.test.ts @@ -147,6 +147,8 @@ async function fixture() { binary, `#!${process.execPath} if (process.argv.includes("hang")) await Bun.sleep(60_000); +if (process.argv.includes("plan-change")) { console.error(JSON.stringify({code:"graph_plan_reconcile",message:"synthetic-secret-diagnostic",plan_change:{version:1,service:"deps",field:"dependency_cache_volume"}})); process.exit(23); } +if (process.argv.includes("plan-change-unsafe")) { console.error(JSON.stringify({code:"graph_hostname_change",message:"synthetic-secret-diagnostic",plan_change:{version:1,service:"synthetic secret diagnostic",field:"hostnames"}})); process.exit(23); } if (process.argv.includes("structured")) { console.error(JSON.stringify({code:"source_conflict",message:"synthetic-secret-diagnostic"})); process.exit(23); } if (process.argv.includes("foreground-stopped")) { console.error(JSON.stringify({code:"native_graph_foreground",cause_code:"runtime_not_running",message:"synthetic-secret-diagnostic"})); process.exit(23); } if (process.argv.includes("foreground-other")) { console.error(JSON.stringify({code:"native_graph_foreground",cause_code:"engine_protocol",message:"synthetic-secret-diagnostic"})); process.exit(23); } @@ -767,6 +769,35 @@ test("native failure preserves only its validated structured code", async () => } }); +test("a refused Compose edit names its service and field and how to apply it", async () => { + const runtime = await fixture(); + const reconcile: unknown = await invokeNativeRuntime({ + runtime, + cwd: runtime.home, + args: ["plan-change"], + }).catch((caught: unknown) => caught); + expect(reconcile).toBeInstanceOf(NativeRuntimeRequestError); + expect(reconcile).toMatchObject({ nativeCode: "graph_plan_reconcile" }); + const message = String(reconcile); + expect(message).toContain( + "Native runtime request failed (graph_plan_reconcile); this Compose edit (service `deps`, `hack.dependencies.cache-volume`) cannot be applied to the retained run." + ); + expect(message).toContain("`hack down --remove-data` and then `hack up`"); + expect(message).not.toContain("synthetic-secret-diagnostic"); + // An unbounded service name is dropped; the closed guidance remains. + const hostname = String( + await invokeNativeRuntime({ + runtime, + cwd: runtime.home, + args: ["plan-change-unsafe"], + }).catch((caught: unknown) => caught) + ); + expect(hostname).toContain( + "Native runtime request failed (graph_hostname_change); the hostname change cannot be applied" + ); + expect(hostname).not.toContain("synthetic"); +}); + test("failures omit subprocess diagnostics and timeouts are bounded", async () => { const runtime = await fixture(); await expect( From 139be6c345509152d0e0da7bc074b2732b243f51 Mon Sep 17 00:00:00 2001 From: Dimitri Kennedy <344842+roodboi@users.noreply.github.com> Date: Fri, 6 Nov 2026 21:27:34 -0500 Subject: [PATCH 2/3] fix(native): bind every cache-volume mount into the cache identity The v2 dependency-cache identity bound the mount layout only when a mount used a subpath. Adding or changing another service that mounts the shared cache volume read-write therefore kept the same identity, so a new writer could change contents that other runs and instances reuse. The current identity now always binds the full layout: every active service that mounts the cache volume, with its target, subpath and read-only flag. Adding, removing or changing a writer selects a fresh cache; an environment-only edit to a service keeps it. Mounts stay as declared, as in Compose and v4, rather than being forced read-only. The legacy whole-document identity is unchanged, so earlier receipts still match exactly. Regression tests cover a new read-write mount, its access mode, an env edit to that writer, a second initializer, and reconciliation selecting a fresh cache when a writer service is added. Refs HACK-1937 Co-Authored-By: Claude Opus 5.5 --- docs/guides/native-candidate.md | 11 ++- packages/runtime-core/README.md | 3 +- .../src/provider/graph/dependency_cache.rs | 86 +++++++++++++------ .../src/provider/graph/plan_reconcile.rs | 23 +++++ tests/models/tla/README.md | 5 +- .../native-cache-reconcile/CacheReconcile.tla | 5 +- 6 files changed, 99 insertions(+), 34 deletions(-) diff --git a/docs/guides/native-candidate.md b/docs/guides/native-candidate.md index a0a7230d6..56dd369fd 100644 --- a/docs/guides/native-candidate.md +++ b/docs/guides/native-candidate.md @@ -718,10 +718,13 @@ namespace that created it. Graphs with `hack.dependencies.*` caches reconcile the same way. A cache's identity covers only its own inputs: the initializer's service definition and resolved command, entrypoint, environment and user, the cache declaration, its image, the -declared lockfile and runtime-file contents, and the cache volume layout. An edit -to another service, such as an environment value on the app, keeps the cache. An -edit to one of those inputs, including a lockfile, selects the cache for the new -identity as a fresh `up` would, so the initializer installs into it; the old cache +declared lockfile and runtime-file contents, and the cache volume layout: every +service that mounts the cache volume, with its target, subpath and `:ro` mode. Any +of those services can write the shared contents, so adding, removing or changing +such a mount is a cache input; mounts stay as declared, as in Compose and v4, and +are not forced read-only. Any other edit to another service, such as an +environment value on the app, keeps the cache. An edit to one of those inputs, +including a lockfile, selects the cache for the new identity as a fresh `up` would, so the initializer installs into it; the old cache is shared and is only released by this run. Each such `up` publishes the current source snapshot. A retained named volume is never reused as a dependency cache: declaring one refuses and names the service and the `hack.dependencies.cache-volume` diff --git a/packages/runtime-core/README.md b/packages/runtime-core/README.md index 35c2d007b..9a7221df2 100644 --- a/packages/runtime-core/README.md +++ b/packages/runtime-core/README.md @@ -1453,7 +1453,8 @@ created exclusively, and retained volumes the plan no longer declares stay in th receipt. Run, owner, namespace and the ownership plan on every label are unchanged. `graph source-compatibility` reports `"reconcile": true` for this path. Dependency caches reconcile too: a cache whose freshly resolved identity (the initializer's own -definition and inputs, not the whole Compose digest) equals the recorded binding is +definition and inputs plus every service mount of the cache volume, not the whole +Compose digest) equals the recorded binding is kept with its provenance; a changed identity is selected like a fresh admission (adopted by labels or created) with a freshly published source revision, and the old shared cache is only released. A retained run-owned volume newly declared as a cache diff --git a/packages/runtime-core/src/provider/graph/dependency_cache.rs b/packages/runtime-core/src/provider/graph/dependency_cache.rs index ae7cdc624..1e7a409b6 100644 --- a/packages/runtime-core/src/provider/graph/dependency_cache.rs +++ b/packages/runtime-core/src/provider/graph/dependency_cache.rs @@ -179,12 +179,27 @@ pub fn resolve_with_legacy( return Err(refused()); } } + // Every active service that mounts the cache volume, with its target, + // subpath and access mode. Any of them can write the shared contents, so a + // writer added, removed or changed elsewhere is a cache input, even though + // the rest of that service's definition is not. + let layout = plan + .services + .iter() + .filter(|(_, s)| s.active) + .flat_map(|(name, s)| { + s.mounts + .iter() + .filter(|m| m.kind == "volume" && m.source == declaration.volume) + .map(move |m| (name, &m.target, &m.subpath, m.read_only)) + }) + .collect::>(); // The plan's argv and literal values are redacted, so the resolved public // command, entrypoint, environment, user and hosts are bound explicitly. // Script content belongs in explicitly declared runtime files; whole source // revisions would prevent compatible branches with unrelated source changes // from sharing. The legacy identity also bound the whole Compose digest. - let base_fingerprint = hash(&( + let current_fingerprint = hash(&( "hack-dependency-cache-v2", scope, &declaration.volume, @@ -200,6 +215,7 @@ pub fn resolve_with_legacy( &public.user, &public.extra_hosts, &service.working_dir, + &layout, ))?; let legacy_fingerprint = hash(&( "hack-dependency-cache-v1", @@ -217,26 +233,12 @@ pub fn resolve_with_legacy( &public.extra_hosts, &service.working_dir, ))?; - // Include the whole shared-volume layout, not only initializer mounts. - // Keep historical cache keys unchanged when no subpath is requested. - let layout = plan - .services - .iter() - .filter(|(_, s)| s.active) - .flat_map(|(name, s)| { - s.mounts - .iter() - .filter(|m| m.kind == "volume" && m.source == declaration.volume) - .map(move |m| (name, &m.target, &m.subpath, m.read_only)) - }) - .collect::>(); - let subpaths = layout.iter().any(|(_, _, subpath, _)| subpath.is_some()); - let with_layout = |fingerprint: String| -> Result { - if subpaths { - hash(&("hack-cache-volume-subpaths-v1", fingerprint, &layout)) - } else { - Ok(fingerprint) - } + // The legacy identity reproduces the earlier keys exactly: its Compose + // digest covered the layout, and only subpaths were bound again. + let legacy_fingerprint = if layout.iter().any(|(_, _, subpath, _)| subpath.is_some()) { + hash(&("hack-cache-volume-subpaths-v1", legacy_fingerprint, &layout))? + } else { + legacy_fingerprint }; let binding = |fingerprint| CacheBinding { scope: scope.into(), @@ -246,12 +248,12 @@ pub fn resolve_with_legacy( insert_binding( &mut current, &declaration.volume, - binding(with_layout(base_fingerprint)?), + binding(current_fingerprint), )?; insert_binding( &mut legacy, &declaration.volume, - binding(with_layout(legacy_fingerprint)?), + binding(legacy_fingerprint), )?; } Ok(Resolved { current, legacy }) @@ -804,9 +806,39 @@ mod tests { // Another service, with its own environment, is not a cache input. let mut app = plan.services["deps"].clone(); app.dependency_cache = None; + let cache_mount = app.mounts.clone(); app.mounts.clear(); - changed.services.insert("app".into(), app); + changed.services.insert("app".into(), app.clone()); assert_eq!(baseline, resolve(&changed, &manifest, &scope).unwrap()); + // But a service that can write the shared cache is: adding a read-write + // mount of the cache volume changes the identity, with or without subpaths. + app.mounts = cache_mount; + assert!( + app.mounts + .iter() + .all(|m| !m.read_only && m.subpath.is_none()) + ); + changed.services.insert("app".into(), app.clone()); + let writer = resolve(&changed, &manifest, &scope).unwrap(); + assert_ne!(baseline, writer); + // Its access mode and target are part of the layout too. + let mut reader = app.clone(); + reader.mounts[0].read_only = true; + changed.services.insert("app".into(), reader); + let read_only = resolve(&changed, &manifest, &scope).unwrap(); + assert_ne!(writer, read_only); + assert_ne!(baseline, read_only); + // An environment edit to that writer keeps the identity it now has. + let mut edited = app; + edited.environment.insert( + "MARKER".into(), + crate::project::RedactedText { + environment_references: Vec::new(), + literal_redacted: true, + }, + ); + changed.services.insert("app".into(), edited); + assert_eq!(writer, resolve(&changed, &manifest, &scope).unwrap()); changed = plan.clone(); let mut other = changed.services["deps"].clone(); other.dependency_cache.as_mut().unwrap().bootstrap = false; @@ -820,7 +852,11 @@ mod tests { .as_mut() .unwrap() .bootstrap = true; - assert_eq!(baseline, resolve(&changed, &manifest, &scope).unwrap()); + // Both initializers agree on one identity; the second writer of the shared + // volume is part of it. + let shared = resolve(&changed, &manifest, &scope).unwrap(); + assert_eq!(shared.len(), 1); + assert_ne!(baseline, shared); } #[test] fn missing_lockfiles_and_symlink_inputs_refuse() { diff --git a/packages/runtime-core/src/provider/graph/plan_reconcile.rs b/packages/runtime-core/src/provider/graph/plan_reconcile.rs index f05b72997..90bedcad1 100644 --- a/packages/runtime-core/src/provider/graph/plan_reconcile.rs +++ b/packages/runtime-core/src/provider/graph/plan_reconcile.rs @@ -1044,6 +1044,29 @@ mod tests { assert_eq!(rebuilt.phase, "reserved"); } + #[test] + fn adding_a_cache_writer_selects_a_fresh_cache() { + let (project, receipt, _) = cached_project(); + let old = receipt.resources["volume:deps"].clone(); + // A new service that mounts the shared cache read-write can change what + // every run sharing it reuses, so it is part of the cache identity. + let mut next = cached("one", "/bin/install"); + next["services"]["worker"] = json!({ + "image": image('a'), + "network_mode": "none", + "entrypoint": ["/bin/worker"], + "volumes": ["deps:/deps"], + }); + let (_, projection) = reconcile_cached(&project, &receipt, next); + let fresh = &projection.resources["volume:deps"]; + assert_ne!(fresh.cache, old.cache); + assert_eq!(fresh.phase, "reserved"); + assert!(same( + &projection.resources["volume:data"], + &receipt.resources["volume:data"] + )); + } + #[test] fn retained_run_data_is_never_reselected_as_a_dependency_cache() { let project = Project::new(); diff --git a/tests/models/tla/README.md b/tests/models/tla/README.md index 19a8dfce7..2d3b09877 100644 --- a/tests/models/tla/README.md +++ b/tests/models/tla/README.md @@ -746,8 +746,9 @@ or application data contents. cache key when a stopped graph is reconciled after a Compose edit. A cache is a shared volume named by an identity of its inputs; run-owned data uses the run's own names. Edits change the cache's own inputs (initializer definition, declaration, -image, lockfiles), anything else in the Compose file, or whether the key is declared -as a cache. Two values for each explore 54 distinct states. +image, lockfiles, and every service mount of the cache volume, since any of those +services can write it), anything else in the Compose file, or whether the key is +declared as a cache. Two values for each explore 54 distinct states. | Model action | Implementation boundary | | --- | --- | diff --git a/tests/models/tla/native-cache-reconcile/CacheReconcile.tla b/tests/models/tla/native-cache-reconcile/CacheReconcile.tla index 0b03c7e04..f59d4be26 100644 --- a/tests/models/tla/native-cache-reconcile/CacheReconcile.tla +++ b/tests/models/tla/native-cache-reconcile/CacheReconcile.tla @@ -3,8 +3,9 @@ Compose edit. A cache is a shared volume named by an identity of its inputs; run-owned data lives under the run's own names. Compute is always recreated, so only which volume backs the cache key is modeled. `inputs` are the cache's - own inputs (initializer definition, declaration, image, lockfiles); `other` is - every other part of the Compose file. Broken constants are negative controls. *) + own inputs (initializer definition, declaration, image, lockfiles and every + service mount of the cache volume, since each can write it); `other` is every + other part of the Compose file. Broken constants are negative controls. *) EXTENDS Naturals, TLC CONSTANTS Values, WholeDocument, \* identity also binds `other` (the earlier formula) From 592a9b1dcbb53aad32e13d89595ec5178fdef2ad Mon Sep 17 00:00:00 2001 From: Dimitri Kennedy <344842+roodboi@users.noreply.github.com> Date: Fri, 6 Nov 2026 21:46:23 -0500 Subject: [PATCH 3/3] fix(native): scope dependency caches with writable consumers to one instance A service other than the initializer that mounts a dependency cache read-write can change the cache contents through its own image, command, environment or source, none of which the cache identity hashes. On a contributor branch it could therefore poison a cache that a linked worktree later reuses. Within one checkout the same author controls every input, so the trust boundary is sharing across worktrees and branch instances. - A cache with a writable non-initializer consumer binds the plan namespace (this checkout and branch instance) into its scope, so it is never shared across linked worktrees. Caches whose other consumers all mount read-only keep sharing; the initializer's definition, image and lockfiles stay in the identity. - Such graphs always re-prove the cache through reconciliation, and no earlier whole-document identity is matched for them: a run created by an earlier build moves to its instance-scoped cache once instead of reusing the shared one. Env-only edits inside one instance still keep the cache. - The native-cache-reconcile model adds writable consumers and foreign writes (2,208 states) with a `poison` negative control that keeps such caches shared and fails `NoForeignWrites`. Refs HACK-1937 Co-Authored-By: Claude Opus 5.5 --- docs/guides/native-candidate.md | 9 +- docs/reference/v5-model-coverage.md | 2 +- packages/runtime-core/README.md | 6 +- .../src/provider/graph/dependency_cache.rs | 120 ++++++++++++++++-- .../src/provider/graph/plan_reconcile.rs | 80 +++++++++--- scripts/lib/tla-runtime-models.ts | 8 +- tests/models/tla/README.md | 33 +++-- .../native-cache-reconcile/CacheReconcile.tla | 113 ++++++++++------- .../native-cache-reconcile/data-as-cache.cfg | 4 +- .../tla/native-cache-reconcile/negative.cfg | 4 +- .../tla/native-cache-reconcile/poison.cfg | 4 + .../tla/native-cache-reconcile/positive.cfg | 4 +- .../tla/native-cache-reconcile/stale.cfg | 4 +- 13 files changed, 300 insertions(+), 91 deletions(-) create mode 100644 tests/models/tla/native-cache-reconcile/poison.cfg diff --git a/docs/guides/native-candidate.md b/docs/guides/native-candidate.md index 56dd369fd..d073f2b18 100644 --- a/docs/guides/native-candidate.md +++ b/docs/guides/native-candidate.md @@ -722,7 +722,14 @@ declared lockfile and runtime-file contents, and the cache volume layout: every service that mounts the cache volume, with its target, subpath and `:ro` mode. Any of those services can write the shared contents, so adding, removing or changing such a mount is a cache input; mounts stay as declared, as in Compose and v4, and -are not forced read-only. Any other edit to another service, such as an +are not forced read-only. Caches are shared across linked worktrees and branch +instances only while every service other than the initializers mounts them +read-only. A service that mounts the cache read-write can change its contents +through its own image, command, environment or source, which the identity does not +cover, so that cache is scoped to this checkout and branch instance and never +shared. To share it again, mount it with `:ro` in the other services. A run created +by an earlier build whose cache has such a writer moves to its own instance cache +once instead of reusing the shared one. Any other edit to another service, such as an environment value on the app, keeps the cache. An edit to one of those inputs, including a lockfile, selects the cache for the new identity as a fresh `up` would, so the initializer installs into it; the old cache is shared and is only released by this run. Each such `up` publishes the current diff --git a/docs/reference/v5-model-coverage.md b/docs/reference/v5-model-coverage.md index 386fec859..70cf0dab3 100644 --- a/docs/reference/v5-model-coverage.md +++ b/docs/reference/v5-model-coverage.md @@ -67,7 +67,7 @@ liveness/reachability controls have their own documented assumptions. | Model | Positive distinct states | Configurations | | --- | ---: | ---: | | [native-plan-reconcile](../../tests/models/tla/native-plan-reconcile/Reconcile.tla) | 747,656 | 4 | -| [native-cache-reconcile](../../tests/models/tla/native-cache-reconcile/CacheReconcile.tla) | 54 | 4 | +| [native-cache-reconcile](../../tests/models/tla/native-cache-reconcile/CacheReconcile.tla) | 2,208 | 5 | | [pre-ready-retirement](../../tests/models/tla/pre-ready-retirement/Retirement.tla) | 10,965 | 8 | | [native-persistent-enrollment](../../tests/models/tla/native-persistent-enrollment/Enrollment.tla) | 38 | 6 | | [native-frontend-recovery](../../tests/models/tla/native-frontend-recovery/Recovery.tla) | 602 | 10 | diff --git a/packages/runtime-core/README.md b/packages/runtime-core/README.md index 9a7221df2..03f988806 100644 --- a/packages/runtime-core/README.md +++ b/packages/runtime-core/README.md @@ -1457,7 +1457,11 @@ definition and inputs plus every service mount of the cache volume, not the whol Compose digest) equals the recorded binding is kept with its provenance; a changed identity is selected like a fresh admission (adopted by labels or created) with a freshly published source revision, and the old -shared cache is only released. A retained run-owned volume newly declared as a cache +shared cache is only released. A cache that a non-initializer service mounts +read-write (`dependency_cache::instance_scoped_volumes`) binds the plan namespace +into its scope, so it is never shared across linked worktrees or branch instances; +such graphs always re-prove the cache through reconciliation, and no earlier +whole-document identity is matched for them. A retained run-owned volume newly declared as a cache refuses with `graph_plan_reconcile` and a `plan_change` diagnostic naming the service and field. A receipt recorded under the earlier whole-document identity keeps that cache while the review still resolves to it (`config::retain_recorded_legacy_caches`). diff --git a/packages/runtime-core/src/provider/graph/dependency_cache.rs b/packages/runtime-core/src/provider/graph/dependency_cache.rs index 1e7a409b6..e3bc2b500 100644 --- a/packages/runtime-core/src/provider/graph/dependency_cache.rs +++ b/packages/runtime-core/src/provider/graph/dependency_cache.rs @@ -82,6 +82,28 @@ fn selected(manifest: &ContentRevision, path: &str) -> Result, Can _ => Err(refused()), } } +/// Logical cache volumes that a service other than their initializers mounts +/// read-write. Such a consumer can change the shared contents with inputs the +/// identity does not hash (its image, command, environment or source), so the +/// cache is scoped to this checkout and branch instance (the plan namespace) +/// rather than shared across linked worktrees. Read-only consumers keep sharing. +pub fn instance_scoped_volumes(plan: &PlanData) -> std::collections::BTreeSet { + let active = || plan.services.iter().filter(|(_, s)| s.active); + active() + .filter_map(|(_, s)| s.dependency_cache.as_ref().map(|d| d.volume.clone())) + .filter(|volume| { + active().any(|(_, s)| { + s.dependency_cache + .as_ref() + .is_none_or(|d| &d.volume != volume) + && s.mounts + .iter() + .any(|m| m.kind == "volume" && &m.source == volume && !m.read_only) + }) + }) + .collect() +} + /// Cache identities for one review: `current` names the volumes a fresh /// admission selects; `legacy` recomputes the earlier whole-document identity for /// the same inputs, so a retained receipt recorded under it can still be matched @@ -134,6 +156,12 @@ pub fn resolve_with_legacy( } let mut current = BTreeMap::new(); let mut legacy = BTreeMap::new(); + let scoped = instance_scoped_volumes(plan); + let instance_scope = hash(&( + "hack-dependency-cache-instance-scope-v1", + scope, + &plan.namespace, + ))?; for (name, service) in plan.services.iter().filter(|(_, s)| s.active) { let Some(declaration) = &service.dependency_cache else { continue; @@ -199,9 +227,15 @@ pub fn resolve_with_legacy( // Script content belongs in explicitly declared runtime files; whole source // revisions would prevent compatible branches with unrelated source changes // from sharing. The legacy identity also bound the whole Compose digest. + let writable = scoped.contains(&declaration.volume); + let current_scope = if writable { + instance_scope.as_str() + } else { + scope + }; let current_fingerprint = hash(&( "hack-dependency-cache-v2", - scope, + current_scope, &declaration.volume, image, service, @@ -240,7 +274,7 @@ pub fn resolve_with_legacy( } else { legacy_fingerprint }; - let binding = |fingerprint| CacheBinding { + let binding = |scope: &str, fingerprint| CacheBinding { scope: scope.into(), fingerprint, image: image.clone(), @@ -248,13 +282,18 @@ pub fn resolve_with_legacy( insert_binding( &mut current, &declaration.volume, - binding(current_fingerprint), - )?; - insert_binding( - &mut legacy, - &declaration.volume, - binding(legacy_fingerprint), + binding(current_scope, current_fingerprint), )?; + // An earlier shared cache with a writable consumer may hold another + // worktree's writes, so it is never matched again: such a receipt moves to + // its instance-scoped cache once. + if !writable { + insert_binding( + &mut legacy, + &declaration.volume, + binding(scope, legacy_fingerprint), + )?; + } } Ok(Resolved { current, legacy }) } @@ -858,6 +897,71 @@ mod tests { assert_eq!(shared.len(), 1); assert_ne!(baseline, shared); } + #[test] + fn a_writable_consumer_scopes_the_cache_to_one_instance() { + let (_source, _home, plan, manifest) = prepared(); + let scope = "a".repeat(64); + // Two linked worktrees (or branch instances) share the scope root but + // have their own plan namespaces. + let worktree = |plan: &PlanData, namespace: char| { + let mut plan = plan.clone(); + plan.namespace = namespace.to_string().repeat(64); + plan + }; + let with_consumer = |read_only: bool| { + let mut plan = plan.clone(); + let mut app = plan.services["deps"].clone(); + app.dependency_cache = None; + app.mounts[0].read_only = read_only; + plan.services.insert("app".into(), app); + plan + }; + // Only initializers write: shared across worktrees. + assert!(instance_scoped_volumes(&plan).is_empty()); + assert_eq!( + resolve(&worktree(&plan, 'b'), &manifest, &scope).unwrap(), + resolve(&worktree(&plan, 'c'), &manifest, &scope).unwrap() + ); + // A read-only consumer cannot change the contents: still shared. + let reader = with_consumer(true); + assert!(instance_scoped_volumes(&reader).is_empty()); + let shared = resolve(&worktree(&reader, 'b'), &manifest, &scope).unwrap(); + assert_eq!(shared["deps"].scope, scope); + assert_eq!( + shared, + resolve(&worktree(&reader, 'c'), &manifest, &scope).unwrap() + ); + // A writable consumer in worktree A never shares with worktree B, and has + // no earlier shared identity a receipt could keep. + let writer = with_consumer(false); + assert_eq!( + instance_scoped_volumes(&writer), + BTreeSet::from(["deps".to_owned()]) + ); + let a = super::resolve_with_legacy( + &worktree(&writer, 'b'), + &manifest, + &scope, + &executable(&writer), + ) + .unwrap(); + let b = resolve(&worktree(&writer, 'c'), &manifest, &scope).unwrap(); + assert_ne!(a.current["deps"].scope, scope); + assert_ne!(a.current, b); + assert_ne!(a.current["deps"].name(), b["deps"].name()); + assert!(a.legacy.is_empty()); + // Inside one instance an environment edit to the writer keeps the cache. + let mut edited = worktree(&writer, 'b'); + edited.services.get_mut("app").unwrap().environment.insert( + "MARKER".into(), + crate::project::RedactedText { + environment_references: Vec::new(), + literal_redacted: true, + }, + ); + assert_eq!(a.current, resolve(&edited, &manifest, &scope).unwrap()); + } + #[test] fn missing_lockfiles_and_symlink_inputs_refuse() { let (_source, _home, mut plan, mut manifest) = prepared(); diff --git a/packages/runtime-core/src/provider/graph/plan_reconcile.rs b/packages/runtime-core/src/provider/graph/plan_reconcile.rs index 90bedcad1..fd8b864fd 100644 --- a/packages/runtime-core/src/provider/graph/plan_reconcile.rs +++ b/packages/runtime-core/src/provider/graph/plan_reconcile.rs @@ -77,7 +77,17 @@ fn eligible(receipt: &Receipt) -> bool { /// declared set (a dependency cache takes an index but keeps its content name). /// Once a reconciliation reattached data out of that order, or retains data no /// longer declared, only this projection can restore the graph again. +/// A cache with a writable consumer is scoped to this instance; a receipt recorded +/// before that scoping names a shared cache that may hold another worktree's +/// writes. Such graphs always take this path, which keeps the cache only when its +/// freshly resolved instance-scoped identity equals the recorded binding exactly. fn ordinary_layout(receipt: &Receipt, plan: &project::PlanData) -> bool { + let scoped = dependency_cache::instance_scoped_volumes(plan); + if receipt.resources.values().any(|resource| { + resource.kind == Kind::Volume && resource.cache.is_some() && scoped.contains(&resource.key) + }) { + return false; + } let declared = active_volume_keys(plan); let recorded = receipt .resources @@ -905,9 +915,18 @@ mod tests { assert_eq!(missing.code, "graph_data_missing"); } - /// An initializer populating a shared dependency cache, beside an app that - /// mounts the cache and its own run-owned data. + /// An initializer populating a dependency cache, beside an app that mounts + /// the cache read-write (so the cache is instance-scoped) and its own data. fn cached(marker: &str, installer: &str) -> Value { + cached_with(marker, installer, "deps:/deps") + } + + /// The same graph whose app only reads the cache, so the cache is shared. + fn cached_shared(marker: &str, installer: &str) -> Value { + cached_with(marker, installer, "deps:/deps:ro") + } + + fn cached_with(marker: &str, installer: &str, consumer: &str) -> Value { json!({ "services": { "deps": { @@ -926,7 +945,7 @@ mod tests { "network_mode": "none", "entrypoint": ["/bin/app"], "environment": {"MARKER": marker}, - "volumes": ["deps:/deps", "data:/data"], + "volumes": [consumer, "data:/data"], }, }, "volumes": {"deps": {}, "data": {}}, @@ -934,10 +953,14 @@ mod tests { } fn cached_project() -> (Project, Receipt, config::Prepared) { + cached_project_with(cached("one", "/bin/install")) + } + + fn cached_project_with(document: Value) -> (Project, Receipt, config::Prepared) { let project = Project::new(); fs::write(project.root.join("lock.txt"), "v1").unwrap(); - let (report, identity, prepared) = - project.prepared_with(cached("one", "/bin/install"), true); + let shared = document["services"]["app"]["volumes"][0] == "deps:/deps:ro"; + let (report, identity, prepared) = project.prepared_with(document, true); let mut receipt = stopped(&prepared, &identity); // A completed first admission recorded the cache's provenance fence. let provenance: cache_provenance::CacheProvenance = serde_json::from_value(json!({ @@ -952,13 +975,12 @@ mod tests { .unwrap() .cache_provenance = Some(provenance); assert!(receipt.resources["volume:deps"].cache.is_some()); - assert!(!applies( - &receipt, - &report.plan_id, - &report.plan, - &identity, - false - )); + // A shared cache keeps strict replay; an instance-scoped one always + // re-proves its identity through reconciliation. + assert_eq!( + applies(&receipt, &report.plan_id, &report.plan, &identity, false), + !shared + ); (project, receipt, prepared) } @@ -1119,7 +1141,8 @@ mod tests { #[test] fn legacy_cache_identity_is_kept_only_while_its_inputs_still_match() { - let (project, mut receipt, original) = cached_project(); + let (project, mut receipt, original) = + cached_project_with(cached_shared("one", "/bin/install")); let legacy = original.legacy_caches["deps"].clone(); assert_ne!( Some(&legacy), @@ -1130,7 +1153,7 @@ mod tests { deps.name = legacy.name(); // Unchanged review: strict replay keeps the recorded legacy cache. let (report, identity, mut prepared) = - project.prepared_with(cached("one", "/bin/install"), true); + project.prepared_with(cached_shared("one", "/bin/install"), true); // The review's source metadata is fresh; the receipt is that admission's. receipt.plan_id = report.plan_id.clone(); assert!(!applies( @@ -1145,13 +1168,40 @@ mod tests { assert!(mounts(&prepared, "app").contains(&legacy.name())); // An edit changes the legacy whole-document identity: the current one is // selected once, after which edits elsewhere keep it. - let (_, projection) = reconcile_cached(&project, &receipt, cached("two", "/bin/install")); + let (_, projection) = + reconcile_cached(&project, &receipt, cached_shared("two", "/bin/install")); let fresh = &projection.resources["volume:deps"]; assert_ne!(fresh.name, legacy.name()); assert_eq!(fresh.cache, original.resources["volume:deps"].cache); assert_eq!(fresh.phase, "reserved"); } + #[test] + fn an_earlier_shared_cache_with_a_writable_consumer_moves_to_this_instance() { + let (project, mut receipt, original) = cached_project(); + // No earlier identity is ever matched for a writable consumer. + assert!(!original.legacy_caches.contains_key("deps")); + let scoped = original.resources["volume:deps"].cache.clone().unwrap(); + // A receipt from an earlier build names a cache shared across worktrees. + let shared = dependency_cache::CacheBinding { + scope: dependency_cache::scope(&project.root).unwrap(), + fingerprint: "c".repeat(64), + image: scoped.image.clone(), + }; + assert_ne!(shared.scope, scoped.scope); + let deps = receipt.resources.get_mut("volume:deps").unwrap(); + deps.cache = Some(shared.clone()); + deps.name = shared.name(); + // Even the unchanged review re-proves identity and selects this + // instance's cache once; the shared one is never mounted again. + let (prepared, projection) = + reconcile_cached(&project, &receipt, cached("one", "/bin/install")); + let fresh = &projection.resources["volume:deps"]; + assert_eq!(fresh.cache.as_ref(), Some(&scoped)); + assert_eq!(fresh.phase, "reserved"); + assert!(!mounts(&prepared, "app").contains(&shared.name())); + } + #[test] fn reserved_shared_caches_may_exist_but_reserved_run_names_may_not() { let (project, receipt, _) = cached_project(); diff --git a/scripts/lib/tla-runtime-models.ts b/scripts/lib/tla-runtime-models.ts index ebbc0f737..1bbc93bb0 100644 --- a/scripts/lib/tla-runtime-models.ts +++ b/scripts/lib/tla-runtime-models.ts @@ -152,7 +152,7 @@ const contracts: readonly ModelContract[] = [ { name: "native-cache-reconcile", module: "CacheReconcile", - states: 54, + states: 2208, invariant: "UnrelatedEditKeepsCache", action: "UpCache", fields: ["needlessRebuild = TRUE", "staleMounted = FALSE"], @@ -169,6 +169,12 @@ const contracts: readonly ModelContract[] = [ invariant: "NoDataAsCache", fields: ["dataMounted = TRUE", "staleMounted = FALSE"], }, + { + name: "poison", + negative: true, + invariant: "NoForeignWrites", + fields: ["foreignMounted = TRUE", "staleMounted = FALSE"], + }, ], }, { diff --git a/tests/models/tla/README.md b/tests/models/tla/README.md index 2d3b09877..c9017c6de 100644 --- a/tests/models/tla/README.md +++ b/tests/models/tla/README.md @@ -744,16 +744,21 @@ or application data contents. `native-cache-reconcile/CacheReconcile.tla` checks which volume backs a dependency cache key when a stopped graph is reconciled after a Compose edit. A cache is a -shared volume named by an identity of its inputs; run-owned data uses the run's own -names. Edits change the cache's own inputs (initializer definition, declaration, -image, lockfiles, and every service mount of the cache volume, since any of those -services can write it), anything else in the Compose file, or whether the key is -declared as a cache. Two values for each explore 54 distinct states. +volume named by an identity of its inputs; run-owned data uses the run's own names. +Edits change the cache's own inputs (initializer definition, declaration, image, +lockfiles, and every service mount of the cache volume), anything else in the +Compose file, whether a non-initializer service mounts the cache read-write, or +whether the key is declared as a cache. Such a writable consumer can change the +contents with inputs the identity does not hash, so its cache is scoped to this +checkout or branch instance; another instance with its own writable consumer may +write into the caches it selects (`ForeignWrite`). Two values for each explore +2,208 distinct states. | Model action | Implementation boundary | | --- | --- | -| `EditInputs` / `EditOther` / `EditDeclaration` | Compose or lockfile edit between ups; `dependency_cache::resolve_with_legacy` computes the current identity | -| `UpCache` | `plan_reconcile::prepare` refuses run data declared as a cache; `Verified::project` keeps a cache of the same identity or selects the new identity's shared cache, then `Session::create_resources` adopts it by labels or creates it | +| `EditInputs` / `EditOther` / `EditConsumer` / `EditDeclaration` | Compose or lockfile edit between ups; `dependency_cache::resolve_with_legacy` computes the current identity and `instance_scoped_volumes` the scope | +| `ForeignWrite` | A linked worktree or branch instance whose writable consumer changes the cache it mounts | +| `UpCache` | `plan_reconcile::prepare` refuses run data declared as a cache; `Verified::project` keeps a cache of the same identity or selects the new identity's cache, then `Session::create_resources` adopts it by labels or creates it | | `UpData` | A key that is no longer a cache gets a fresh run-owned volume; the cache reference is released, never deleted | | `Stop` | Ctrl-C or `down` keeps every recorded volume | @@ -762,14 +767,18 @@ earlier formula) and must fail `UnrelatedEditKeepsCache` in an `UpCache` state w `needlessRebuild = TRUE`. The `stale` control reattaches the recorded cache whatever its identity and must fail `CacheMatchesInputs` with `staleMounted = TRUE`. The `data-as-cache` control mounts retained run data newly declared as a cache and must -fail `NoDataAsCache` with `dataMounted = TRUE`. +fail `NoDataAsCache` with `dataMounted = TRUE`. The `poison` control keeps caches +with a writable consumer shared across instances and must fail `NoForeignWrites` +with `foreignMounted = TRUE`. Assumptions: identities are exact (no collisions), the initializer populates a newly -selected cache before dependents start, and admission holds the provider lease. The +selected cache before dependents start, read-only consumers and initializers only +produce what the identity describes, and admission holds the provider lease. Within +one instance the same author controls every input, so writes there are trusted. The compatibility path that keeps a receipt recorded under the earlier identity while -its inputs still match is covered by `plan_reconcile.rs` tests, not this model. It -does not prove initializer idempotence, cache content, capacity limits or cache-wide -collection. +its inputs still match (never for a writable consumer) is covered by +`plan_reconcile.rs` tests, not this model. It does not prove initializer +idempotence, cache content, capacity limits or cache-wide collection. ## Graph admission diff --git a/tests/models/tla/native-cache-reconcile/CacheReconcile.tla b/tests/models/tla/native-cache-reconcile/CacheReconcile.tla index f59d4be26..8dc981632 100644 --- a/tests/models/tla/native-cache-reconcile/CacheReconcile.tla +++ b/tests/models/tla/native-cache-reconcile/CacheReconcile.tla @@ -1,71 +1,94 @@ ------------------------- MODULE CacheReconcile ------------------------- (* Dependency-cache selection when a stopped native graph is reconciled after a - Compose edit. A cache is a shared volume named by an identity of its inputs; - run-owned data lives under the run's own names. Compute is always recreated, - so only which volume backs the cache key is modeled. `inputs` are the cache's - own inputs (initializer definition, declaration, image, lockfiles and every - service mount of the cache volume, since each can write it); `other` is every - other part of the Compose file. Broken constants are negative controls. *) + Compose edit. A cache is a volume named by an identity of its inputs; run-owned + data lives under the run's own names. Compute is always recreated, so only + which volume backs the cache key is modeled, for one trusted instance. `inputs` + are the cache's own inputs (initializer definition, declaration, image, + lockfiles and every service mount of the cache volume); `other` is every other + part of the Compose file. `writable` says a non-initializer service mounts the + cache read-write: it can change the contents with inputs the identity does not + hash, so the cache is scoped to this instance. A linked worktree or branch + instance with its own writable consumer may write into the caches it selects. + Broken constants are negative controls. *) EXTENDS Naturals, TLC CONSTANTS Values, WholeDocument, \* identity also binds `other` (the earlier formula) KeepStale, \* reattach the recorded cache whatever its identity - DataAsCache \* reselect retained run data newly declared as a cache -None == [kind |-> "none", id |-> <<0, 0>>, rin |-> 0] -Id(i, o) == IF WholeDocument THEN <> ELSE <> -VARIABLES phase, inputs, other, declared, recorded, caches, mounted, - staleMounted, dataMounted, needlessRebuild -vars == <> + DataAsCache, \* reselect retained run data newly declared as a cache + ShareWritable \* keep a cache with a writable consumer shared +Entry(k, id, i, w) == [kind |-> k, id |-> id, rin |-> i, rw |-> w] +None == Entry("none", <<0, 0, "none">>, 0, FALSE) +Scope(w) == IF w /\ ~ShareWritable THEN "here" ELSE "shared" +Id(i, o, w) == <> +VARIABLES phase, inputs, other, writable, declared, recorded, caches, tainted, + mounted, staleMounted, dataMounted, needlessRebuild, foreignMounted +vars == <> +flags == <> -\* A first admission populated the cache for the initial inputs. +\* A first admission populated the cache for the initial inputs; it was shared. Init == /\ phase = "stopped" - /\ inputs = 1 /\ other = 1 /\ declared = "cache" - /\ recorded = [kind |-> "cache", id |-> Id(1, 1), rin |-> 1] - /\ caches = {Id(1, 1)} + /\ inputs = 1 /\ other = 1 /\ writable = FALSE /\ declared = "cache" + /\ recorded = Entry("cache", Id(1, 1, FALSE), 1, FALSE) + /\ caches = {Id(1, 1, FALSE)} + /\ tainted = {} /\ mounted = None - /\ staleMounted = FALSE /\ dataMounted = FALSE /\ needlessRebuild = FALSE + /\ staleMounted = FALSE /\ dataMounted = FALSE + /\ needlessRebuild = FALSE /\ foreignMounted = FALSE -\* Edits between ups: the cache's own inputs, anything else, or whether the key -\* is declared as a cache at all. +\* Edits between ups: the cache's own inputs, anything else, a writable consumer +\* added or removed, or whether the key is declared as a cache at all. EditInputs(v) == /\ phase = "stopped" /\ v # inputs /\ inputs' = v - /\ UNCHANGED <> + /\ UNCHANGED <> EditOther(v) == /\ phase = "stopped" /\ v # other /\ other' = v - /\ UNCHANGED <> + /\ UNCHANGED <> +EditConsumer == /\ phase = "stopped" /\ writable' = ~writable + /\ UNCHANGED <> EditDeclaration == /\ phase = "stopped" /\ declared' = IF declared = "cache" THEN "data" ELSE "cache" - /\ UNCHANGED <> + /\ UNCHANGED <> + +\* Another instance whose writable consumer runs with any inputs writes into the +\* cache it selects. Its own instance-scoped identity is never "here". +ForeignWrite(v, o) == + LET id == <> IN + /\ tainted' = tainted \cup {id} + /\ caches' = caches \cup {id} + /\ UNCHANGED <> \* plan_reconcile::Verified::project then Session::create_resources: keep a -\* recorded cache of the same identity; otherwise select that identity's shared -\* cache (adopt or create; the initializer populates it) and release the old +\* recorded cache of the same identity; otherwise select that identity's cache +\* (adopt or create; the initializer populates it) and release the old \* reference. Retained run data declared as a cache is refused. UpCache == - LET want == Id(inputs, other) - entry == [kind |-> "cache", id |-> want, rin |-> inputs] IN + LET want == Id(inputs, other, writable) + entry == Entry("cache", want, inputs, writable) IN /\ phase = "stopped" /\ declared = "cache" /\ IF recorded.kind = "data" THEN IF DataAsCache THEN /\ phase' = "running" /\ mounted' = recorded /\ dataMounted' = TRUE - /\ UNCHANGED <> - ELSE UNCHANGED <> + /\ UNCHANGED <> + ELSE UNCHANGED <> ELSE IF recorded.kind = "cache" /\ (recorded.id = want \/ KeepStale) THEN /\ phase' = "running" /\ mounted' = recorded /\ staleMounted' = (staleMounted \/ recorded.rin # inputs) + /\ foreignMounted' = (foreignMounted \/ recorded.id \in tainted) /\ UNCHANGED <> ELSE /\ phase' = "running" /\ mounted' = entry /\ recorded' = entry /\ caches' = caches \cup {want} /\ needlessRebuild' = (needlessRebuild \/ (recorded.kind = "cache" /\ recorded.rin = inputs - /\ want \notin caches)) + /\ recorded.rw = writable /\ want \notin caches)) + /\ foreignMounted' = (foreignMounted \/ want \in tainted) /\ UNCHANGED <> - /\ UNCHANGED <> + /\ UNCHANGED <> \* The key is ordinary run data: reattach recorded data, or create fresh run data \* when it was a cache (whose shared volume is only released, never deleted). @@ -73,21 +96,21 @@ UpData == /\ phase = "stopped" /\ declared = "data" /\ phase' = "running" /\ recorded' = IF recorded.kind = "data" THEN recorded - ELSE [kind |-> "data", id |-> <<0, 0>>, rin |-> 0] + ELSE Entry("data", <<0, 0, "none">>, 0, FALSE) /\ mounted' = recorded' - /\ UNCHANGED <> + /\ UNCHANGED <> Stop == /\ phase = "running" /\ phase' = "stopped" /\ mounted' = None - /\ UNCHANGED <> + /\ UNCHANGED <> Next == \/ \E v \in Values : EditInputs(v) \/ EditOther(v) - \/ EditDeclaration \/ UpCache \/ UpData \/ Stop + \/ \E v, o \in Values : ForeignWrite(v, o) + \/ EditConsumer \/ EditDeclaration \/ UpCache \/ UpData \/ Stop Spec == Init /\ [][Next]_vars TypeOK == /\ phase \in {"stopped", "running"} - /\ inputs \in Values /\ other \in Values + /\ inputs \in Values /\ other \in Values /\ writable \in BOOLEAN /\ declared \in {"cache", "data"} /\ recorded.kind \in {"none", "cache", "data"} /\ mounted.kind \in {"none", "cache", "data"} @@ -98,7 +121,9 @@ CacheMatchesInputs == /\ ~staleMounted mounted.rin = inputs \* Run-owned data is never mounted as a shared cache. NoDataAsCache == ~dataMounted -\* An edit that leaves the cache's own inputs unchanged keeps the cache: it never -\* selects a not-yet-populated cache for the same inputs. +\* An edit that leaves the cache's own inputs and consumers unchanged keeps the +\* cache: it never selects a not-yet-populated cache for the same inputs. UnrelatedEditKeepsCache == ~needlessRebuild +\* A cache that another instance's writable consumer wrote is never mounted here. +NoForeignWrites == ~foreignMounted ============================================================================= diff --git a/tests/models/tla/native-cache-reconcile/data-as-cache.cfg b/tests/models/tla/native-cache-reconcile/data-as-cache.cfg index 2c5f19a6f..4dd13de17 100644 --- a/tests/models/tla/native-cache-reconcile/data-as-cache.cfg +++ b/tests/models/tla/native-cache-reconcile/data-as-cache.cfg @@ -1,4 +1,4 @@ SPECIFICATION Spec CONSTANTS Values = {1, 2} - WholeDocument = FALSE KeepStale = FALSE DataAsCache = TRUE -INVARIANTS TypeOK CacheMatchesInputs NoDataAsCache UnrelatedEditKeepsCache + WholeDocument = FALSE KeepStale = FALSE DataAsCache = TRUE ShareWritable = FALSE +INVARIANTS TypeOK CacheMatchesInputs NoDataAsCache UnrelatedEditKeepsCache NoForeignWrites diff --git a/tests/models/tla/native-cache-reconcile/negative.cfg b/tests/models/tla/native-cache-reconcile/negative.cfg index d8c5edf62..bdd5118ab 100644 --- a/tests/models/tla/native-cache-reconcile/negative.cfg +++ b/tests/models/tla/native-cache-reconcile/negative.cfg @@ -1,4 +1,4 @@ SPECIFICATION Spec CONSTANTS Values = {1, 2} - WholeDocument = TRUE KeepStale = FALSE DataAsCache = FALSE -INVARIANTS TypeOK CacheMatchesInputs NoDataAsCache UnrelatedEditKeepsCache + WholeDocument = TRUE KeepStale = FALSE DataAsCache = FALSE ShareWritable = FALSE +INVARIANTS TypeOK CacheMatchesInputs NoDataAsCache UnrelatedEditKeepsCache NoForeignWrites diff --git a/tests/models/tla/native-cache-reconcile/poison.cfg b/tests/models/tla/native-cache-reconcile/poison.cfg new file mode 100644 index 000000000..f2aea6d89 --- /dev/null +++ b/tests/models/tla/native-cache-reconcile/poison.cfg @@ -0,0 +1,4 @@ +SPECIFICATION Spec +CONSTANTS Values = {1, 2} + WholeDocument = FALSE KeepStale = FALSE DataAsCache = FALSE ShareWritable = TRUE +INVARIANTS TypeOK CacheMatchesInputs NoDataAsCache UnrelatedEditKeepsCache NoForeignWrites diff --git a/tests/models/tla/native-cache-reconcile/positive.cfg b/tests/models/tla/native-cache-reconcile/positive.cfg index cbcf0c537..1235af9d0 100644 --- a/tests/models/tla/native-cache-reconcile/positive.cfg +++ b/tests/models/tla/native-cache-reconcile/positive.cfg @@ -1,4 +1,4 @@ SPECIFICATION Spec CONSTANTS Values = {1, 2} - WholeDocument = FALSE KeepStale = FALSE DataAsCache = FALSE -INVARIANTS TypeOK CacheMatchesInputs NoDataAsCache UnrelatedEditKeepsCache + WholeDocument = FALSE KeepStale = FALSE DataAsCache = FALSE ShareWritable = FALSE +INVARIANTS TypeOK CacheMatchesInputs NoDataAsCache UnrelatedEditKeepsCache NoForeignWrites diff --git a/tests/models/tla/native-cache-reconcile/stale.cfg b/tests/models/tla/native-cache-reconcile/stale.cfg index cc68f47cd..086641289 100644 --- a/tests/models/tla/native-cache-reconcile/stale.cfg +++ b/tests/models/tla/native-cache-reconcile/stale.cfg @@ -1,4 +1,4 @@ SPECIFICATION Spec CONSTANTS Values = {1, 2} - WholeDocument = FALSE KeepStale = TRUE DataAsCache = FALSE -INVARIANTS TypeOK CacheMatchesInputs NoDataAsCache UnrelatedEditKeepsCache + WholeDocument = FALSE KeepStale = TRUE DataAsCache = FALSE ShareWritable = FALSE +INVARIANTS TypeOK CacheMatchesInputs NoDataAsCache UnrelatedEditKeepsCache NoForeignWrites