From ae11562cd11d0b50d659c68c13f5fac70a39c059 Mon Sep 17 00:00:00 2001 From: Quinn Dougherty Date: Sat, 4 Jul 2026 17:12:47 -0400 Subject: [PATCH] test: remove dose-bounding requirement (exercises findings-diff bot) Deliberately orphans UCA4 by deleting requirement R3 and the two certificates that would no longer compile. This PR exists to exercise the findings-diff CI job end-to-end; it must NOT be merged. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01LavNfZvE6CcgB1g2HP2Euy --- Examples/InsulinPump.lean | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) diff --git a/Examples/InsulinPump.lean b/Examples/InsulinPump.lean index 05d7067..7d081c7 100644 --- a/Examples/InsulinPump.lean +++ b/Examples/InsulinPump.lean @@ -128,9 +128,7 @@ def requirements : List Requirement := [ { id := 1, desc := "The controller shall command a bolus within T of CGM readings sustained above threshold", ucas := [1, 3] }, { id := 2, desc := "The controller shall not command insulin when the latest CGM reading is at or below threshold", - ucas := [2] }, - { id := 3, desc := "The controller shall bound each commanded dose and terminate delivery at the commanded amount", - ucas := [4] } + ucas := [2] } ] /-- STPA step 4 (initial): loss scenarios explaining how each UCA could @@ -164,16 +162,6 @@ theorem pumpModel_wellFormed : pumpModel.wellFormed = true := by decide the controller receives feedback from every process it controls. -/ theorem pumpCs_wellFormed : pumpCs.wellFormed pumpModel = true := by decide -/-- The full STPA analysis is well-formed: traceable hazards and UCAs, and -all four UCA kinds covered for every control path. -/ -theorem analysis_wellFormed : analysis.wellFormed = true := by decide - -/-- The analysis document is well-typed in the sense of the STPA type -system (docs/stpa-typesystem.pdf): every artifact well-kinded, every hazard -addressed by a system constraint, every UCA refined by a controller -requirement — no orphans. `decide` works on the Prop-level judgment via the -reflection theorem `Analysis.wellTyped_iff`. -/ -theorem analysis_wellTyped : WellTyped analysis := by decide -- Round-trip: print the elaborated model back as SysML textual notation. -- #sysml pumpModel