String rewrite system based definition of offset normalization #9
Conversation
| *) | ||
|
|
||
| (** | ||
| Another (incomplete) consistency proof for [PTRS], based on Krebbers' PhD thesis, and |
There was a problem hiding this comment.
You should revise this text.
| Require Import bedrock.lang.cpp.model.simple_pointers_utils. | ||
| Require Import bedrock.lang.cpp.model.inductive_pointers_utils. | ||
|
|
||
| From Equations Require Import Equations. |
There was a problem hiding this comment.
I think this should move up towards the top of the file since it is a Rocq library.
There was a problem hiding this comment.
Also, we generally seem to avoid From...Require
| Module PTRS_IMPL <: PTRS_INTF. | ||
| Import canonical_tu address_sums merge_elems. | ||
|
|
||
| Inductive raw_offset_seg : Set := |
There was a problem hiding this comment.
I propose adding a comment here or somewhere to outline the setup. Maybe we can put all of the non-canonical stuff in a module like:
Module raw_offset.
End raw_offset.
Definition offset := { o : raw_offset.t | raw_offset.is_canonical o }.And then hide most of the non-canonical stuff.
|
|
||
| From Equations Require Import Equations. | ||
|
|
||
| Axiom irr : ∀ (P : Prop) (p q : P), p = q. |
There was a problem hiding this comment.
Probably not ultimately necessary.
There was a problem hiding this comment.
Maybe not strictly necessary, but it does make it much easier to prove equality of offsets (since we don't have to prove equalities of proofs).
| Proof. solve_decision. Defined. | ||
| #[global] Declare Instance raw_offset_seg_countable : Countable raw_offset_seg. | ||
|
|
||
| Definition offset_seg : Set := raw_offset_seg * Z. |
There was a problem hiding this comment.
@Blaisorblade @ehatti I forget, what is the motivation for including the Z here? Can it be removed? It seems like it is always computed from the other component (given a genv) so maybe this naturally comes in at another layer.
There was a problem hiding this comment.
@ehatti I think this is the main technical comment, so I wanted to highlight it here.
| Module PTRS_IMPL <: PTRS_INTF. | ||
| Import canonical_tu address_sums merge_elems. | ||
|
|
||
| Inductive raw_offset_seg : Set := |
There was a problem hiding this comment.
| Inductive raw_offset_seg : Set := | |
| Variant raw_offset_seg : Set := |
| Lemma rw_bwd_r : | ||
| ∀ o1 o2 o2' o3, | ||
| roff_rw o2 o2' -> | ||
| roff_rw (o1 ++ o2) o3 -> | ||
| roff_rw (o1 ++ o2') o3. |
There was a problem hiding this comment.
This lemma vaguely looks like a Proper instance.
There was a problem hiding this comment.
It would be a Proper instance for the function composition fun o => roff_rw (o1 ++ o) o3 — this isn't really applicable. But roff_rw_cong can be a Proper instance, then rw_bwd_r would be proved by move => o1 o2 o2' o3 ->., and I'd suggest deleting it entirely and using rewrite at the call site.
There was a problem hiding this comment.
Sounds good, I'll go ahead and make it a Proper instance
| by destruct H3. | ||
| Qed. | ||
|
|
||
| Inductive root_ptr : Set := |
There was a problem hiding this comment.
| Inductive root_ptr : Set := | |
| Variant root_ptr : Set := |
| | offset_ptr (p : root_ptr) (o : offset). | ||
| Definition ptr := ptr_. | ||
|
|
||
| Program Definition __offset_ptr (p : ptr) (o : offset) : ptr := |
There was a problem hiding this comment.
| Program Definition __offset_ptr (p : ptr) (o : offset) : ptr := | |
| #[program] Definition __offset_ptr (p : ptr) (o : offset) : ptr := |
| | fun_ptr_ (tu : translation_unit_canon) (o : obj_name) | ||
| | alloc_ptr_ (a : alloc_id). | ||
|
|
||
| Inductive ptr_ : Set := |
There was a problem hiding this comment.
| Inductive ptr_ : Set := | |
| Variant ptr_ : Set := |
| Lemma roff_rw_cong : | ||
| ∀ ol1 ol2 or1 or2, | ||
| roff_rw ol1 or1 -> | ||
| roff_rw ol2 or2 -> | ||
| roff_rw (ol1 ++ ol2) (or1 ++ or2). |
There was a problem hiding this comment.
I think this should be roughly:
| Lemma roff_rw_cong : | |
| ∀ ol1 ol2 or1 or2, | |
| roff_rw ol1 or1 -> | |
| roff_rw ol2 or2 -> | |
| roff_rw (ol1 ++ ol2) (or1 ++ or2). | |
| #[global] Instance roff_rw_cong : | |
| Proper (roff_rw ==> roff_rw ==> roff_rw) (++). |
| roff_rw (o1 ++ o2) o3 -> | ||
| roff_rw (o1' ++ o2) o3. | ||
| Proof. | ||
| Admitted. |
There was a problem hiding this comment.
Best delete, like rw_bwd_r.
There was a problem hiding this comment.
These are actually needed, they essentially states that normalization is order-independent, which is a crucial property as it's what allows the proofs of the offset equalities to be very easy.
Redefines the definition of pointer offset normalization in this file as a string rewrite system. Current progress: The pointer equalities in the
PTRSinterface are all provable,vaddrandalloc_idaxioms have not been proven -- those are orthogonal to the definition of normalization however.roff_rw_localdefines the local rewrites, namely thato_baseando_derivedcancel out, that indexing the 0th element is a no-op, and that sequenceso_subs should be merged together.roff_rw_globallifts this to a rewrite relation on entire offsets, and finallyroff_rwtakes the closure of this to define the rewrite system.From there we define a function
normalize-- which is used to ensure the result of offset composition is still normalized -- and prove it is equivalent toroff_rw. I've proven that it is sound wrtroff_rw, but I still need to prove the opposite direction.I'm using the Equations library to get nicer well-founded recursion, since
Program Fixpointgenerates quite unworkable terms. Let me know if adding this extra dependency is a problem, if it is then we can switch to a different definition fornormalize.Equations is just nice because it "just works" and so makes it faster to get the idea into Coq.