Automatically add triggers to function definition/specification axioms
I think it would be helpful to add triggers to the definitions/specifications of functions/predicates (possibly via a transformation or meta/attribute). One possible strategy would be:
For non-recursive functions/predicates: add result
/(the function being defined) as the trigger for both the definition and specification axioms.
module Add1
use int.Int
let function add1 (arg: int) : int
ensures { result > arg }
=
arg + 1
goal test: add1 0 = 1
end
module Add1Trigger
use int.Int
function add1 (arg:int) : int
axiom add1_def : forall arg:int [add1 arg]. add1 arg = arg + 1
axiom add1_spec : forall arg:int [add1 arg]. add1 arg > arg
goal test: add1 0 = 1
end
For recursive functions/predicates: create a new "limited" function with the same arguments as the function being defined. Create a new axiom stating that it's equivalent to the original function. In the definition axiom replace that the recursive calls with the "limited" function and trigger on the original.
In the specification axiom using "limited" function in place of 'result' and as the trigger, ends up being slightly stronger as it means the prover can learn it even after unfolding the definition.
module Id
use int.Int
let rec function id (arg: int) : int
requires { arg >= 0}
variant {arg}
ensures { arg = 0 -> result = 0 }
=
if arg = 0 then 0 else id(arg - 1) + 1
goal test0: id 0 = 0
goal test1: id 1 = 1
goal test2: id 2 = 2
goal test20: id 20 = 20 (*Takes >5000 steps with Alt-ergo on https://why3.lri.fr/try/*)
end
module IdTrigger
use int.Int
function id_lim int : int
function id int : int
axiom id_def :
forall arg:int [id arg].
arg >= 0 ->
(if arg = 0 then id arg = 0 else id arg = (id_lim (arg - 1) + 1))
axiom id_spec : forall arg:int [id_lim arg]. arg >= 0 -> arg = 0 -> id_lim arg = 0
axiom id_lim_spec : forall arg:int [id arg]. id arg = id_lim arg
goal test0: id 0 = 0
goal test1: id 1 = 1 (*Succeeds only because we used the limited function in the spec axiom*)
goal test2: id 2 = 2 (*Fails*)
goal test20: id 20 = 20 (*Fails*)
end
One other issue I found is, when verifying and recursive item (function/predicate/lemma) which calls a recursive function/predicate under a quantifier in a post-condition (maybe also pre-condition), the task might fail even when it intuitively only requires a single unfolding. This is because the prover might use the not-"limited" in the trigger for the quantifier when expanding the recursive call, so the quantifier won't apply at all to the unfolded definition. One solution would be to duplicate the post-condition, where the second version uses the "limited" function instead (in all places). A slight improvement would be to only modify the VC task and duplicate the post-condition in the assumption from the recursive call, the goal wouldn't need to be changed since the original version function can always be proved if the other one can. A similar trick could also be used for quantifiers in loop-invariants.
module IdLemma
use int.Int
use Id
let rec lemma idLemma(arg: int)
requires {arg >= 0}
variant {arg}
ensures {forall i:int. 0 <= i < arg -> id i = i}
= if arg <> 0 then idLemma (arg - 1)
end
module IdLemmaBroken
use int.Int
use IdTrigger
let rec lemma idLemma(arg: int)
requires {arg >= 0}
variant {arg}
ensures {forall i:int. 0 <= i < arg -> id i = i} (*Fails*)
= if arg <> 0 then idLemma (arg - 1)
end
module IdLemmaFix
use int.Int
use IdTrigger
let rec lemma idLemma(arg: int)
requires {arg >= 0}
variant {arg}
ensures {forall i:int. 0 <= i < arg -> id i = i}
ensures {forall i:int. 0 <= i < arg -> id_lim i = i}
= if arg <> 0 then idLemma (arg - 1)
end
module IdLemmaFix2
use int.Int
use IdTrigger
goal idLemma_vc :
forall arg:int.
arg >= 0 ->
(let (=)_result_unused_unused = (if arg = 0 then True else False) in
(not arg = 0 -> (let o = arg - 1 in (0 <= arg /\ o < arg) /\ o >= 0)) /\
(arg = 0 \/
(let o = arg - 1 in
(forall i:int. 0 <= i /\ i < o -> id i = i) /\
(forall i:int. 0 <= i /\ i < o -> id_lim i = i)) ->
(forall i:int. 0 <= i /\ i < arg -> id i = i)))
end