diff --git a/Blase/Blase/Fast/Aiger.lean b/Blase/Blase/Fast/Aiger.lean index eedc0acce0..0b2f36d6a2 100644 --- a/Blase/Blase/Fast/Aiger.lean +++ b/Blase/Blase/Fast/Aiger.lean @@ -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 + } diff --git a/Blase/Blase/MultiWidth/Tactic.lean b/Blase/Blase/MultiWidth/Tactic.lean index 1e1ac16be8..034b9447f9 100644 --- a/Blase/Blase/MultiWidth/Tactic.lean +++ b/Blase/Blase/MultiWidth/Tactic.lean @@ -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} diff --git a/Blase/lake-manifest.json b/Blase/lake-manifest.json index fcfbf744b0..35f4cecd31 100644 --- a/Blase/lake-manifest.json +++ b/Blase/lake-manifest.json @@ -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", diff --git a/Blase/lakefile.toml b/Blase/lakefile.toml index 3fd26702cb..cecd8ab2ac 100644 --- a/Blase/lakefile.toml +++ b/Blase/lakefile.toml @@ -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 index e697dd49a8..b4502225a8 100644 --- 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,