Skip to content

Commit

Permalink
Only encode non-zero fuel condition in trigger
Browse files Browse the repository at this point in the history 
This allows approach allows us to limit user defined with triggers in a sensible way
  • Loading branch information
@ole-thoeb
ole-thoeb committed Nov 12, 2024
1 parent 75ae9fb commit c2cb67f
Show file tree
Hide file tree
Showing 2 changed files with 70 additions and 54 deletions.
109 changes: 64 additions & 45 deletions src/smt/limited.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,44 +56,6 @@ fn create_call_scope<'smt, 'ctx>(
scope
}

/// Creates an axiom that should be read from left to right.
/// It has the form:
/// ```txt
/// forall <vars...> @trigger(lhs) . lhs == rhs
/// ```
/// Where fuel parameters in `lhs` must be non-zero and are decremented in `rhs`.
fn translate_defining_axiom<'smt, 'ctx>(
translate: &mut TranslateExprs<'smt, 'ctx>,
func: &FuncDecl,
lhs: &Expr,
rhs: &Expr,
) -> Bool<'ctx> {
translate.set_fuel_context(FuelContext::head());

let symbolic_lhs = translate.t_symbolic(lhs).into_dynamic(translate.ctx);

// reuse same fuel in body
let quantified_fuel = translate
.fuel_context_mut()
.take_quantified_fuel()
.unwrap_or_default();
translate.set_fuel_context(FuelContext::body_with_fuel(quantified_fuel));
let symbolic_rhs = translate.t_symbolic(rhs).into_dynamic(translate.ctx);

let scope = create_call_scope(translate, func);
let axiom = scope.forall(
&[&Pattern::new(
translate.ctx.ctx,
&[&symbolic_lhs as &dyn Ast<'ctx>],
)],
&symbolic_lhs.smt_eq(&symbolic_rhs),
);

translate.set_fuel_context(FuelContext::Call); // reset to default

axiom
}

