Fupd in idempotent core spec can't have rpcRequestInvN in namespace

mit-pdos · Jan 21, 2021 · e7e9247 · e7e9247
1 parent 190f7c9
commit e7e9247
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/src/program_proof/lockservice/kv_durable.v b/src/program_proof/lockservice/kv_durable.v
@@ -93,7 +93,7 @@ Lemma wpc_put_core γ (srv:loc) args kvserver :
             KVServer_core_own_vol srv kvserver' ∗
             □ (P' -∗ Put_Pre γ args) ∗
             (* TODO: putting this here because need to be discretizable *)
-            □ (▷ P' -∗ KVServer_core_own_ghost γ kvserver ={⊤}=∗ Put_Post γ args r ∗ KVServer_core_own_ghost γ kvserver')
+            □ (▷ P' -∗ KVServer_core_own_ghost γ kvserver ={⊤∖↑rpcRequestInvN}=∗ Put_Post γ args r ∗ KVServer_core_own_ghost γ kvserver')
 }}}
 {{{
      Put_Pre γ args

diff --git a/src/program_proof/lockservice/rpc.v b/src/program_proof/lockservice/rpc.v
@@ -437,7 +437,7 @@ Lemma server_executes_durable_request' (req:RPCRequest) reply γrpc γreq PreCon
   RPCServer_own_processing γrpc req lastSeqM lastReplyM -∗
   own γreq.(pre) (Excl()) -∗
   SP -∗ (* strengthened precond *)
-  (▷ SP -∗ ctx ==∗ PostCond req.(Req_Args) reply ∗ ctx') -∗
+  (▷ SP -∗ ctx ={⊤ ∖ ↑rpcRequestInvN}=∗ PostCond req.(Req_Args) reply ∗ ctx') -∗
   ctx ={⊤}=∗
   (RPCReplyReceipt γrpc req reply ∗
   RPCServer_own γrpc (<[req.(Req_CID):=req.(Req_Seq)]> lastSeqM) (<[req.(Req_CID):=reply]> lastReplyM) ∗

diff --git a/src/program_proof/lockservice/rpc_durable_proof.v b/src/program_proof/lockservice/rpc_durable_proof.v
@@ -233,7 +233,7 @@ Lemma RPCServer__HandleRequest_is_rpcHandler γrpc :
             core_own_vol server' ∗
             □ (P' -∗ PreCond args) ∗
             (* TODO: putting this here because need to be discretizable *)
-            □ (▷ P' -∗ core_own_ghost server ={⊤}=∗ PostCond args r ∗ core_own_ghost server')
+            □ (▷ P' -∗ core_own_ghost server ={⊤∖↑rpcRequestInvN}=∗ PostCond args r ∗ core_own_ghost server')
  }}}
  {{{
       (PreCond args)