Preserve water-warning obligations across detector updates

.github/workflows/verify.yml

@@ -44,6 +44,8 @@ jobs:
           persist-credentials: false
       - name: Recheck proofs, rejection controls, runtime and observed agreement
         run: python3 proofs/agda/verify.py --ci
+      - name: Exercise water-warning continuity and acknowledgement scenarios
+        run: mix run -e 'Firmboot.WaterLeak.Experiment.run()'
       - name: Ensure observed witnesses are reproducible
         run: |
           git -c safe.directory="$GITHUB_WORKSPACE" -C "$GITHUB_WORKSPACE" rev-parse --show-toplevel

PURPOSE.md

@@ -56,10 +56,12 @@ as a distinct objective. USGS documents the public uses and quality assurance of
 [streamflow monitoring](https://www.usgs.gov/programs/groundwater-and-streamflow-information-program/streamflow-monitoring).
 Those sources motivate the domains; they provide no validation of Firmboot.
 
-A useful first domain study would be **continuity of a water-leak warning
-episode**, using recorded or simulated inputs. It maps directly to the existing
-experiment's history and no-duplicate-report questions. Establish the observation
-contract and detection-quality limits before considering any physical control.
+The first domain study now implements **continuity of a water-leak warning
+episode**, using simulated interval volumes. Its resident ledger preserves raw
+measurements, warning identity and outstanding operator acknowledgements across
+a detector update. See the [reproducible experiment and proof boundaries](docs/water-leak-experiment.md).
+It establishes a finite software contract; detection quality, physical control
+and measured ecological benefits remain separate obligations.
 
 ## Continuity must include limits and stopping
 

README.md

@@ -11,7 +11,8 @@ part is the system's continuing obligations; its implementation may evolve.
 This directory contains the first **Elixir executable reference model**, a
 specification, an independent event oracle, controlled fault injections, a
 buffered-restart comparison, a **live preparation-failure experiment**, and
-**machine-checked Lean continuity and controller proofs**, and an **Agda
+an **ecological water-warning continuity simulation**, **machine-checked Lean
+continuity and controller proofs**, and an **Agda
 activation contract using the repaired epistemic and Echo foundations**.
 It is a research prototype, with two known detector implementations and checked
 models; a released language and general live-code loading remain future work.
@@ -46,6 +47,7 @@ mix compile --warnings-as-errors
 mix test --seed 0
 mix run -e 'Firmboot.Experiment.run()'
 mix run -e 'Firmboot.LiveExperiment.run()'
+mix run -e 'Firmboot.WaterLeak.Experiment.run()'
 bash proofs/lean/verify.sh
 sonar analyze secrets proofs/agda/verify.py
 python3 proofs/agda/verify.py --epistemic-src /path/to/epistemic-types/src --report-dir /path/to/verification-output
@@ -73,20 +75,30 @@ modeled capacity. It preserves the same input and event meaning where capacity
 suffices, but completion is delayed. With a sufficiently relaxed decision deadline,
 that simpler baseline is adequate. See [the experiment report](REPORT.md).
 
+The [water-warning experiment](docs/water-leak-experiment.md) adds simulated raw
+volume readings and a resident warning/acknowledgement ledger. An active warning
+retains its identity through a detector update. Its obligation remains pending
+after the signal clears until explicitly acknowledged. The experiment checks
+acknowledgement before and after activation, plus rejection of a corrupt migration.
+
 ## What is and is not established
 
 - **Implemented:** a deterministic transition model for two known detector
   versions; state migration checks; assigned timing budgets; an independent
-  logical event oracle; a finite buffered-restart model.
+  logical event oracle; a finite buffered-restart model; a finite water-warning
+  simulation with exact raw-reading and acknowledgement journals.
 - **Test evidence:** exact executed commands, finite coverage and outcomes are
   recorded in [REPORT.md](REPORT.md).
 - **Live process evidence:** preparation runs separately with cancellation,
   timeouts, stale-reply checks and acknowledged worker retirement. The expanded
-  suite passes 33 tests. See [LIVE-REPORT.md](LIVE-REPORT.md).
+  live experiment's recorded suite had 33 tests. See [LIVE-REPORT.md](LIVE-REPORT.md).
+  The current suite has 43 tests, including ten water-warning tests and 640 short
+  domain trajectories. See [the domain evidence and limits](docs/water-leak-experiment.md).
 - **Formal proof:** Lean 4.33.1 checks migration, arbitrary finite-run input and
   event continuity, boundary ownership, rejection, conditional assigned-cost
-  deadlines, and bounded resolution of an abstract update attempt. All 79 named
-  lemmas and witnesses have a pinned axiom audit; five false-claim controls are
+  deadlines, bounded resolution of an abstract update attempt, and preservation of
+  water-warning obligations and receipts. All 95 named
+  lemmas and witnesses have a pinned axiom audit; seven false-claim controls are
   rejected. See the
   [proof report and reproduction command](proofs/lean/README.md). Correspondence
   of the complete Elixir implementation to that model remains unproved.
@@ -129,6 +141,8 @@ have been demonstrated.
 | [proofs/agda](proofs/agda/README.md) | Current-state/Echo activation checker, service-preserving lifecycle proofs and concrete Elixir comparisons |
 | [live.ex](lib/firmboot/live.ex) | Live preparation worker, timeout/cancellation protocol and bounded diagnostics |
 | [live_experiment.ex](lib/firmboot/live_experiment.ex) | Reproducible hung-worker and recovery experiment |
+| [water_leak.ex](lib/firmboot/water_leak.ex) | Resident raw-reading, warning and acknowledgement ledgers |
+| [water-warning experiment](docs/water-leak-experiment.md) | Reproduction, independent fixture checks, scoped proofs and domain limits |
 | [CONTINUITY.md](CONTINUITY.md) | Continuity contracts, remaining failure domains and next implementation milestones |
 
 ## Next research step

VERIFICATION.md

@@ -12,8 +12,8 @@ the workflows in this checkout. A configured workflow is not a successful run.
 
 | Check | Evidence required |
 |---|---|
-| Agda contract and Elixir agreement | Every Agda source module checks with safe mode, without K, internal double checking and warnings as errors; all 11 intentional false claims fail for the specified type mismatch; a nonempty Elixir test suite passes; all 64 observed agreement witnesses regenerate and check; the generated source remains unchanged. |
-| Lean continuity and axiom audit | Every discovered `Firmboot/` module builds with warnings as errors; all named axiom expectations in `Audit.lean` match; all declarations owned by those modules use only the three allowed standard Lean axioms; a planted custom axiom and all five false-claim controls are rejected for the intended reason. |
+| Agda contract and Elixir agreement | Every Agda source module checks with safe mode, without K, internal double checking and warnings as errors; all 11 intentional false claims fail for the specified type mismatch; a nonempty Elixir test suite passes, including the water-warning scenarios, 640 short domain traces and checker mutation controls; the water-warning CLI succeeds; all 64 observed agreement witnesses regenerate and check; the generated source remains unchanged. |
+| Lean continuity and axiom audit | Every discovered `Firmboot/` module builds with warnings as errors; all named axiom expectations in `Audit.lean` match; all declarations owned by those modules use only the three allowed standard Lean axioms; a planted custom axiom and all seven false-claim controls are rejected for the intended reason. |
 | Actions dependency lock | The authoritative GitHub verifier confirms native lockfile coverage of workflow dependencies. |
 | CodeQL (actions), CodeQL (python) | Analyze the workflow and verifier languages actually present. Agda and Elixir semantics are checked by their proof/compiler/test tools. |
 | secret-scan / gitleaks | The shared secret scanner checks the repository for credentials. |
@@ -56,6 +56,7 @@ python3 proofs/agda/verify.py \
   --epistemic-src /path/to/epistemic-types/src \
   --report-dir /path/to/verification-output
 bash proofs/lean/verify.sh
+mix run -e 'Firmboot.WaterLeak.Experiment.run()'
 actionlint
 gh actions-lock --no-fix
 ```
@@ -71,3 +72,8 @@ The Agda model and Lean model have separate assumptions. The 64 comparisons with
 Elixir are finite observations; an arbitrary-run refinement between the models,
 the language and the runtime remains an open obligation. No total memory or
 wall-clock progress guarantee is established by these checks.
+
+The water-warning contract and its narrower source/model correspondence are
+documented in [the domain experiment](docs/water-leak-experiment.md). Its receipt
+ledger is resident, in memory and unauthenticated; the checks do not establish
+durable delivery, leak-classification quality or physical water-system safety.

docs/water-leak-experiment.md

@@ -0,0 +1,133 @@
+# Water-warning continuity during an update
+
+This finite experiment changes Firmboot's detector while a simulated water warning
+is awaiting acknowledgement. It preserves the original measurements, the warning's
+identity and its first acknowledgement receipt. A return to a normal signal does
+not acknowledge the warning. The purpose is to make ecological service continuity
+concrete without claiming that software continuity establishes physical safety or
+water savings.
+
+## Run
+
+With the Elixir/OTP toolchain described in the [README](../README.md):
+
+```sh
+mix run -e 'Firmboot.WaterLeak.Experiment.run()'
+mix test --seed 0
+bash proofs/lean/verify.sh
+```
+
+The command executes three scenarios and checks every prefix against its original
+fixture: acknowledgement after activation, acknowledgement during preparation,
+and rejection of a migration which would erase the detector's report flag.
+All inputs are generated locally. No sensor, network or actuator is involved.
+
+## Observation and responsibility contract
+
+Each input is exactly `{seq, inlet_ml, outlet_ml}`: a consecutive positive sequence
+number and nonnegative integer volumes for the same simulated interval. The
+source label is `sim-loop`. The fixed threshold is 100 ml of inlet-minus-outlet
+imbalance. Values below it produce a low sample; values at or above it produce a
+high sample. Gaps, duplicates, fractional or negative quantities, and extra input
+fields are rejected before capture. The threshold and source cannot be changed
+through the detector-update request.
+
+The illustrative twelve-sample fixture uses 1,000 ml inlet volume throughout,
+with outlet volumes of 1,000 ml for low samples and 850 ml for high samples:
+
+```text
+sequence: 1 2 3 4 5 6 7 8 9 10 11 12
+signal:   0 0 1 1 1 1 0 0 1  1  1  0
+```
+
+This is a synthetic interpretation, not a calibrated leak classifier. Storage
+changes, legitimate demand, timing differences and measurement error would need
+their own treatment in a physical system. Neither the threshold nor the fixture
+justifies a control decision.
+
+V1 reports after two high samples; V2 requires three. A warning ID consists of the
+source and the first high sequence number, for example `{"sim-loop", 3}`. A later
+separate signal episode gets a different ID. The first warning's original
+reporting version and detection position remain in the ledger after the update.
+
+An acknowledgement names an existing warning and an operator label, and records
+the current sample boundary. It means the simulated operator acknowledged that
+warning, **not that a leak was repaired or an incident resolved**. A same-operator
+retry leaves the first receipt unchanged. A different operator cannot overwrite
+it. Unknown warnings, a different source and empty operator labels are rejected.
+Labels are not credentials; there is no authentication or authorisation protocol.
+
+The measurement journal, warning ledger and receipt journal remain resident.
+The update changes only which of the two already compiled detectors is dispatched.
+Preservation follows from this restricted boundary; it does not demonstrate
+migration of the ledger itself or admission of arbitrary replacement code.
+
+## Executed boundary trace
+
+The normal scenario requests V2 immediately before sample 5, with one preparation
+tick. Each sample is processed before the update phase at that boundary.
+
+| Boundary | Detector processing that sample | Detector active afterward | First warning |
+|---|---|---|---|
+| 4 | V1 | V1 | Reported with ID `sim-loop:3`; acknowledgement pending |
+| 5 | V1 | V1 | Preparation runs; warning remains pending |
+| 6 | V1 | V2 | Activation succeeds; the same warning remains pending |
+| 7 | V2 | V2 | Signal clears; explicit acknowledgement records the first receipt |
+| 11 | V2 | V2 | A new warning, `sim-loop:9`, is reported and remains pending |
+
+A separate run without acknowledgement confirms that clearing the signal at 7
+leaves the first obligation outstanding. When acknowledgement is issued at 5,
+its exact receipt survives activation at 6. When the candidate's report flag is
+deliberately corrupted, activation is rejected; V1 continues observing and reports
+the second warning at 10. Every complete CLI scenario retains all twelve raw
+readings, two warning identities and one receipt, with only `sim-loop:9` pending.
+
+## Evidence and its limits
+
+| Layer | Checked result | Scope |
+|---|---|---|
+| Executable scenarios | Raw readings, detector events, warning identities and receipts match the original fixture and issued acknowledgement transcript at every prefix | Three finite twelve-sample scenarios in `WaterLeak.Experiment`; uses the pure `Model`, not the separate live worker runner |
+| Runtime tests | Ten domain tests, including 640 six-sample trajectories: all 64 binary traces, both initial versions and five request positions | Some short traces defer or end before activation; these are checked too. The complete repository suite has 43 tests |
+| Checker controls | Dropped/rewritten readings, erased/duplicated warnings, altered threshold, erased/invented receipts, premature/duplicate/out-of-order acknowledgement commands are rejected | Test mutations exercise failure as well as success; the checker receives the original input and command transcript from the test caller |
+| Lean model | Sixteen named lemmas and witnesses for handover, receipt preservation, acknowledgement, exact capture and pending obligations | Kernel-checked statements about the explicitly defined `WaterLeak` semantics; audited together with the existing proofs |
+| False-claim controls | Lean rejects claims that activation clears the pending warning or that an acknowledgement for another source discharges it | Both must fail because the proposition is false, not because of a syntax or import error |
+
+The domain checker reconstructs expected warnings from detector events only after
+the existing independent binary oracle has checked those events. A failed detector
+check makes the domain check fail. The oracle uses the update audit as the intended
+version timeline; it is not an authenticated external execution log. Command
+transcripts are trusted, well-shaped test inputs, not an untrusted network API.
+
+The [Lean module](../proofs/lean/Firmboot/WaterLeak.lean) proves for arbitrary model
+states and candidates that handover preserves raw readings, committed reports,
+receipts and the outstanding status of each key. Sampling preserves receipts and
+cannot discharge an already outstanding warning. Valid capture prepends the exact
+reading; a wrong sequence leaves state unchanged. Acknowledgement discharges the
+named pending obligation and cannot overwrite its first receipt. Acknowledgement
+and activation commute **at the same observation boundary**. This does not say an
+acknowledgement can be moved across a sample that first creates its warning.
+
+The model uses natural numbers for opaque source/operator labels and returns
+unchanged state for rejected acknowledgement/capture operations. Elixir validates
+text labels and quantities and returns error tuples for rejected operations.
+The formal sampling function takes a positive threshold at each call; the runtime
+fixes it at construction. The preservation lemmas hold for any supplied threshold,
+but do not prove a threshold-update admission policy. Neither representation is a
+formally verified translation of the other. The tests supply finite agreement
+evidence; a whole-program refinement proof remains open.
+
+All journals here are finite, growing, in-memory lists/maps. There is no durable
+restart recovery, bounded total storage, multi-source aggregation, independent
+standby, remote delivery guarantee or protection from arbitrary memory corruption.
+The existing model's assigned timing costs cover its detector/update transitions;
+the additional raw-record and acknowledgement work is not included in those costs.
+No wall-clock deadline or full water-monitoring timing theorem follows.
+
+## Next obligation
+
+Keep this fixture as a regression contract. Relate the concrete wrapper and
+detector transitions to the formal semantics before broadening claims about the
+implementation. A subsequent failure experiment can target a resident journal
+with explicit recovery and acknowledgement replay rules, including the exact
+boundary at which a receipt becomes durable. Physical measurements, calibration,
+energy/water accounting and control authority require separate domain evidence.