|
| 1 | +--- |
| 2 | +metadata: |
| 3 | + version: "1.0.0" |
| 4 | + kind: pattern |
| 5 | + created: "2026-08-10" |
| 6 | + author: "PAIML Engineering" |
| 7 | + description: | |
| 8 | + Source-content identity — the BYTES a `source:` names are part of the |
| 9 | + desired state, not just the path string. |
| 10 | +
|
| 11 | + hash_desired_state hashes resource FIELD STRINGS. For `content:` that is |
| 12 | + correct: the content IS the field. For `source:` the field is a PATH, so |
| 13 | + editing the referenced file left the hash identical, determine_present_action |
| 14 | + planned NoOp, and `apply` printed "unchanged" over stale content on the |
| 15 | + machine. |
| 16 | +
|
| 17 | + This is the completeness leg of idempotent-apply-v1. That contract asserts |
| 18 | + "Converged lock entry with differing hash always plans Update", which is |
| 19 | + sound but vacuous if the hash cannot differ when the deployed artifact |
| 20 | + differs. A declarative tool that reports success while not converging is |
| 21 | + strictly worse than one that fails loudly. |
| 22 | +
|
| 23 | + IMPLEMENTATION NOTES |
| 24 | +
|
| 25 | + canonical_source_content returns the empty string when `source:` is absent, |
| 26 | + and the component is pushed only when non-empty — APPENDING, never inserting, |
| 27 | + because field order is hash identity and a reorder would invalidate every |
| 28 | + recorded hash on every machine in the fleet. |
| 29 | +
|
| 30 | + The path is read exactly as written, matching resources::file's own |
| 31 | + source_file_base64: both resolve relative to the process CWD, so the planner |
| 32 | + hashes precisely the bytes that apply would upload. |
| 33 | +
|
| 34 | + An unreadable source folds its error into the component rather than hashing |
| 35 | + as absent, so a file that appears or disappears changes the hash instead of |
| 36 | + masquerading as "unchanged"; apply still fails loudly with |
| 37 | + "cannot read source file". |
| 38 | +
|
| 39 | + Failure mode is plan_update rather than an assert: when the bytes differ the |
| 40 | + resource simply plans Update, which is the correct convergent behaviour. |
| 41 | +
|
| 42 | + NO KANI HARNESS, DELIBERATELY. The property quantifies over the CONTENTS OF |
| 43 | + THE FILESYSTEM, which is outside Kani's model — a harness here could only |
| 44 | + prove something about a stubbed read, i.e. prove nothing about the bug. The |
| 45 | + obligations are discharged by the seven falsification tests instead, of which |
| 46 | + FALSIFY-SRC-006 is the end-to-end one that actually reproduces the reported |
| 47 | + defect. Declaring an unrunnable harness to satisfy a schema would be exactly |
| 48 | + the vacuous-contract failure this repo's review process exists to catch. |
| 49 | + references: |
| 50 | + - "issue: https://github.com/paiml/forjar/issues/206" |
| 51 | + - "idempotent-apply-v1.yaml — the soundness leg this completes" |
| 52 | + - "paiml/infra PMAT-204 — observed live: an edited reconciler script reported |
| 53 | + 'converged' three times while the machine kept running the previous copy" |
| 54 | + - "src/core/planner/hashing.rs — canonical_source_content" |
| 55 | + |
| 56 | +equations: |
| 57 | + source_content_identity: |
| 58 | + formula: | |
| 59 | + ∀ r ∈ Resource with r.source = Some(p): |
| 60 | + bytes(p) ≠ bytes'(p) ⟹ hash_desired_state(r) ≠ hash_desired_state'(r) |
| 61 | + domain: "r ∈ Resource, p ∈ Path" |
| 62 | + codomain: "String ('blake3:' || hex digest)" |
| 63 | + invariants: |
| 64 | + - "Changing the bytes at `source:` changes the desired-state hash" |
| 65 | + - "Identical bytes at an identical path hash identically (determinism)" |
| 66 | + - "Identical bytes at DIFFERENT paths hash differently: the path remains |
| 67 | + part of resource identity" |
| 68 | + - "A source file appearing or disappearing changes the hash" |
| 69 | + |
| 70 | + source_free_stability: |
| 71 | + formula: | |
| 72 | + ∀ r ∈ Resource with r.source = None: |
| 73 | + hash_desired_state_after(r) = hash_desired_state_before(r) |
| 74 | + domain: "r ∈ Resource without a source field" |
| 75 | + codomain: "String" |
| 76 | + invariants: |
| 77 | + - "Resources without `source:` keep their pre-existing hash: the content |
| 78 | + component is APPENDED and only when non-empty, so no recorded hash on |
| 79 | + any machine in the fleet is invalidated" |
| 80 | + |
| 81 | +proof_obligations: |
| 82 | + - type: completeness |
| 83 | + property: "A change to deployed bytes is always observable in the hash" |
| 84 | + formal: "bytes(p) ≠ bytes'(p) ⟹ hash ≠ hash'" |
| 85 | + tolerance: 0.0 |
| 86 | + applies_to: "file resources declaring source:" |
| 87 | + - type: determinism |
| 88 | + property: "Hashing the same resource over unchanged bytes is stable" |
| 89 | + formal: "hash_desired_state(r) = hash_desired_state(r)" |
| 90 | + tolerance: 0.0 |
| 91 | + applies_to: all |
| 92 | + - type: independence |
| 93 | + property: "Path identity survives content equality" |
| 94 | + formal: "p ≠ q ∧ bytes(p) = bytes(q) ⟹ hash(r_p) ≠ hash(r_q)" |
| 95 | + tolerance: 0.0 |
| 96 | + applies_to: "file resources declaring source:" |
| 97 | + - type: invariant |
| 98 | + property: "Source-less resources retain their existing hash identity" |
| 99 | + formal: "r.source = None ⟹ hash unchanged across this change" |
| 100 | + tolerance: 0.0 |
| 101 | + applies_to: "resources without source:" |
| 102 | + |
| 103 | +falsification_tests: |
| 104 | + - id: FALSIFY-SRC-001 |
| 105 | + rule: "Source content change is observable" |
| 106 | + prediction: "Rewriting a source file changes hash_desired_state" |
| 107 | + test: "src/core/planner/tests_hash_source.rs::source_content_change_changes_desired_hash" |
| 108 | + if_fails: "plan reports NoOp and apply deploys stale content while printing 'unchanged'" |
| 109 | + - id: FALSIFY-SRC-002 |
| 110 | + rule: "Determinism preserved" |
| 111 | + prediction: "Two hashes over unchanged bytes are equal" |
| 112 | + test: "src/core/planner/tests_hash_source.rs::identical_source_content_hashes_identically" |
| 113 | + if_fails: "every apply re-uploads every source file — spurious churn, no fixed point" |
| 114 | + - id: FALSIFY-SRC-003 |
| 115 | + rule: "Path remains part of identity" |
| 116 | + prediction: "Same bytes at two paths hash differently" |
| 117 | + test: "src/core/planner/tests_hash_source.rs::two_sources_with_same_content_but_different_paths_differ" |
| 118 | + if_fails: "two resources collide whenever their sources happen to match" |
| 119 | + - id: FALSIFY-SRC-004 |
| 120 | + rule: "Appearance of a source file is observable" |
| 121 | + prediction: "missing → present changes the hash" |
| 122 | + test: "src/core/planner/tests_hash_source.rs::missing_source_is_distinguishable_from_present_source" |
| 123 | + if_fails: "a resource stays pinned at 'unchanged' after its source appears" |
| 124 | + - id: FALSIFY-SRC-005 |
| 125 | + rule: "Source-less resources unaffected" |
| 126 | + prediction: "package and inline-content resources hash as before" |
| 127 | + test: "src/core/planner/tests_hash_source.rs::resource_without_source_is_unaffected" |
| 128 | + if_fails: "every recorded hash on every machine in the fleet is invalidated" |
| 129 | + - id: FALSIFY-SRC-006 |
| 130 | + rule: "End-to-end convergence" |
| 131 | + prediction: "apply → edit source → apply deploys the NEW bytes without --force" |
| 132 | + test: "manual: see contracts/README or the GH-206 reproduction; asserts deployed |
| 133 | + content equals the edited source after a second plain apply" |
| 134 | + if_fails: "the user-visible bug is still present regardless of unit-test status" |
| 135 | + - id: FALSIFY-SRC-007 |
| 136 | + rule: "No regression in the existing suite" |
| 137 | + prediction: "cargo test --lib reports 0 failures" |
| 138 | + test: "cargo test --lib" |
| 139 | + if_fails: "hash identity change broke planner, lock, or drift behaviour" |
| 140 | + |
| 141 | +qa_gate: |
| 142 | + id: F-SRC-001 |
| 143 | + name: "Source Content Identity Contract" |
| 144 | + description: "The bytes behind `source:` are part of the desired state" |
| 145 | + checks: |
| 146 | + - "source_content_identity" |
| 147 | + - "source_free_stability" |
| 148 | + pass_criteria: "All 7 falsification tests pass, including the end-to-end reproduction" |
| 149 | + falsification: "Revert canonical_source_content to hashing only the path string; |
| 150 | + FALSIFY-SRC-001 and -004 must then fail" |
| 151 | + |
| 152 | +verification_level: L3 |
0 commit comments