Require spawn and terminate covariance

Author: k32

theories/Handlers/Mailbox.v

@@ -122,6 +122,8 @@ Section defn.
       h_handler _ req := mailbox_step req;
       h_initial := new;
       h_spawn pid mb_t := put pid {| mb_t := mb_t; mb_q := empty |};
+      h_spawn_covariance pid mb_t s s' H := ltac:(now rewrite H);
       h_terminate pid := delete pid;
+      h_terminate_covariance pid s s' H := ltac:(now rewrite H);
     |}.
 End defn.

theories/Handlers/Storage.v

@@ -77,7 +77,9 @@ Section storage_handler.
       h_handler _ req := storage_mfun req;
       h_initial := stor.new;
       h_spawn _ _ := id;
+      h_spawn_covariance _ _ _ _ H := H;
       h_terminate _ := id;
+      h_terminate_covariance _ _ _ H := H;
     |}.
 End storage_handler.
 

theories/IOHandler.v

@@ -17,14 +17,21 @@ Section IOHandler.
   Definition MFunRet Ret State `{HRet : Setoid Ret} `{HState : Setoid State} :=
     @MFun State (Ret * State) HState (@pair_setoid _ _ HRet HState).
 
+
   Class IOHandler := {
       h_state : Type;
       h_setoid : Setoid h_state;
       h_handler (pid : Ref) (req : Request) : MFunRet (Reply req) h_state;
       h_initial : h_state;
 
       h_spawn (pid : Ref) (mailbox_t : Set) : h_state -> h_state;
+      h_spawn_covariance : forall pid mailbox_t s s',
+        s == s' ->
+        h_spawn pid mailbox_t s == h_spawn pid mailbox_t s';
       h_terminate (pid : Ref) : h_state -> h_state;
+      h_terminate_covariance : forall pid s s',
+        s == s' ->
+        h_terminate pid s == h_terminate pid s';
     }.
 End IOHandler.