Commit fcd36ce1 authored by Ralf Jung's avatar Ralf Jung
Browse files

minor tweaks

parent 09b43741
...@@ -153,7 +153,8 @@ read and written. Also notice that the sets of boxed and unboxed values are ...@@ -153,7 +153,8 @@ read and written. Also notice that the sets of boxed and unboxed values are
disjoint. *) disjoint. *)
Definition lit_is_unboxed (l: base_lit) : Prop := Definition lit_is_unboxed (l: base_lit) : Prop :=
match l with match l with
(* disallow comparing (erased) prophecies with (erased) prophecies, by considering them boxed *) (** Disallow comparing (erased) prophecies with (erased) prophecies, by
considering them boxed. *)
| LitProphecy _ | LitErased => False | LitProphecy _ | LitErased => False
| _ => True | _ => True
end. end.
......
...@@ -593,7 +593,7 @@ Proof. ...@@ -593,7 +593,7 @@ Proof.
Qed. Qed.
Lemma wp_load_offset_vec s E l sz (off : fin sz) (vs : vec val sz) : Lemma wp_load_offset_vec s E l sz (off : fin sz) (vs : vec val sz) :
{{{ l ↦∗ vs }}} ! #(l + off) @ s; E {{{ RET (vs !!! off); l ↦∗ vs }}}. {{{ l ↦∗ vs }}} ! #(l + off) @ s; E {{{ RET vs !!! off; l ↦∗ vs }}}.
Proof. apply wp_load_offset. by apply vlookup_lookup. Qed. Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
Lemma wp_store_offset s E l off vs v : Lemma wp_store_offset s E l off vs v :
...@@ -628,7 +628,7 @@ Proof. ...@@ -628,7 +628,7 @@ Proof.
Qed. Qed.
Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 : Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
(vs !!! off) = v1 vs !!! off = v1
vals_compare_safe (vs !!! off) v1 vals_compare_safe (vs !!! off) v1
{{{ l ↦∗ vs }}} {{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E CmpXchg #(l + off) v1 v2 @ s; E
...@@ -655,7 +655,7 @@ Proof. ...@@ -655,7 +655,7 @@ Proof.
Qed. Qed.
Lemma wp_cmpxchg_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 : Lemma wp_cmpxchg_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
(vs !!! off) v1 vs !!! off v1
vals_compare_safe (vs !!! off) v1 vals_compare_safe (vs !!! off) v1
{{{ l ↦∗ vs }}} {{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E CmpXchg #(l + off) v1 v2 @ s; E
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment