Skip to content

Commit 304a6f8

Browse files
dranovdranov
committed
refactor: sat trace functionality and bmc_sat
This changes the goal generated by `sat trace` to clearly state what is actually checked. Previously, we universally quantified over the `type`s and type class instance assumptions, but that wasn't actually what the SMT query meant, which was confusing. Now the goal shown to the user exactly matches what is checked. Moreover, this commit prints models on `sat trace` queries.
1 parent 691ba7d commit 304a6f8

File tree

7 files changed

+136
-60
lines changed

7 files changed

+136
-60
lines changed

‎Test/BmcSat.lean‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
import Veil
2+
3+
veil module BmcSat
4+
5+
individual flag : Prop
6+
7+
#gen_state
8+
9+
after_init {
10+
flag := False
11+
}
12+
13+
action set_flag = {
14+
flag := True;
15+
}
16+
17+
invariant ¬ flag
18+
19+
#gen_spec
20+
21+
#guard_msgs(drop warning) in
22+
sat trace { } by bmc_sat
23+
24+
#guard_msgs(drop warning, drop info) in
25+
sat trace {
26+
set_flag
27+
set_flag
28+
} by bmc_sat
29+
30+
/-- error: the goal is false -/
31+
#guard_msgs in
32+
sat trace {
33+
assert False
34+
} by bmc_sat
35+
36+
end BmcSat

‎Veil/DSL/Trace/Main.lean‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -127,11 +127,12 @@ def elabTraceSpec (r : TSyntax `expected_smt_result) (name : Option (TSyntax `id
127127
-- unsat trace -> ∀ states, ¬ (conjunction of assertions)
128128
let stateTp ← getStateTpStx
129129
let binderNames : Array (TSyntax ``Lean.binderIdent) := stateNames.map toBinderIdent
130+
let vdE ← vd.mapM toExplicitBinders
130131
let assertion ← match r with
131-
| `(expected_smt_result| unsat) => `(∀ ($[$stateNames]* : $stateTp), ¬ $conjunction)
132-
| `(expected_smt_result| sat) => `(∃ ($[$binderNames]* : $stateTp), $conjunction)
132+
| `(expected_smt_result| unsat) => `(∀ $[$vd]* ($[$stateNames]* : $stateTp), ¬ $conjunction)
133+
| `(expected_smt_result| sat) => `(∃ $[$vdE]* ($[$binderNames]* : $stateTp), $conjunction)
133134
| _ => dbg_trace "expected result is neither sat nor unsat!" ; unreachable!
134-
`(theorem $th_id $[$vd]* : $assertion := by exact $pf)
135+
`(theorem $th_id : $assertion := by exact $pf)
135136
elabCommand $ th
136137

137138
elab_rules : command

‎Veil/SMT/Main.lean‎

Lines changed: 0 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -77,37 +77,4 @@ def failureGoalStr : String := "solver invocation failed"
7777
| .Failure reason => throwError "{failureGoalStr}{if reason.isSome then s!": {reason.get!}" else ""}"
7878
| .Unsat => mv.admit (synthetic := false)
7979

80-
81-
open Lean.Meta in
82-
/-- UNSAFE: Switches the goal with its negation!
83-
This is unsound unless we use `admit_if_satisfiable` on the resulting goal! -/
84-
elab "negate_goal" : tactic => withMainContext do
85-
let goal ← getMainGoal
86-
let goalType ← getMainTarget
87-
let negatedGoalType ← mkAppM `Not #[goalType]
88-
let negatedGoal ← mkFreshExprMVar $ negatedGoalType
89-
goal.admit (synthetic := false)
90-
setGoals [negatedGoal.mvarId!]
91-
92-
syntax (name := admit_if_satisfiable) "admit_if_satisfiable" Smt.Tactic.smtHints Smt.Tactic.smtTimeout : tactic
93-
94-
open Lean.Meta in
95-
/-- UNSAFE: admits the goal if it is satisfiable.
96-
This is unsound unless we use `negate_goal` on the goal first!
97-
MOREOVER, we need to pass in all the hypotheses in the context.
98-
-/
99-
@[tactic admit_if_satisfiable] def evalAdmitIfSat : Tactic := fun stx => withMainContext do
100-
let mv ← Tactic.getMainGoal
101-
let hs ← Smt.Tactic.parseHints ⟨stx[1]⟩
102-
let withTimeout ← parseTimeout ⟨stx[2]⟩
103-
let cmdString ← Veil.SMT.prepareLeanSmtQuery mv hs
104-
let res ← Veil.SMT.querySolver cmdString withTimeout (retryOnUnknown := true)
105-
match res with
106-
| .Sat _ =>
107-
trace[veil.smt.result] "The negation of the goal is satisfiable, hence the goal is valid."
108-
mv.admit (synthetic := false)
109-
| .Unsat => throwError "the goal is false"
110-
| .Unknown _ => throwError "the solver returned {res}"
111-
| .Failure _ => throwError "solver invocation {res}"
112-
11380
end Veil.SMT

‎Veil/SMT/Quantifiers/Elimination.lean‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,10 @@ def HO_exists_push_left_impl : Simp.Simproc := fun e => do
6969
-- The body of an `∃` is a lambda
7070
let step : Simp.Step ← lambdaBoundedTelescope eBody (maxFVars := 1) (fun ks lBody => do
7171
let_expr Exists t' eBody' := lBody | return .continue
72-
if (← isHigherOrder t') && !(← isHigherOrder t) then
72+
-- We only want to push HO types left over non-HO types. But we must be
73+
-- careful: if `t'` depends on the value of the previous binder, we cannot
74+
-- swap them.
75+
if (← isHigherOrder t') && !(← isHigherOrder t) && !(dependsOn t' ks) then
7376
let step : Simp.Step ← lambdaBoundedTelescope eBody' (maxFVars := 1) (fun ks' lBody' => do
7477
-- swap the quantifiers
7578
let innerExists := mkAppN e.getAppFn #[t, ← mkLambdaFVars ks lBody']
@@ -82,6 +85,9 @@ def HO_exists_push_left_impl : Simp.Simproc := fun e => do
8285
return .continue
8386
)
8487
return step
88+
where
89+
dependsOn (child : Expr) (deps : Array Expr) : Bool :=
90+
child.find? (fun e => deps.contains e) != none
8591

