Repository navigation
Preserve water-warning obligations across detector updates - #2
Conversation
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Team Run ID: 📒 Files selected for processing (16)
Included review availability: Your plan provides up to 1 included review per hour; 0 remain after this review. 📜 Recent review details⏰ Context from checks skipped due to timeout. (1)
🧰 Additional context used🪛 LanguageToolVERIFICATION.md[grammar] ~15-~15: The verb “double-checking” is spelled with a hyphen. (DOUBLE_HYPHEN) docs/water-leak-experiment.md[uncategorized] ~55-~55: Use a comma before “or” if it connects two independent clauses (unless they are closely connected and short). (COMMA_COMPOUND_SENTENCE_2) [style] ~58-~58: Would you like to use the Oxford spelling “authorization”? The spelling ‘authorisation’ is also correct. (OXFORD_SPELLING_Z_NOT_S) 🔇 Additional comments (8)
📝 SummarySummary by CodeRabbit
WalkthroughThe change adds a finite water-warning simulation with raw-reading retention, warning identity, acknowledgements, independent checking, Lean proofs, executable scenarios, expanded tests, and verification documentation. ChangesWater-warning continuity
Estimated code review effort: 4 (Complex) | ~45 minutes Merge Risk: ⚪ Minimal · up to This adds an in-memory simulated water-warning ledger that retains readings, warning identity, and acknowledgements across detector updates. Current merge-readiness risk is minimal within the documented experimental scope. Sequence Diagram(s)sequenceDiagram
participant Experiment as Firmboot.WaterLeak.Experiment
participant Ledger as Firmboot.WaterLeak
participant Model as Firmboot.Model
participant Checker as Firmboot.WaterLeak.Checker
Experiment->>Ledger: request detector update
Experiment->>Ledger: sample reading
Ledger->>Model: apply transition
Model-->>Ledger: return updated model state
Ledger-->>Experiment: return warnings and observations
Experiment->>Ledger: acknowledge warning
Experiment->>Checker: verify transcript and state
Checker-->>Experiment: return :ok or violations
Poem
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
Full details: Docstring CoverageExplanation Docstring coverage is 9.09% which is insufficient. The required threshold is 80.00%. Docstring coverage is scoped to functions touched by this diff. Analyzed 11 functions across 5 files. (11 skipped: 11 unsupported.)
✨ Finishing Touches 💡 1📝 Generate docstrings 💡
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
A detector update during an active simulated water warning must preserve the original readings, the warning's identity and its outstanding operator acknowledgement. This change adds a resident domain ledger around the existing detector model and checks acknowledgements before and after activation, signal clearance without acknowledgement, and rejection of a migration which erases report ownership.
The reproducible command is
mix run -e 'Firmboot.WaterLeak.Experiment.run()'. The required Agda/Elixir job also runs it. The experiment uses finite synthetic interval volumes and two already compiled detector implementations; it does not perform physical leak detection, actuation, durable storage or general code loading. The domain report states the observation contract and source/model correspondence gaps.Validation:
The Lean results prove properties of the defined model. A whole-program refinement proof for the Elixir implementation remains open; domain ledger costs are not included in the existing assigned detector timing budget.