Email Gateway (Aug 19 2022 at 08:08): Email Gateway (Aug 19 2022 at 08:08):From: Lars Noschinski <noschinl@in.tum.de>
Hi everyone,
I am working on formalizing some algorithms using Simpl from the AFP.
Is there some lightweight way (in a procedures definition) to annotate a
loop with the property that a variable stays unchanged? For procedures,
there is the may-not-modify-globals syntax; but a similar thing does not
seem to exist for loops (and it is not clear, how this would fit in). At
the moment, I am using the ANNO command for this purpose:
procedures mult1 (n :: nat, m :: nat | r :: nat)
"
ANNO τ.
{τ}
´r :== (0 :: nat) ;;
WHILE ´n ≠ 0
INV ⦃ ´m = ⇗τ⇖m ∧ ´m * ⇗τ⇖n = ´r + ´m * ´n ⦄
DO
´r :== ´r + ´m ;;
´n :== ´n - 1
OD
⦃ ´r = ⇗τ⇖m * ⇗τ⇖n ⦄
"
lemma (in mult1_impl) mult1:
"∀m n. Γ ⊢ ⦃´m = m ∧ ´n = n⦄ ´r :== PROC mult1(´m, ´n) ⦃´r = m * n⦄"
apply vcg
apply (simp_all add: mult_Suc_right[symmetric])
done
Here I need a full write down a full specification already in the
procedure definition. This is particularly annoying for ANNO statements
deeper in the procedure definition.
The only other solution I have found would be adding the invariants only
in the proof:
procedures mult2 (n :: nat, m :: nat | r :: nat)
"
´r :== (0 :: nat) ;;
WHILE ´n ≠ 0
DO
´r :== ´r + ´m ;;
´n :== ´n - 1
OD
"
lemma (in mult2_impl) mult2:
"∀m n. Γ ⊢ ⦃´m = m ∧ ´n = n⦄ ´r :== PROC mult2(´m, ´n) ⦃´r = m * n⦄"
apply vcg_step
apply (hoare_rule HoarePartial.Seq)
defer
apply (hoare_rule I="⦃ ´m = m ∧ ´m * n = ´r + ´m * ´n ⦄" in
HoarePartial.reannotateWhileNoGuard)
apply vcg
apply (simp_all add: mult_Suc_right[symmetric])
apply vcg
apply simp
done
Here, it is harder to see which invariants are actually used for which
loop (and I can only use the full vcg after I reached the loop), so I
would like to know about nicer solutions (if there are any).
-- Lars
Email Gateway (Aug 19 2022 at 08:08):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Hi Lars,
This is what we used for the kernel proof. It doesn't look nice and has the disadvantages you explain. It does have the advantage that you can pick different invariants/annotations for each proof about that function.
Slight side rant: It's strange that Hoare logic insists that one would only ever prove one property about a function, have one invariant, and one annotation that fits them all. In theory this is all equivalent and there is a "complete specification", but in practise that is not how things are proved or should be proved.
Just think about what we do for functional programs in Isabelle. Nothing is more cumbersome and useless than having to state one lemma that says everything about one function.
From that point of view, I'm fairly convinced that annotations and invariants belong with the proof, not with the program (or everything belongs with the program). It would be nice to have a better notation for connecting them, though.
Cheers,
Gerwin
Email Gateway (Aug 19 2022 at 08:08):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Hi Lars.
You may not necessarily need to single-step the vcg. Have a look at
whileAnno_def: "whileAnno b I V c == While b c". Since this is full
equality, you can add or remove annotations with fold/unfold if this is
useful.
The annotations are really just hints to the vcg, not elements of the
syntax or semantics of SIMPL.
So, one thing you could do is annotate the loops with names, and then
substitute them on the spot.
definition "name_loop v = UNIV"
(in proc defn):
"
WHILE ´n ≠ 0
INV name_loop ''foo''
DO ... OD
"
lemma annotate_named_loop:
"whileAnno b (name_loop v) V c = whileAnno b I V c"
by (simp add: whileAnno_def)
(in unfolding)
apply (simp add: annotate_named_loop[where name="''foo''" and I="..."])
Not a lot nicer, but maybe a bit less fiddly.
I guess it would be nicer if SIMPL provided a facility by which you
could add such invariant declarations/redeclarations into the context
and have the vcg notice them as necessary. There might even be a way to
do this already, though I can't think what it would be.
Yours,
Thomas.
Email Gateway (Aug 19 2022 at 08:09):From: Lars Noschinski <noschinl@in.tum.de>
Hi,
On 10.07.2012 03:27, Thomas Sewell wrote:
You may not necessarily need to single-step the vcg. Have a look at
whileAnno_def: "whileAnno b I V c == While b c". Since this is full
equality, you can add or remove annotations with fold/unfold if this is
useful.
[...]
definition "name_loop v = UNIV"
[...]
lemma annotate_named_loop:
"whileAnno b (name_loop v) V c = whileAnno b I V c"
by (simp add: whileAnno_def)
[...]
(in unfolding)
apply (simp add: annotate_named_loop[where name="''foo''" and I="..."])
[...]
thank you both for your answers! This renaming indeed provides a less
fiddly solution (somehow I did not think about using the simplifier on
Simpl programs ...).
-- Lars
Email Gateway (Aug 19 2022 at 08:09):From: Lars Noschinski <noschinl@in.tum.de>
Actually, this fails if the invariant needs to meta-quantified variables
-- I don't think we have a substitution variant of (rule_tac x=... in ...).
-- Lars
Email Gateway (Aug 19 2022 at 08:09):From: John Wickerson <jpw48@cam.ac.uk>
Slight side rant: It's strange that Hoare logic insists that one would only ever prove one property about a function, have one invariant, and one annotation that fits them all. In theory this is all equivalent and there is a "complete specification", but in practise that is not how things are proved or should be proved.
I think it's fine in Hoare logic to prove multiple properties of a function C, like {P1}C{Q1} and {P2}C{Q2}. The point of the rules of conjunction
{P1}C{Q1} {P2}C{Q2}
{P1∧P2}C{Q1∧Q2}
and disjunction
{P1}C{Q1} {P2}C{Q2}
{P1∨P2}C{Q1∨Q2}
are to allow these multiple properties to be combined. But in the "proof outline" representation of a Hoare logic proof, where the program text is interspersed with assertions, you can't really represent this without writing out the program text multiple times, which is a hassle.
John
Email Gateway (Aug 19 2022 at 08:09):From: Lukas Bulwahn <bulwahn@in.tum.de>
This observation motivated me back in 2007 to NOT define a Hoare logic
for Imperative-HOL, but to do all the case studies just with a simple
predicate capturing the operational semantics. Composition of facts of
the same program therefore does not even require any special rule and
use of object connectives, but can be done with resolution, e.g. the OF
attribute.
As that was so non-standard, other people seem to have defined a Hoare
logic for Imperative-HOL nevertheless.
I tried to prove properties of the imperative programs separately.
In my case studies, the properties of the functions relied heavily one
on the previous one, which required me to re-state properties again and
again.
The solution I then came up with is still quite adhoc: I came up with
richer induction rules to obtain already proved facts in the context
with names.
With the infrastructure at the moment, I think proving all the facts at
once would have been simpler in my case.
The most difficult case study, the imperative unification algorithm, is
still managable by proving all properties at once, and the most
reasoning of the different properties overlap in various places in the
proof.
Kernel functions in seL4 have probably a different flavor.
Lukas
Email Gateway (Aug 19 2022 at 08:09):From: Gerwin Klein <gerwin.klein@nicta.com.au>
On 10/07/2012, at 6:26 PM, John Wickerson wrote:
Slight side rant: It's strange that Hoare logic insists that one would only ever prove one property about a function, have one invariant, and one annotation that fits them all. In theory this is all equivalent and there is a "complete specification", but in practise that is not how things are proved or should be proved.
I think it's fine in Hoare logic to prove multiple properties of a function C, like {P1}C{Q1} and {P2}C{Q2}. The point of the rules of conjunction
{P1}C{Q1} {P2}C{Q2}
{P1∧P2}C{Q1∧Q2}
and disjunction
{P1}C{Q1} {P2}C{Q2}
{P1∨P2}C{Q1∨Q2}
are to allow these multiple properties to be combined.
Sure. Maybe I should clarify: I'm not objecting to Hoare logic as such, it's perfectly capable of showing multiple independent properties about a program (that's what we've used in the seL4 proofs I was mentioning, precisely with rules as above). I'm objecting to how it is usually used and presented, and to what tools in turn usually imply for your workflow.
The fact that there is precisely one specification statement and one invariant that you can annotate for each procedure/loop in usual tools and presentations is the problem. This is hard to avoid if these annotations go into the program, because it is awkward to differentiate between multiple proofs in one invariant annotation (possible, but very annoying).
But in the "proof outline" representation of a Hoare logic proof, where the program text is interspersed with assertions, you can't really represent this without writing out the program text multiple times, which is a hassle.
That is the direction I meant, only that this is already the case with just invariants (which will need to be provided somehow, at least if there is automation/vcg support in some form). It is perfectly possible to mention these annotations in the proof only, and I'm arguing that this is where they belong.
Cheers,
Gerwin
Email Gateway (Aug 19 2022 at 08:10):From: Gerwin Klein <gerwin.klein@nicta.com.au>
On 10/07/2012, at 6:53 PM, Lukas Bulwahn wrote:
On 07/10/2012 01:09 AM, Gerwin Klein wrote:
This is what we used for the kernel proof. It doesn't look nice and has the disadvantages you explain. It does have the advantage that you can pick different invariants/annotations for each proof about that function.
Slight side rant: It's strange that Hoare logic insists that one would only ever prove one property about a function, have one invariant, and one annotation that fits them all. In theory this is all equivalent and there is a "complete specification", but in practise that is not how things are proved or should be proved.
Just think about what we do for functional programs in Isabelle. Nothing is more cumbersome and useless than having to state one lemma that says everything about one function.
This observation motivated me back in 2007 to NOT define a Hoare logic for Imperative-HOL, but to do all the case studies just with a simple predicate capturing the operational semantics. Composition of facts of the same program therefore does not even require any special rule and use of object connectives, but can be done with resolution, e.g. the OF attribute.As that was so non-standard, other people seem to have defined a Hoare logic for Imperative-HOL nevertheless.
I tried to prove properties of the imperative programs separately.
I'd argue that Hoare logic or not is a separate issue from proving properties separately or not. Any combination of these is possible. It's just that most Hoare logic frameworks practically force you in one direction (and they shouldn't).
In my case studies, the properties of the functions relied heavily one on the previous one, which required me to re-state properties again and again.
We have seen some of that effect in our proofs as well, but not everywhere. Some loops for instance need a fairly complex invariant just to be able to say anything about them, and in this case it can be easier to get the strongest statement you can come up with and be done with it. This can be awkward to use, because you will either get a fairly large precondition with many cases or one that is fairly strong and may be harder to establish than necessary, but it may still be worth it overall.
On the other hand, depending on the use context you might just be interested in the fact that a certain function doesn't change certain parts of the state. This can be a completely automatic proof where you don't even have to state the specification, because a tool can figure it out for you. But if you are only allowed to have precisely one specification per function, you can't make use of such simple automatic side proofs.
In the functional world, the first case is similar to a complex recursion that you may only want to go through once with a specific complex induction, strong induction hypothesis etc. You can be better off proving everything you'll ever need about that function in one go. The second case are the many simple, small functions that make up the bulk of the program. For these you want nice, clean simp and other rules to set up automation.
The point is, you should have the choice to do what fits best.
Cheers,
Gerwin
Email Gateway (Aug 19 2022 at 08:10):From: Lars Noschinski <noschinl@in.tum.de>
I guess, Simpl accounts for this case with the _modifies specifications?
-- Lars
Email Gateway (Aug 19 2022 at 08:10):From: Lars Noschinski <noschinl@in.tum.de>
It turns out that this is fairly easy to implement:
fun eqsubst_inst_tac ctxt occL insts thm =
Subgoal.FOCUS (fn {context=ctxt,...} => let
val thm' = thm |> Rule_Insts.read_instantiate ctxt insts
in EqSubst.eqsubst_tac ctxt occL [thm'] 1 end) ctxt
fun subst_method inst_tac tac =
Args.goal_spec --
Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
Scan.optional (Scan.lift
(Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!!
Args.name_source)) --|
Args.$$$ "in")) [] --
Attrib.thms >>
(fn (((quant, occL), insts), thms) => fn ctxt => METHOD (fn facts =>
if null insts then quant (Method.insert_tac facts THEN' tac ctxt
occL thms)
else
(case thms of
[thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt
occL insts thm)
| _ => error "Cannot have instantiations with multiple rules")));
val eqsubst_inst_meth = subst_method
eqsubst_inst_tac EqSubst.eqsubst_tac
So now I can do:
lemma (in mult3_impl) mult3:
"∀m n. Γ ⊢ ⦃´m = m ∧ ´n = n⦄ ´r :== PROC mult3(´m, ´n) ⦃´r = m * n⦄"
apply vcg_step
apply (subst_tac I="⦃ ´m = m ∧ ´m * n = ´r + ´m * ´n ⦄" in
annotate_named_loop[where name="''mult3_loop''"])
Email Gateway (Aug 19 2022 at 08:10):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Yes, Simpl does, and a few other frameworks have the same special case, because it occurs so often that it can't be ignored. There is nothing in between, though. If your memory model has separate heap framing conditions, you're already out of luck.
Simpl can easily be extended to allow the vcg to use an arbitrary lemma as spec for a function to get all that (not sure if we've pushed that change to the AFP yet -- we should). With that, there is only the problem of nice syntax for annotations left.
Cheers,
Gerwin
Email Gateway (Aug 19 2022 at 08:11):From: Lars Noschinski <noschinl@in.tum.de>
[...]
I've refined this now to a specialized tactic, so I can just write
apply (anno_loop_tac my_named_loop="{...}").
Now this aspect feels quite natural.
-- Lars
Email Gateway (Aug 19 2022 at 08:11):From: Gerwin Klein <gerwin.klein@nicta.com.au>
That does indeed look quite nice. Would you be happy to include your tactic in the AFP Simpl entry?
Gerwin
Last updated: Nov 21 2024 at 12:39 UTC