8692
simproc HO_exists_push_left (∃ _ _, _) := HO_exists_push_left_impl
8793
attribute [quantifierSimp] HO_exists_push_left

‎Veil/Tactic/Main.lean‎

Lines changed: 71 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -319,25 +319,74 @@ elab "bmc" : tactic => withMainContext do
319319
trace[veil.smt] "{tac}"
320320
evalTactic $ tac
321321

322-
/-- Tactic to solve `sat_trace` goals. -/
323-
elab "bmc_sat" : tactic => withMainContext do
324-
let prep_tac ← `(tactic|
325-
(try simplify_all);
326-
(try
327-
negate_goal;
328-
simp only [Classical.exists_elim, Classical.not_not];
329-
(unhygienic intros);
330-
sdestruct_hyps);
331-
(try simplify_all);
332-
/- Needed to work around [lean-smt#100](https://github.com/ufmg-smite/lean-smt/issues/100) -/
333-
(try rename_binders)
334-
)
335-
trace[veil.smt] "{prep_tac}"
336-
evalTactic prep_tac
337-
if (← getUnsolvedGoals).length != 0 then
338-
/- After preparing the context, call `sauto` on it. -/
339-
withMainContext do
340-
let idents ← getPropsInContext
341-
let auto_tac ← `(tactic| admit_if_satisfiable [$[$idents:ident],*])
342-
trace[veil.smt] "{auto_tac}"
343-
evalTactic auto_tac
322+
open Lean.Meta in
323+
def bmcSat : TacticM Unit := withMainContext do
324+
let originalGoal ← Tactic.getMainGoal
325+
-- Operate on a duplicated goal
326+
let goal' ← mkFreshExprMVar (← Tactic.getMainTarget)
327+
replaceMainGoal [goal'.mvarId!]
328+
run `(tactic| simplify_all)
329+
if (← getUnsolvedGoals).length == 0 then
330+
trace[veil.info] "goal is solved by initial simplification"
331+
originalGoal.admit (synthetic := false)
332+
else
333+
trace[veil.info] "goal is not solved by initial simplification"
334+
existIntoForall
335+
let simpLemmas := mkSimpLemmas $ #[`smtSimp].map mkIdent
336+
withMainContext do run `(tactic| unhygienic intros; sdestruct_hyps; (try simp only [$simpLemmas,*]))
337+
if (← getUnsolvedGoals).length == 0 then
338+
trace[veil.info] "goal is solved by existential elimination"
339+
originalGoal.admit (synthetic := false)
340+
else
341+
trace[veil.info] "proceeding with SMT"
342+
trace[veil.info] "goal: {← Tactic.getMainTarget}"
343+
admitIfSat
344+
if (← getUnsolvedGoals).length == 0 then
345+
originalGoal.admit (synthetic := false)
346+
else
347+
throwError "goal is not solved by SMT"
348+
where
349+
existIntoForall := withMainContext do
350+
let goalType' ← turnExistsIntoForall (← Tactic.getMainTarget)
351+
let goal' ← mkFreshExprMVar goalType'
352+
replaceMainGoal [goal'.mvarId!]
353+
/-- UNSAFE: admits the goal if it is satisfiable, taking into account
354+
all hypotheses in the context. -/
355+
admitIfSat : TacticM Unit := withMainContext do
356+
let opts ← getOptions
357+
let mv ← Tactic.getMainGoal
358+
let idents ← getPropsInContext
359+
let hints ← `(Smt.Tactic.smtHints|[$[$idents:ident],*])
360+
let hs ← Smt.Tactic.parseHints ⟨hints⟩
361+
let withTimeout := veil.smt.timeout.get opts
362+
-- IMPORTANT: `prepareLeanSmtQuery` (in `Smt.prepareSmtQuery`) negates
363+
-- the goal (it's designed for validity checking), so we negate it here
364+
-- to counter-act this.
365+
-- NOTE: we don't respect `veil.smt.translator` here, since we want to
366+
-- print a readable model, which requires `lean-smt`.
367+
let mv' ← mkFreshExprMVar (mkNot $ ← Tactic.getMainTarget)
368+
let leanSmtQueryString ← Veil.SMT.prepareLeanSmtQuery mv'.mvarId! hs
369+
let res ← Veil.SMT.querySolver leanSmtQueryString withTimeout (retryOnUnknown := true)
370+
match res with
371+
| .Sat .none => mv.admit (synthetic := false)
372+
| .Sat (some modelString) =>
373+
-- try to generate a readable model, using `lean-smt`
374+
let resStr := match ← Veil.SMT.getReadableModel leanSmtQueryString withTimeout (minimize := veil.smt.model.minimize.get opts) with
375+
| .some fostruct => s!"{fostruct}"
376+
| .none => s!"(could not get readable model)\n{modelString}"
377+
logInfo resStr
378+
mv.admit (synthetic := false)
379+
| .Unknown reason => throwError "{Veil.SMT.unknownGoalStr}{if reason.isSome then s!": {reason.get!}" else ""}"
380+
| .Failure reason => throwError "{Veil.SMT.failureGoalStr}{if reason.isSome then s!": {reason.get!}" else ""}"
381+
| .Unsat => throwError "{Veil.SMT.satGoalStr}"
382+
383+
/-- Tactic to solve `sat trace` goals.
384+
385+
Given a goal of the form `∃ x, P x` (valid), we prove it by showing `P c`
386+
is _satisfiable_ for some constant `c`.
387+
388+
In principle, we could use the model returned by the SMT solver to
389+
instantiate the existential quantifiers, and thus avoid the need to
390+
trust the solver, but this is not implemented yet.
391+
-/
392+
elab "bmc_sat" : tactic => bmcSat

‎Veil/Util/Meta.lean‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,14 @@ def toBracketedBinderArray (stx : TSyntax `Lean.explicitBinders) : MetaM (TSynta
4444
pure ()
4545
| _ => throwError "unexpected syntax in explicit binder: {stx}"
4646
return binders
47+
/-- Convert definition binders into existential binders. -/
48+
def toExplicitBinders [Monad m] [MonadError m] [MonadQuotation m] (stx : TSyntax `Lean.Parser.Term.bracketedBinder) : m (TSyntax `Lean.bracketedExplicitBinders) := do
49+
match stx with
50+
| `(bracketedBinder| ($id:ident : $tp:term))
51+
| `(bracketedBinder| [$id:ident : $tp:term])
52+
| `(bracketedBinder| {$id:ident : $tp:term}) =>
53+
return ← `(bracketedExplicitBinders|($(toBinderIdent id) : $tp))
54+
| _ => throwError "unexpected syntax in explicit binder: {stx}"
4755

4856
/-- Convert existential binders into function binders. -/
4957
def toFunBinderArray (stx : TSyntax `Lean.explicitBinders) : MetaM (TSyntaxArray `Lean.Parser.Term.funBinder) := do
@@ -241,3 +249,12 @@ def combineLemmas (op : Name) (exps: List Expr) (vs : Array Expr) (name : String
241249
exps <- mkAppM op #[exp, exps]
242250
mkLambdaFVars args exps
243251
instantiateLambda exps vs
252+
253+
open Meta in
254+
partial def turnExistsIntoForall (e : Expr) : MetaM Expr := do
255+
match_expr e with
256+
| Exists _t eBody =>
257+
lambdaBoundedTelescope eBody (maxFVars := 1) (fun ks lBody => do
258+
mkForallFVars ks (← turnExistsIntoForall lBody)
259+
)
260+
| _ => return e

‎Veil/Util/Quantifiers.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -220,7 +220,7 @@ abbrev QuantElimM := StateT QEState n
220220

221221
def isHigherOrder (e : Expr) : MetaM Bool := do
222222
let t ← inferType e
223-
let isHO := !t.isProp && (e.isArrow || e.isAppOf (← getStateName))
223+
let isHO := (!t.isProp) && (e.isArrow || e.isAppOf (← getStateName))
224224
return isHO
225225

226226
partial def forEachExprSane'

0 commit comments

Comments
 (0)