Commit 9d4b5fb1 authored by Ralf Jung's avatar Ralf Jung

make cas_offset_vec lemmas more consistent

parent 353f1c11
......@@ -586,10 +586,9 @@ Proof.
iNext. iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.
Lemma wp_cas_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v' v1 v2 :
vs !!! off = v'
val_for_compare v' = val_for_compare v1
vals_cas_compare_safe v' v1
Lemma wp_cas_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
val_for_compare (vs !!! off) = val_for_compare v1
vals_cas_compare_safe (vs !!! off) v1
{{{ l ↦∗ vs }}}
CAS #(l + off) v1 v2 @ s; E
{{{ RET #true; l ↦∗ vinsert off v2 vs }}}.
......
Markdown is supported
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