From f6a29c8efd8dd882e46e5eeaba37738fb8a5dd10 Mon Sep 17 00:00:00 2001 From: Petr Date: Sat, 26 Sep 2026 02:25:58 +0200 Subject: [PATCH] test(sync): formal verification pilot of the sync engine (#792) TLA+ model (TLC) and Lean 4 model of the sync pull/diff/push decision logic, plus one pytest per consolidated finding (A-K) replayed against the real SyncService. Reproduced bugs are strict xfail tests; remove the marker when the fix lands. Models are documentation, not a CI gate. --- formal/sync/README.md | 119 +++ formal/sync/lean/.gitignore | 1 + formal/sync/lean/SyncModel.lean | 11 + formal/sync/lean/SyncModel/Diff.lean | 445 +++++++++++ formal/sync/lean/SyncModel/Pull.lean | 211 +++++ formal/sync/lean/lake-manifest.json | 6 + formal/sync/lean/lakefile.toml | 5 + formal/sync/lean/lean-toolchain | 1 + formal/sync/tla/.gitignore | 4 + formal/sync/tla/SyncEngine.cfg | 20 + formal/sync/tla/SyncEngine.tla | 569 +++++++++++++ formal/sync/tla/run_all.sh | 20 + formal/sync/tla/run_one.sh | 29 + formal/sync/tla/trace.py | 73 ++ tests/test_sync_formal_counterexamples.py | 923 ++++++++++++++++++++++ 15 files changed, 2437 insertions(+) create mode 100644 formal/sync/README.md create mode 100644 formal/sync/lean/.gitignore create mode 100644 formal/sync/lean/SyncModel.lean create mode 100644 formal/sync/lean/SyncModel/Diff.lean create mode 100644 formal/sync/lean/SyncModel/Pull.lean create mode 100644 formal/sync/lean/lake-manifest.json create mode 100644 formal/sync/lean/lakefile.toml create mode 100644 formal/sync/lean/lean-toolchain create mode 100644 formal/sync/tla/.gitignore create mode 100644 formal/sync/tla/SyncEngine.cfg create mode 100644 formal/sync/tla/SyncEngine.tla create mode 100755 formal/sync/tla/run_all.sh create mode 100755 formal/sync/tla/run_one.sh create mode 100755 formal/sync/tla/trace.py create mode 100644 tests/test_sync_formal_counterexamples.py diff --git a/formal/sync/README.md b/formal/sync/README.md new file mode 100644 index 000000000..df9d8cd01 --- /dev/null +++ b/formal/sync/README.md @@ -0,0 +1,119 @@ +# Formal models of the `kbagent sync` engine (issue #792) + +Pilot: can a small model checker find real bugs in `sync pull | diff | push`? +`tla/` holds a TLA+ model checked with TLC. `lean/` is a separate Lean +effort, not covered here. + +## What the TLA+ model covers + +`tla/SyncEngine.tla` is a small finite model of the engine. Every operator +names the Python function and line range it mirrors. + +- **Remote**: 2 branches (`prod`, plus `dev` as a copy of prod). There are + 2 initial config ids, and 2 more ids for configs created during the run. + Content versions are 0..2. One component (`mcp`) can become ignored. +- **Local**: 2 trees (`main/`, `devt/`) and 5 directory paths. Each + `_config.yml` is a record with fields for the component, the id, the name + and the content. It also carries two abstract bits: + - `cosm`: a byte-only edit. It changes the RAW sha256 (`pull_hash`) but + not `config_hash`. + - `drift`: the local form of the content hashes differently from the + API's view of the same content (#686). +- **Manifest**: one entry per id: `branchId`, `path`, `componentId`, + `pull_hash` (the RAW hash) and `pull_config_hash` (the normalized base). +- **Actors**: + - **User**: edit content, cosmetic edit, `rm -rf` a directory, + `config new` scaffold, `config new --push --output-dir`, mark a + component ignored. + - **Remote**: edit, delete (trash looks the same to sync), create a + config, optionally reusing an existing config's name. + - **Sync**: `sync pull` (plain / `--force` / `--theirs`), `sync push`, and + `sync push` aborted by `ENCRYPTION_FAILED` after some of its changes + were already applied. Any of these can use `--branch` for either + branch, which also covers `branch use`. + - `diff` is a pure function that every invariant can call. +- **Ghost fields**, used only by invariants: + - lineage (which config a file or remote config descends from); + - `ed`: the file holds work that is on no remote; + - `sv`: the remote version the file was last synced with; + - the user-deleted directories; + - flags for the last operation. + +**Abstracted away**: +- rows, so I10 is not checked; +- renames and the name-collision suffix (a pull where two configs land on + one path is disabled); +- `config_hash_version` / legacy-shape migration; +- companion code files; +- dry-run; +- baseline read-back failures; +- variable and flow-task backfill. + +The id pool is bounded: a push that needs more new ids than are free is +disabled. `PushAbort` applies an arbitrary strict prefix of the changes in +path/id order. That over-approximates the diff order the code uses. + +## How to run + +The model needs Java 17 and `tla2tools.jar`. + +```sh +cd formal/sync/tla +java -XX:+UseParallelGC -cp ~/tools/tla/tla2tools.jar tlc2.TLC -workers auto \ + -config SyncEngine.cfg SyncEngine.tla # clean run: invariants that hold +./run_all.sh # every invariant, one TLC run each (~15 min) +./trace.py out/.json # compact counterexample +``` + +The depth is bounded by `MaxSteps` (a state constraint). `MaxSteps = 4` +explores traces of up to 5 actions. BFS returns the shortest counterexample. + +## Results (MaxSteps = 4; up to 153k distinct states per run) + +| Invariant | Result | +|---|---| +| I3 ignored component never planned | **holds** (153,077 states; 196,569 at depth 5 on prod only) | +| I4 diff/push act only on the source tree | **holds** (153,077 states) | +| I7 never-fetched entry never deleted | **holds** (104,809 states, never-fetched initial entry) | +| I1 no double create | violated: a promote push re-creates configs on every run; a resurrect followed by an `ENCRYPTION_FAILED` abort also creates a copy | +| I2 push deletes only user-removed dirs | violated: **pull's stale-entry sweep deletes a directory the same pull just wrote, and the next push deletes the live remote config** | +| I2b delete requires `--force` | violated: `push()` never reads `force` (S1) | +| I5 pull keeps local work | violated: a remote delete plus a local edit ends with plain or `--force` pull deleting the edited directory silently | +| I6 push then diff is clean | violated on `--branch` promote. Holds on production only (30,334 states) | +| I8 manifest matches disk | violated: the stale sweep, and a promote write-back that records a `devt/` entry for a file in `main/` | +| I9 an aborted push is atomic | violated (strong reading): the changes before the failing one reached the API and the manifest was never saved | +| I11 no lost remote update | violated: an adopted file with a config id is diffed 2-way, so push reverts a UI edit | +| I11b no silent resurrect | violated: a remote delete followed by any push re-creates the config, even with no local edit (S2) | +| I12 a pull resolves REMOTE MODIFIED | violated: after a cosmetic edit, plain pull skips the file forever and `--force` raises a conflict (S3) | + +Each violation was checked against the code. The main ones were replayed +against the real `SyncService` with a stateful fake API (the scratch harness +from the #792 pilot). Details are in the pilot report. + +## Consolidated findings (A..K) + +The spec's suspicious spots (S1..S5), the Lean refutations (F1..F8) and the +TLA+ counterexamples (I1..I12) overlap heavily -- several independently +rediscover the same code path. This table is the deduplicated result, with +the regression test for each in `tests/test_sync_formal_counterexamples.py`. + +| ID | Finding | Sources | Severity | Test | +|----|---------|---------|----------|------| +| A | Remote delete + recreate under the same name: pull writes the new config into the old directory, the stale sweep then deletes that directory; the next push DELETEs the live new config | Lean F8, TLA I2 | HIGH | `test_a_recreate_under_same_name_does_not_delete_new_config` | +| B | Pull compares only `_config.yml`: local edits in `transform.sql`/`code.py`/`_description.md` are silently overwritten when the remote changed, no SYNC_CONFLICT | Lean F6 | HIGH | `test_b_pull_never_overwrites_local_sql_edit` | +| C | Remote delete + local edit: pull (plain/`--force`) deletes the locally-edited directory with no conflict | Lean F7, TLA I5 | HIGH | `test_c_pull_never_deletes_locally_edited_dir_on_remote_delete` | +| D | `sync push --branch dev` (promote) creates another dev copy of a prod-only config on every push | TLA I6/I1 | HIGH | `test_d_promote_push_is_idempotent` | +| E | An untracked file carrying a config id (`config new --push --output-dir` scaffold / adopted orphan) is diffed 2-way: push overwrites a UI edit made after the scaffold was written | TLA I11 | MED | `test_e_adopted_scaffold_push_does_not_overwrite_remote_edit` | +| F | A push aborted by `ENCRYPTION_FAILED` leaves the manifest unsaved; the retry duplicates the change(s) the aborted push already applied | TLA I1b (model trace only; replayed live for this pilot) | MED | `test_f_aborted_push_does_not_duplicate_already_created_config` | +| G | `sync push` deletes remote configs with no `--force`; the CLI help text says `--force` gates deletion (soft delete to trash since 0.89.0, restorable) | Spec S1, Lean F1, TLA I2b | MED (product decision) | `test_g_push_without_force_does_not_delete_remote_config` | +| H | A config deleted remotely by another actor is silently re-created by the next push, no warning | Spec S2, Lean F2, TLA I11b | MED | `test_h_push_does_not_silently_resurrect_deleted_config` | +| I | Moving a config's directory by hand (`mv`/`git mv`) is seen as remote DELETE + CREATE under a new id | Lean F3 | LOW-MED | `test_i_moving_config_dir_is_not_delete_plus_create` | +| J | `sync pull --branch dev` reports untouched production configs as "removed" | Spec S4 | LOW | `test_j_branch_scoped_pull_does_not_report_other_branch_configs_removed` | +| K | A cosmetic local edit (raw vs normalized hash) blocks pull from ever applying a real remote change; `--force` raises a conflict | Spec S3, TLA I12 | LOW (documented, conservative behavior) | `test_k_cosmetic_edit_is_conservative_not_unsafe` (unmarked regression guard, not xfail) | + +A..F, H and I reproduce on current code and are `xfail(strict=True)` -- +flipping to a hard failure the moment a fix lands is the point: delete the +`xfail` marker to adopt the fix. G is kept `xfail` too even though the fix +direction is a product decision (see the test's docstring). J reproduces and +is `xfail`. K is deliberate, documented behavior, so it is an ordinary +(unmarked) regression guard instead. diff --git a/formal/sync/lean/.gitignore b/formal/sync/lean/.gitignore new file mode 100644 index 000000000..01f8cdb63 --- /dev/null +++ b/formal/sync/lean/.gitignore @@ -0,0 +1 @@ +.lake/ diff --git a/formal/sync/lean/SyncModel.lean b/formal/sync/lean/SyncModel.lean new file mode 100644 index 000000000..8d83b4c09 --- /dev/null +++ b/formal/sync/lean/SyncModel.lean @@ -0,0 +1,11 @@ +/- +Formal-verification pilot for the kbagent sync engine (keboola/cli#792). + +Pure decision functions of `sync diff` / `sync push` / `sync pull`, modelled +per config key from the Python sources, plus safety theorems about them. +Core Lean only (no Mathlib). Refuted properties are kept as `Prop` +definitions and their NEGATION is proved with a concrete witness -- see +the `-- FINDING` comments and the pilot report. +-/ +import SyncModel.Diff +import SyncModel.Pull diff --git a/formal/sync/lean/SyncModel/Diff.lean b/formal/sync/lean/SyncModel/Diff.lean new file mode 100644 index 000000000..3216eec7c --- /dev/null +++ b/formal/sync/lean/SyncModel/Diff.lean @@ -0,0 +1,445 @@ +/- +Diff classification + push planning, per config key. + +Abstraction: one config key `(component_id, config_id)` on the TARGET branch. +Hashes are abstract `Nat`s standing for `config_hash(...)` values +(`diff_engine.py:142-145`); equal hash = equal normalized content. Row keys are +modelled separately at the end of the file. + +All line numbers refer to this worktree as of 2026-09-26. +-/ +namespace SyncModel + +/-- `ConfigChange.change_type` (`diff_engine.py:308-443`). `none` = unchanged. -/ +inductive Change where + | added | modified | remoteModified | conflict | deleted + deriving DecidableEq, Repr + +/-- 3-way compare of an entry whose id resolves on the remote. +Mirrors `diff_engine.py:377-402`: equal hashes -> skipped (`:379-381`); +no base -> 2-way fallback `local_changed=True, remote_changed=False` +(`:389-391`), i.e. `modified`; otherwise conflict / remote_modified / modified +(`:393-402`). -/ +def classifyExisting (lh rh : Nat) (base : Option Nat) : Option Change := + if lh = rh then none else + match base with + | none => some .modified + | some b => + if lh ≠ b ∧ rh ≠ b then some .conflict + else if rh ≠ b ∧ lh = b then some .remoteModified + else some .modified + +/-- One local entry fed to `compute_changeset`. +Mirrors `diff_engine.py:344-368`: no `config_id`, or id not in +`remote_configs` -> `added`; else `classifyExisting`. -/ +def classifyLocal (idKnown : Bool) (remote : Option Nat) (lh : Nat) (base : Option Nat) : + Option Change := + if idKnown then + match remote with + | none => some .added + | some rh => classifyExisting lh rh base + else some .added + +/-- Tail loop `diff_engine.py:417-441`: a remote key not seen among local +entries is `deleted` iff it is in `tracked_keys`. (`diff()` always passes a +non-`None` set, `sync_service.py:1455-1461`.) -/ +def sweep (remotePresent seen tracked : Bool) : Option Change := + if remotePresent && !seen && tracked then some .deleted else none + +/-- Partition of one manifest entry, `scope_manifest` `branch_scope.py:163-201`. -/ +inductive Part where + | dropped | neverFetched | inTree | orphaned + deriving DecidableEq, Repr + +/-- `branch_scope.py:163-201`: ignored component -> dropped (`:174-175`); +empty `pull_hash` and no `_config.yml` -> never_fetched (`:183-193`); +tree == source tree -> in_tree (`:197-199`); else orphaned (`:201-203`). -/ +def scopeEntry (ignored pullHashSet fileExists inSourceTree : Bool) : Part := + if ignored then .dropped + else if !pullHashSet && !fileExists then .neverFetched + else if inSourceTree then .inTree else .orphaned + +/-- `classify_untracked` verdicts (`branch_scope.py:63-65`). -/ +inductive Verdict where + | create | adopt | orphan + deriving DecidableEq, Repr + +/-- `classify_untracked`, `branch_scope.py:263-279`. `held` = claims by any +tree; `sameTreeClaim` = a claim from the source tree. -/ +def classifyUntracked (idKnown sameTreeClaim otherTreeClaim remoteHas : Bool) : Verdict := + if !idKnown then .create + else if sameTreeClaim then .create + else if remoteHas then .adopt + else if sameTreeClaim || otherTreeClaim then .orphan + else .create + +/-- The manifest entry for the key (at most one per key per tree). -/ +structure Entry where + pullHashSet : Bool -- `metadata.pull_hash` non-empty + fileExists : Bool -- `_config.yml` readable at `tree/cfg.path` (`sync_service.py:1325-1328`) + inSourceTree : Bool -- `branch_tree_path(cfg.branch_id) == source_branch_path` + localHash : Nat -- local_h: override hash or `config_hash(merged data)` (`:1364-1368`, `diff_engine.py:374-375`) + base : Option Nat -- `base_hashes[key]` (`sync_service.py:1440-1453`) + deriving DecidableEq + +/-- An untracked `_config.yml` in the source tree (`find_untracked_configs`, +`branch_scope.py:307-373`) whose `_keboola.component_id` is this key's component. +`idKnown` = its `_keboola.config_id` is this key's id (false = id-less file). -/ +structure Untracked where + idKnown : Bool + localHash : Nat + deriving DecidableEq + +/-- Everything `diff()` sees about one key. -/ +structure KeyWorld where + ignored : Bool -- component in `_effective_ignored_components` (`sync_service.py:468-480`) + entry : Option Entry + otherTreeClaim : Bool -- another (non-never-fetched) manifest entry for this key in ANOTHER tree + remote : Option Nat -- remote config on the target branch (hash), before the ignore filter + untracked : List Untracked + +/-- `remote_configs` skips ignored components (`sync_service.py:1279-1282`). -/ +def KeyWorld.effRemote (w : KeyWorld) : Option Nat := + if w.ignored then none else w.remote + +def KeyWorld.part (w : KeyWorld) : Option Part := + w.entry.map fun e => scopeEntry w.ignored e.pullHashSet e.fileExists e.inSourceTree + +/-- key ∈ `scope.tracked_keys` (`branch_scope.py:118-121`). -/ +def KeyWorld.inTree (w : KeyWorld) : Bool := w.part == some .inTree + +/-- claims held by another tree (`branch_scope.py:195`, orphaned entries claim too). -/ +def KeyWorld.otherClaim (w : KeyWorld) : Bool := + !w.ignored && (w.otherTreeClaim || w.part == some .orphaned) + +/-- A local config dict handed to `compute_changeset`. -/ +structure LocalCfg where + idKnown : Bool + lh : Nat + base : Option Nat + deriving DecidableEq + +/-- In-tree entry whose file is readable (`sync_service.py:1323-1376`). -/ +def trackedLocals (w : KeyWorld) : List LocalCfg := + match w.entry with + | some e => if w.inTree && e.fileExists then [⟨true, e.localHash, e.base⟩] else [] + | none => [] + +/-- Untracked walk, `sync_service.py:1382-1435`: ignored -> skipped (`:1391-1392`); +ORPHAN -> reported only (`:1411-1420`); CREATE -> id cleared (`:1421-1422`); +ADOPT -> keeps id. `base_hashes` is built only from `scope.in_tree` +(`:1443-1453`), and ADOPT implies no in-tree claim, so an adopted file has no base. -/ +def untrackedLocal (w : KeyWorld) (u : Untracked) : Option LocalCfg := + if w.ignored then none else + match classifyUntracked u.idKnown w.inTree w.otherClaim w.effRemote.isSome with + | .orphan => none + | .create => some ⟨false, u.localHash, none⟩ + | .adopt => some ⟨true, u.localHash, none⟩ + +def locals (w : KeyWorld) : List LocalCfg := + trackedLocals w ++ w.untracked.filterMap (untrackedLocal w) + +/-- `seen_remote_keys` membership for this key (`diff_engine.py:365-366`, `:371`). -/ +def seen (w : KeyWorld) : Bool := (locals w).any (·.idKnown) + +/-- The changes `diff()` emits for this key (config level). -/ +def diffKey (w : KeyWorld) : List Change := + (locals w).filterMap (fun l => classifyLocal l.idKnown w.effRemote l.lh l.base) ++ + (match sweep w.effRemote.isSome (seen w) w.inTree with + | some c => [c] + | none => []) + +/-- Remote API writes issued by push. -/ +inductive Action where + | create | update | delete + deriving DecidableEq, Repr + +/-- `sync_service.py:1620-1621` (pushable = added/modified/deleted) and the +Phase-A dispatch `:1726` / `:1786` / `:1826-1831`. `force` is accepted by +`push()` (`:1579`) but never read in its body -- modelled faithfully as unused. -/ +def pushAction (_force : Bool) : Change → Option Action + | .added => some .create + | .modified => some .update + | .deleted => some .delete + | _ => none + +def pushPlan (force : Bool) (w : KeyWorld) : List Action := + (diffKey w).filterMap (pushAction force) + +/-! ## Proved theorems -/ + +/-- T1: the 3-way compare emits nothing iff the hashes agree. -/ +theorem classifyExisting_none_iff (lh rh : Nat) (b : Option Nat) : + classifyExisting lh rh b = none ↔ lh = rh := by + unfold classifyExisting + by_cases h : lh = rh + · simp [h] + · simp only [h, ite_false, iff_false] + cases b with + | none => simp + | some b => + by_cases h1 : lh ≠ b ∧ rh ≠ b <;> by_cases h2 : rh ≠ b ∧ lh = b <;> simp [h1, h2] + +/-- T2..T5: the spec's classification table rows (`sync_model_spec.md` §3), each proved. -/ +theorem table_twoWay (lh rh : Nat) (h : lh ≠ rh) : + classifyExisting lh rh none = some .modified := by simp [classifyExisting, h] + +theorem table_remoteModified (lh rh b : Nat) (h : lh ≠ rh) (hl : lh = b) : + classifyExisting lh rh (some b) = some .remoteModified := by + subst hl; have : rh ≠ lh := fun e => h e.symm + simp [classifyExisting, h, this] + +theorem table_modified (lh rh b : Nat) (h : lh ≠ rh) (hl : lh ≠ b) (hr : rh = b) : + classifyExisting lh rh (some b) = some .modified := by + subst hr; simp [classifyExisting, h] + +theorem table_conflict (lh rh b : Nat) (h : lh ≠ rh) (hl : lh ≠ b) (hr : rh ≠ b) : + classifyExisting lh rh (some b) = some .conflict := by + simp [classifyExisting, h, hl, hr] + +/-- T6: the spec's "unreachable" row really is unreachable: L=B and R=B force L=R. -/ +theorem table_unreachable (lh rh b : Nat) (hl : lh = b) (hr : rh = b) : + classifyExisting lh rh (some b) = none := by + subst hl; subst hr; simp [classifyExisting] + +/-- T7 (3-way soundness): with a base, `modified` (the only push-UPDATE verdict) +implies the remote is still exactly at the base -- push never clobbers a +remote change it can see. -/ +theorem modified_with_base_sound (lh rh b : Nat) : + classifyExisting lh rh (some b) = some .modified → lh ≠ b ∧ rh = b := by + unfold classifyExisting + by_cases h : lh = rh + · simp [h] + · simp only [h, ite_false] + by_cases hl : lh = b <;> by_cases hr : rh = b <;> simp [hl, hr] + · subst hl; subst hr; exact absurd rfl h + +/-- T8: `conflict` only when both sides moved away from the base. -/ +theorem conflict_sound (lh rh : Nat) (b : Option Nat) : + classifyExisting lh rh b = some .conflict → ∃ b', b = some b' ∧ lh ≠ b' ∧ rh ≠ b' := by + unfold classifyExisting + by_cases h : lh = rh + · simp [h] + · cases b with + | none => simp [h] + | some b => + simp only [h, ite_false] + by_cases hl : lh = b <;> by_cases hr : rh = b <;> simp [hl, hr] + +theorem classifyLocal_ne_deleted (i : Bool) (r : Option Nat) (lh : Nat) (b : Option Nat) : + classifyLocal i r lh b ≠ some .deleted := by + unfold classifyLocal classifyExisting + cases i <;> cases r <;> simp + split <;> (try split) <;> (try split) <;> simp + +theorem inTree_spec (w : KeyWorld) : + w.inTree = true ↔ ∃ e, w.entry = some e ∧ w.ignored = false ∧ + e.inSourceTree = true ∧ (e.pullHashSet = true ∨ e.fileExists = true) := by + unfold KeyWorld.inTree KeyWorld.part scopeEntry + cases w.entry with + | none => simp + | some e => + cases hi : w.ignored <;> cases hp : e.pullHashSet <;> cases hf : e.fileExists <;> + cases hs : e.inSourceTree <;> simp [hp, hf, hs] + +/-- T9 (I2 as implemented + I7 + part of I4): a remote DELETE is planned only for +a key that is (a) of a non-ignored component, (b) tracked by a manifest entry in +the SOURCE tree, (c) whose `_config.yml` is gone, (d) that was materialized once +(non-empty pull_hash, so never_fetched entries are excluded), and (e) that exists +on the target remote. -/ +theorem deleted_requires (w : KeyWorld) (h : Change.deleted ∈ diffKey w) : + w.ignored = false ∧ ∃ e, w.entry = some e ∧ e.inSourceTree = true ∧ + e.fileExists = false ∧ e.pullHashSet = true ∧ w.remote.isSome = true := by + unfold diffKey at h + rcases List.mem_append.mp h with h1 | h2 + · obtain ⟨l, _, hl⟩ := List.mem_filterMap.mp h1 + exact absurd hl (classifyLocal_ne_deleted _ _ _ _) + · unfold sweep at h2 + split at h2 + · rename_i c hc + split at hc + · rename_i hcond + simp only [Bool.and_eq_true, Bool.not_eq_true'] at hcond + obtain ⟨⟨hr, hs⟩, ht⟩ := hcond + obtain ⟨e, he, hig, hsrc, hpf⟩ := (inTree_spec w).mp ht + have hfe : e.fileExists = false := by + cases hfx : e.fileExists + · rfl + · exfalso + have : seen w = true := by + unfold seen locals trackedLocals + simp [he, ht, hfx] + rw [this] at hs; exact Bool.noConfusion hs + refine ⟨hig, e, he, hsrc, hfe, ?_, ?_⟩ + · rcases hpf with hp | hp + · exact hp + · rw [hfe] at hp; exact Bool.noConfusion hp + · unfold KeyWorld.effRemote at hr; simpa [hig] using hr + · simp at hc + · simp at h2 + +/-- T10 (I7): a never-fetched manifest entry is never planned as a remote DELETE. -/ +theorem neverFetched_no_delete (w : KeyWorld) (e : Entry) (he : w.entry = some e) + (hp : e.pullHashSet = false) : Change.deleted ∉ diffKey w := by + intro h + obtain ⟨_, e', he', _, _, hp', _⟩ := deleted_requires w h + rw [he] at he'; cases he'; rw [hp] at hp'; exact Bool.noConfusion hp' + +/-- T11 (I3): an ignored component yields no change at all, hence no remote write +of any kind (create / update / delete). -/ +theorem ignored_no_changes (w : KeyWorld) (hi : w.ignored = true) : diffKey w = [] := by + have hr : w.effRemote = none := by simp [KeyWorld.effRemote, hi] + have ht : w.inTree = false := by + unfold KeyWorld.inTree KeyWorld.part scopeEntry + cases w.entry <;> simp [hi] + have hu : w.untracked.filterMap (untrackedLocal w) = [] := by + simp [List.filterMap_eq_nil_iff, untrackedLocal, hi] + have htl : trackedLocals w = [] := by + unfold trackedLocals; cases w.entry <;> simp [ht] + simp [diffKey, locals, htl, hu, sweep, hr, ht] + +theorem ignored_no_remote_write (w : KeyWorld) (f : Bool) (hi : w.ignored = true) : + pushPlan f w = [] := by + simp [pushPlan, ignored_no_changes w hi] + +/-- T12 (I4): an entry tracked only on ANOTHER branch's tree, with no untracked +file in the source tree, contributes nothing to the target branch's changeset. -/ +theorem otherTree_no_changes (w : KeyWorld) (e : Entry) (he : w.entry = some e) + (hs : e.inSourceTree = false) (hu : w.untracked = []) : diffKey w = [] := by + have ht : w.inTree = false := by + unfold KeyWorld.inTree KeyWorld.part scopeEntry + rw [he]; cases hi : w.ignored <;> cases hp : e.pullHashSet <;> cases hf : e.fileExists <;> simp [hp, hf, hs] + have htl : trackedLocals w = [] := by unfold trackedLocals; rw [he]; simp [ht] + simp [diffKey, locals, htl, hu, sweep, ht] + +/-- T13: an in-tree file untouched since pull (local hash = stored base) never +yields a pushable UPDATE/CONFLICT while its id still resolves remotely. -/ +theorem unchanged_existing_no_update (lh rh : Nat) : + classifyExisting lh rh (some lh) ≠ some .modified ∧ + classifyExisting lh rh (some lh) ≠ some .conflict := by + unfold classifyExisting + by_cases h : lh = rh + · simp [h] + · have : rh ≠ lh := fun e => h e.symm + simp [h, this] + +/-- T14: bounded output -- one verdict per local entry plus at most one delete. -/ +theorem diffKey_length_le (w : KeyWorld) : (diffKey w).length ≤ w.untracked.length + 2 := by + unfold diffKey + have h1 := List.length_filterMap_le (fun l => classifyLocal l.idKnown w.effRemote l.lh l.base) (locals w) + have h2 : (locals w).length ≤ w.untracked.length + 1 := by + unfold locals + have := List.length_filterMap_le (untrackedLocal w) w.untracked + have ht : (trackedLocals w).length ≤ 1 := by + unfold trackedLocals; split + · split <;> simp + · simp + simp only [List.length_append]; omega + have h3 : (match sweep w.effRemote.isSome (seen w) w.inTree with + | some c => [c] | none => []).length ≤ 1 := by split <;> simp + simp only [List.length_append]; omega + +/-! ## Refuted properties (FINDINGS). Statement kept, negation proved. -/ + +/-- A world: tracked in the source tree, directory removed, remote still there. -/ +def wDirDeleted : KeyWorld := + { ignored := false, + entry := some { pullHashSet := true, fileExists := false, inSourceTree := true, + localHash := 0, base := some 0 }, + otherTreeClaim := false, remote := some 0, untracked := [] } + +/-- F1 (spec S1). The CLI documents `sync push --force` as "Allow deletion of +remote configs that were removed locally" (`commands/sync.py:982-986`), i.e. +"without --force no remote DELETE". FALSE: `push()` never reads `force`. -/ +def DeleteRequiresForce : Prop := ∀ w, Action.delete ∉ pushPlan false w + +theorem deleteRequiresForce_refuted : ¬ DeleteRequiresForce := by + intro h; exact h wDirDeleted (by decide) + +/-- F2 (spec S2). "Push only sends LOCAL changes": a tracked config whose files +are untouched since pull never causes a remote write. FALSE: if another actor +deleted (or trashed) it remotely, `remote_key not in remote_configs` makes it +`added` (`diff_engine.py:355`) and push re-creates it under a new id. -/ +def UnchangedLocalNoWrite : Prop := + ∀ w e, w.entry = some e → e.fileExists = true → e.base = some e.localHash → + w.untracked = [] → pushPlan false w = [] + +def wRemoteGone : KeyWorld := + { ignored := false, + entry := some { pullHashSet := true, fileExists := true, inSourceTree := true, + localHash := 7, base := some 7 }, + otherTreeClaim := false, remote := none, untracked := [] } + +theorem unchangedLocalNoWrite_refuted : ¬ UnchangedLocalNoWrite := by + intro h + have := h wRemoteGone _ rfl rfl rfl rfl + revert this; decide + +/-- F3. "A config whose directory still exists in the source tree (e.g. after +`mv` / `git mv` to a new folder name) is never deleted remotely." FALSE: the old +path's entry has no file -> `deleted`; the moved copy carries the same id but is +claimed by the same-tree entry -> CREATE (`branch_scope.py:273-274`). Push +DELETEs the original and CREATEs a new id. -/ +def ContentPresentNoDelete : Prop := + ∀ w, (∃ u ∈ w.untracked, u.idKnown = true) → Action.delete ∉ pushPlan false w + +def wMovedDir : KeyWorld := + { wDirDeleted with untracked := [{ idKnown := true, localHash := 0 }] } + +theorem contentPresentNoDelete_refuted : ¬ ContentPresentNoDelete := by + intro h + exact h wMovedDir ⟨_, List.mem_singleton.mpr rfl, rfl⟩ (by decide) + +theorem movedDir_plan : pushPlan false wMovedDir = [.create, .delete] := by decide + +/-- F4. "Push issues at most one UPDATE per remote config." FALSE: two untracked +directories carrying the same `_keboola.config_id` that resolves remotely and is +claimed by no manifest entry both ADOPT (`branch_scope.py:275-276`), so the +fork-by-copy protection of #482/#497 does not apply and both PUT the same id; +the last one silently wins. -/ +def AtMostOneUpdate : Prop := + ∀ w, ((pushPlan false w).filter (· == .update)).length ≤ 1 + +def wTwoAdopts : KeyWorld := + { ignored := false, entry := none, otherTreeClaim := false, remote := some 5, + untracked := [{ idKnown := true, localHash := 1 }, { idKnown := true, localHash := 2 }] } + +theorem atMostOneUpdate_refuted : ¬ AtMostOneUpdate := by + intro h; have := h wTwoAdopts; revert this; decide + +/-- F5. "A push UPDATE only happens when the remote is still at the base the +local edit was made against" (the 3-way guarantee). FALSE for adopted untracked +files: they never have a base (2-way fallback, `diff_engine.py:389-391`), so a +remote edit made by someone else is overwritten without a `conflict`. (T7 shows +it DOES hold for tracked entries that have a base.) -/ +def UpdateOnlyAtBase : Prop := + ∀ w, ∀ l ∈ locals w, classifyLocal l.idKnown w.effRemote l.lh l.base = some .modified → + ∃ b, l.base = some b ∧ w.effRemote = some b + +def wAdoptRemoteMoved : KeyWorld := + { ignored := false, entry := none, otherTreeClaim := false, remote := some 9, + untracked := [{ idKnown := true, localHash := 1 }] } + +theorem updateOnlyAtBase_refuted : ¬ UpdateOnlyAtBase := by + intro h + obtain ⟨b, hb, _⟩ := h wAdoptRemoteMoved ⟨true, 1, none⟩ (by decide) (by decide) + cases hb + +/-! ## Rows (`compute_row_changeset`, `diff_engine.py:446-575`) -/ + +/-- Row-level delete for one row key: `tracked_row_keys` is filled only from +parents in `scope.in_tree` (`sync_service.py:1472-1476`); a row is `seen` iff +its parent is in-tree and its file is readable (`:1478-1490`); tail loop +`diff_engine.py:555-575`. -/ +def rowDeleted (parent : Part) (rowFileExists remoteRowPresent : Bool) : Bool := + let tracked := parent == .inTree + let seenRow := tracked && rowFileExists + remoteRowPresent && !seenRow && tracked + +/-- T15 (I10): a row delete is planned only when its parent is in the source tree +(never for never-fetched / other-branch / ignored parents). -/ +theorem rowDeleted_requires_parent_inTree (p : Part) (f r : Bool) : + rowDeleted p f r = true → p = .inTree := by + cases p <;> simp [rowDeleted] + +end SyncModel diff --git a/formal/sync/lean/SyncModel/Pull.lean b/formal/sync/lean/SyncModel/Pull.lean new file mode 100644 index 000000000..58b065200 --- /dev/null +++ b/formal/sync/lean/SyncModel/Pull.lean @@ -0,0 +1,211 @@ +/- +`sync pull` per-config decision (plain / --force / --theirs), and the +stale-entry sweep. Hashes are abstract `Nat`s: `curHash` / `pullHash` are RAW +sha256 values of `_config.yml`; `cfgBase` / `apiHash` are normalized +`config_hash` values. `dry_run` does not change the decision, only whether the +chosen write happens, so it is not modelled. +-/ +import SyncModel.Diff + +namespace SyncModel + +structure PullIn where + isNew : Bool -- key not in the old manifest (`sync_service.py:682`) + theirs : Bool + force : Bool + fileExists : Bool -- `_config.yml` present at the tracked path + pullHash : Option Nat -- stored `pull_hash` ("" = none) + curHash : Nat -- current raw hash of `_config.yml` + extrasChanged : Bool -- some `pull_extra_hashes` companion (transform.sql, code.py, ...) differs or is missing + shapeMigration : Bool -- `needs_shape_migration(...)` (`_sync_baseline.py:265-285`) + cfgBase : Option Nat -- effective stored `pull_config_hash` + apiHash : Nat -- `config_hash` of the freshly fetched remote + branchSwitched : Bool -- `sync_service.py:830-832` + typeRewrite : Bool -- data-app type rewrite (`:855-858`) + deriving DecidableEq, Repr + +inductive PullOut where + | abort -- SyncConflictError before any write + | preserve -- local files kept, old baseline kept + | skip -- idempotent, nothing written + | write -- `_config.yml` AND companion code files rewritten from remote + deriving DecidableEq, Repr + +/-- `_config.yml` differs from its recorded pull state (`sync_service.py:768-774`). -/ +def ymlModified (p : PullIn) : Bool := + match p.pullHash with + | some h => p.fileExists && decide (p.curHash ≠ h) + | none => false + +/-- Force-pull guard: `sync_service.py:654-667` calling `detect_force_pull_conflicts` +/ `_is_conflict` (`_sync_baseline.py:423-445`, `:447-507`). Only `_config.yml` is +hashed; brand-new remote configs are skipped (`:494-495`). -/ +def forceConflict (p : PullIn) : Bool := + p.force && !p.theirs && !p.isNew && + match p.pullHash, p.cfgBase with + | some h, some b => p.fileExists && decide (p.curHash ≠ h) && decide (p.apiHash ≠ b) + | _, _ => false + +/-- `locally_modified`, `sync_service.py:766-790`: only `_config.yml`, except +during a #686 shape migration where companions are checked too (`:780-790`). -/ +def locallyModified (p : PullIn) : Bool := + !p.isNew && !p.theirs && (ymlModified p || (p.shapeMigration && p.extrasChanged)) + +/-- `_local_files_match_pull_state`, `sync_service.py:442-465`. -/ +def bytesMatch (p : PullIn) : Bool := + match p.pullHash with + | some h => p.fileExists && decide (p.curHash = h) && !p.extrasChanged + | none => false + +/-- `remote_unchanged`, `sync_service.py:829-858`. -/ +def remoteUnchanged (p : PullIn) : Bool := + let r := !p.isNew && !p.branchSwitched && p.cfgBase == some p.apiHash && p.fileExists + let r := if p.theirs then r && bytesMatch p else r + r && !p.typeRewrite + +/-- Per-config pull decision, `sync_service.py:654-667` then `:792-871`. -/ +def pullDecide (p : PullIn) : PullOut := + if forceConflict p then .abort + else if locallyModified p then .preserve + else if remoteUnchanged p then .skip + else .write + +/-- Stale-entry sweep, `sync_service.py:1062-1094`: an OLD manifest entry whose +key is missing from this fetch gets `rmtree(branch_dir / old_cfg.path)` -- +unconditionally (no local-modification check, no --theirs check). -/ +def sweepRemovesDir (keyInFetch dirExists : Bool) : Bool := !keyInFetch && dirExists + +/-! ## Proved -/ + +/-- P1 (I5): `pull --force` aborts on a true conflict in `_config.yml`. -/ +theorem force_conflict_aborts (p : PullIn) (h b : Nat) + (hf : p.force = true) (ht : p.theirs = false) (hn : p.isNew = false) + (hp : p.pullHash = some h) (he : p.fileExists = true) (hc : p.curHash ≠ h) + (hb : p.cfgBase = some b) (ha : p.apiHash ≠ b) : pullDecide p = .abort := by + simp [pullDecide, forceConflict, hf, ht, hn, hp, hb, he, hc, ha] + +/-- P2: without --theirs an edited `_config.yml` of a tracked config is never +overwritten by pull (abort or preserve). -/ +theorem yml_edit_not_overwritten (p : PullIn) (ht : p.theirs = false) (hn : p.isNew = false) + (hm : ymlModified p = true) : pullDecide p = .abort ∨ pullDecide p = .preserve := by + unfold pullDecide + by_cases hc : forceConflict p = true + · simp [hc] + · have : locallyModified p = true := by simp [locallyModified, ht, hn, hm] + simp [hc, this] + +/-- P3: --theirs never preserves and never aborts (remote wins). -/ +theorem theirs_remote_wins (p : PullIn) (ht : p.theirs = true) : + pullDecide p = .skip ∨ pullDecide p = .write := by + have h1 : forceConflict p = false := by simp [forceConflict, ht] + have h2 : locallyModified p = false := by simp [locallyModified, ht] + unfold pullDecide; rw [h1, h2]; simp only [Bool.false_eq_true, ite_false] + split <;> simp + +/-- P4: under --theirs, an idempotent skip implies every tracked file is +byte-identical to its pull state (edited companions are re-materialized). -/ +theorem theirs_skip_requires_clean (p : PullIn) (ht : p.theirs = true) + (hs : pullDecide p = .skip) : bytesMatch p = true := by + have h1 : forceConflict p = false := by simp [forceConflict, ht] + have h2 : locallyModified p = false := by simp [locallyModified, ht] + unfold pullDecide at hs; rw [h1, h2] at hs + simp only [Bool.false_eq_true, ite_false] at hs + split at hs + · rename_i hr + simp only [remoteUnchanged, ht, ite_true, Bool.and_eq_true] at hr + exact hr.1.2 + · cases hs + +/-- P5: pull is idempotent -- nothing changed on either side => nothing written. -/ +theorem idempotent_skip (p : PullIn) (h : Nat) + (hn : p.isNew = false) (ht : p.theirs = false) (hp : p.pullHash = some h) + (he : p.fileExists = true) (hc : p.curHash = h) (hx : p.shapeMigration = false) + (hb : p.cfgBase = some p.apiHash) (hs : p.branchSwitched = false) (hty : p.typeRewrite = false) : + pullDecide p = .skip := by + simp [pullDecide, forceConflict, locallyModified, ymlModified, remoteUnchanged, + hn, ht, hp, he, hc, hx, hb, hs, hty] + +/-! ## Refuted (FINDINGS) -/ + +/-- F6. Documented: "Pull protects local edits: locally-modified files are +skipped by default" (sync-workflow.md "Key behaviors") and "--force: local +edited AND remote changed -> abort". Stated over ALL tracked files: FALSE. +Only `_config.yml` is compared, so an edit to `transform.sql` / `code.py` / +`_description.md` is overwritten whenever the remote changed -- by plain pull +AND by `pull --force` (no SYNC_CONFLICT). Acknowledged in a code comment +(`_sync_baseline.py:289-294`) but not in user docs. Reproduced against the real +SyncService (scratch repro R1). -/ +def PullNeverOverwritesLocalEdits : Prop := + ∀ p : PullIn, p.theirs = false → p.isNew = false → + (ymlModified p || p.extrasChanged) = true → pullDecide p ≠ .write + +/-- Only transform.sql edited; remote changed since the pull. -/ +def pSqlEdit (force : Bool) : PullIn := + { isNew := false, theirs := false, force := force, fileExists := true, + pullHash := some 1, curHash := 1, extrasChanged := true, shapeMigration := false, + cfgBase := some 10, apiHash := 11, branchSwitched := false, typeRewrite := false } + +theorem pullNeverOverwritesLocalEdits_refuted : ¬ PullNeverOverwritesLocalEdits := by + intro h; exact h (pSqlEdit false) rfl rfl rfl (by decide) + +theorem forcePull_sqlEdit_writes : pullDecide (pSqlEdit true) = .write := by decide + +/-- F7. Pull-side loss of a `_config.yml` edit, including the stale sweep: +"pull without --theirs never destroys an edited `_config.yml`". P2 proves it for +configs still on the remote; FALSE when the remote config was deleted: the sweep +`rmtree`s the edited directory (`sync_service.py:1078-1094`). Reproduced (R2). -/ +def PullNeverDeletesEditedDir : Prop := + ∀ (p : PullIn) (remoteDeleted : Bool), p.theirs = false → p.isNew = false → + ymlModified p = true → + (if remoteDeleted then sweepRemovesDir false p.fileExists else pullDecide p == .write) = false + +theorem pullNeverDeletesEditedDir_refuted : ¬ PullNeverDeletesEditedDir := by + intro h + have := h { pSqlEdit false with curHash := 2, extrasChanged := false } true rfl rfl (by decide) + revert this; decide + +/-- The same property restricted to configs still on the remote holds (= P2). -/ +theorem pullNeverDeletesEditedDir_liveRemote (p : PullIn) (ht : p.theirs = false) + (hn : p.isNew = false) (hm : ymlModified p = true) : (pullDecide p == .write) = false := by + rcases yml_edit_not_overwritten p ht hn hm with h | h <;> simp [h] + +/-! ### F8: same-name re-create -> fresh config deleted locally -> push DELETEs it + +`used_paths` is per-pull (`sync_service.py:724-728`) and never contains the +paths of OLD entries that disappeared from the fetch. When the remote config X +at path P was deleted and a NEW config Y of the same component with the same +name appears (UI delete + re-create, or a rename collision), Y is generated at +the same P and WRITTEN (`:862-871`); the sweep then `rmtree`s P for X +(`:1078-1094`), deleting Y's fresh files. Y stays in the manifest with a +non-empty pull_hash, so the next `diff` classifies Y `deleted` and `push` +DELETEs the config that was just created remotely. Reproduced (R3). -/ + +/-- Directory state at P after one pull: write loop first, sweep second. -/ +def dirAfterPull (writtenThisPull sweptOldEntryAtSamePath existedBefore : Bool) : Bool := + if sweptOldEntryAtSamePath then false else writtenThisPull || existedBefore + +/-- Y's manifest entry after the pull, when its generated path collides (or not) +with a vanished old entry's path. -/ +def yEntryAfterPull (collides : Bool) (h : Nat) : Entry := + { pullHashSet := true, fileExists := dirAfterPull true collides true, + inSourceTree := true, localHash := h, base := some h } + +def yWorld (collides : Bool) (h : Nat) : KeyWorld := + { ignored := false, entry := some (yEntryAfterPull collides h), otherTreeClaim := false, + remote := some h, untracked := [] } + +/-- "A config just brought in by `sync pull` and not touched locally is never +planned as a remote DELETE by the next push." -/ +def FreshPullNeverDeleted : Prop := + ∀ collides h, Action.delete ∉ pushPlan false (yWorld collides h) + +theorem freshPullNeverDeleted_refuted : ¬ FreshPullNeverDeleted := by + intro hf; exact hf true 0 (by decide) + +/-- Without a path collision the property holds. -/ +theorem freshPull_noCollision_safe (h : Nat) : pushPlan false (yWorld false h) = [] := by + simp [pushPlan, diffKey, locals, trackedLocals, yWorld, yEntryAfterPull, dirAfterPull, + KeyWorld.inTree, KeyWorld.part, scopeEntry, KeyWorld.effRemote, classifyLocal, + classifyExisting, seen, sweep] + +end SyncModel diff --git a/formal/sync/lean/lake-manifest.json b/formal/sync/lean/lake-manifest.json new file mode 100644 index 000000000..4b349cdd3 --- /dev/null +++ b/formal/sync/lean/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "SyncModel", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/formal/sync/lean/lakefile.toml b/formal/sync/lean/lakefile.toml new file mode 100644 index 000000000..5d6c49a35 --- /dev/null +++ b/formal/sync/lean/lakefile.toml @@ -0,0 +1,5 @@ +name = "SyncModel" +defaultTargets = ["SyncModel"] + +[[lean_lib]] +name = "SyncModel" diff --git a/formal/sync/lean/lean-toolchain b/formal/sync/lean/lean-toolchain new file mode 100644 index 000000000..ba8ebf2db --- /dev/null +++ b/formal/sync/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.34.1 diff --git a/formal/sync/tla/.gitignore b/formal/sync/tla/.gitignore new file mode 100644 index 000000000..b4d579003 --- /dev/null +++ b/formal/sync/tla/.gitignore @@ -0,0 +1,4 @@ +out/ +states/ +*_TTrace_*.tla +*_TTrace_*.bin diff --git a/formal/sync/tla/SyncEngine.cfg b/formal/sync/tla/SyncEngine.cfg new file mode 100644 index 000000000..9b3dc7ae4 --- /dev/null +++ b/formal/sync/tla/SyncEngine.cfg @@ -0,0 +1,20 @@ +\* Clean run: the invariants that HOLD on the current code (depth 4, every +\* actor enabled). Every other invariant has a genuine counterexample -- see +\* run_all.sh and ../README.md. I7 is re-checked with InitNeverFetched = TRUE +\* in run_all.sh (it is vacuous from this initial state). +CONSTANTS + MaxSteps = 4 + NV = 3 + InitNeverFetched = FALSE + MaxScaffolds = 1 + EnableAbort = TRUE + EnableRemote = TRUE + EnableIgnore = TRUE + EnableDev = TRUE +SPECIFICATION Spec +CONSTRAINT StepBound +INVARIANTS + TypeOK + I3_IgnoredUntouched + I4_BranchIsolation + I7_NeverFetchedNotDeleted diff --git a/formal/sync/tla/SyncEngine.tla b/formal/sync/tla/SyncEngine.tla new file mode 100644 index 000000000..7a1ef2c31 --- /dev/null +++ b/formal/sync/tla/SyncEngine.tla @@ -0,0 +1,569 @@ +---------------------------- MODULE SyncEngine ---------------------------- +(***************************************************************************) +(* Finite model of the kbagent GitOps sync engine (`kbagent sync *) +(* pull|diff|push`), issue keboola/cli#792. *) +(* *) +(* Every operator below mirrors a specific piece of the Python code; the *) +(* file:line references are to this repository at the time of writing: *) +(* services/sync_service.py pull() 482-1128, diff() 1232-1568, *) +(* push() 1574-1966, *) +(* _resolve_source_branch_path 2387-2420 *) +(* sync/diff_engine.py compute_changeset 308-443 *) +(* sync/branch_scope.py scope_manifest 133-211, *) +(* classify_untracked 244-279, *) +(* find_untracked_configs 307-373 *) +(* services/_sync_writeback.py stamp_created_config / stamp_updated_config*) +(* / writeback_create_config_in_manifest *) +(* services/_sync_baseline.py detect_force_pull_conflicts / _is_conflict *) +(* *) +(* Abstractions (see README.md): rows, renames, config_hash_version *) +(* migration, extra code files, dry-run, name-collision suffixes and *) +(* unstampable read-backs are not modelled. Content is a small integer; *) +(* the RAW file hash (sha256 of _config.yml bytes) and the NORMALIZED *) +(* config hash (config_hash) are separate abstract values. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets, Sequences, TLC + +CONSTANTS + MaxSteps, \* depth bound (state constraint) + NV, \* content versions 0..NV-1 + InitNeverFetched, \* TRUE: start with a legacy never-fetched entry for i1 + MaxScaffolds, \* how many `config new` scaffolds the user may create + EnableAbort, \* model ENCRYPTION_FAILED aborts inside push + EnableRemote, \* enable the concurrent remote actor + EnableIgnore, \* enable "component becomes ignored" + EnableDev \* allow operations against the dev branch + +Branches == {"prod", "dev"} +Trees == {"main", "devt"} +TreeOf(b) == IF b = "prod" THEN "main" ELSE "devt" +DefaultTree == "main" \* manifest.branches[0].path + +InitIds == {"i1", "i2"} +NewIds == {"n1", "n2"} +Ids == InitIds \cup NewIds +Paths == {"p1", "p2", "q1", "q2", "ps"} +DefPath(id) == CASE id = "i1" -> "p1" [] id = "i2" -> "p2" + [] id = "n1" -> "q1" [] id = "n2" -> "q2" +V == 0..(NV - 1) +IgnComp == "mcp" \* e.g. keboola.mcp-server-tool +Sids == {"s1", "s2"} \* lineage ids for scaffolded files + +OpBranches == IF EnableDev THEN Branches ELSE {"prod"} + +(* ---- value encodings (records always carry an `ex` flag so TLC never *) +(* compares values of different type) *) + +\* Local _config.yml. comp/cid/nm are the `_keboola` block + name (part of +\* the RAW bytes, stripped by normalization); v = logical content; +\* cosm = a byte-level-only difference (key order, whitespace, is_disabled: +\* false vs absent) that changes the RAW hash but not config_hash; +\* drift = the local representation hashes differently from the API's view +\* of the SAME logical content (#686: multi-statement script shape). +\* Ghost fields: sid = lineage (which remote config / scaffold this file +\* descends from), ed = holds user work not yet on any remote, sv = the +\* remote content version this file was last synced with (pull or push). +NoFile == [ex |-> FALSE, comp |-> "tx", cid |-> "none", nm |-> "p1", v |-> 0, + cosm |-> FALSE, drift |-> FALSE, sid |-> "none", ed |-> FALSE, sv |-> 99] + +\* Remote configuration on one branch. org = lineage of the local file / +\* remote actor that created it. +Absent == [ex |-> FALSE, v |-> 0, nm |-> "p1", comp |-> "tx", org |-> "none"] + +\* Hashes. RAW hash = everything in the file except ghost fields. +Raw(f) == <> +NoHash == <<"", "", "", 99, FALSE, FALSE>> +NormLocal(f) == <> \* config_hash(local file) +ApiH(r) == <> \* config_hash(api_config_to_local(remote)) +NoBase == <<99, FALSE>> + +\* ManifestConfiguration: branchId, path, componentId, metadata.pull_hash, +\* metadata.pull_config_hash. +NoEntry == [ex |-> FALSE, br |-> "prod", path |-> "p1", comp |-> "tx", + ph |-> NoHash, base |-> NoBase] + +NoOp == [kind |-> "init", b |-> "prod", wrote |-> {}, force |-> FALSE, + i2 |-> TRUE, i2b |-> TRUE, i3 |-> TRUE, i7 |-> TRUE, + lost |-> TRUE, resur |-> TRUE, loss |-> TRUE, abortWrites |-> {}] + +VARIABLES fl, mn, rm, ig, used, userDel, nextSid, lastOp, steps +vars == <> + +St == [fl |-> fl, mn |-> mn, rm |-> rm, ig |-> ig, used |-> used] + +(***************************************************************************) +(* diff() -- pure function of the state *) +(***************************************************************************) +Ign(st) == IF st.ig THEN {IgnComp} ELSE {} + +\* _resolve_source_branch_path (sync_service.py:2387-2420): the target +\* branch's tree if it holds any config, else the default tree (promote). +Src(st, b) == IF \E p \in Paths : st.fl[TreeOf(b)][p].ex THEN TreeOf(b) ELSE DefaultTree + +\* remote_configs, ignored components filtered (sync_service.py:1281-1282) +RKeys(st, b) == {id \in Ids : st.rm[b][id].ex /\ st.rm[b][id].comp \notin Ign(st)} + +\* scope_manifest (branch_scope.py:164-199) +Live(st) == {id \in Ids : st.mn[id].ex /\ st.mn[id].comp \notin Ign(st)} +EntryTree(st, id) == TreeOf(st.mn[id].br) +NeverFetched(st) == {id \in Live(st) : st.mn[id].ph = NoHash + /\ ~st.fl[EntryTree(st, id)][st.mn[id].path].ex} +Claimed(st) == Live(st) \ NeverFetched(st) +InTree(st, S) == {id \in Claimed(st) : EntryTree(st, id) = S} + +\* find_untracked_configs (branch_scope.py:331-371): tracked_paths is built +\* from ALL manifest entries (ignored and never-fetched included). +TrackedPaths(st, S) == {st.mn[id].path : id \in {i \in Ids : st.mn[i].ex /\ EntryTree(st, i) = S}} +Untracked(st, S) == {p \in Paths : st.fl[S][p].ex /\ p \notin TrackedPaths(st, S) + /\ st.fl[S][p].comp \notin Ign(st)} \* :1394 + +\* classify_untracked (branch_scope.py:244-279) +Verdict(st, b, S, p) == + LET cid == st.fl[S][p].cid + claims == IF cid \in Claimed(st) THEN {EntryTree(st, cid)} ELSE {} + IN IF cid = "none" THEN "create" + ELSE IF S \in claims THEN "create" + ELSE IF cid \in RKeys(st, b) THEN "adopt" + ELSE IF claims # {} THEN "orphan" + ELSE "create" + +\* in-tree locals (sync_service.py:1320-1384) + base_hashes (:1441-1452) +Unchanged(st, S, id) == st.mn[id].ph # NoHash /\ Raw(st.fl[S][st.mn[id].path]) = st.mn[id].ph +TrackedLocals(st, S) == + { [id |-> id, path |-> st.mn[id].path, trk |-> TRUE, + base |-> IF st.mn[id].base # NoBase THEN st.mn[id].base + ELSE IF Unchanged(st, S, id) THEN NormLocal(st.fl[S][st.mn[id].path]) + ELSE NoBase, + lh |-> IF Unchanged(st, S, id) /\ st.mn[id].base # NoBase THEN st.mn[id].base + ELSE NormLocal(st.fl[S][st.mn[id].path])] + : id \in {i \in InTree(st, S) : st.fl[S][st.mn[i].path].ex} } + +UntrackedLocals(st, b, S) == + { [id |-> IF Verdict(st, b, S, p) = "adopt" THEN st.fl[S][p].cid ELSE "none", + path |-> p, trk |-> FALSE, base |-> NoBase, lh |-> NormLocal(st.fl[S][p])] + : p \in {q \in Untracked(st, S) : Verdict(st, b, S, q) # "orphan"} } + +Locals(st, b) == LET S == Src(st, b) IN TrackedLocals(st, S) \cup UntrackedLocals(st, b, S) + +\* compute_changeset (diff_engine.py:352-402) +Kind(st, b, le) == + IF le.id = "none" \/ le.id \notin RKeys(st, b) THEN "added" + ELSE LET rh == ApiH(st.rm[b][le.id]) IN + IF le.lh = rh THEN "none" + ELSE IF le.base = NoBase THEN "modified" + ELSE LET lc == le.lh # le.base + rc == rh # le.base + IN IF lc /\ rc THEN "conflict" + ELSE IF rc THEN "remote_modified" + ELSE "modified" + +\* diff_engine.py:417-441: tracked (in-tree) remote keys no local entry saw +Deleted(st, b) == + LET S == Src(st, b) + seen == {le.id : le \in Locals(st, b)} + IN {id \in RKeys(st, b) \cap InTree(st, S) : id \notin seen} + +Changes(st, b) == + LET S == Src(st, b) IN + { [kind |-> Kind(st, b, le), id |-> le.id, path |-> le.path, trk |-> le.trk, + comp |-> st.fl[S][le.path].comp, base |-> le.base] + : le \in {l \in Locals(st, b) : Kind(st, b, l) # "none"} } + \cup + { [kind |-> "deleted", id |-> id, path |-> st.mn[id].path, trk |-> TRUE, + comp |-> st.mn[id].comp, base |-> st.mn[id].base] : id \in Deleted(st, b) } + +Pushable(st, b) == {c \in Changes(st, b) : c.kind \in {"added", "modified", "deleted"}} +KindOf(st, b, id) == + LET cs == {c \in Changes(st, b) : c.id = id} IN + IF cs = {} THEN "none" ELSE (CHOOSE c \in cs : TRUE).kind + +(***************************************************************************) +(* pull() -- sync_service.py:482-1128 *) +(***************************************************************************) +PPathFor(st, b, id) == IF st.mn[id].ex THEN st.mn[id].path ELSE st.rm[b][id].nm +PFile(st, b, id) == st.fl[TreeOf(b)][PPathFor(st, b, id)] + +\* :767-774 +LocMod(st, b, mode, id) == + /\ st.mn[id].ex /\ mode # "theirs" /\ st.mn[id].ph # NoHash + /\ PFile(st, b, id).ex /\ Raw(PFile(st, b, id)) # st.mn[id].ph +\* :829-850 +RemUnch(st, b, mode, id) == + /\ st.mn[id].ex /\ st.mn[id].br = b /\ st.mn[id].base # NoBase + /\ st.mn[id].base = ApiH(st.rm[b][id]) /\ PFile(st, b, id).ex + /\ (mode = "theirs" => Raw(PFile(st, b, id)) = st.mn[id].ph) +Written(st, b, mode, id) == ~LocMod(st, b, mode, id) /\ ~RemUnch(st, b, mode, id) +PulledFile(st, b, id) == + LET r == st.rm[b][id] IN + [ex |-> TRUE, comp |-> r.comp, cid |-> id, nm |-> r.nm, v |-> r.v, + cosm |-> FALSE, drift |-> FALSE, sid |-> r.org, ed |-> FALSE, sv |-> r.v] +\* :990-1051 +PEntry(st, b, mode, id) == + IF LocMod(st, b, mode, id) + THEN [ex |-> TRUE, br |-> b, path |-> PPathFor(st, b, id), comp |-> st.rm[b][id].comp, + ph |-> st.mn[id].ph, base |-> st.mn[id].base] + ELSE [ex |-> TRUE, br |-> b, path |-> PPathFor(st, b, id), comp |-> st.rm[b][id].comp, + ph |-> IF Written(st, b, mode, id) THEN Raw(PulledFile(st, b, id)) + ELSE Raw(PFile(st, b, id)), + base |-> ApiH(st.rm[b][id])] + +\* detect_force_pull_conflicts / _is_conflict (_sync_baseline.py:423-529) +ForceConflict(st, b) == + \E id \in RKeys(st, b) : + /\ st.mn[id].ex /\ st.mn[id].ph # NoHash /\ st.mn[id].base # NoBase + /\ PFile(st, b, id).ex + /\ Raw(PFile(st, b, id)) # st.mn[id].ph + /\ ApiH(st.rm[b][id]) # st.mn[id].base + +\* two fetched configs landing on one path: the code appends an id suffix +\* (:726-729); not modelled -- such pulls are disabled. +PullPathsDistinct(st, b) == + \A x, y \in RKeys(st, b) : x # y => PPathFor(st, b, x) # PPathFor(st, b, y) + +\* stale-entry sweep (:1053-1094): against the WHOLE old manifest, rmtree +\* under the pulled branch's tree, AFTER the fetch loop wrote its files. +Stale(st, b) == {id \in Ids : st.mn[id].ex /\ id \notin RKeys(st, b)} +StalePaths(st, b) == {st.mn[id].path : id \in Stale(st, b)} +IgnoredStalePaths(st, b) == {st.mn[id].path : id \in {i \in Stale(st, b) : st.mn[i].comp \in Ign(st)}} + +PullFiles(st, b, mode) == + LET T == TreeOf(b) IN + [t \in Trees |-> IF t # T THEN st.fl[t] ELSE + [p \in Paths |-> + IF p \in StalePaths(st, b) THEN NoFile + ELSE IF \E id \in RKeys(st, b) : PPathFor(st, b, id) = p /\ Written(st, b, mode, id) + THEN PulledFile(st, b, CHOOSE id \in RKeys(st, b) : + PPathFor(st, b, id) = p /\ Written(st, b, mode, id)) + ELSE st.fl[T][p]]] + +PullState(st, b, mode) == + [st EXCEPT !.fl = PullFiles(st, b, mode), + !.mn = [id \in Ids |-> IF id \in RKeys(st, b) THEN PEntry(st, b, mode, id) + ELSE NoEntry]] + +Destroys(old, new) == old.ex /\ (~new.ex \/ new.v # old.v \/ new.drift # old.drift) + +(***************************************************************************) +(* push() -- sync_service.py:1574-1966 (Phase A, configs only) *) +(***************************************************************************) +PathIdx(p) == CASE p = "p1" -> 1 [] p = "p2" -> 2 [] p = "q1" -> 3 [] p = "q2" -> 4 [] p = "ps" -> 5 +IdIdx(i) == CASE i = "none" -> 0 [] i = "i1" -> 1 [] i = "i2" -> 2 [] i = "n1" -> 3 [] i = "n2" -> 4 +Key(c) == PathIdx(c.path) * 10 + IdIdx(c.id) +MinC(cs) == CHOOSE c \in cs : \A d \in cs : Key(c) <= Key(d) +FreeIds(st) == NewIds \ st.used +FreshId(st) == CHOOSE n \in FreeIds(st) : \A m \in FreeIds(st) : IdIdx(n) <= IdIdx(m) + +ApplyOne(st, c, b, S) == + CASE c.kind = "added" -> + \* push_create + writeback_after_push (new id written into the file) + \* + stamp_created_config / writeback_create_config_in_manifest + LET nid == FreshId(st) + f == st.fl[S][c.path] + nf == [f EXCEPT !.cid = nid, !.ed = FALSE, !.sv = f.v] + r == [ex |-> TRUE, v |-> f.v, nm |-> f.nm, comp |-> f.comp, org |-> f.sid] + match == {i \in Ids : st.mn[i].ex /\ st.mn[i].br = b /\ st.mn[i].comp = c.comp + /\ st.mn[i].path = c.path} + old == IF match # {} THEN CHOOSE i \in match : TRUE ELSE "none" + e == IF old # "none" THEN st.mn[old] + ELSE [ex |-> TRUE, br |-> b, path |-> c.path, comp |-> c.comp, + ph |-> NoHash, base |-> NoBase] + ne == [e EXCEPT !.ph = Raw(nf), !.base = ApiH(r)] + IN [st EXCEPT !.rm[b][nid] = r, !.fl[S][c.path] = nf, !.used = @ \cup {nid}, + !.mn = [i \in Ids |-> IF i = nid THEN ne + ELSE IF i = old THEN NoEntry ELSE st.mn[i]]] + [] c.kind = "modified" -> + \* push_update + stamp_updated_config: entry looked up by id ONLY + \* (no branch filter), created if missing (adopt-by-id). + LET f == st.fl[S][c.path] + r == [st.rm[b][c.id] EXCEPT !.v = f.v] + ne == IF st.mn[c.id].ex THEN [st.mn[c.id] EXCEPT !.ph = Raw(f), !.base = ApiH(r)] + ELSE [ex |-> TRUE, br |-> b, path |-> c.path, comp |-> c.comp, + ph |-> Raw(f), base |-> ApiH(r)] + IN [st EXCEPT !.rm[b][c.id] = r, !.fl[S][c.path].ed = FALSE, + !.fl[S][c.path].sv = f.v, !.mn[c.id] = ne] + [] c.kind = "deleted" -> + \* client.delete_config unconditionally (:1826-1838); force unused + [st EXCEPT !.rm[b][c.id] = Absent, !.mn[c.id] = NoEntry] + +RECURSIVE ApplyAll(_, _, _, _) +ApplyAll(st, cs, b, S) == + IF cs = {} THEN st ELSE LET c == MinC(cs) IN ApplyAll(ApplyOne(st, c, b, S), cs \ {c}, b, S) + +WritesOf(cs, st0, st1, b) == + {<> : i \in {j \in Ids : st1.rm[b][j] # st0.rm[b][j]}} + +(***************************************************************************) +(* Initial state: production pulled once into main/ *) +(***************************************************************************) +InitRem == [id \in Ids |-> + IF id = "i1" THEN [ex |-> TRUE, v |-> 0, nm |-> "p1", comp |-> "tx", org |-> "i1"] + ELSE IF id = "i2" THEN [ex |-> TRUE, v |-> 0, nm |-> "p2", comp |-> IgnComp, org |-> "i2"] + ELSE Absent] +PF(id) == [ex |-> TRUE, comp |-> InitRem[id].comp, cid |-> id, nm |-> InitRem[id].nm, + v |-> 0, cosm |-> FALSE, drift |-> FALSE, sid |-> id, ed |-> FALSE, sv |-> 0] + +Init == + /\ rm = [b \in Branches |-> InitRem] \* dev branch = copy of prod + /\ fl = [t \in Trees |-> [p \in Paths |-> + IF t = "main" /\ p = "p1" /\ ~InitNeverFetched THEN PF("i1") + ELSE IF t = "main" /\ p = "p2" THEN PF("i2") ELSE NoFile]] + /\ mn = [id \in Ids |-> + IF id \in InitIds + THEN [ex |-> TRUE, br |-> "prod", path |-> DefPath(id), comp |-> InitRem[id].comp, + ph |-> IF id = "i1" /\ InitNeverFetched THEN NoHash ELSE Raw(PF(id)), + base |-> ApiH(InitRem[id])] + ELSE NoEntry] + /\ ig = FALSE + /\ used = InitIds + /\ userDel = [t \in Trees |-> {}] + /\ nextSid = 1 + /\ lastOp = NoOp + /\ steps = 0 + +Op(k, b) == [NoOp EXCEPT !.kind = k, !.b = b] +Tick == steps' = steps + 1 + +(***************************************************************************) +(* User actions *) +(***************************************************************************) +UEdit(t, p, dr) == + /\ fl[t][p].ex + /\ fl' = [fl EXCEPT ![t][p].v = (@ + 1) % NV, ![t][p].drift = dr, ![t][p].ed = TRUE] + /\ lastOp' = Op("user_edit", "prod") /\ Tick + /\ UNCHANGED <> + +UCosmetic(t, p) == + /\ fl[t][p].ex /\ ~fl[t][p].cosm + /\ fl' = [fl EXCEPT ![t][p].cosm = TRUE] + /\ lastOp' = Op("user_cosmetic", "prod") /\ Tick + /\ UNCHANGED <> + +UDeleteDir(t, p) == + /\ fl[t][p].ex + /\ fl' = [fl EXCEPT ![t][p] = NoFile] + /\ userDel' = [userDel EXCEPT ![t] = @ \cup {p}] + /\ lastOp' = Op("user_rm", "prod") /\ Tick + /\ UNCHANGED <> + +SidOf(k) == IF k = 1 THEN "s1" ELSE "s2" + +\* `kbagent config new` scaffold (no --push): untracked file, no id +UScaffold(t) == + /\ nextSid <= MaxScaffolds /\ ~fl[t]["ps"].ex + /\ fl' = [fl EXCEPT ![t]["ps"] = [ex |-> TRUE, comp |-> "tx", cid |-> "none", nm |-> "ps", + v |-> 0, cosm |-> FALSE, drift |-> FALSE, + sid |-> SidOf(nextSid), ed |-> TRUE, sv |-> 99]] + /\ nextSid' = nextSid + 1 + /\ userDel' = [userDel EXCEPT ![t] = @ \ {"ps"}] + /\ lastOp' = Op("user_scaffold", "prod") /\ Tick + /\ UNCHANGED <> + +\* `kbagent config new --push --output-dir`: creates the remote config and +\* writes the scaffold, carrying _keboola.config_id, into the branch's tree +\* (#644). No manifest entry is written. +UScaffoldPush(b) == + /\ nextSid <= MaxScaffolds /\ FreeIds(St) # {} /\ ~fl[TreeOf(b)]["ps"].ex + /\ LET nid == FreshId(St) IN + /\ rm' = [rm EXCEPT ![b][nid] = [ex |-> TRUE, v |-> 0, nm |-> "ps", comp |-> "tx", + org |-> SidOf(nextSid)]] + /\ fl' = [fl EXCEPT ![TreeOf(b)]["ps"] = + [ex |-> TRUE, comp |-> "tx", cid |-> nid, nm |-> "ps", v |-> 0, + cosm |-> FALSE, drift |-> FALSE, sid |-> SidOf(nextSid), ed |-> FALSE, + sv |-> 0]] + /\ used' = used \cup {nid} + /\ nextSid' = nextSid + 1 + /\ userDel' = [userDel EXCEPT ![TreeOf(b)] = @ \ {"ps"}] + /\ lastOp' = Op("user_scaffold_push", b) /\ Tick + /\ UNCHANGED <> + +\* component added to manifest.ignoredComponents (or hardcoded by an upgrade) +BecomeIgnored == + /\ ~ig /\ ig' = TRUE + /\ lastOp' = Op("ignore", "prod") /\ Tick + /\ UNCHANGED <> + +(***************************************************************************) +(* Remote actor (web UI / API / another kbagent) *) +(***************************************************************************) +REdit(b, id) == + /\ rm[b][id].ex + /\ rm' = [rm EXCEPT ![b][id].v = (@ + 1) % NV] + /\ lastOp' = Op("remote_edit", b) /\ Tick + /\ UNCHANGED <> + +\* delete or trash: sync never queries the trash, both look like absence +RDelete(b, id) == + /\ rm[b][id].ex + /\ rm' = [rm EXCEPT ![b][id] = Absent] + /\ lastOp' = Op("remote_delete", b) /\ Tick + /\ UNCHANGED <> + +\* create a config; its name may reuse the name of i1 (dir "p1") +RCreate(b, nm) == + /\ FreeIds(St) # {} + /\ LET nid == FreshId(St) IN + /\ rm' = [rm EXCEPT ![b][nid] = [ex |-> TRUE, v |-> 0, nm |-> nm, comp |-> "tx", org |-> nid]] + /\ used' = used \cup {nid} + /\ lastOp' = Op("remote_create", b) /\ Tick + /\ UNCHANGED <> + +(***************************************************************************) +(* kbagent sync pull [--force | --theirs] [--branch b] *) +(***************************************************************************) +Pull(b, mode) == + /\ PullPathsDistinct(St, b) + /\ ~(mode = "force" /\ ForceConflict(St, b)) \* SYNC_CONFLICT abort = no-op + /\ LET ns == PullState(St, b, mode) + T == TreeOf(b) + lossPaths == {p \in Paths : fl[T][p].ex /\ fl[T][p].ed + /\ Destroys(fl[T][p], ns.fl[T][p]) + /\ p \notin IgnoredStalePaths(St, b)} + IN /\ fl' = ns.fl /\ mn' = ns.mn + /\ userDel' = [userDel EXCEPT ![T] = {p \in @ : ~ns.fl[T][p].ex}] + /\ lastOp' = [Op("pull_" \o mode, b) EXCEPT !.loss = (mode = "theirs" \/ lossPaths = {})] + /\ Tick + /\ UNCHANGED <> + +(***************************************************************************) +(* kbagent sync push [--force] [--branch b] *) +(***************************************************************************) +\* `force` is not an argument: push() never reads it (sync_service.py:1574-1966), +\* so `sync push` and `sync push --force` are the same transition. The model +\* runs push WITHOUT --force and I2b checks the CLI's documented contract. +PushFlags(cs, b, S) == + LET dels == {c \in cs : c.kind = "deleted"} IN + [NoOp EXCEPT + !.force = FALSE, + \* I2: every planned remote DELETE traces to a user `rm -rf` + !.i2 = \A c \in dels : c.path \in userDel[S], + \* I2b: CLI help "--force: Allow deletion of remote configs ..." + !.i2b = (dels = {}), + \* I3: nothing of an ignored component is planned + !.i3 = \A c \in cs : c.comp \notin Ign(St), + \* I7: no never-fetched entry is planned as a delete + !.i7 = \A c \in dels : c.id \notin NeverFetched(St), + \* I11: a "modified" decided WITHOUT a 3-way base (2-way fallback, + \* diff_engine.py:389-391 -- adopt-by-id) only overwrites a remote value + \* this file was synced with; otherwise a remote edit is silently lost. + \* (With a base, remote_changed => conflict/remote_modified, never pushed.) + !.lost = \A c \in cs : (c.kind = "modified" /\ c.base = NoBase) + => rm[b][c.id].v = fl[S][c.path].sv, + \* I11b: no tracked config deleted on the remote is silently re-created + !.resur = \A c \in cs : ~(c.kind = "added" /\ c.trk)] + +Push(b) == + LET cs == Pushable(St, b) + S == Src(St, b) + nadd == Cardinality({c \in cs : c.kind = "added"}) + IN + /\ cs # {} + /\ nadd <= Cardinality(FreeIds(St)) \* id-pool bound + /\ LET ns == ApplyAll(St, cs, b, S) IN + /\ fl' = ns.fl /\ mn' = ns.mn /\ rm' = ns.rm /\ used' = ns.used + /\ lastOp' = [PushFlags(cs, b, S) EXCEPT !.kind = "push", !.b = b, + !.wrote = WritesOf(cs, St, ns, b)] + /\ Tick + /\ UNCHANGED <> + +\* ENCRYPTION_FAILED on change k: changes ordered before k already reached +\* the API (and wrote the new id into their files); the exception propagates +\* past save_manifest (:1842-1852, :1945), so the manifest is NOT updated. +PushAbort(b) == + LET cs == Pushable(St, b) + S == Src(St, b) + IN + /\ EnableAbort + /\ Cardinality(cs) >= 2 + /\ Cardinality({c \in cs : c.kind = "added"}) <= Cardinality(FreeIds(St)) + /\ \E k \in cs : + LET pre == {c \in cs : Key(c) < Key(k)} + ns == ApplyAll(St, pre, b, S) + IN /\ pre # {} + /\ fl' = ns.fl /\ rm' = ns.rm /\ used' = ns.used + /\ mn' = mn + /\ lastOp' = [PushFlags(cs, b, S) EXCEPT !.kind = "push_abort", !.b = b, + !.abortWrites = WritesOf(pre, St, ns, b)] + /\ Tick + /\ UNCHANGED <> + +Next == + \/ \E t \in Trees, p \in Paths, dr \in BOOLEAN : UEdit(t, p, dr) + \/ \E t \in Trees, p \in Paths : UCosmetic(t, p) \/ UDeleteDir(t, p) + \/ \E t \in Trees : UScaffold(t) + \/ \E b \in OpBranches : UScaffoldPush(b) + \/ (EnableIgnore /\ BecomeIgnored) + \/ EnableRemote /\ \E b \in OpBranches, id \in Ids : REdit(b, id) \/ RDelete(b, id) + \/ EnableRemote /\ \E b \in OpBranches, nm \in {"p1", "q1"} : RCreate(b, nm) + \/ \E b \in OpBranches, mode \in {"plain", "force", "theirs"} : Pull(b, mode) + \/ \E b \in OpBranches : Push(b) \/ PushAbort(b) + +Spec == Init /\ [][Next]_vars + +StepBound == steps <= MaxSteps + +(***************************************************************************) +(* Invariants I1..I12 *) +(***************************************************************************) +TypeOK == + /\ ig \in BOOLEAN + /\ used \subseteq Ids + /\ \A b \in Branches, i \in Ids : rm[b][i].ex => rm[b][i].v \in V + +\* I1: no two live remote configs on one branch descend from the same local +\* config instance (a double create). +I1_NoDoubleCreate == + \A b \in Branches, x, y \in Ids : + (x # y /\ rm[b][x].ex /\ rm[b][y].ex) => rm[b][x].org # rm[b][y].org + +\* I2: push only deletes a remote config whose local dir the user removed. +I2_DeleteOnlyUserRemoved == lastOp.i2 +\* I2b: ... and only with --force (CLI help text, commands/sync.py:982-986). +I2b_DeleteNeedsForce == lastOp.i2b + +\* I3: push never plans anything for an ignored component. +I3_IgnoredUntouched == lastOp.i3 + +\* I4: diff/push act only on entries of the ONE source tree (scope_manifest +\* partition) -- every tracked change refers to an in-tree entry. +I4_BranchIsolation == + \A b \in OpBranches : \A c \in Changes(St, b) : + (c.trk /\ c.id # "none") => EntryTree(St, c.id) = Src(St, b) + +\* I5 (generalized): a pull other than --theirs never destroys user work +\* (a file carrying edits that are on no remote), except the documented +\* ignored-component cleanup. +I5_PullKeepsLocalWork == lastOp.loss + +\* I6: right after a successful push, a fresh diff of the same branch plans +\* nothing pushable and shows no drift on anything the push wrote. +I6_PushThenDiffClean == + lastOp.kind = "push" => + /\ Pushable(St, lastOp.b) = {} + /\ \A w \in lastOp.wrote : KindOf(St, lastOp.b, w[2]) = "none" + +\* I7: never-fetched entries are never planned as deletes. +I7_NeverFetchedNotDeleted == lastOp.i7 + +\* I8: every live manifest entry has its file in its own tree, unless it is +\* never-fetched or the user removed the dir. +I8_ManifestMatchesDisk == + \A id \in Live(St) : + LET t == EntryTree(St, id) IN + fl[t][mn[id].path].ex \/ mn[id].ph = NoHash \/ mn[id].path \in userDel[t] + +\* I9: an ENCRYPTION_FAILED push leaves no remote write unrecorded in the +\* manifest (strong, atomic reading). +I9_AbortLeavesNoUnrecordedWrites == lastOp.kind = "push_abort" => lastOp.abortWrites = {} + +\* I11: push never reverts a remote change with content the user never edited. +I11_NoLostUpdate == lastOp.lost +\* I11b: push never silently re-creates a tracked config deleted remotely. +I11b_NoSilentResurrect == lastOp.resur + +\* I12 (S3 as safety): whenever diff says REMOTE MODIFIED, a plain +\* `sync pull` of that branch brings the config in sync. +I12_PullResolvesRemoteModified == + \A b \in OpBranches : PullPathsDistinct(St, b) => + \A id \in Ids : KindOf(St, b, id) = "remote_modified" => + KindOf(PullState(St, b, "plain"), b, id) # "remote_modified" +============================================================================= diff --git a/formal/sync/tla/run_all.sh b/formal/sync/tla/run_all.sh new file mode 100755 index 000000000..e076aaa2a --- /dev/null +++ b/formal/sync/tla/run_all.sh @@ -0,0 +1,20 @@ +#!/bin/sh +# Re-run every check behind ../README.md. Each line prints either +# "No error has been found" or the violated invariant; traces land in +# out/.json (render with ./trace.py out/.json). +# Args of run_one.sh: INV MaxSteps InitNeverFetched EnableAbort EnableRemote EnableIgnore EnableDev +cd "$(dirname "$0")" +for inv in I1_NoDoubleCreate I2_DeleteOnlyUserRemoved I2b_DeleteNeedsForce \ + I3_IgnoredUntouched I4_BranchIsolation I5_PullKeepsLocalWork \ + I6_PushThenDiffClean I8_ManifestMatchesDisk I9_AbortLeavesNoUnrecordedWrites \ + I11_NoLostUpdate I11b_NoSilentResurrect I12_PullResolvesRemoteModified; do + echo "== $inv (depth 4, all actors)"; ./run_one.sh $inv 4 +done +echo "== I7 (never-fetched initial entry)"; TAG=nf ./run_one.sh I7_NeverFetchedNotDeleted 4 TRUE +# single-branch (production only) variants: separate the root causes that do +# not need a dev branch from the promote/cross-branch ones +for inv in I2_DeleteOnlyUserRemoved I6_PushThenDiffClean I8_ManifestMatchesDisk; do + echo "== $inv (production only)"; TAG=prod ./run_one.sh $inv 4 FALSE TRUE TRUE TRUE FALSE +done +echo "== I1 (production only, depth 5)"; TAG=prod ./run_one.sh I1_NoDoubleCreate 5 FALSE TRUE TRUE TRUE FALSE +echo "== I3 (production only, depth 5)"; TAG=prod ./run_one.sh I3_IgnoredUntouched 5 FALSE TRUE TRUE TRUE FALSE diff --git a/formal/sync/tla/run_one.sh b/formal/sync/tla/run_one.sh new file mode 100755 index 000000000..ba23a5636 --- /dev/null +++ b/formal/sync/tla/run_one.sh @@ -0,0 +1,29 @@ +#!/bin/sh +# usage: run_one.sh INVARIANT MaxSteps [InitNeverFetched] [EnableAbort] [EnableRemote] [EnableIgnore] [EnableDev] [MaxScaffolds] +# Checks ONE invariant (plus TypeOK) and writes out/.{cfg,log,json}; +# NAME = or _$TAG when the TAG env var is set. +set -e +cd "$(dirname "$0")" +INV=$1; STEPS=$2; NF=${3:-FALSE}; AB=${4:-TRUE}; RE=${5:-TRUE}; IG=${6:-TRUE}; DEV=${7:-TRUE}; SC=${8:-1} +N=$INV${TAG:+_$TAG} +mkdir -p out +cat > out/$N.cfg < $N.log 2>&1 || true +rm -rf "states_$N" +grep -E "violated|No error|states generated|distinct states|Error:" $N.log | head -5 diff --git a/formal/sync/tla/trace.py b/formal/sync/tla/trace.py new file mode 100755 index 000000000..a30f74385 --- /dev/null +++ b/formal/sync/tla/trace.py @@ -0,0 +1,73 @@ +#!/usr/bin/env python3 +"""Compact printer for a TLC `-dumpTrace json` counterexample of SyncEngine. + +usage: trace.py out/.json +Prints, per step, the action with its arguments and the model state that +changed: local files (tree/path), live manifest entries, remote configs. +""" + +import json +import sys + + +def steps(d): + """[(label, state)]: initial state, then (action(args), successor).""" + acts = d["counterexample"]["action"] + out = [("Init", acts[0][0][1])] + for _pre, act, post in acts: + args = ",".join(f"{k}={v}" for k, v in act.get("context", {}).items()) + out.append((f"{act['name']}({args})", post[1])) + return out + + +def fmt_file(f): + flags = "".join( + k for k, on in (("~cosm", f["cosm"]), ("~drift", f["drift"]), ("*edited", f["ed"])) if on + ) + return f"{f['comp']}:{f['cid']} v{f['v']}{flags} (lineage {f['sid']})" + + +def snap(s): + files = {f"{t}/{p}": fmt_file(f) for t, ps in s["fl"].items() for p, f in ps.items() if f["ex"]} + man = {} + for i, e in s["mn"].items(): + if e["ex"]: + ph = ( + "none" + if e["ph"][3] == 99 + else f"{e['ph'][1]}/v{e['ph'][3]}" + + ("~c" if e["ph"][4] else "") + + ("~d" if e["ph"][5] else "") + ) + base = "none" if e["base"][0] == 99 else f"v{e['base'][0]}" + man[i] = f"{e['comp']} br={e['br']} path={e['path']} pull_hash={ph} base={base}" + rem = { + f"{b}/{i}": f"{r['comp']} v{r['v']} name={r['nm']} lineage={r['org']}" + for b, rs in s["rm"].items() + for i, r in rs.items() + if r["ex"] + } + return {"file": files, "manifest": man, "remote": rem, "ignored": s["ig"]} + + +def main(): + with open(sys.argv[1]) as fh: + d = json.load(fh) + prev = None + for n, (lab, s) in enumerate(steps(d)): + cur = snap(s) + print(f"--- step {n}: {lab} lastOp={s['lastOp']['kind']}@{s['lastOp']['b']}") + for sect in ("file", "manifest", "remote"): + for k, v in cur[sect].items(): + if prev is None or prev[sect].get(k) != v: + print(f" {sect:8} {k:10} {v}") + if prev is not None: + for k in prev[sect]: + if k not in cur[sect]: + print(f" {sect:8} {k:10} (gone)") + if prev is not None and prev["ignored"] != cur["ignored"]: + print(f" ignored -> {cur['ignored']}") + prev = cur + + +main() diff --git a/tests/test_sync_formal_counterexamples.py b/tests/test_sync_formal_counterexamples.py new file mode 100644 index 000000000..a4e30adc8 --- /dev/null +++ b/tests/test_sync_formal_counterexamples.py @@ -0,0 +1,923 @@ +"""Counterexample / regression tests from the issue #792 formal-verification pilot. + +Issue: https://github.com/keboola/cli/issues/792 +Models: ``formal/sync/README.md`` (TLA+ model + Lean model, both mirroring the +real ``sync pull`` / ``sync diff`` / ``sync push`` code line-by-line). + +Each test drives the real ``SyncService`` against a mocked/faked Keboola +client, one test per consolidated finding A..K from the pilot (see the +findings table in ``formal/sync/README.md``). Findings A..K deduplicate the +independent hits from the spec (S1..S5), the Lean refutations (F1..F8) and +the TLA+ counterexamples (I1..I12) -- several tools independently rediscovered +the same code paths. + +Outcome legend: + +- REPRODUCED on current code: the test asserts the SAFE behavior and is + marked ``@pytest.mark.xfail(strict=True, ...)``. ``strict=True`` means the + test suite goes RED the moment the behavior is fixed -- that is + deliberate. To adopt a fix, delete the ``xfail`` marker (and this note in + the docstring pointing at it); the test then becomes an ordinary + regression guard. +- NOT reproduced / intentional documented behavior: a plain, unmarked + regression guard asserting the current (safe or deliberately conservative) + behavior. + +Two simple test doubles are used, matching what the finding needs: + +- ``_make_mock_client`` / ``_init_and_pull``: a single-shot ``MagicMock`` + client, for findings that need only one pull followed by one push/diff + (mirrors the fixtures already used in ``tests/test_sync_service.py``). +- ``FakeApi`` / ``World``: a small stateful, branch-aware in-memory Storage + API (ported from the pilot's ``scratchpad/replay/harness.py`` scratch + harness) for findings that need a multi-step story: pull, an out-of-band + remote/user action, then a second pull/diff/push. +""" + +from __future__ import annotations + +import copy +import itertools +import shutil +from pathlib import Path +from typing import Any +from unittest.mock import MagicMock + +import pytest +import yaml + +from helpers import setup_single_project +from keboola_agent_cli.config_store import ConfigStore +from keboola_agent_cli.constants import CONFIG_FILENAME +from keboola_agent_cli.errors import ErrorCode, KeboolaApiError +from keboola_agent_cli.models import TokenVerifyResponse +from keboola_agent_cli.services.sync_service import SyncService +from keboola_agent_cli.sync.manifest import load_manifest, save_manifest + +# =========================================================================== +# Shared fixtures -- single-shot mock client (mirrors test_sync_service.py) +# =========================================================================== + +SAMPLE_VERIFY_TOKEN = TokenVerifyResponse( + token_id="tok-001", + token_description="kbagent-cli", + project_id=258, + project_name="Production", + owner_name="My Org", +) + +SAMPLE_BRANCHES = [ + {"id": 12345, "name": "Main", "isDefault": True}, +] + +SAMPLE_BRANCHES_WITH_DEV = [ + {"id": 12345, "name": "Main", "isDefault": True}, + {"id": 99999, "name": "feature-x", "isDefault": False}, +] + +SAMPLE_COMPONENTS_NO_ROWS = [ + { + "id": "keboola.ex-http", + "type": "extractor", + "configurations": [ + { + "id": "cfg-001", + "name": "My HTTP Extractor", + "description": "Fetches data", + "configuration": { + "parameters": {"baseUrl": "https://api.example.com"}, + }, + "rows": [], + } + ], + }, +] + + +def _empty_component() -> list: + """Same component family as SAMPLE_COMPONENTS_NO_ROWS, but no configs at all -- + models "the config was deleted/trashed remotely by another actor".""" + return [{**SAMPLE_COMPONENTS_NO_ROWS[0], "configurations": []}] + + +def _make_mock_client( + verify_token_response: TokenVerifyResponse | None = None, + components_response: list | None = None, + branches_response: list | None = None, +) -> MagicMock: + client = MagicMock() + client.__enter__ = MagicMock(return_value=client) + client.__exit__ = MagicMock(return_value=False) + if verify_token_response: + client.verify_token.return_value = verify_token_response + if components_response is not None: + client.list_components_with_configs.return_value = components_response + if branches_response is not None: + client.list_dev_branches.return_value = branches_response + return client + + +def _init_and_pull( + tmp_config_dir: Path, + project_root: Path, + components: list, +) -> ConfigStore: + """init_sync + pull, returning the ConfigStore with a materialized tree.""" + init_client = _make_mock_client( + verify_token_response=SAMPLE_VERIFY_TOKEN, + branches_response=SAMPLE_BRANCHES, + ) + store = setup_single_project(tmp_config_dir) + SyncService( + config_store=store, + client_factory=lambda url, token: init_client, + ).init_sync(alias="prod", project_root=project_root) + + pull_client = _make_mock_client(components_response=components) + SyncService( + config_store=store, + client_factory=lambda url, token: pull_client, + ).pull(alias="prod", project_root=project_root) + return store + + +def _svc_with_client(store: ConfigStore, components: list) -> tuple[SyncService, MagicMock]: + client = _make_mock_client(components_response=components) + svc = SyncService(config_store=store, client_factory=lambda url, token: client) + return svc, client + + +# =========================================================================== +# Shared fixtures -- stateful fake API (ported from scratchpad/replay/harness.py) +# =========================================================================== + +PROD = 12345 +DEV = 99999 +COMP = "keboola.ex-http" + + +class FakeApi: + """Branch-aware in-memory Storage API: remote[branch_id][config_id] = cfg. + + Lets a test drive a realistic multi-step story (pull, an out-of-band + remote/user action, pull/diff/push again) through the real + ``SyncService`` without re-fetching a static mock response each time. + """ + + def __init__(self) -> None: + self.remote: dict[int, dict[str, dict[str, Any]]] = {PROD: {}, DEV: {}} + self._ids = itertools.count(100) + self.log: list[str] = [] + # Optional hook for encryption-failure scenarios (finding F): + # signature (project_id, component_id, data) -> dict[str, str]. + self.encrypt_values: Any = None + + def put(self, branch: int, cid: str, name: str, value: str, extra: dict | None = None) -> None: + params: dict[str, Any] = {"value": value} + if extra: + params.update(extra) + self.remote[branch][cid] = { + "id": cid, + "name": name, + "description": "", + "configuration": {"parameters": params}, + "rows": [], + "isDisabled": False, + } + + def ids(self, branch: int) -> list[str]: + return sorted(self.remote[branch]) + + def client(self) -> MagicMock: + c = MagicMock() + c.__enter__ = MagicMock(return_value=c) + c.__exit__ = MagicMock(return_value=False) + c.verify_token.return_value = TokenVerifyResponse( + token_id="t", token_description="d", project_id=258, project_name="P", owner_name="O" + ) + c.list_dev_branches.return_value = [ + {"id": PROD, "name": "Main", "isDefault": True}, + {"id": DEV, "name": "dev", "isDefault": False}, + ] + c.list_buckets_with_metadata.return_value = [] + c.list_tables_with_metadata.return_value = [] + c.list_jobs_grouped.return_value = [] + c.list_config_metadata.return_value = [] + c.list_components_with_configs.side_effect = self._list + c.create_config.side_effect = self._create + c.update_config.side_effect = self._update + c.delete_config.side_effect = self._delete + c.get_config_detail.side_effect = self._detail + if self.encrypt_values is not None: + c.encrypt_values.side_effect = self.encrypt_values + return c + + def _b(self, branch_id: int | None) -> int: + return PROD if branch_id in (None, 0, PROD) else branch_id + + def _list(self, branch_id: int | None = None, **_: Any) -> list[dict[str, Any]]: + cfgs = [copy.deepcopy(v) for v in self.remote[self._b(branch_id)].values()] + return [{"id": COMP, "type": "extractor", "configurations": cfgs}] if cfgs else [] + + def _create( + self, + component_id: str, + name: str, + configuration: dict, + description: str = "", + branch_id: int | None = None, + is_disabled: bool = False, + **_: Any, + ) -> dict: + cid = f"cfg-{next(self._ids)}" + b = self._b(branch_id) + self.remote[b][cid] = { + "id": cid, + "name": name, + "description": description, + "configuration": copy.deepcopy(configuration), + "rows": [], + "isDisabled": is_disabled, + } + self.log.append(f"CREATE {cid} on {b}") + return copy.deepcopy(self.remote[b][cid]) + + def _update( + self, + component_id: str, + config_id: str, + name: str | None = None, + configuration: dict | None = None, + description: str | None = None, + change_description: str = "", + branch_id: int | None = None, + is_disabled: bool | None = None, + **_: Any, + ) -> dict: + b = self._b(branch_id) + cfg = self.remote[b][config_id] + if configuration is not None: + cfg["configuration"] = copy.deepcopy(configuration) + if name is not None: + cfg["name"] = name + self.log.append(f"UPDATE {config_id} on {b}") + return copy.deepcopy(cfg) + + def _delete(self, component_id: str, config_id: str, branch_id: int | None = None) -> None: + b = self._b(branch_id) + self.remote[b].pop(config_id) + self.log.append(f"DELETE {config_id} on {b}") + + def _detail(self, component_id: str, config_id: str, branch_id: int | None = None, **_: Any): + return copy.deepcopy(self.remote[self._b(branch_id)][config_id]) + + +class World: + """SyncService bound to a FakeApi + a real (tmp) sync working tree.""" + + def __init__(self, tmp: Path) -> None: + self.api = FakeApi() + self.root = tmp / "project" + self.root.mkdir(parents=True) + cfgdir = tmp / "cfg" + cfgdir.mkdir() + self.store = setup_single_project(cfgdir) + self.svc = SyncService( + config_store=self.store, client_factory=lambda url, token: self.api.client() + ) + + def init(self) -> None: + self.svc.init_sync(alias="prod", project_root=self.root) + + def pull(self, branch: int | None = None, **kw: Any) -> dict: + return self.svc.pull(alias="prod", project_root=self.root, branch_override=branch, **kw) + + def diff(self, branch: int | None = None) -> dict: + return self.svc.diff(alias="prod", project_root=self.root, branch_override=branch) + + def push(self, branch: int | None = None, **kw: Any) -> dict: + return self.svc.push(alias="prod", project_root=self.root, branch_override=branch, **kw) + + def files(self) -> list[str]: + return sorted( + str(p.parent.relative_to(self.root)) + for p in self.root.rglob("_config.yml") + if "rows" not in p.parts + ) + + def manifest(self) -> list[tuple[int, str, str]]: + m = load_manifest(self.root) + return [(c.branch_id, c.id, c.path) for c in m.configurations] + + def config_dir(self, path_fragment: str) -> Path: + (d,) = (p.parent for p in self.root.rglob("_config.yml") if path_fragment in str(p)) + return d + + +def changes(d: dict) -> list[tuple[str, str]]: + return [(c["change_type"], c.get("config_id", "")) for c in d["changes"]] + + +# =========================================================================== +# A -- remote delete+recreate under the same name/path: pull's stale sweep +# deletes the freshly-written config, next push deletes it remotely. +# =========================================================================== + + +@pytest.mark.xfail( + strict=True, + reason=( + "#792 A: pull's stale-entry sweep (sync_service.py ~1062-1094) runs " + "AFTER the fetch loop has written the new config to the same path " + "(paths are per-pull, not globally unique). When a remote actor " + "deletes a config and creates a new one of the same name, the new " + "config lands on the old path, then the sweep rmtree's that same " + "path for the vanished old id -- deleting the new files. The next " + "push then classifies the (still manifest-tracked) new config as " + "DELETED and destroys it on the remote. Confirmed live via " + "Lean F8 + TLA I2 (independently found) and replayed against the " + "real SyncService (scratchpad/replay/r_stale_sweep.py)." + ), +) +def test_a_recreate_under_same_name_does_not_delete_new_config(tmp_path: Path) -> None: + """Invariant: a config that a pull just fetched and wrote to disk must + never be deleted -- locally or remotely -- by that same pull's stale-entry + sweep, and a subsequent plain push must not delete a live remote config + nobody removed locally. + + Issue #792 finding A. + """ + w = World(tmp_path) + w.api.put(PROD, "cfg-1", "Orders", "a") + w.init() + w.pull() + + # Remote actor: delete "Orders" (cfg-1) and create a NEW config, also + # named "Orders", so it lands on the same local path. + w.api.remote[PROD].pop("cfg-1") + w.api.put(PROD, "cfg-2", "Orders", "b") + w.pull() + + # Safe expectation: the new config (cfg-2) is still on disk after the + # pull that fetched it, and a subsequent push never deletes it remotely. + assert any("orders" in f.lower() for f in w.files()), ( + "the freshly-pulled config was deleted by its own pull" + ) + + push_result = w.push() + assert push_result.get("deleted", 0) == 0 + assert "cfg-2" in w.api.remote[PROD], "push deleted a live remote config nobody removed locally" + + +# =========================================================================== +# B -- pull compares only _config.yml; edits to companion files (SQL/code) +# are silently overwritten, plain or --force, with no conflict. +# =========================================================================== + + +@pytest.mark.xfail( + strict=True, + reason=( + "#792 B: pull's 'locally modified' guard (sync_service.py:766-790, " + "_sync_baseline.py:423-445) hashes only _config.yml. A companion " + "file (transform.sql / code.py / _description.md) that was edited " + "locally is not detected as modified, so a remote change to the same " + "transformation silently overwrites the local SQL edit -- plain pull " + "AND `pull --force` -- with no 'skipped' entry and no SYNC_CONFLICT. " + "Confirmed via Lean F6 and replayed live (scratchpad/repro/" + "test_lean_refutations.py::test_R1)." + ), +) +def test_b_pull_never_overwrites_local_sql_edit(tmp_path: Path) -> None: + """Invariant: a locally-edited companion file (here: transform.sql on a + tracked SQL transformation) must never be silently overwritten by pull + just because _config.yml itself is unchanged -- it must be treated the + same as an edited _config.yml (skip, or SYNC_CONFLICT under --force). + + Issue #792 finding B. + """ + w = World(tmp_path) + comp = "keboola.snowflake-transformation" + + def sql_client_pull(sql_stmt: str) -> None: + api_client = w.api.client() + api_client.list_components_with_configs.side_effect = None + api_client.list_components_with_configs.return_value = [ + { + "id": comp, + "type": "transformation", + "configurations": [ + { + "id": "t1", + "name": "My SQL", + "description": "", + "rows": [], + "configuration": { + "parameters": { + "blocks": [ + {"name": "B", "codes": [{"name": "C", "script": [sql_stmt]}]} + ] + } + }, + } + ], + } + ] + w.svc = SyncService(config_store=w.store, client_factory=lambda url, token: api_client) + + sql_client_pull("SELECT 1;") + w.svc.init_sync(alias="prod", project_root=w.root) + w.svc.pull(alias="prod", project_root=w.root) + + sql_file = next(w.root.rglob("transform.sql")) + sql_file.write_text(sql_file.read_text().replace("SELECT 1", "SELECT 42 /* my local edit */")) + + sql_client_pull("SELECT 100;") # remote changed the SQL in the meantime + w.svc.pull(alias="prod", project_root=w.root) + + assert "SELECT 42" in sql_file.read_text(), ( + "the local SQL edit was silently overwritten by pull" + ) + + +# =========================================================================== +# C -- remote delete + local edit: pull deletes the locally edited dir. +# =========================================================================== + + +@pytest.mark.xfail( + strict=True, + reason=( + "#792 C: pull's stale-entry sweep (sync_service.py:1062-1094) runs " + "an unconditional rmtree for every manifest entry whose remote key " + "vanished -- it never checks pull_hash against the current file " + "content. A config edited locally and then deleted remotely is " + "silently rmtree'd by the next pull (plain or --force), with no " + "conflict raised even under --force (detect_force_pull_conflicts " + "only iterates remote configs, _sync_baseline.py:485). Confirmed " + "via Lean F7 + TLA I5 (independently found) and replayed " + "(scratchpad/replay/r_misc.py)." + ), +) +def test_c_pull_never_deletes_locally_edited_dir_on_remote_delete(tmp_path: Path) -> None: + """Invariant: pull must never destroy a directory carrying an unpushed + local edit just because the remote config was deleted in the meantime -- + at minimum it should be left alone (or flagged), never silently rmtree'd. + + Issue #792 finding C. + """ + w = World(tmp_path) + w.api.put(PROD, "cfg-1", "Orders", "a") + w.init() + w.pull() + + config_dir = w.config_dir("orders") + edited_file = config_dir / CONFIG_FILENAME + data = yaml.safe_load(edited_file.read_text()) + data["parameters"]["value"] = "MY-UNPUSHED-EDIT" + edited_file.write_text(yaml.dump(data, default_flow_style=False)) + + w.api.remote[PROD].pop("cfg-1") + w.pull() + + assert config_dir.exists(), "pull deleted a directory carrying an unpushed local edit" + assert "MY-UNPUSHED-EDIT" in edited_file.read_text() + + +# =========================================================================== +# D -- `sync push --branch dev` (promote) re-creates the same config on +# every push instead of being idempotent. +# =========================================================================== + + +@pytest.mark.xfail( + strict=True, + reason=( + "#792 D: when the target dev branch has no materialized subtree, " + "push promotes main/ as the read source (KFR-07), but " + "stamp_created_config's writeback only matches an existing manifest " + "entry by (branch_id, component_id, path) (_sync_writeback.py:" + "147-151). The promoted config's entry is written with branchId=dev, " + "leaving the ORIGINAL main-branch entry (branchId=prod) untouched -- " + "so it never resolves on dev and stays 'added' forever. Every " + "`sync push --branch dev` after the first creates ANOTHER dev copy " + "of the same config. Found via TLA I6/I1 and replayed " + "(scratchpad/replay/r_misc.py). Whether the intent is 'promote once, " + "then track on dev' is a product decision (see the finding's action " + "column), but duplicating on every push is not intended." + ), +) +def test_d_promote_push_is_idempotent(tmp_path: Path) -> None: + """Invariant: promoting a production-only config to a dev branch via + `sync push --branch ` must be idempotent -- a second promote push + with no further local change must not create a second dev copy of the + same config. + + Issue #792 finding D. + """ + w = World(tmp_path) + w.api.put(PROD, "cfg-1", "Orders", "a") + w.init() + w.pull() + + first = w.push(branch=DEV) + assert first.get("created", 0) == 1 + assert len(w.api.remote[DEV]) == 1 + + second = w.push(branch=DEV) + assert second.get("created", 0) == 0, "a second promote push created another dev copy" + assert len(w.api.remote[DEV]) == 1, "dev branch now holds more than one copy of the same config" + + +# =========================================================================== +# E -- an untracked file carrying `_keboola.config_id` (a `config new --push +# --output-dir` scaffold, or an adopted orphan) is diffed 2-way, so +# push silently overwrites a remote edit made after the scaffold was +# written -- and two copies of it both "adopt" the same remote id. +# =========================================================================== + + +@pytest.mark.xfail( + strict=True, + reason=( + "#792 E: classify_untracked ADOPTs a file carrying " + "`_keboola.config_id` (branch_scope.py:275-276), but base_hashes is " + "built from in-tree manifest entries only (sync_service.py:" + "1441-1452). With no base, compute_changeset's 2-way fallback turns " + "ANY difference into 'modified' (diff_engine.py:388-391) -- so a " + "remote edit made after the scaffold was written (e.g. in the web " + "UI) is silently reverted by the next `sync push`, no conflict " + "shown. Found via TLA I11 and replayed " + "(scratchpad/replay/r_adopt_lost_update.py)." + ), +) +def test_e_adopted_scaffold_push_does_not_overwrite_remote_edit(tmp_path: Path) -> None: + """Invariant: a `sync push` must never silently revert a remote edit made + to a config in between that config's on-disk scaffold being written and + the next push, even when the local file is untracked-but-adopts-by-id. + + Issue #792 finding E. + """ + w = World(tmp_path) + w.api.put(PROD, "cfg-1", "Orders", "a") + w.init() + w.pull() + + # Emulate the `config new --push --output-dir` scaffold shape: a file on + # disk carrying the config id, with NO manifest entry (#644). + m = load_manifest(w.root) + m.configurations = [] + save_manifest(w.root, m) + + # The config is edited remotely (e.g. in the web UI) after the scaffold + # was written, before the next push. + w.api.put(PROD, "cfg-1", "Orders", "EDITED-IN-UI") + + w.push() + + assert w.api.remote[PROD]["cfg-1"]["configuration"]["parameters"]["value"] == "EDITED-IN-UI", ( + "push silently reverted a remote edit made to an adopted-by-id scaffold config" + ) + + +# =========================================================================== +# F -- a push aborted by ENCRYPTION_FAILED leaves the manifest unsaved, so a +# change it already applied (a resurrect CREATE) is re-applied by the +# retry, duplicating it. +# =========================================================================== + + +@pytest.mark.xfail( + strict=True, + reason=( + "#792 F: push() re-raises ENCRYPTION_FAILED instead of continuing " + "(sync_service.py:1842-1852), but save_manifest only runs after the " + "whole Phase A/B/C/D loop completes (:1946) -- so a CREATE applied " + "to the remote before the failing change is never recorded in the " + "manifest. Re-running push after the encryption problem is fixed " + "creates that same config again, duplicating it. This is a model " + "trace only in the original TLA pilot (I1(b), not previously " + "replayed against real SyncService); replayed here directly by " + "making the second config's secret fail Encryption API mock." + ), +) +def test_f_aborted_push_does_not_duplicate_already_created_config(tmp_path: Path) -> None: + """Invariant: retrying a push after an ENCRYPTION_FAILED abort must not + re-apply a change (here: a resurrect CREATE) that the aborted push had + already sent to the remote before it failed. + + Issue #792 finding F. + """ + w = World(tmp_path) + w.api.put(PROD, "cfg-1", "Orders", "a", extra={"#token": "ok-secret"}) + w.api.put(PROD, "cfg-2", "Contacts", "b", extra={"#token": "will-fail"}) + w.init() + w.pull() + + # Remote deletes cfg-1 (resurrect precondition): local file untouched. + w.api.remote[PROD].pop("cfg-1") + # Local edit to cfg-2's secret triggers the encryption failure below. + contacts_file = w.config_dir("contacts") / CONFIG_FILENAME + data = yaml.safe_load(contacts_file.read_text()) + data["parameters"]["#token"] = "FAIL_MARKER" + contacts_file.write_text(yaml.dump(data, default_flow_style=False)) + + def flaky_encrypt(project_id: int, component_id: str, data: dict[str, str]) -> dict[str, str]: + if "FAIL_MARKER" in data.values(): + raise RuntimeError("Encryption API unavailable") + return {k: f"KBC::Encrypted=={v}" for k, v in data.items()} + + w.api.encrypt_values = flaky_encrypt + + with pytest.raises(KeboolaApiError) as exc_info: + w.push() + assert exc_info.value.error_code == ErrorCode.ENCRYPTION_FAILED + + creates_before_retry = [line for line in w.api.log if line.startswith("CREATE")] + + # Fix the encryption problem and retry, exactly as a user would. + contacts_file.write_text( + yaml.dump( + {**data, "parameters": {**data["parameters"], "#token": "fixed-secret"}}, + default_flow_style=False, + ) + ) + w.api.encrypt_values = lambda project_id, component_id, data: { + k: f"KBC::Encrypted=={v}" for k, v in data.items() + } + w.push() + + creates_after_retry = [line for line in w.api.log if line.startswith("CREATE")] + # Safe expectation: the resurrect CREATE for "Orders" happened exactly + # once across both push attempts, not once per attempt. + assert len(creates_before_retry) == 1, "expected exactly one CREATE before the encryption abort" + assert len(creates_after_retry) == len(creates_before_retry), ( + "retrying the push after the encryption fix duplicated the already-applied resurrect CREATE: " + f"log={w.api.log}" + ) + + +# =========================================================================== +# G -- `sync push` deletes a remote config with no `--force`, contradicting +# the CLI's own help text ("--force: allow deletion of remote configs +# removed locally"). Product decision (soft-delete to trash since +# 0.89.0, so it is recoverable) -- xfail per the task's own note. +# =========================================================================== + + +@pytest.mark.xfail( + strict=True, + reason=( + "#792 G: SyncService.push() accepts `force` but never reads it in " + "its body (grep sync_service.py:1574-1966) -- only pull()'s conflict " + "guard does. The CLI help text for `sync push --force` " + "(commands/sync.py:982-986) promises 'Allow deletion of remote " + "configs that were removed locally', implying a plain push should " + "NOT delete, but push deletes a remote config the instant its local " + "directory is missing, force=True or not. This is a PRODUCT " + "DECISION (the delete is soft, into the Storage trash, since " + "0.89.0, so it is recoverable via `sync restore`) -- kept xfail per " + "issue #792 rather than resolved either way here." + ), +) +def test_g_push_without_force_does_not_delete_remote_config( + tmp_config_dir: Path, tmp_path: Path +) -> None: + """CLI-contract invariant: `sync push` (no --force) must not delete a + remote config just because its local directory was removed -- --force + is documented as the gate for that. + + Issue #792 finding G. + """ + project_root = tmp_path / "project" + project_root.mkdir() + store = _init_and_pull(tmp_config_dir, project_root, SAMPLE_COMPONENTS_NO_ROWS) + + manifest = load_manifest(project_root) + cfg = next(c for c in manifest.configurations if c.component_id == "keboola.ex-http") + config_dir = project_root / "main" / cfg.path + (config_dir / CONFIG_FILENAME).unlink() + + svc, client = _svc_with_client(store, SAMPLE_COMPONENTS_NO_ROWS) + push_result = svc.push(alias="prod", project_root=project_root, force=False) + + client.delete_config.assert_not_called() + assert push_result.get("deleted", 0) == 0 + + +# =========================================================================== +# H -- a config deleted remotely by another actor is silently re-created +# (no warning) by the next push, even with no local change. +# =========================================================================== + + +@pytest.mark.xfail( + strict=True, + reason=( + "#792 H: compute_changeset routes ANY local entry whose remote_key " + "is absent into 'added' (diff_engine.py:355), regardless of whether " + "the id was previously tracked. A tracked config deleted/trashed " + "remotely by another actor -- with NO local change at all -- is " + "silently recreated under a brand-new id on the next push, with no " + "warning distinguishing it from a genuinely new config. Confirmed " + "via spec S2, Lean F2 and TLA I11b (three independent hits) and " + "replayed (scratchpad/repro/test_lean_refutations.py::test_R6, " + "scratchpad/replay/r_misc.py)." + ), +) +def test_h_push_does_not_silently_resurrect_deleted_config(tmp_path: Path) -> None: + """Invariant: push must not silently POST a fresh create for a config + another actor deleted remotely when the local user made no change to it + at all -- it should surface a warning/orphan report instead of a + business-as-usual CREATE. + + Issue #792 finding H. + """ + w = World(tmp_path) + w.api.put(PROD, "cfg-1", "Orders", "a") + w.init() + w.pull() + + w.api.remote[PROD].pop("cfg-1") # another actor deletes it; local untouched + + result = w.push() + + assert result.get("created", 0) == 0, ( + "push silently recreated a remotely-deleted, locally-untouched config" + ) + assert "cfg-1" not in w.api.remote[PROD] + + +# =========================================================================== +# I -- moving/renaming a config's directory by hand (`mv` / `git mv`) is +# seen as DELETE + CREATE, minting a brand-new remote config id. +# =========================================================================== + + +@pytest.mark.xfail( + strict=True, + reason=( + "#792 I: the old path's manifest entry has no file left, so it is " + "classified 'deleted'; the moved directory carries the same " + "_keboola.config_id but a same-tree claim is always CREATE by " + "design (branch_scope.py:273-274, the #482/#497 fork-by-copy " + "protection). A hand `mv`/`git mv` of a tracked config directory " + "therefore destroys the original remote config id (job history, " + "schedules, flow references) and mints a new one -- with no warning " + "that `config rename --directory` was the supported path. Confirmed " + "via Lean F3 and replayed " + "(scratchpad/repro/test_lean_refutations.py::test_R4)." + ), +) +def test_i_moving_config_dir_is_not_delete_plus_create(tmp_path: Path) -> None: + """Invariant: renaming a tracked config's directory on disk (outside of + `config rename --directory`) must not be classified as delete-the-old + plus create-a-new-id -- the config's identity should survive a plain + filesystem move. + + Issue #792 finding I. + """ + w = World(tmp_path) + w.api.put(PROD, "cfg-1", "Orders", "a") + w.init() + w.pull() + + original_dir = w.config_dir("orders") + shutil.move(str(original_dir), str(original_dir.parent / "orders-renamed")) + + diff_result = w.diff() + change_types = sorted(c["change_type"] for c in diff_result["changes"]) + + assert change_types != ["added", "deleted"], ( + "a plain directory move was classified as delete + create" + ) + + +# =========================================================================== +# J -- `sync pull --branch dev` reports untouched production configs as +# "removed" because the stale-entry sweep is unscoped by branch tree. +# =========================================================================== + + +@pytest.mark.xfail( + strict=True, + reason=( + "#792 J: pull()'s stale-entry sweep (sync_service.py ~1063) compares " + "the freshly-fetched keys against the FULL old manifest." + "configurations, not scoped to the branch just pulled. A `sync pull " + "--branch dev` after a production pull reports every untouched " + "production entry as 'removed' -- the exact label sync-workflow.md " + "documents as meaning 'the config was genuinely deleted on the " + "remote', which it was not. Confirmed via spec S4." + ), +) +def test_j_branch_scoped_pull_does_not_report_other_branch_configs_removed( + tmp_config_dir: Path, tmp_path: Path +) -> None: + """Invariant: pulling a different branch than the one the manifest + currently reflects must never report an untouched, still-live config on + the ORIGINAL branch as `"removed"` -- that label is documented to mean + the remote genuinely deleted it. + + Issue #792 finding J. + """ + project_root = tmp_path / "project" + project_root.mkdir() + store = _init_and_pull(tmp_config_dir, project_root, SAMPLE_COMPONENTS_NO_ROWS) + + # Dev branch fetch does not carry keboola.ex-http/cfg-001 at all (a + # different component entirely) -- production's cfg-001 is untouched and + # still live, just not part of THIS fetch. + dev_components = [ + { + "id": "keboola.snowflake-transformation", + "type": "transformation", + "configurations": [ + { + "id": "cfg-dev-only", + "name": "Dev Only", + "description": "", + "configuration": {"parameters": {}}, + "rows": [], + } + ], + } + ] + dev_client = _make_mock_client( + components_response=dev_components, + branches_response=SAMPLE_BRANCHES_WITH_DEV, + ) + dev_svc = SyncService(config_store=store, client_factory=lambda url, token: dev_client) + result = dev_svc.pull(alias="prod", project_root=project_root, branch_override=99999) + + removed = [d for d in result["details"] if d["action"] == "removed"] + assert removed == [], ( + "production's cfg-001 was reported 'removed' by a dev-branch pull that never touched production" + ) + + +# =========================================================================== +# K -- a cosmetic local edit (raw-hash change, not a semantic change) blocks +# pull from ever applying a real remote change. Documented, intentional +# conservative behavior -- NOT a safety violation, so this is a plain +# (unmarked) regression guard on the safe half of the trade-off. +# =========================================================================== + + +def test_k_cosmetic_edit_is_conservative_not_unsafe(tmp_config_dir: Path, tmp_path: Path) -> None: + """NOT a safety violation: pull's raw-file-hash check is documented, + intentional, conservative behavior ("Pull protects local edits: + locally-modified files are skipped by default", + plugins/kbagent/skills/kbagent/references/sync-workflow.md). A purely + cosmetic edit (here: an appended YAML comment, which changes the raw + file hash but not `config_hash`) is still treated as "locally modified" + and the file is preserved rather than overwritten with the real remote + change underneath it. + + This regression test asserts the SAFE half of that trade-off: pull + never silently discards/corrupts local content, even when it happens to + be byte-different-but-semantically-identical to the last pulled base. + The liveness cost (a real remote change is stuck until the cosmetic + edit is reverted, or `--theirs` is used) is a deliberate, documented + trade-off, not the safety property this pilot models -- issue #792 + finding K (spec S3, TLA I12). + """ + project_root = tmp_path / "project" + project_root.mkdir() + store = _init_and_pull(tmp_config_dir, project_root, SAMPLE_COMPONENTS_NO_ROWS) + + manifest = load_manifest(project_root) + cfg = next(c for c in manifest.configurations if c.component_id == "keboola.ex-http") + config_file = project_root / "main" / cfg.path / CONFIG_FILENAME + original_bytes = config_file.read_bytes() + + # Purely cosmetic edit: append a YAML comment. Parses to the identical + # dict (config_hash unchanged) but the raw file hash changes. + config_file.write_bytes(original_bytes + b"\n# cosmetic comment, no semantic change\n") + + # Remote genuinely changes in the meantime. + base_component: dict[str, Any] = SAMPLE_COMPONENTS_NO_ROWS[0] + base_config: dict[str, Any] = base_component["configurations"][0] + changed_remote = [ + { + **base_component, + "configurations": [ + { + **base_config, + "configuration": { + "parameters": {"baseUrl": "https://real-remote-change.example.com"} + }, + } + ], + } + ] + svc, _ = _svc_with_client(store, changed_remote) + result = svc.pull(alias="prod", project_root=project_root) + + # Safe: the cosmetically-edited file is preserved verbatim, never + # silently clobbered by the remote write. + after = config_file.read_text(encoding="utf-8") + assert "cosmetic comment" in after + detail = next(d for d in result["details"] if d["component_id"] == "keboola.ex-http") + assert detail["action"] == "skipped" + assert detail["reason"] == "locally modified"