opencompl · georgerennie · Dec 18, 2025 · Nov 29, 2025
@@ -1,101 +1,62 @@
 import Mathlib.Data.Fintype.Defs
 import Blase.Fast.FiniteStateMachine
+import Valaig.Aig.FromStd
+import Valaig.External
 
 import Lean
-open Std Sat AIG
-
-variable {α : Type} [Hashable α] [DecidableEq α]
-
-private structure Latch (aig : AIG α) where
-  init : Bool
-  state : aig.Ref
-  next : aig.Ref
-
--- Note that this currently does not require much in the way of wellformedness,
--- it could specify multiple references as the same latch/input etc
-structure Aiger (α : Type) [Hashable α] [DecidableEq α] where
-  aig : AIG α
-  latches : Array (Latch aig)
-  inputs : Array aig.Ref
-  bad : aig.Ref
+open Std Sat AIG Valaig
 
 def _root_.FSM.toAiger {arity : Type}
     [Hashable arity] [Fintype arity] [DecidableEq arity]
-    (fsm : FSM arity) : Aiger (fsm.α ⊕ arity) :=
-  let aig := .empty
-
-  let ⟨aig, inputs⟩ : (aig : AIG _) × Array aig.Ref :=
-    (@Fintype.elems arity).val.liftOn
-      (fun elems => elems.foldl (init := ⟨aig, .empty⟩)
-        (fun ⟨aig, vec⟩ s =>
-          let ⟨aig, ref⟩ := aig.mkAtomCached (.inr s)
-          let vec := vec.map (.cast . sorry)
-          ⟨aig, vec.push ref⟩))
-      -- Functions that operate on a quotient should be provably indistinguishable
-      -- up to the quotienting however in this case we will not be equivalent
-      -- because the aiger we produce will depend on the ordering of elements
-      -- however the actual solvability of the system does not depend on the
-      -- ordering of elements therefore this sorry is in fact benign
-      sorry
-
-  -- Array of next state variables with their function
-  let ⟨aig, latches⟩ : (aig : AIG _) × Array (Latch aig) := fsm.i.toList.foldl
-    (fun ⟨aig, vec⟩ var =>
-      let res := fsm.nextStateCirc var |>.toAIGAux aig
-      let aig := res.out
-      let next := res.ref
-
-      let ⟨aig, state⟩ := aig.mkAtomCached (.inl var)
-      let init := fsm.initCarry var
-      let vec := vec.map (fun l => { l with state := l.state.cast sorry, next := l.next.cast sorry })
-      ⟨aig, vec.push {init, state, next := next.cast sorry}⟩)
-    ⟨aig, .empty⟩
-
-  let res := fsm.outputCirc.toAIGAux aig
-  let aig := res.out
+    (fsm : FSM arity) : Aiger :=
+  -- First we build a Std.Sat.AIG using toAIGAux by iterating the latches
+  -- and bad, adding them to the new AIG. As we go, we take note of what these
+  -- next state variables map to
+  let res : (aig : AIG _) × Std.HashMap fsm.α aig.Ref :=
+    fsm.i.toList.foldl
+      (fun ⟨aig, map⟩ var =>
+        let res := fsm.nextStateCirc var |>.toAIGAux aig
+        let map := map.map fun _ r => r.cast res.le_size
+        let map := map.insert var res.ref
+        ⟨res.out, map⟩)
+      ⟨.empty, .emptyWithCapacity⟩
+
+  let stdAig := res.fst
+  let nextMap := res.snd
+
+  have hmapmem {a : fsm.α} : a ∈ nextMap := by
+    have : ∀ {a} (_ : a ∈ fsm.i.toList), a ∈ nextMap := by
+      let motive idx (state : (aig : AIG (fsm.α ⊕ arity)) × Std.HashMap _ aig.Ref) : Prop :=
+        ∀ {i : Nat} {_ : idx ≤ fsm.i.toList.length} (_ : i < idx), fsm.i.toList[i]'(by grind) ∈ state.snd
+      subst nextMap res
+      simp only [←List.mem_toArray, ←Array.forall_getElem]
+      rw [←List.foldl_toArray]
+      intro i
+      apply Array.foldl_induction motive
+      · unfold motive; omega
+      · unfold motive; grind
+      · trivial
+    exact this (FinEnum.mem_toList a)
+
+  let res := fsm.outputCirc.toAIGAux stdAig
+  let stdAig := res.out
   let bad := res.ref
