From 72422af969b3991ab24c6337a8c10275f5aec8b9 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 7 Sep 2026 04:33:52 +0100 Subject: [PATCH] Model water-warning continuity and acknowledgements across updates --- .github/workflows/verify.yml | 2 + PURPOSE.md | 10 +- README.md | 24 ++- VERIFICATION.md | 10 +- docs/water-leak-experiment.md | 133 +++++++++++++++ lib/firmboot/water_leak.ex | 101 ++++++++++++ lib/firmboot/water_leak/checker.ex | 62 +++++++ lib/firmboot/water_leak/experiment.ex | 77 +++++++++ proofs/lean/Audit.lean | 64 ++++++++ proofs/lean/Firmboot.lean | 1 + proofs/lean/Firmboot/WaterLeak.lean | 148 +++++++++++++++++ proofs/lean/README.md | 34 +++- .../lean/controls/AcknowledgeOtherSource.lean | 5 + .../lean/controls/ClearWarningOnUpdate.lean | 5 + proofs/lean/verify.sh | 4 +- test/firmboot/water_leak_test.exs | 155 ++++++++++++++++++ 16 files changed, 816 insertions(+), 19 deletions(-) create mode 100644 docs/water-leak-experiment.md create mode 100644 lib/firmboot/water_leak.ex create mode 100644 lib/firmboot/water_leak/checker.ex create mode 100644 lib/firmboot/water_leak/experiment.ex create mode 100644 proofs/lean/Firmboot/WaterLeak.lean create mode 100644 proofs/lean/controls/AcknowledgeOtherSource.lean create mode 100644 proofs/lean/controls/ClearWarningOnUpdate.lean create mode 100644 test/firmboot/water_leak_test.exs diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 9f17f1b..3a96584 100644 --- a/.github/workflows/verify.yml +++ b/.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 diff --git a/PURPOSE.md b/PURPOSE.md index d89da51..1263e2f 100644 --- a/PURPOSE.md +++ b/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 diff --git a/README.md b/README.md index 5ae6468..ff90c33 100644 --- a/README.md +++ b/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 diff --git a/VERIFICATION.md b/VERIFICATION.md index 4a86b18..c505072 100644 --- a/VERIFICATION.md +++ b/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. diff --git a/docs/water-leak-experiment.md b/docs/water-leak-experiment.md new file mode 100644 index 0000000..d8e3d51 --- /dev/null +++ b/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. diff --git a/lib/firmboot/water_leak.ex b/lib/firmboot/water_leak.ex new file mode 100644 index 0000000..eef9ca9 --- /dev/null +++ b/lib/firmboot/water_leak.ex @@ -0,0 +1,101 @@ +defmodule Firmboot.WaterLeak do + @moduledoc """ + Finite water-monitoring simulation over Firmboot's existing transition model. + + Each reading contains inlet/outlet millilitres for the same simulated interval. + An imbalance at or above the fixed threshold is a high detector sample. This + is a synthetic signal interpretation, not a validated physical leak detector. + + A warning is identified by {source, first_high_sequence}. The resident ledger + outlives the active signal episode: a low sample does not acknowledge a warning. + Only detector dispatch changes during an update. Journals are in memory and + grow for the finite run; operator labels are not authenticated identities. + """ + alias Firmboot.{Model, Update} + + defstruct [:source, :threshold_ml, :model, observations: [], warnings: %{}, receipts: []] + + def new(options \\ []) do + options = Keyword.validate!(options, source: "sim-loop", threshold_ml: 100, model: []) + + unless label?(options[:source]) and is_integer(options[:threshold_ml]) and + options[:threshold_ml] > 0 do + raise ArgumentError, "source must be a nonempty label and threshold_ml a positive integer" + end + + %__MODULE__{ + source: options[:source], + threshold_ml: options[:threshold_ml], + model: Model.new(options[:model]) + } + end + + def request(state, %Update{} = update), do: %{state | model: Model.request(state.model, update)} + + def sample(state, %{seq: seq, inlet_ml: inlet, outlet_ml: outlet} = reading) + when is_integer(seq) and seq > 0 and is_integer(inlet) and inlet >= 0 and + is_integer(outlet) and outlet >= 0 and map_size(reading) == 3 do + if seq == state.model.seq + 1 do + value = if inlet - outlet >= state.threshold_ml, do: 1, else: 0 + model = Model.tick(state.model, value) + event = Enum.find(model.events, &(&1.detected_at == seq)) + + warnings = + if event do + id = {state.source, event.episode} + + if Map.has_key?(state.warnings, id), + do: raise("detector attempted to publish a duplicate warning") + + Map.put(state.warnings, id, %{ + id: id, + detected_at: event.detected_at, + version: event.version, + acknowledgement: nil + }) + else + state.warnings + end + + {:ok, + %{state | model: model, observations: [reading | state.observations], warnings: warnings}} + else + {:error, {:expected_sequence, state.model.seq + 1}} + end + end + + def sample(_state, _reading), do: {:error, :invalid_reading} + + def acknowledge(state, id, operator) do + if label?(operator) do + case Map.fetch(state.warnings, id) do + :error -> + {:error, :unknown_warning} + + {:ok, %{acknowledgement: nil} = warning} -> + receipt = %{id: id, by: operator, after_seq: state.model.seq} + warnings = Map.put(state.warnings, id, %{warning | acknowledgement: receipt}) + {:ok, %{state | warnings: warnings, receipts: [receipt | state.receipts]}} + + {:ok, %{acknowledgement: %{by: ^operator}}} -> + {:ok, state} + + {:ok, _warning} -> + {:error, :already_acknowledged} + end + else + {:error, :invalid_operator} + end + end + + def outstanding(state) do + state.warnings + |> Map.values() + |> Enum.filter(&is_nil(&1.acknowledgement)) + |> Enum.map(& &1.id) + |> Enum.sort() + end + + defp label?(value), + do: is_binary(value) and String.valid?(value) and String.trim(value) != "" +end diff --git a/lib/firmboot/water_leak/checker.ex b/lib/firmboot/water_leak/checker.ex new file mode 100644 index 0000000..5ff1b47 --- /dev/null +++ b/lib/firmboot/water_leak/checker.ex @@ -0,0 +1,62 @@ +defmodule Firmboot.WaterLeak.Checker do + @moduledoc """ + Independent fixture comparison for the water-warning journal. + + Inputs and successfully issued acknowledgement commands come from the caller's + original transcript, not from the state being checked. The binary event oracle + independently establishes detector reports; this checker then reconstructs the + expected warning and receipt ledgers. It does not call WaterLeak transitions. + This is finite test evidence, not a proof of runtime refinement or authenticity. + """ + + def verify(readings, acknowledgements, state, contract) do + source = Keyword.fetch!(contract, :source) + threshold = Keyword.fetch!(contract, :threshold_ml) + initial = Keyword.get(contract, :version, :v1) + values = Enum.map(readings, &if(&1.inlet_ml - &1.outlet_ml >= threshold, do: 1, else: 0)) + core = Firmboot.Checker.verify(values, state.model, initial) + events = Enum.reverse(state.model.events) + reports = Map.new(events, &{{source, &1.episode}, &1}) + receipts = Map.new(acknowledgements, &{&1.id, &1}) + + valid_commands = + map_size(receipts) == length(acknowledgements) and + acknowledgements == Enum.sort_by(acknowledgements, & &1.after_seq) and + Enum.all?(acknowledgements, fn receipt -> + case Map.fetch(reports, receipt.id) do + {:ok, event} -> + is_integer(receipt.after_seq) and receipt.after_seq >= event.detected_at and + receipt.after_seq <= length(readings) and is_binary(receipt.by) and + String.valid?(receipt.by) and String.trim(receipt.by) != "" + + :error -> + false + end + end) + + expected = + Map.new(reports, fn {id, event} -> + {id, + %{ + id: id, + detected_at: event.detected_at, + version: event.version, + acknowledgement: Map.get(receipts, id) + }} + end) + + errors = + [ + {state.source == source and state.threshold_ml == threshold, :observation_contract}, + {Enum.reverse(state.observations) == readings, :raw_observation_history}, + {core == :ok, {:detector_contract, core}}, + {valid_commands, :acknowledgement_transcript}, + {state.warnings == expected, :warning_ledger}, + {Enum.reverse(state.receipts) == acknowledgements, :acknowledgement_journal} + ] + |> Enum.reject(&elem(&1, 0)) + |> Enum.map(&elem(&1, 1)) + + if errors == [], do: :ok, else: {:error, errors} + end +end diff --git a/lib/firmboot/water_leak/experiment.ex b/lib/firmboot/water_leak/experiment.ex new file mode 100644 index 0000000..1c96311 --- /dev/null +++ b/lib/firmboot/water_leak/experiment.ex @@ -0,0 +1,77 @@ +defmodule Firmboot.WaterLeak.Experiment do + @moduledoc "Reproducible simulated warning, update and acknowledgement scenarios." + alias Firmboot.{Update, WaterLeak} + alias Firmboot.WaterLeak.Checker + + def contract, do: [source: "sim-loop", threshold_ml: 100] + + def readings do + [0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 1, 0] + |> Enum.with_index(1) + |> Enum.map(fn {high, seq} -> + %{seq: seq, inlet_ml: 1_000, outlet_ml: if(high == 1, do: 850, else: 1_000)} + end) + end + + def scenario(ack_at \\ 7, fault \\ :none) do + Enum.reduce(readings(), {WaterLeak.new(contract()), [], []}, fn reading, + {state, receipts, snapshots} -> + state = + if reading.seq == 5 do + WaterLeak.request(state, %Update{ + id: :water_window_upgrade, + target: :v2, + prepare_ticks: 1, + fault: fault + }) + else + state + end + + {:ok, state} = WaterLeak.sample(state, reading) + + {state, receipts} = + if reading.seq == ack_at do + receipt = %{id: {"sim-loop", 3}, by: "operator-A", after_seq: reading.seq} + {:ok, state} = WaterLeak.acknowledge(state, receipt.id, receipt.by) + {state, receipts ++ [receipt]} + else + {state, receipts} + end + + :ok = Checker.verify(Enum.take(readings(), reading.seq), receipts, state, contract()) + {state, receipts, snapshots ++ [state]} + end) + end + + def run do + IO.puts("Firmboot water-warning continuity — simulated interval volumes, no actuation.") + + for {label, at, fault} <- [ + {"acknowledge after update and after the signal clears", 7, :none}, + {"acknowledge during preparation", 5, :none}, + {"reject a migration that erases report ownership", 7, :reported} + ] do + {state, receipts, _snapshots} = scenario(at, fault) + :ok = Checker.verify(readings(), receipts, state, contract()) + IO.puts("PASS: #{label}") + + IO.puts( + " observations=#{length(state.observations)} warnings=#{map_size(state.warnings)} " <> + "receipts=#{length(receipts)} outstanding=#{inspect(WaterLeak.outstanding(state))}" + ) + end + + {_, _, snapshots} = scenario() + IO.puts("\nBoundary trace: seq / detector used / active after / outstanding warnings") + + for state <- Enum.slice(snapshots, 3, 4) do + IO.puts( + " #{state.model.seq} / #{hd(state.model.frames).version} / #{state.model.version} / " <> + inspect(WaterLeak.outstanding(state)) + ) + end + + :ok + end +end diff --git a/proofs/lean/Audit.lean b/proofs/lean/Audit.lean index ca69032..1aeecd3 100644 --- a/proofs/lean/Audit.lean +++ b/proofs/lean/Audit.lean @@ -315,3 +315,67 @@ import Firmboot /-- info: 'Firmboot.roundtrip_v2' depends on axioms: [propext] -/ #guard_msgs in #print axioms Firmboot.roundtrip_v2 + +/-- info: 'Firmboot.WaterLeak.handover_readings' does not depend on any axioms -/ +#guard_msgs in +#print axioms Firmboot.WaterLeak.handover_readings + +/-- info: 'Firmboot.WaterLeak.handover_receipts' does not depend on any axioms -/ +#guard_msgs in +#print axioms Firmboot.WaterLeak.handover_receipts + +/-- info: 'Firmboot.WaterLeak.handover_reports' depends on axioms: [propext] -/ +#guard_msgs in +#print axioms Firmboot.WaterLeak.handover_reports + +/-- info: 'Firmboot.WaterLeak.handover_outstanding' depends on axioms: [propext, Quot.sound] -/ +#guard_msgs in +#print axioms Firmboot.WaterLeak.handover_outstanding + +/-- info: 'Firmboot.WaterLeak.acknowledgement_discharges' depends on axioms: [propext, Quot.sound] -/ +#guard_msgs in +#print axioms Firmboot.WaterLeak.acknowledgement_discharges + +/-- info: 'Firmboot.WaterLeak.acknowledgement_idempotent' depends on axioms: [propext, Quot.sound] -/ +#guard_msgs in +#print axioms Firmboot.WaterLeak.acknowledgement_idempotent + +/-- info: 'Firmboot.WaterLeak.wrong_source_unchanged' depends on axioms: [propext, Quot.sound] -/ +#guard_msgs in +#print axioms Firmboot.WaterLeak.wrong_source_unchanged + +/-- info: 'Firmboot.WaterLeak.unknown_warning_unchanged' depends on axioms: [propext, Quot.sound] -/ +#guard_msgs in +#print axioms Firmboot.WaterLeak.unknown_warning_unchanged + +/-- info: 'Firmboot.WaterLeak.acknowledge_preserves_readings' depends on axioms: [propext, Quot.sound] -/ +#guard_msgs in +#print axioms Firmboot.WaterLeak.acknowledge_preserves_readings + +/-- info: 'Firmboot.WaterLeak.sample_preserves_receipts' does not depend on any axioms -/ +#guard_msgs in +#print axioms Firmboot.WaterLeak.sample_preserves_receipts + +/-- info: 'Firmboot.WaterLeak.sample_records_exact_reading' depends on axioms: [propext] -/ +#guard_msgs in +#print axioms Firmboot.WaterLeak.sample_records_exact_reading + +/-- info: 'Firmboot.WaterLeak.wrong_sequence_unchanged' depends on axioms: [propext] -/ +#guard_msgs in +#print axioms Firmboot.WaterLeak.wrong_sequence_unchanged + +/-- info: 'Firmboot.WaterLeak.sample_preserves_outstanding' depends on axioms: [propext, Quot.sound] -/ +#guard_msgs in +#print axioms Firmboot.WaterLeak.sample_preserves_outstanding + +/-- info: 'Firmboot.WaterLeak.acknowledge_handover_commute' depends on axioms: [propext, Quot.sound] -/ +#guard_msgs in +#print axioms Firmboot.WaterLeak.acknowledge_handover_commute + +/-- info: 'Firmboot.WaterLeak.active_warning_survives' depends on axioms: [propext, Quot.sound] -/ +#guard_msgs in +#print axioms Firmboot.WaterLeak.active_warning_survives + +/-- info: 'Firmboot.WaterLeak.clear_signal_keeps_obligation' depends on axioms: [propext, Quot.sound] -/ +#guard_msgs in +#print axioms Firmboot.WaterLeak.clear_signal_keeps_obligation diff --git a/proofs/lean/Firmboot.lean b/proofs/lean/Firmboot.lean index 9f41a16..b69f2c9 100644 --- a/proofs/lean/Firmboot.lean +++ b/proofs/lean/Firmboot.lean @@ -3,3 +3,4 @@ import Firmboot.Continuity import Firmboot.Timing import Firmboot.Witnesses import Firmboot.Supervision +import Firmboot.WaterLeak diff --git a/proofs/lean/Firmboot/WaterLeak.lean b/proofs/lean/Firmboot/WaterLeak.lean new file mode 100644 index 0000000..d65c2b5 --- /dev/null +++ b/proofs/lean/Firmboot/WaterLeak.lean @@ -0,0 +1,148 @@ +import Firmboot.Continuity + +/-! +A resident warning/acknowledgement ledger around the reduced detector semantics. +Source and operator identifiers are opaque natural-number labels, not credentials. +Only the detector component is updateable. Raw measurements and acknowledgement +receipts stay resident. This is a model, not a refinement proof for Elixir or a +physical leak-detection theorem. Every list denotes a finite in-memory journal. +-/ +namespace Firmboot.WaterLeak + +structure Key where + source : Nat + episode : Nat + deriving DecidableEq, Repr + +structure Reading where + seq : Nat + inletMl : Nat + outletMl : Nat + deriving DecidableEq, Repr + +structure Receipt where + key : Key + operator : Nat + afterSeq : Nat + deriving DecidableEq, Repr + +structure State where + source : Nat + detector : Continuity.State + readings : List Reading + receipts : List Receipt + deriving DecidableEq, Repr + +def outstanding (s : State) (key : Key) : Bool := + decide (key.source = s.source ∧ key.episode ∈ Continuity.ids s.detector) && + !s.receipts.any (fun r => r.key == key) + +def handover (s : State) (candidate : Option Continuity.Candidate) : State := + { s with detector := Continuity.activate s.detector candidate } + +def acknowledge (s : State) (key : Key) (operator : Nat) : State := + if outstanding s key then + { s with receipts := ⟨key, operator, s.detector.cursor.position⟩ :: s.receipts } + else s + +/-- Volumes cover the same interval; this chosen threshold has no physical calibration. -/ +def sample (s : State) (threshold : Nat) (reading : Reading) : State := + if 0 < threshold ∧ reading.seq = s.detector.cursor.position + 1 then + { s with + detector := Continuity.process s.detector + (decide (reading.outletMl + threshold ≤ reading.inletMl)) + readings := reading :: s.readings } + else s + +@[simp] theorem handover_readings (s : State) (c : Option Continuity.Candidate) : + (handover s c).readings = s.readings := rfl + +@[simp] theorem handover_receipts (s : State) (c : Option Continuity.Candidate) : + (handover s c).receipts = s.receipts := rfl + +@[simp] theorem handover_reports (s : State) (c : Option Continuity.Candidate) : + (handover s c).detector.events = s.detector.events := + Continuity.activate_events s.detector c + +@[simp] theorem handover_outstanding (s : State) (c : Option Continuity.Candidate) (key : Key) : + outstanding (handover s c) key = outstanding s key := by + simp [outstanding, handover, Continuity.ids] + +theorem acknowledgement_discharges (s : State) (key : Key) (operator : Nat) : + outstanding (acknowledge s key operator) key = false := by + unfold acknowledge + split + · simp [outstanding] + · rename_i h + simpa using h + +theorem acknowledgement_idempotent (s : State) (key : Key) (operator other : Nat) : + acknowledge (acknowledge s key operator) key other = acknowledge s key operator := by + rw [acknowledge, acknowledgement_discharges] + rfl + +theorem wrong_source_unchanged (s : State) (key : Key) (operator : Nat) + (h : key.source ≠ s.source) : acknowledge s key operator = s := by + simp [acknowledge, outstanding, h] + +theorem unknown_warning_unchanged (s : State) (key : Key) (operator : Nat) + (h : key.episode ∉ Continuity.ids s.detector) : acknowledge s key operator = s := by + simp [acknowledge, outstanding, h] + +theorem acknowledge_preserves_readings (s : State) (key : Key) (operator : Nat) : + (acknowledge s key operator).readings = s.readings := by + simp [acknowledge] <;> split <;> rfl + +theorem sample_preserves_receipts (s : State) (threshold : Nat) (reading : Reading) : + (sample s threshold reading).receipts = s.receipts := by + simp [sample] <;> split <;> rfl + +theorem sample_records_exact_reading (s : State) (threshold : Nat) (reading : Reading) + (positive : 0 < threshold) (next : reading.seq = s.detector.cursor.position + 1) : + (sample s threshold reading).readings = reading :: s.readings := by + simp [sample, positive, next] + +theorem wrong_sequence_unchanged (s : State) (threshold : Nat) (reading : Reading) + (h : reading.seq ≠ s.detector.cursor.position + 1) : sample s threshold reading = s := by + simp [sample, h] + +/-- Sampling cannot discharge a previously outstanding warning, even after its +signal clears. Only the acknowledgement operation can add a receipt. -/ +theorem sample_preserves_outstanding (s : State) (threshold : Nat) (reading : Reading) + (key : Key) (h : outstanding s key = true) : + outstanding (sample s threshold reading) key = true := by + unfold sample + split + · obtain ⟨added, journal⟩ := Continuity.process_preserves_journal s.detector + (decide (reading.outletMl + threshold ≤ reading.inletMl)) + simp only [outstanding, Bool.and_eq_true, decide_eq_true_eq] at h ⊢ + refine ⟨⟨h.1.1, ?_⟩, h.2⟩ + simp only [Continuity.ids, journal, List.map_append, List.mem_append] + exact Or.inr h.1.2 + · exact h + +/-- Acknowledgement and detector activation commute at the SAME observation boundary. +They are not claimed to commute across a sample that can create a new warning. -/ +theorem acknowledge_handover_commute (s : State) (c : Option Continuity.Candidate) + (key : Key) (operator : Nat) : + acknowledge (handover s c) key operator = handover (acknowledge s key operator) c := by + simp only [acknowledge, handover_outstanding] + split <;> simp [handover] + +def warned : State := + ⟨7, [false, false, true, true, true, true].foldl Continuity.process Continuity.initial, + [⟨6, 1000, 850⟩, ⟨5, 1000, 850⟩, ⟨4, 1000, 850⟩, + ⟨3, 1000, 850⟩, ⟨2, 1000, 1000⟩, ⟨1, 1000, 1000⟩], []⟩ + +def upgrade : Continuity.Candidate := + ⟨.v2, warned.detector.cursor, warned.detector.window⟩ + +theorem active_warning_survives : + (handover warned (some upgrade)).detector.owner = .v2 ∧ + outstanding (handover warned (some upgrade)) ⟨7, 3⟩ = true := by decide + +theorem clear_signal_keeps_obligation : + outstanding (sample (handover warned (some upgrade)) 100 ⟨7, 1000, 1000⟩) ⟨7, 3⟩ = true := by + decide + +end Firmboot.WaterLeak diff --git a/proofs/lean/README.md b/proofs/lean/README.md index 5a602ad..00fc17a 100644 --- a/proofs/lean/README.md +++ b/proofs/lean/README.md @@ -14,15 +14,16 @@ bash verify.sh `lean-toolchain` pins the already installed toolchain. The script builds both the proof library and the axiom audit, treating build warnings as failures. It then -checks five deliberately false claims. These control files are **expected to +checks seven deliberately false claims. These control files are **expected to fail** when passed directly to Lean; the script checks the actual diagnostic, including that `decide` proved the proposition false. A missing tool, import failure, syntax error, warning, or unexpected exit is not a successful control. -The original complete command exited **0**. All **79 named theorems** in +The original complete command exited **0** and audited **79 named theorems** in `Migration.lean`, `Continuity.lean`, `Timing.lean`, `Witnesses.lean`, and -`Supervision.lean` appear in -[Audit.lean](Audit.lean). This count includes helper lemmas and concrete witnesses; +`Supervision.lean`. The current [Audit.lean](Audit.lean) also includes the 16 +water-warning lemmas and witnesses: **95 named theorems in six modules**. +This count includes helper lemmas and concrete witnesses; it is not a count of independent product guarantees. The original output and manifest are in the [historical record](../../docs/history/2026-09-06/README.md) and describe that snapshot. Current verification uses the script and CI in this @@ -89,7 +90,7 @@ kernel-checked witnesses execute both directions, retain an existing episode's single report, and demonstrate V2 ignoring a two-high-sample episode which V1 reports. The guard therefore does not satisfy safety by rejecting every change. -Five executable rejection controls accompany the positive proofs: +Seven executable rejection controls accompany the positive proofs: 1. **Reset ownership without the guard.** An already reported episode is reported again, giving event IDs `[1, 1]`. Lean rejects the no-duplicates claim for this @@ -103,6 +104,10 @@ Five executable rejection controls accompany the positive proofs: token activates the successor, even when the candidate has current state. 5. **Block processing while preparation is pending.** Lean rejects the claim that a deliberately blocking controller advances the next input position. +6. **Clear an outstanding warning on update.** Lean rejects the claim that + activating V2 discharges the resident water-warning obligation. +7. **Acknowledge another source.** Lean rejects the claim that a receipt command + for another source discharges the existing warning. `pause_exceeds_deadline` additionally proves a general lower bound: if a decision cannot complete before a pause plus nonnegative work, a pause longer than the @@ -173,10 +178,27 @@ mechanisms and exercises them in tests; it is not a verified extraction of this controller. These new results strengthen logical liveness assumptions without establishing physical scheduling or hardware availability. +## Resident water-warning obligations + +[WaterLeak.lean](Firmboot/WaterLeak.lean) adds a resident raw-reading and receipt +journal to the normalized detector. Its 16 lemmas and witnesses establish exact +valid capture, rejection of a wrong sequence, preservation of readings/reports/ +receipts/outstanding warnings at handover, acknowledgement idempotence, and the +inability of a subsequent sample to discharge an outstanding warning. Activation +and acknowledgement commute at the same sample boundary. Concrete witnesses +exercise an accepted V1-to-V2 update with a pending warning and a later low sample. + +The model uses opaque natural-number source/operator labels. Rejected operations +leave state unchanged, whereas the runtime validates textual labels and returns +error tuples. The formal sampling function takes its threshold per call; the +runtime fixes it at construction. There is no general refinement or extraction +proof. See the [domain experiment](../../docs/water-leak-experiment.md) for the +executable evidence, exact observation contract and remaining gaps. + ## Proof trust [Audit.lean](Audit.lean) uses Lean's `#print axioms` with `#guard_msgs` to pin the -transitive dependency output of every named theorem in the five proof modules. +transitive dependency output of every named theorem in the six proof modules. Only `propext`, `Classical.choice`, and `Quot.sound` occur; some theorems use none. These are Lean's standard logical axioms, **not axioms asserting Firmboot works**. There is no `sorryAx`, custom axiom, `Lean.trustCompiler`, `native_decide`, or diff --git a/proofs/lean/controls/AcknowledgeOtherSource.lean b/proofs/lean/controls/AcknowledgeOtherSource.lean new file mode 100644 index 0000000..45f19ae --- /dev/null +++ b/proofs/lean/controls/AcknowledgeOtherSource.lean @@ -0,0 +1,5 @@ +import Firmboot.WaterLeak + +open Firmboot.WaterLeak +-- Expected rejection: the same episode number on another source is not this warning. +example : outstanding (acknowledge warned ⟨8, 3⟩ 42) ⟨7, 3⟩ = false := by decide diff --git a/proofs/lean/controls/ClearWarningOnUpdate.lean b/proofs/lean/controls/ClearWarningOnUpdate.lean new file mode 100644 index 0000000..3d66a1f --- /dev/null +++ b/proofs/lean/controls/ClearWarningOnUpdate.lean @@ -0,0 +1,5 @@ +import Firmboot.WaterLeak + +open Firmboot.WaterLeak +-- Expected rejection: updating the detector cannot acknowledge its warning. +example : outstanding (handover warned (some upgrade)) ⟨7, 3⟩ = false := by decide diff --git a/proofs/lean/verify.sh b/proofs/lean/verify.sh index 64ef14e..e537248 100644 --- a/proofs/lean/verify.sh +++ b/proofs/lean/verify.sh @@ -46,7 +46,7 @@ if [[ "$axiom_status" -ne 1 ]] || fi printf 'PASS: the axiom policy rejected an additional custom assumption\n' -for control in ResetOwnership DropObservation OverlapPhases StaleReply BlockingPreparation; do +for control in ResetOwnership DropObservation OverlapPhases StaleReply BlockingPreparation ClearWarningOnUpdate AcknowledgeOtherSource; do control_status=0 control_output="$(lake env lean "controls/${control}.lean" 2>&1)" || control_status=$? if [[ "$control_status" -ne 1 ]] || @@ -61,4 +61,4 @@ for control in ResetOwnership DropObservation OverlapPhases StaleReply BlockingP printf 'PASS: Lean rejected the false %s claim\n' "$control" done -printf 'PASS: proof build, both axiom audits, custom-axiom control and five false-claim controls\n' +printf 'PASS: proof build, both axiom audits, custom-axiom control and seven false-claim controls\n' diff --git a/test/firmboot/water_leak_test.exs b/test/firmboot/water_leak_test.exs new file mode 100644 index 0000000..22f5b40 --- /dev/null +++ b/test/firmboot/water_leak_test.exs @@ -0,0 +1,155 @@ +defmodule Firmboot.WaterLeakTest do + use ExUnit.Case, async: true + alias Firmboot.{Update, WaterLeak} + alias Firmboot.WaterLeak.{Checker, Experiment} + + @contract [source: "sim-loop", threshold_ml: 100] + @first {"sim-loop", 3} + + test "an outstanding warning and every raw reading survive the active-episode update" do + {state, receipts, snapshots} = Experiment.scenario() + before = Enum.at(snapshots, 3) + boundary = Enum.at(snapshots, 5) + assert before.model.version == :v1 + assert boundary.model.version == :v2 + assert hd(boundary.model.frames).version == :v1 + assert before.warnings == boundary.warnings + assert WaterLeak.outstanding(boundary) == [@first] + assert Enum.take(boundary.observations, -4) == before.observations + assert :ok == Checker.verify(Experiment.readings(), receipts, state, @contract) + end + + test "signal clearance is not an acknowledgement; later warnings get new identities" do + {state, [], snapshots} = Experiment.scenario(nil) + cleared = Enum.at(snapshots, 6) + assert cleared.model.detector.episode == nil + assert WaterLeak.outstanding(cleared) == [@first] + assert WaterLeak.outstanding(state) == [@first, {"sim-loop", 9}] + assert state.warnings[{"sim-loop", 9}].detected_at == 11 + assert state.warnings[{"sim-loop", 9}].version == :v2 + end + + test "an acknowledgement during preparation survives activation without being rewritten" do + {state, [receipt], snapshots} = Experiment.scenario(5) + assert receipt.after_seq == 5 + assert Enum.at(snapshots, 4).model.version == :v1 + assert Enum.at(snapshots, 5).model.version == :v2 + assert state.warnings[@first].acknowledgement == receipt + assert WaterLeak.outstanding(state) == [{"sim-loop", 9}] + assert {:ok, ^state} = WaterLeak.acknowledge(state, @first, "operator-A") + assert {:error, :already_acknowledged} = WaterLeak.acknowledge(state, @first, "operator-B") + end + + test "wrong-source and unknown acknowledgements cannot discharge a warning" do + {state, [], _} = Experiment.scenario(nil) + assert {:error, :unknown_warning} = WaterLeak.acknowledge(state, {"other-loop", 3}, "op") + assert {:error, :unknown_warning} = WaterLeak.acknowledge(state, {"sim-loop", 100}, "op") + assert {:error, :invalid_operator} = WaterLeak.acknowledge(state, @first, " ") + assert WaterLeak.outstanding(state) == [@first, {"sim-loop", 9}] + end + + test "a rejected migration keeps warning ownership and continues observing" do + {state, receipts, _} = Experiment.scenario(7, :reported) + assert state.model.version == :v1 + assert Enum.any?(state.model.audit, &(&1.kind == :rejected and &1.reason == :migration)) + assert length(state.observations) == 12 + assert state.warnings[{"sim-loop", 9}].detected_at == 10 + assert :ok == Checker.verify(Experiment.readings(), receipts, state, @contract) + end + + test "gaps, duplicate samples and malformed quantities are rejected before capture" do + state = WaterLeak.new(@contract) + [first | _] = Experiment.readings() + assert {:error, {:expected_sequence, 1}} = WaterLeak.sample(state, %{first | seq: 2}) + assert {:error, :invalid_reading} = WaterLeak.sample(state, %{first | inlet_ml: -1}) + assert {:error, :invalid_reading} = WaterLeak.sample(state, %{first | inlet_ml: 1.0}) + assert {:error, :invalid_reading} = WaterLeak.sample(state, Map.put(first, :units, :litres)) + assert {:ok, next} = WaterLeak.sample(state, first) + assert {:error, {:expected_sequence, 2}} = WaterLeak.sample(next, first) + assert next.observations == [first] + end + + test "classification retains the exact threshold and raw quantities" do + state = WaterLeak.new(@contract) + {:ok, state} = WaterLeak.sample(state, %{seq: 1, inlet_ml: 1_000, outlet_ml: 901}) + {:ok, state} = WaterLeak.sample(state, %{seq: 2, inlet_ml: 1_000, outlet_ml: 900}) + {:ok, state} = WaterLeak.sample(state, %{seq: 3, inlet_ml: 1_000, outlet_ml: 899}) + assert Enum.map(Enum.reverse(state.model.frames), & &1.value) == [0, 1, 1] + assert WaterLeak.outstanding(state) == [{"sim-loop", 2}] + end + + test "independent checker rejects dropped or rewritten readings and warning identities" do + {state, receipts, _} = Experiment.scenario() + [latest | older] = state.observations + assert_error(%{state | observations: older}, receipts, :raw_observation_history) + changed = [%{latest | inlet_ml: latest.inlet_ml + 1} | older] + assert_error(%{state | observations: changed}, receipts, :raw_observation_history) + + assert_error( + %{state | warnings: Map.delete(state.warnings, @first)}, + receipts, + :warning_ledger + ) + + duplicate = Map.put(state.warnings, {"sim-loop", 30}, state.warnings[@first]) + assert_error(%{state | warnings: duplicate}, receipts, :warning_ledger) + assert_error(%{state | threshold_ml: 101}, receipts, :observation_contract) + end + + test "independent checker rejects erased, invented and premature acknowledgements" do + {state, [receipt] = receipts, _} = Experiment.scenario() + cleared = put_in(state.warnings[@first].acknowledgement, nil) + assert_error(cleared, receipts, :warning_ledger) + assert_error(%{state | receipts: []}, receipts, :acknowledgement_journal) + assert_error(state, [], :warning_ledger) + assert_error(state, [%{receipt | after_seq: 3}], :acknowledgement_transcript) + assert_error(state, [receipt, receipt], :acknowledgement_transcript) + + second = %{id: {"sim-loop", 9}, by: "operator-A", after_seq: 12} + assert_error(state, [second, receipt], :acknowledgement_transcript) + end + + test "640 short traces preserve ledgers across both update directions and acknowledgements" do + for mask <- 0..63, initial <- [:v1, :v2], request_after <- 1..5 do + contract = Keyword.put(@contract, :version, initial) + start = WaterLeak.new(Keyword.put(@contract, :model, version: initial)) + + readings = + for seq <- 1..6 do + high = Bitwise.band(Bitwise.bsr(mask, seq - 1), 1) + %{seq: seq, inlet_ml: 1_000, outlet_ml: 1_000 - 150 * high} + end + + {state, receipts} = + Enum.reduce(readings, {start, []}, fn reading, {state, receipts} -> + state = + if reading.seq == request_after + 1 do + target = if initial == :v1, do: :v2, else: :v1 + + WaterLeak.request(state, %Update{id: :short_trace, target: target, prepare_ticks: 0}) + else + state + end + + {:ok, state} = WaterLeak.sample(state, reading) + + case {rem(reading.seq, 2), WaterLeak.outstanding(state)} do + {0, [id | _]} -> + receipt = %{id: id, by: "operator-A", after_seq: reading.seq} + {:ok, state} = WaterLeak.acknowledge(state, id, receipt.by) + {state, receipts ++ [receipt]} + + _ -> + {state, receipts} + end + end) + + assert :ok == Checker.verify(readings, receipts, state, contract) + end + end + + defp assert_error(state, receipts, expected) do + assert {:error, errors} = Checker.verify(Experiment.readings(), receipts, state, @contract) + assert expected in errors + end +end