/// Creates a call to the function.
fn build_call(tcx: &TyCtx, func: &FuncDecl) -> Expr {
let span = func.span.variant(SpanVariant::VC);
Expand Down Expand Up @@ -121,17 +83,40 @@ pub fn fuel_synonym_axiom<'smt, 'ctx>(
) -> Option<Bool<'ctx>> {
if translate.ctx.is_limited_function_decl(func) {
let app = build_call(translate.ctx.tcx, func);
Some(translate_defining_axiom(translate, func, &app, &app))

translate.set_fuel_context(FuelContext::head());
let symbolic_head_app = translate.t_symbolic(&app).into_dynamic(translate.ctx);

// reuse same fuel in body
let quantified_fuel = translate
.fuel_context_mut()
.take_quantified_fuel()
.unwrap_or_default();
translate.set_fuel_context(FuelContext::body_with_fuel(quantified_fuel));
let symbolic_body_app = translate.t_symbolic(&app).into_dynamic(translate.ctx);

let scope = create_call_scope(translate, func);
let axiom = scope.forall(
&[&Pattern::new(
translate.ctx.ctx,
&[&symbolic_head_app as &dyn Ast<'ctx>],
)],
&symbolic_head_app.smt_eq(&symbolic_body_app),
);

translate.set_fuel_context(FuelContext::Call); // reset to default

Some(axiom)
} else {
None
}
}

/// Creates the default defining axiom for a function. It has the form:
/// ```txt
/// forall fuel: Fuel, <args...> @trigger(func_name(Succ(fuel), <args...>)) . func_name(Succ(fuel), <args...>) = <body>
/// forall fuel: Fuel, <args...> @trigger(func_name(Succ(fuel), <args...>)) . func_name(fuel, <args...>) = <body>
/// ```
/// where only `fuel` is used as the fuel parameter in `<body>`.
/// The trigger requires a non-zero fuel value to match. The axiom itself has no such requirement.
///
/// The axiom is only generated for functions that have an immediate definition (body).
pub fn defining_axiom<'smt, 'ctx>(
Expand All @@ -140,7 +125,31 @@ pub fn defining_axiom<'smt, 'ctx>(
) -> Option<Bool<'ctx>> {
func.body.borrow().as_ref().map(|body| {
let app = build_call(translate.ctx.tcx, func);
translate_defining_axiom(translate, func, &app, body)

translate.set_fuel_context(FuelContext::head());
let app_pattern = translate.t_symbolic(&app).into_dynamic(translate.ctx);

// reuse same fuel in body
let quantified_fuel = translate
.fuel_context_mut()
.take_quantified_fuel()
.unwrap_or_default();
translate.set_fuel_context(FuelContext::body_with_fuel(quantified_fuel));
let symbolic_app = translate.t_symbolic(&app).into_dynamic(translate.ctx);
let symbolic_body = translate.t_symbolic(body).into_dynamic(translate.ctx);

let scope = create_call_scope(translate, func);
let axiom = scope.forall(
&[&Pattern::new(
translate.ctx.ctx,
&[&app_pattern as &dyn Ast<'ctx>],
)],
&symbolic_app.smt_eq(&symbolic_body),
);

translate.set_fuel_context(FuelContext::Call); // reset to default

axiom
})
}

Expand Down Expand Up @@ -230,12 +239,13 @@ pub fn return_value_invariant<'smt, 'ctx>(
/// Translates an arbitrary user defined axiom, that might contain references to limited functions.
/// If the axiom contains a limited function, the whole axiom is wrapped in a `forall`
/// quantifying over the fuel.
///
/// For the usual case that the axiom starts with a `forall` the `forall fuel: Fuel` is merged with
/// the `forall` of the axiom. Additionally, any provided triggers require a non-zero fuel value.
pub fn free_axiom<'smt, 'ctx>(
translate: &mut TranslateExprs<'smt, 'ctx>,
axiom_decl: &AxiomDecl,
) -> Bool<'ctx> {
translate.set_fuel_context(FuelContext::body());

let axiom = match &axiom_decl.axiom.kind {
// Optimisation: If the axiom starts with a forall -> merge the `forall fuel: Fuel` with
// the `forall` of the axiom.
Expand All @@ -249,15 +259,24 @@ pub fn free_axiom<'smt, 'ctx>(
operand,
) => {
// TODO: duplicate logic from TranslateExpression::t_bool
let operand = translate.t_bool(operand);
translate.set_fuel_context(FuelContext::head());
let patterns: Vec<_> = translate.t_triggers(&ann.triggers);
let patterns: Vec<_> = patterns.iter().collect();

let quantified_fuel = translate
.fuel_context_mut()
.take_quantified_fuel()
.unwrap_or_default();
translate.set_fuel_context(FuelContext::body_with_fuel(quantified_fuel));
let operand = translate.t_bool(operand);

let mut scope = translate.mk_scope(quant_vars);
scope.extend(translate.fuel_context().quantified_fuel_scope());
scope.forall(&patterns, &operand)
}
_ => {
translate.set_fuel_context(FuelContext::body());

let mut axiom = translate.t_bool(&axiom_decl.axiom);
if let Some(fuel_scope) = translate.fuel_context().quantified_fuel_scope() {
axiom = fuel_scope.forall(&[], &axiom);
Expand Down
15 changes: 6 additions & 9 deletions tests/boolean/reason_about_comprehensions_sum.heyvl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,22 +3,19 @@
// Sum examples from the paper "Reasoning about Comprehensions with First-Order SMT Solvers" (Section 3.4)

domain Sum {
// When using limited functions, although one axiom can be created from the other using the split_range axiom,
// both axioms are required. The fuel value of 1 does not allow for it.

// Induction below axiom
func elementSum(lo: UInt, hi: UInt, a: []Int): Int = ite(lo < hi, select(a, lo) + elementSum(lo + 1, hi, a), 0)

/*axiom induction_below forall lo: UInt, hi: UInt, a: []Int @trigger(elementSum(lo, hi, a)) .
(lo < hi) ==> (elementSum(lo, hi, a) == select(a, lo) + elementSum(lo + 1, hi, a))
axiom induction_above forall lo: UInt, hi: UInt, a: []Int @trigger(elementSum(lo, hi, a)) .
(lo < hi) ==> (elementSum(lo, hi, a) == select(a, lo) + elementSum(lo, hi - 1, a))*/

//axiom empty forall lo: UInt, hi: UInt, a: []Int @trigger(elementSum(lo, hi, a)) . (hi <= lo) ==> (elementSum(lo, hi, a) == 0)
elementSum(lo, hi, a) == ite(lo < hi, select(a, hi - 1) + elementSum(lo, hi - 1, a), 0)

// Omitting triggers here is detrimental to the performance
axiom split_range forall lo: UInt, mid: UInt, hi: UInt, a: []Int @trigger(elementSum(lo, mid, a), elementSum(mid, hi, a)) @trigger(elementSum(lo, mid, a), elementSum(lo, hi, a)) @trigger(elementSum(lo, hi, a), elementSum(mid, hi, a)) .
(lo <= mid && mid <= hi) ==> (elementSum(lo, mid, a) + elementSum(mid, hi, a) == elementSum(lo, hi, a))
/* axiom split_range forall lo: UInt, mid: UInt, hi: UInt, a: []Int @trigger(elementSum(lo, mid, a), elementSum(mid, hi, a)) @trigger(elementSum(lo, mid, a), elementSum(lo, hi, a)) @trigger(elementSum(lo, hi, a), elementSum(mid, hi, a)) .
(lo <= mid && mid <= hi) ==> (elementSum(lo, mid, a) + elementSum(mid, hi, a) == elementSum(lo, hi, a)) */

/*axiom unit forall lo: UInt, hi: UInt, a: []Int @trigger(elementSum(lo, hi, a)) .
(forall k: UInt . (lo <= k && k < hi) ==> (select(a, k) == 0)) ==> (elementSum(lo, hi, a) == 0)*/
}

proc Sum1(a: []Int) -> (s: Int)
Expand Down

0 comments on commit c2cb67f

Please sign in to comment.