Email Gateway (Aug 19 2022 at 15:22): Email Gateway (Aug 19 2022 at 15:22):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Hello Isabelle users.
I've been putting a little time into updating the l4.verified proofs to
isabelle-2014 (partly because I wanted to know what fraction of the
problems would be caused by my hypsubst change). I've had a few problems
I will soon report on. The simplest problem to report involves the
simplifier.
I haven't been following closely, but I take it the simplifier is now a
bit more aggressive in figuring out how to instantiate assumptions. This
is probably a good thing, and has shrunk a few of the proofs in the
repository already.
The problem is that this new mechanism sometimes leads to divergence,
and I don't know how to turn it off. Here's an example I came across (or
see the attached theory):
theory Scratch imports Main begin
lemma foo:
"⋀a aa b ba ab bb bc.
pasDomainAbs initial_aag (cur_domain b)
∈ subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) ⟹
u = Partition a ⟹
s = ((aa, b), ba) ⟹
s' = ((ab, bb), bc) ⟹
states_equiv_for
(λx. pasObjectAbs initial_aag x ∈ subjectReads (pasPolicy
initial_aag) (OrdinaryLabel a))
(λx. pasIRQAbs initial_aag x ∈ subjectReads (pasPolicy
initial_aag) (OrdinaryLabel a))
(λx. pasASIDAbs initial_aag x ∈ subjectReads (pasPolicy
initial_aag) (OrdinaryLabel a))
(λx. pasDomainAbs initial_aag x ∈ subjectReads (pasPolicy
initial_aag) (OrdinaryLabel a))
(λx. ptr_range x 12) b bb ⟹
pasDomainAbs initial_aag (cur_domain b)
∈ subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) ⟶
cur_domain b = cur_domain bb ∧
globals_equiv b bb ∧
scheduler_action b = scheduler_action bb ∧
work_units_completed b = work_units_completed bb ∧
equiv_irq_state (machine_state b) (machine_state bb) ∧
(user_modes ba ⟶ aa = ab) ∧
ba = bc ∧ equiv_for (λx. pasObjectAbs initial_aag x = SilcLabel)
kheap b bb ⟹
pasDomainAbs initial_aag (cur_domain bb)
∈ subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) ⟶
cur_domain b = cur_domain bb ∧
globals_equiv b bb ∧
scheduler_action b = scheduler_action bb ∧
work_units_completed b = work_units_completed bb ∧
equiv_irq_state (machine_state b) (machine_state bb) ∧
(user_modes ba ⟶ aa = ab) ∧
ba = bc ∧ equiv_for (λx. pasObjectAbs initial_aag x = SilcLabel)
kheap b bb ⟹
(user_modes ba ⟶ aa = ab) ∧ ba = bc
"
This is just a copy of a goal that came up in a proof somewhere. I don't
know what any of this means either, and it turns out it doesn't matter.
The behaviour is the same in a scratch theory with none of the constants
defined.
This problem will cause "simp" or "(simp only: )" to loop. It will be
solved immediately by clarify or blast. It can be solved by metis if we
adjust the problem a little to ensure the type variables all have sorts.
The news file suggests that [[simp_legacy_precond]] might be relevant to
this issue, but it doesn't seem to change anything.
In detail, this problem is solved by simplifying the implication whose
premise is already known, i.e. apply (drule(1) mp). It happens the
script "apply (drule(1) mp, simp)" solves the goal.
This weakness of simp is quite frustrating. To generate the above goal,
I had to work around the possible simp divergence by simplifying in stages:
apply (simp add: uwr_def sameFor_def sameFor_subject_def)
apply clarify
apply (simp(no_asm_use))
apply clarify
I'm willing to accept the argument that this is not a bug but rather a
tradeoff, with the default behaviour now being to solve more problems
but sometimes time out more often. However I'd really like a way to turn
this off. I've already had to dance around the problem in a couple of
places, and it seems to be a generally unpleasant experience. My usual
workarounds (simp only: ) and (simp(no_asm_use)) can't help me here.
I attach my scratch theory with this problem.
I hope there's a simple fix.
Cheers,
Thomas.
Scratch.thy
Email Gateway (Aug 19 2022 at 15:22):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Thomas,
I just tried your file with Isabelle2013-2 and simp looped. This corroborates
your experience that [[simp_legacy_precond]] doesn't do anything, because the
divergence is not related to it. In any case, the only simplifier change I am
aware of relates to the handling of conjunctions in the premises of conditional
rewrite rules, and [[simp_legacy_precond]] switches that off.
Tobias
Email Gateway (Aug 19 2022 at 15:23):From: Thomas Sewell <thomas.sewell@nicta.com.au>
It's been pointed out to me that this particular behaviour of the
simplifier predates Isabelle2014.
Apologies to everyone. I assumed that the extracted example was
representative because it also caused the simplifier to loop. Instead it
looks like the context somehow previously allowed the simplifier not to
loop, and this has changed. I will have to investigate further.
Apologies once again,
Thomas.
Email Gateway (Aug 19 2022 at 15:23):From: Thomas Sewell <thomas.sewell@nicta.com.au>
The mystery deepens. This problem is somehow my fault.
It is the presence of the three completely redundant equalities "u =
Partition a" "s = ((aa, b), ba)" "s' = ((ab, bb), bc)" which causes the
simplifier to loop. These have been preserved by the hypothesis
substitution change.
In either case, the simplifier initially loops on the assumption it has
"pasDomainAbs initial_aag (cur_domain b)
∈ subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) ⟶
cur_domain b = cur_domain bb"
But in the old world, the simplifier goes down the rabbit hole - up to a
recursive depth of 100 - then realises it is stuck, gives up, and solves
the problem instead.
In the new world, the simplifier does the same things. But once it has
done that, it starts thinking about the preserved subgoal containing
"aa" which provides a use for one of the conditional rewrites "aa = ab"
floating around. Somehow the simplifier has multiple options now, so
instead of running to a depth of 100 and then giving up and coming back,
it starts backtracking different approaches, and will never finish.
In hindsight this all makes sense, and is entirely my problem. I hope
noone else has to deal with anything this awful as a result of this change.
Thanks to everyone for listening to me talk to myself about simplifier
mysteries.
Cheers,
Thomas.
Email Gateway (Aug 19 2022 at 15:26):From: Makarius <makarius@sketis.net>
This thread seems to be resolved for now. I just want to make sure that
there is nothing left to reconsider for the Isabelle2014 release, which
will be shipped next week.
Some months ago there was a similar surprise about simplifier depth limit
concerning simprocs. See the subject line "Product_Type.split_beta fails"
in October 2013 with the conclusion here:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-February/msg00056.html
The changeset mentioned there is:
changeset: 55375:d79c057c68f0
user: wenzelm
date: Mon Feb 10 13:04:08 2014 +0100
files: src/Pure/raw_simplifier.ML
description:
more elementary put_simpset: exchange the simplifier configuration
outright, which is particularly relevant concerning cumulative depth, e.g.
for Product_Type.split_beta in the subsequent example:
lemma "P (\<lambda>s. (case s of (x, y) \<Rightarrow> c))"
using [[simp_depth_limit = 1]]
apply simp
oops
It falls in the interval between the last release Isabelle2013-2 and the
emerging one Isabelle2014. Thus it might be relevant concerning potential
regressions of Simplifier behaviour due to a change that was meant to
improve the situation.
Makarius
Last updated: Apr 26 2024 at 12:28 UTC