-
-  let inputs := inputs.map (.cast . sorry)
-  let latches := latches.map
-    (fun l => { l with state := l.state.cast sorry, next := l.next.cast sorry })
-
-  { aig, latches, inputs, bad }
-
-namespace Aiger
-
-private def toVarFalseLit (lit : Nat) : Nat := lit * 2
-private def toVarFalse {aig : AIG α} (ref : aig.Ref) : Nat := toVarFalseLit ref.gate
-
-private def toVar {aig : AIG α} (ref : aig.Ref) : Nat := (toVarFalse ref) + ref.invert.toNat
-private def toVarFanin (fanin : Fanin) : Nat := toVarFalseLit fanin.gate + fanin.invert.toNat
-
-def toAagFile (aig : Aiger α) (file : IO.FS.Stream) : IO Unit := do
-  let maxVar := aig.aig.decls.size
-  let numInputs := aig.inputs.size
-  let numLatches := aig.latches.size
-  let ⟨numAnds, body, _⟩ : _ × _ × _ := aig.aig.decls.foldl
-      (fun ⟨numAnds, s, idx⟩ term =>
-        match term with
-        | Decl.gate l r => ⟨numAnds + 1, s ++ s!"{toVarFalseLit idx} {toVarFanin l} {toVarFanin r}\n", idx + 1⟩
-        | _ => ⟨numAnds, s, idx + 1⟩)
-      ⟨0, "", 0⟩
-
-  -- Aiger 1.9 Header M I L O A B C J F
-  file.putStrLn s!"aag {maxVar} {numInputs} {numLatches} 0 {numAnds} 1 0 0 0"
-
-  -- Input lines
-  for input in aig.inputs do
-    assert! !input.invert
-    file.putStrLn s!"{toVarFalse input}"
-
-  -- Latch lines
-  for l in aig.latches do
-    assert! !l.state.invert
-    file.putStrLn s!"{toVarFalse l.state} {toVar l.next} {l.init.toNat}"
-
-  file.putStrLn s!"{toVar aig.bad}"
-
-  file.putStr body
-
-end Aiger
+  let nextMap := nextMap.map fun _ r => r.cast res.le_size
+  have hmapmem : ∀ {a : fsm.α}, a ∈ nextMap := by grind only [HashMap.mem_map]
+
+  let res := Valaig.Aig.fromStdAIG stdAig fun atom =>
+    match atom with
+    | .inl latch =>
+      let next := nextMap[latch]'hmapmem
+      let reset := .inl (fsm.initCarry latch)
+      .latch next reset
+    | .inr input => .input
+
+  let bad := res.refMap bad
+  {
+    aig := res.aig,
+    bads := #[.mk bad],
+    hwf := res.hwf
+    hbads := by simp; exact res.hrefvalid
+  }
 
@@ -38,9 +38,10 @@ structure Config where
   debugFillFinalReflectionProofWithSorry : Bool := false
   /-- Debug print the SMT-LIB version -/
   debugPrintSmtLib : Bool := false
-  /-- Dump the FSM to an Aiger file. -/
-  debugDumpAiger: Option String := none
-deriving DecidableEq, Repr
+  /-- Solve using an external like rIC3. -/
+  externalSolver : Bool := false
+  /-- The config for the external solver when externalSolver is set. -/
+  externalSolverConfig : Valaig.External.SafetyAigerMC := Valaig.External.rIC3 (timeoutMs := some 5000)
 
 /-- Default user configuration -/
 def Config.default : Config := {}
