fix(accuracy): close refinement semantics

.github/workflows/ci.yml

@@ -54,7 +54,30 @@ jobs:
             "https://github.com/jonaprieto/"
       - uses: leanprover/lean-action@v1
         with:
-          build-args: "EventB EventBWidgets Examples gates rossi-dump eventb bench"
+          build-args: "EventB EventBWidgets Examples VariantFixtures gates rossi-dump eventb bench"
+      - name: Kernel-checked refinement adapters
+        run: |
+          lake env lean EventB/POGSoundness.lean
+          lake env lean EventB/POG/RefinementAdapters.lean
+          lake env lean test/EqlFixtures.lean
+          lake env lean test/GuardFixtures.lean
+          lake env lean test/EnabledGuardFixtures.lean
+          lake env lean test/FiniteSetEvaluatorFixtures.lean
+          lake env lean test/FiniteVariantFixtures.lean
+          lake env lean test/FiniteVariantModelFixtures.lean
+          lake env lean test/VwdFixtures.lean
+          lake env lean test/MrgFixtures.lean
+          lake env lean test/MrgSemanticFixtures.lean
+          lake env lean test/MrgAdapterFixtures.lean
+          lake env lean EventB/POG/EQLAdapter.lean
+      - name: Adapter axiom audit
+        run: |
+          audit=$(lake env lean test/AdapterAxiomAudit.lean 2>&1)
+          echo "$audit"
+          if echo "$audit" | grep -Eq 'sorryAx|native_decide'; then
+            echo "::error::acceptance theorem depends on a forbidden proof shortcut"
+            exit 1
+          fi
       - name: CLI and fixture matrix
         run: python3 tools/cli-fixtures.py
       - name: Install pinned Rossi
@@ -92,9 +115,9 @@ jobs:
           } >> "$GITHUB_STEP_SUMMARY"
       - name: Status report generates
         run: |
-          # STATUS.md is untracked, so a `git diff` check on it would always pass.
-          # Running the generator still catches a crash in the reporting path.
           lake exe gates --status
+          git ls-files --error-unmatch STATUS.md baseline/*.tsv
+          git diff --exit-code -- STATUS.md baseline
 
   axioms:
     # The trust ledger. Once POG lands this enumerates, per obligation, whether it is

.gitignore

@@ -6,11 +6,9 @@ bench/results/*/raw/
 docs/event-b.md/
 docs/event-b.md.zip
 
-# Working documents, deliberately untracked: the working agreement, the phase plan,
-# and the generated status report. `lake exe gates --status` rewrites STATUS.md.
+# Working documents, deliberately untracked: the working agreement and the phase plan.
 AGENTS.md
 PLAN.md
-STATUS.md
 
 # The spike vendors Mathlib; do not track its build tree.
 spike/.lake/

CHANGELOG.md

@@ -1,5 +1,23 @@
 # Changelog
 
+## 4.0.10 — 2026-08-15
+
+- Re-derive strict POG obligations from the complete Rodin model-artifact closure,
+  including theory environments, before accepting imported status evidence.
+- Label declared external/SMT metadata, structurally checked Rodin imports, and
+  axiom-bearing kernel replay separately from unproved obligations.
+- Add compositional invariant and refinement contracts for event-local simulation and
+  pre-state parallel assignment semantics.
+- Add explicit frame, gluing, merged-event, witness, variant, and translated-sequent
+  semantic contracts with positive and negative kernel-checked fixtures.
+- Extend the bounded typed evaluator with finite relation application, image,
+  domain/range restriction/subtraction, and override, with malformed and
+  duplicate-function cases failing closed.
+- Add source-bound parameterized enabled-event semantics, finite witness-domain
+  completeness, and well-founded variant contracts with focused positive and negative
+  fixtures; retain explicit fail-closed boundaries for unbounded binders and arbitrary
+  formula interpretation.
+
 ## 4.0.9 — 2026-08-13
 
 - Pin every first-party dependency to its newest released tag.

EventB.lean

@@ -12,7 +12,12 @@ import EventB.Embedding
 import EventB.Formula.Translate
 import EventB.Typing.Infer
 import EventB.Typing.Check
+import EventB.Project
 import EventB.POG
+import EventB.POGSoundness
+import EventB.POGBridge
+import EventB.POG.EQLAdapter
+import EventB.POG.RefinementAdapters
 import EventB.Trust
 import EventB.Trust.Replay
 import EventB.Trust.Rodin

