Are you sure the problem is with fixpoints? Doesn’t the fixpoint get simplified away in your lemma os_access_tlbe_always_hit, leaving you with a sequence of if?
I imagine the goal looks like this:
H' : (if ... then (Some tlbe2) else
if ... then (Some tlbe1) else
if ... then (Some tlbe1) else None) = None
================================================
False
So you have to work through the conditions to find that at least one must be true.
You could simplify the current proof script a bit by removing the unfold find_tlbe in H' on line 295, but that won’t change the state you’re in (where the proof is Admitted).
As a general rule of thumb, never unfold fixpoints, and instead use destruct, induction or rewrite in order to get a constructor in the decreasing argument, and simplify by simpl/cbn. But in your case you already have a concrete argument.
I have removed the inappropriate using of unfold, and come to the following goal:
1 subgoals
ea : int
H : Int.le (Int.repr (to_Z “40000000”)) ea &&
Int.le ea (Int.repr (to_Z “4000FFFF”)) = true
H’ : (if (Int.eq (Int.repr 255) (Int.repr 255)
|| Int.eq (Int.repr 255) Int.zero) &&
Int.eq (Int.shru (Int.repr 1048576) (Int.repr 6))
(Int.and (Int.shru ea (Int.repr 16)) (Int.repr 65535))
then Some tlbe0
else None) = None
______________________________________(1/1)
False
H means that effective address (ea) in the range from 40000000 to 4000ffff, and the if statement in H’ is satisfied. I am realizing that I have used the fixpoint in a concrete case rather than a general one. Despite this , can I have a way to make this proof go on?
this would be easier to answer if you would give more information on where your “Int” module comes from. It looks quite like (https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v) but in the version I am using (3.5 and master) there is no le function. Without knowing what library you are using one cannot tell what facilities this library might have to solve such goals. Easiest (and most polite) is to supply a snippet of Coq code which can be run + information on versions you are using.
In case you are using something similar to the CompCert Integers library, a good way to do partial simplifications on constant terms is the change tactic, which can replace any terms which eventually compute to the same thing. cbn in H does nothing and compute in H probably doesn’t give you what you want. With change you get this far on a simplified goal (because I don’t have le):
Require Import compcert.lib.Integers.
Require Import ZArith.
Require Import Bool.
Goal
forall (tlbe0:int),
forall (ea:int),
(if (Int.eq (Int.repr 255) (Int.repr 255)
|| Int.eq (Int.repr 255) Int.zero) &&
Int.eq (Int.shru (Int.repr 1048576) (Int.repr 6))
(Int.and (Int.shru ea (Int.repr 16)) (Int.repr 65535))
then Some tlbe0
else None) = None
->
False.
Proof.
intros.
change (Int.eq (Int.repr 255) (Int.repr 255)) with true in H. cbn in H.
change (Int.shru (Int.repr 1048576) (Int.repr 6)) with (Int.repr 16384) in H.
results in
1 subgoal
tlbe0, ea : int
H : (if Int.eq (Int.repr 16384) (Int.and (Int.shru ea (Int.repr 16)) (Int.repr 65535))
then Some tlbe0
else None) = None
______________________________________(1/1)
False
I am not aware of any automated tool which can handle inequalities and bit operations, so I guess you have to see what Search Int.shru gives you. May be you can convert the shru to a division in Nat or Z and convert the goal with ring tactics to something lia can solve. But I would think this is a common thing for you, so I would prove some useful lemmas for this.
The “Int” module here comes from Compcert 2.7 except that I had an le function added.
Definition le (x y: int) : bool :=
if zle (signed x) (signed y) then true else false.
(I wonder why there’s no such a commonly used funtion, even in version 3.5).
I have uploaded the modified code to https://github.com/JulianXian/addr_trans/blob/master/Integers.v
and other files can be found here. https://github.com/JulianXian/addr_trans/
The code can run on coq 8.4pl6, a version without tactic cbn. It seems simpl do the same thing.
I’m trying to learn more tactics and prove techniques to make the coq model more accurate.
unless you want to do very minor experiments with an existing development, there is no justification I can think of for using Coq 8.4pl6 and CompCert 2.7. You will be pretty much on your own with this version pick.
If you need additional functions, it is better to have your own IntExt module you can share with others rather than changing CompCert. This makes it easier for others to help you. If you think your functions are generally useful, you should do a PR to CompCert.
I’m ready for upgrading to the latest version of Coq and Compcert.
In order to use original Compcert Intergers library, I change my goal to a tempopary goal
______________________________________(1/2)
Int.lt (Int.repr (to_Z “3fffffff”)) ea &&
Int.lt ea (Int.repr (to_Z “40010000”)) = true ->
Int.eq (Int.repr 16384)
(Int.and (Int.shru ea (Int.repr 16)) (Int.repr 65535)) = true
and a final goal like:
H1:P: Prop
H2: (if Q
then Some tlbe0
else None) == None
H3:P->Q
______________________________________(2/2)
False.
Excuse me, I have a question about referencing the compcert library.
“Require Import compcert.lib.Coqlib.”which is referenced in my coq file, but I get an error during compilation: Cannot find a physical path bound to logical path matching suffix compcert.lib.
How should I solve this problem?