Commit f3576fdc authored by William Mansky's avatar William Mansky

Added kvnode_prots_W to write_spec precondition.

Conceptually, it's part of the writer permission for the kvnode protocol.
parent b43c1414
......@@ -218,7 +218,7 @@ Lemma write_spec ain tid v vals
γ s s' t (E : coPset) (R : vProp)
(Le: s s') (*(HN : physN E) (HNl: persist_locN .@ n E)*):
{{{ ([ list] i seq 0 8, (ain >> (Z.of_nat i)) LitV (kvget i vals))
sGPS_iSP_Writer N kvnode_IP t s v γ
kvnode_prots_W (fst v) (snd v) sGPS_iSP_Writer N kvnode_IP t s v γ
<obj> (F γ t s v ={E}= F γ t s' vals R) }}}
write [ #n; #ain] in tid
{{{ t', RET #; (t < t')%positive sGPS_iSP_Writer N kvnode_IP t' s' vals γ R }}}.
......
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