EventB/DSL.lean

@@ -195,6 +195,19 @@ private def addDefinitionInfo (id : Syntax) (symbol : String) (location : Declar
     mkDocString? := some fun _ => pure s!"Event-B symbol `{symbol}`"
   }
 
+private def nativeSymbolLocation? (id : Ident) : CommandElabM (Option DeclarationLocation) := do
+  let module ← currentModule
+  match ← Lean.findDeclarationRanges? id.getId with
+  | some ranges => pure <| some { module, range := ranges.selectionRange }
+  | none => pure none
+
+private def addReferenceInfo (owners : List String) (id : Ident) : CommandElabM Unit := do
+  let location ← match ← nativeSymbolLocation? id with
+    | some location => pure <| some location
+    | none => symbolLocation? owners id.getId.toString
+  if let some location := location then
+    addDefinitionInfo id.raw id.getId.toString location
+
 private def addFormulaInfos (owners : List String) (stx : Syntax) : CommandElabM Unit := do
   for id in formulaIdentifiers stx do
     if let some location ← symbolLocation? owners id.getId.toString then
@@ -239,6 +252,7 @@ private def eventParts (theoryRoots owners : List String) (parts : Array (TSynta
   for p in parts do
     match p with
     | `(ebEventPart| refines $r:ident) =>
+        addReferenceInfo owners r
         out := out.push (mkElem "refinesEvent" (targetAttrs r.getId.toString) noKids)
     | `(ebEventPart| extends $r:ident) =>
         out := out.push
@@ -662,13 +676,16 @@ private def elabMachine : CommandElab := fun stx => do
       for p in ps do
         match p with
         | `(ebMachinePart| refines $r:ident) =>
+            addReferenceInfo owners r
             kids := kids.push
               (mkElem "refinesMachine" (targetAttrs r.getId.toString) noKids)
         | `(ebMachinePart| sees $ss:ident*) =>
             for sc in ss do
+              addReferenceInfo owners sc
               kids := kids.push
                 (mkElem "seesContext" (targetAttrs sc.getId.toString) noKids)
-        | `(ebMachinePart| uses $_:ident*) => pure ()
+        | `(ebMachinePart| uses $ts:ident*) =>
+            for theory in ts do addReferenceInfo owners theory
         | `(ebMachinePart| variables $xs:ident*) =>
             for x in xs do
               kids := kids.push
@@ -718,9 +735,11 @@ private def elabContext : CommandElab := fun stx => do
         match p with
         | `(ebContextPart| extends $es:ident*) =>
             for e in es do
+              addReferenceInfo owners e
               kids := kids.push
                 (mkElem "extendsContext" (targetAttrs e.getId.toString) noKids)
-        | `(ebContextPart| uses $_:ident*) => pure ()
+        | `(ebContextPart| uses $ts:ident*) =>
+            for theory in ts do addReferenceInfo owners theory
         | `(ebContextPart| sets $xs:ident*) =>
             for x in xs do
               kids := kids.push
@@ -740,10 +759,9 @@ private def elabContext : CommandElab := fun stx => do
       addContextInfos (owners ++ theoryRoots) ps
   | _ => throwUnsupportedSyntax
 
-/-- `#eventb_pog M Ctx ...` prints the obligations generated for the first named
-component, resolving the rest as its project. The point of the DSL is that this is the
-same generator the corpus goes through, so what it prints here is what a `.bum` would
-get. -/
+/-- `#eventb_pog M Ctx ...` prints compatibility obligations for the first named
+component, resolving the rest as its project. Trusted integrations must use the checked
+POG entry points, which reject unresolved scope and model diagnostics. -/
 syntax (name := eventbPog) "#eventb_pog " ident+ : command
 syntax (name := eventbPogIn) "#eventb_pog_in " ident ppSpace ident+ : command
 

EventB/Formula/Parse.lean

@@ -33,7 +33,140 @@ inductive Term where
   /-- Binder: `∀`, `∃`, `λ`, `⋂`, `⋃`, and `{pat · body}` set comprehension, whose kind
   is `"{"`. The body of a comprehension or lambda is `bin "∣" pred expr`. -/
   | bind : String → Term → Term → Term
-  deriving BEq, Repr, Inhabited
+  deriving Repr, Inhabited
+
+mutual
+
+  def termBeq : Term → Term → Bool
+    | .id left, .id right => left == right
+    | .num left, .num right => left == right
+    | .bin leftOp left₁ left₂, .bin rightOp right₁ right₂ =>
+        leftOp == rightOp && termBeq left₁ right₁ && termBeq left₂ right₂
+    | .pre leftOp left, .pre rightOp right
+    | .post leftOp left, .post rightOp right => leftOp == rightOp && termBeq left right
+    | .app leftFunction leftArgument, .app rightFunction rightArgument
+    | .img leftFunction leftArgument, .img rightFunction rightArgument =>
+        termBeq leftFunction rightFunction && termBeq leftArgument rightArgument
+    | .set left, .set right => termListBeq left right
+    | .bind leftKind leftBinder leftBody, .bind rightKind rightBinder rightBody =>
+        leftKind == rightKind && termBeq leftBinder rightBinder && termBeq leftBody rightBody
+    | _, _ => false
+
+  def termListBeq : List Term → List Term → Bool
+    | [], [] => true
+    | left :: lefts, right :: rights => termBeq left right && termListBeq lefts rights
+    | _, _ => false
+
+end
+
+instance : BEq Term := ⟨termBeq⟩
+
+private theorem congrArg₂' {α β γ : Type} (f : α → β → γ)
+    {left left' : α} {right right' : β}
+    (leftEq : left = left') (rightEq : right = right') :
+    f left right = f left' right' := by
+  cases leftEq
+  cases rightEq
+  rfl
+
+theorem Term.eq_of_beq {left right : Term} (equal : left == right) : left = right := by
+  change termBeq left right = true at equal
+  exact (Term.rec
+    (motive_1 := fun left => ∀ right, termBeq left right = true → left = right)
+    (motive_2 := fun left => ∀ right, termListBeq left right = true → left = right)
+    (id := fun name right equal => by
+      cases right with
+      | id other => simp [termBeq] at equal; subst other; rfl
+      | num | bin | pre | post | app | img | set | bind => simp [termBeq] at equal)
+    (num := fun value right equal => by
+      cases right with
+      | num other => simp [termBeq] at equal; subst other; rfl
+      | id | bin | pre | post | app | img | set | bind => simp [termBeq] at equal)
+    (bin := fun op left₁ right₁ ihLeft ihRight right equal => by
+      cases right with
+      | bin otherOp otherLeft otherRight =>
+          simp [termBeq] at equal
+          rcases equal with ⟨⟨opEq, leftEq⟩, rightEq⟩
+          subst otherOp
+          exact congrArg₂' (Term.bin op) (ihLeft otherLeft leftEq) (ihRight otherRight rightEq)
+      | id | num | pre | post | app | img | set | bind => simp [termBeq] at equal)
+    (pre := fun op value ih right equal => by
+      cases right with
+      | pre otherOp otherValue =>
+          simp [termBeq] at equal
+          rcases equal with ⟨opEq, valueEq⟩
+          subst otherOp
+          exact congrArg (Term.pre op) (ih otherValue valueEq)
+      | id | num | bin | post | app | img | set | bind => simp [termBeq] at equal)
+    (post := fun op value ih right equal => by
+      cases right with
+      | post otherOp otherValue =>
+          simp [termBeq] at equal
+          rcases equal with ⟨opEq, valueEq⟩
+          subst otherOp
+          exact congrArg (Term.post op) (ih otherValue valueEq)
+      | id | num | bin | pre | app | img | set | bind => simp [termBeq] at equal)
+    (app := fun function argument ihFunction ihArgument right equal => by
+      cases right with
+      | app otherFunction otherArgument =>
+          simp [termBeq] at equal
+          exact congrArg₂' Term.app (ihFunction otherFunction equal.1)
+            (ihArgument otherArgument equal.2)
+      | id | num | bin | pre | post | img | set | bind => simp [termBeq] at equal)
+    (img := fun relation argument ihRelation ihArgument right equal => by
+      cases right with
+      | img otherRelation otherArgument =>
+          simp [termBeq] at equal
+          exact congrArg₂' Term.img (ihRelation otherRelation equal.1)
+            (ihArgument otherArgument equal.2)
+      | id | num | bin | pre | post | app | set | bind => simp [termBeq] at equal)
+    (set := fun values ih right equal => by
+      cases right with
+      | set otherValues => exact congrArg Term.set (ih otherValues equal)
+      | id | num | bin | pre | post | app | img | bind => simp [termBeq] at equal)
+    (bind := fun quantifier binder body ihBinder ihBody right equal => by
+      cases right with
+      | bind otherQuantifier otherBinder otherBody =>
+          simp [termBeq] at equal
+          rcases equal with ⟨⟨quantifierEq, binderEq⟩, bodyEq⟩
+          subst otherQuantifier
+          exact congrArg₂' (Term.bind quantifier)
+            (ihBinder otherBinder binderEq) (ihBody otherBody bodyEq)
+      | id | num | bin | pre | post | app | img | set => simp [termBeq] at equal)
+    (nil := fun right equal => by
+      cases right with
+      | nil => rfl
+      | cons => simp [termListBeq] at equal)
+    (cons := fun head tail ihHead ihTail right equal => by
+      cases right with
+      | nil => simp [termListBeq] at equal
+      | cons otherHead otherTail =>
+          simp [termListBeq] at equal
+          exact congrArg₂' List.cons (ihHead otherHead equal.1) (ihTail otherTail equal.2))
+    left) right equal
+
+theorem Term.beq_self (term : Term) : termBeq term term = true := by
+  exact Term.rec
+    (motive_1 := fun term => termBeq term term = true)
+    (motive_2 := fun terms => termListBeq terms terms = true)
+    (id := fun _ => by simp [termBeq])
+    (num := fun _ => by simp [termBeq])
+    (bin := fun _ _ _ ihLeft ihRight => by simp [termBeq, ihLeft, ihRight])
+    (pre := fun _ _ ih => by simp [termBeq, ih])
+    (post := fun _ _ ih => by simp [termBeq, ih])
+    (app := fun _ _ ihFunction ihArgument => by simp [termBeq, ihFunction, ihArgument])
+    (img := fun _ _ ihRelation ihArgument => by simp [termBeq, ihRelation, ihArgument])
+    (set := fun _ ih => ih)
+    (bind := fun _ _ _ ihBinder ihBody => by simp [termBeq, ihBinder, ihBody])
+    (nil := by rfl)
+    (cons := fun _ _ ihHead ihTail => by simp [termListBeq, ihHead, ihTail])
+    term
+
+instance : LawfulBEq Term where
+  rfl := Term.beq_self _
+  eq_of_beq := Term.eq_of_beq
+
+instance : DecidableEq Term := instDecidableEqOfLawfulBEq
 
 /-- Binding power, and whether the operator associates. Non-associating operators reject
 `a ∈ b ∈ c` the way Rodin does, rather than silently bracketing it. -/
@@ -90,6 +223,12 @@ private structure St where
   toks : Array Tok
   pos  : Nat
 
+private def hasRemainingOperator (s : St) (operator : String) : Bool :=
+  (s.toks.toList.drop s.pos).any fun token =>
+    match token with
+    | .op value => value == operator
+    | _ => false
+
 private def peek (s : St) : Option Tok := s.toks[s.pos]?
 
 private def expect (s : St) (o : String) : Except String St :=
@@ -154,7 +293,8 @@ private def parsePrefix : Nat → St → Except String (Term × St)
   | some (.id name) => parsePostfix fuel (.id name) { s with pos := s.pos + 1 }
   | some (.op o) =>
     let s := { s with pos := s.pos + 1 }
-    if isBinder o then
+    if isBinder o &&
+        (o != "⋃" && o != "⋂" || hasRemainingOperator s "·") then
       -- The pattern runs up to `·`; comma and `↦` inside it are ordinary operators, so
       -- `∀a1,a2·P` and `λx↦y·P∣E` need no special cases.
       let (pat, s) ← parseAt fuel s 5
@@ -293,6 +433,12 @@ private def sameTree (a b : String) : Bool :=
 -- Binders take a comma-separated pattern, and comprehension keeps predicate and
 -- expression apart.
 #guard (parse "∀a1,a2 · a1 ∈ S ∧ a2 ∈ S ⇒ a1 = a2").isOk
+#guard match parse "⋃S" with
+  | .ok term => term == .pre "⋃" (.id "S")
+  | .error _ => false
+#guard match parse "⋂S" with
+  | .ok term => term == .pre "⋂" (.id "S")
+  | .error _ => false
 #guard (parse "{x · x ∈ S ∣ x + 1}").isOk
 -- The short form of comprehension denotes the same set as the long one.
 #guard sameTree "{x ∣ x ∈ S}" "{x · x ∈ S ∣ x}"