@@ -1168,92 +1169,98 @@ def solve (gorig : MVarId) : SolverM Unit := do
     debugLog m!"fsm circuit size: {termFsmNondep.toFsmZext.circuitSize}"
     if ! (← isDefEq pRawExpr (← mkAppM ``Term.toBV #[benv, nenv, ienv, penv, tenv, pExpr])) then
       throwError m!"internal error: collected predicate expression does not match original predicate. Collected: {indentD pExpr}, original: {indentD pRawExpr}"
-    let (stats, _log) ← FSM.decideIfZerosVerified termFsmNondep.toFsmZext (maxIter := (← read).niter) (startVerifyAtIter := (← read).startVerifyAtIter)
-    if let some filename := (← read).debugDumpAiger then
-      let fn := System.mkFilePath [filename]
-      let handle ← IO.FS.Handle.mk fn IO.FS.Mode.write
-      let stream := IO.FS.Stream.ofHandle handle
-      termFsmNondep.toFsmZext.toAiger.toAagFile stream
-
-    let (stats, _log) ← FSM.decideIfZerosVerified termFsmNondep.toFsmZext (maxIter := (← read).niter) (startVerifyAtIter := (← read).startVerifyAtIter)
-    match stats with
-    | .safetyFailure i =>
-      let suspiciousVars ← collect.logSuspiciousFvars
-      -- | Found precise counter-example to claimed predicate.
-      if suspiciousVars.isEmpty then
-          throwError m!"CEX: Found exact counter-example at iteration {i} for predicate '{pRawExpr}'"
-        else
-          throwError m!"MAYCEX: Found possible counter-example at iteration {i} for predicate '{pRawExpr}'"
-    | .exhaustedIterations _ =>
-      let _ ← collect.logSuspiciousFvars
-      throwError m!"PROOFNOTFOUND: exhausted iterations for predicate '{pRawExpr}'"
-    | .provenByKIndCycleBreaking niters safetyCert indCert =>
-      if (← read).verbose? then
-        let _ ← collect.logSuspiciousFvars
-      debugLog m!"PROVE: proven {pRawExpr}"
-      let prf ← g.withContext <| do
-        let termNondepFsmExpr ← Expr.mkTermFsmNondep collect.wcard collect.tcard collect.bcard collect.ncard collect.icard collect.pcard pNondepExpr
-        debugCheck termNondepFsmExpr
-        -- let fsmExpr := termNondepFsmExpr
-        -- | TODO: refactor into fn.
-        let fsmExpr ← mkAppM (``MultiWidth.TermFSM.toFsmZext) #[termNondepFsmExpr]
-        -- debugCheck fsmExpr
-        let circsExpr ← Expr.KInductionCircuits.mkN fsmExpr (toExpr niters)
-        let circsLawfulExpr ← Expr.KInductionCircuits.mkIsLawful_mkN fsmExpr (toExpr niters)
-        debugLog "making safety certs..."
-        -- | verifyCircuit (mkSafetyCircuit circs)
-        let verifyCircuitMkSafetyCircuitExpr ← Expr.mkVerifyCircuit
-          (← Expr.KInductionCircuits.mkMkSafetyCircuit circsExpr)
-          (toExpr safetyCert)
-        -- debugLog m!"made safety cert expr: {verifyCircuitMkSafetyCircuitExpr}"
-        debugLog "making safety cert = true proof..."
-        let safetyCertProof ←
-          mkEqReflBoolNativeDecideProof `safetyCert verifyCircuitMkSafetyCircuitExpr true
-        -- debugLog m!"made safety cert proof: {safetyCertProof}"
-        let verifyCircuitMkIndHypCircuitExpr ← Expr.mkVerifyCircuit
-            (← Expr.KInductionCircuits.mkIndHypCycleBreaking circsExpr)
-            (toExpr indCert)
-        -- debugLog m!"made verifyCircuit expr: {verifyCircuitMkIndHypCircuitExpr}"
-        let indCertProof ←
-          mkEqReflBoolNativeDecideProof `indCert verifyCircuitMkIndHypCircuitExpr true
-        debugLog m!"made induction cert = true proof..."
-        let prf ← mkAppM ``MultiWidth.Term.toBV_of_KInductionCircuits'
-          #[pRawExpr, -- P : Prop
-            tctx,
-            pExpr, -- p
-            pNondepExpr, -- pNondep
-            ← mkEqRefl pNondepExpr, -- pNondep = .ofDepTerm p
-            termNondepFsmExpr, -- TermFSM ...
-            ← mkEqRefl termNondepFsmExpr,
-            toExpr niters,
-            circsExpr,
-            circsLawfulExpr,
-            toExpr safetyCert,
-            safetyCertProof,
-            toExpr indCert,
-            indCertProof,
-            wenv,
-            tenv,
-            benv,
-            nenv,
-            ienv,
-            penv,
-            ← mkEqRefl pRawExpr]
-        debugCheck prf
-        let prf ←
-          if (← read).debugFillFinalReflectionProofWithSorry then
-            mkSorry (synthetic := true) (← g.getType)
+
+    if (← read).externalSolver then
+      let aig := termFsmNondep.toFsmZext.toAiger
+      let res ← Valaig.External.checkSafety (← read).externalSolverConfig aig
+
+      match res with
+      | .error err => throwError s!"UNKNOWN: {err}"
+      | .ok .counterexample=> throwError "CEX: rIC3 found a counter-example"
+      | .ok .proof =>
+        let prf ← mkSorry (synthetic := true) (← g.getType)
+        let _ ← g.apply prf
+        return
+    else
+      let (stats, _log) ← FSM.decideIfZerosVerified termFsmNondep.toFsmZext (maxIter := (← read).niter) (startVerifyAtIter := (← read).startVerifyAtIter)
+      match stats with
+      | .safetyFailure i =>
+        let suspiciousVars ← collect.logSuspiciousFvars
+        -- | Found precise counter-example to claimed predicate.
+        if suspiciousVars.isEmpty then
+            throwError m!"CEX: Found exact counter-example at iteration {i} for predicate '{pRawExpr}'"
           else
-            instantiateMVars prf
-        pure prf
-      let gs ← g.apply prf
-      if gs.isEmpty then
-        debugLog m!"unified goal with proof."
-      else
-        let mut msg := m!"Expected proof cerificate to close goal, but failed. Leftover goals:"
-        for g in gs do
-          msg := msg ++ m!"{indentD g}"
-        throwError msg
+            throwError m!"MAYCEX: Found possible counter-example at iteration {i} for predicate '{pRawExpr}'"
+      | .exhaustedIterations _ =>
+        let _ ← collect.logSuspiciousFvars
+        throwError m!"PROOFNOTFOUND: exhausted iterations for predicate '{pRawExpr}'"
+      | .provenByKIndCycleBreaking niters safetyCert indCert =>
+        if (← read).verbose? then
+          let _ ← collect.logSuspiciousFvars
+        debugLog m!"PROVE: proven {pRawExpr}"
+        let prf ← g.withContext <| do
+          let termNondepFsmExpr ← Expr.mkTermFsmNondep collect.wcard collect.tcard collect.bcard collect.ncard collect.icard collect.pcard pNondepExpr
+          debugCheck termNondepFsmExpr
+          -- let fsmExpr := termNondepFsmExpr
+          -- | TODO: refactor into fn.
+          let fsmExpr ← mkAppM (``MultiWidth.TermFSM.toFsmZext) #[termNondepFsmExpr]
+          -- debugCheck fsmExpr
+          let circsExpr ← Expr.KInductionCircuits.mkN fsmExpr (toExpr niters)
+          let circsLawfulExpr ← Expr.KInductionCircuits.mkIsLawful_mkN fsmExpr (toExpr niters)
+          debugLog "making safety certs..."
+          -- | verifyCircuit (mkSafetyCircuit circs)
+          let verifyCircuitMkSafetyCircuitExpr ← Expr.mkVerifyCircuit
+            (← Expr.KInductionCircuits.mkMkSafetyCircuit circsExpr)
+            (toExpr safetyCert)
+          -- debugLog m!"made safety cert expr: {verifyCircuitMkSafetyCircuitExpr}"
+          debugLog "making safety cert = true proof..."
+          let safetyCertProof ←
+            mkEqReflBoolNativeDecideProof `safetyCert verifyCircuitMkSafetyCircuitExpr true
+          -- debugLog m!"made safety cert proof: {safetyCertProof}"
+          let verifyCircuitMkIndHypCircuitExpr ← Expr.mkVerifyCircuit
+              (← Expr.KInductionCircuits.mkIndHypCycleBreaking circsExpr)
+              (toExpr indCert)
+          -- debugLog m!"made verifyCircuit expr: {verifyCircuitMkIndHypCircuitExpr}"
+          let indCertProof ←
+            mkEqReflBoolNativeDecideProof `indCert verifyCircuitMkIndHypCircuitExpr true
+          debugLog m!"made induction cert = true proof..."
+          let prf ← mkAppM ``MultiWidth.Term.toBV_of_KInductionCircuits'
+            #[pRawExpr, -- P : Prop
+              tctx,
+              pExpr, -- p
+              pNondepExpr, -- pNondep
+              ← mkEqRefl pNondepExpr, -- pNondep = .ofDepTerm p
+              termNondepFsmExpr, -- TermFSM ...
+              ← mkEqRefl termNondepFsmExpr,
+              toExpr niters,
+              circsExpr,
+              circsLawfulExpr,
+              toExpr safetyCert,
+              safetyCertProof,
+              toExpr indCert,
+              indCertProof,
+              wenv,
+              tenv,
+              benv,
+              nenv,
+              ienv,
+              penv,
+              ← mkEqRefl pRawExpr]
+          debugCheck prf
+          let prf ←
+            if (← read).debugFillFinalReflectionProofWithSorry then
+              mkSorry (synthetic := true) (← g.getType)
+            else
+              instantiateMVars prf
+          pure prf
+        let gs ← g.apply prf
+        if gs.isEmpty then
+          debugLog m!"unified goal with proof."
+        else
+          let mut msg := m!"Expected proof cerificate to close goal, but failed. Leftover goals:"
+          for g in gs do
+            msg := msg ++ m!"{indentD g}"
+          throwError msg
 
 def solveEntrypoint (g : MVarId) (cfg : Config) : TermElabM Unit :=
   let ctx := { toConfig := cfg}

@@ -1,7 +1,17 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"type": "path",
+ [{"url": "https://github.com/opencompl/valaig",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "7bcb9df848cc53100152ebfb7f94458a056a553a",
+   "name": "valaig",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "7bcb9df848cc53100152ebfb7f94458a056a553a",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"type": "path",
    "scope": "",
    "name": "SexprPBV",
    "manifestFile": "lake-manifest.json",

@@ -26,3 +26,8 @@ name = "BlaseEval"
 name = "SexprPBV"
 path = "../SexprPBV"
 rev = "main"
+
+[[require]]
+name = "valaig"
+git = "https://github.com/opencompl/valaig"
+rev = "7bcb9df848cc53100152ebfb7f94458a056a553a"
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -69,6 +69,16 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/opencompl/valaig",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "7bcb9df848cc53100152ebfb7f94458a056a553a",
+   "name": "valaig",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "7bcb9df848cc53100152ebfb7f94458a056a553a",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4-nightly-testing",
    "type": "git",
    "subDir": null,