Add [mfix_post] axiom

theories/Contribs/MFixFacts.v

@@ -5,17 +5,23 @@ From FreeSpec.Contribs Require Import Raise MFix.
 [((t -> impure ix u) -> t -> impure ix u) -> t -> impure ix u]
 *)
 
-Fixpoint mfix_with_gas `{Provide2 ix MFIX (RAISE w)}
-   `(rec : (t -> impure ix u) -> t -> impure ix u) (gas : nat)
-    (err : w) (x : t)
+Fixpoint mfix_with_gas `{Provide2 ix MFIX (RAISE t)}
+   `(rec : (t -> impure ix u) -> t -> impure ix u) (gas : nat) (x : t)
   : impure ix u :=
   match gas with
-  | O => raise err
-  | S n => rec (mfix_with_gas rec n err) x
+  | O => raise x
+  | S n => rec (mfix_with_gas rec n) x
   end.
 
 Axiom mfix_pre
-  : forall `{MayProvide ix i, Provide2 ix MFIX (RAISE w)} `(c : contract i Ω)
+  : forall `{MayProvide ix i, Provide2 ix MFIX (RAISE t)} `(c : contract i Ω)
            `(rec : (t -> impure ix u) -> t -> impure ix u) (ω : Ω) (x : t),
     pre (to_hoare c (mfix rec x)) ω
-    <-> forall gas err, pre (to_hoare c (mfix_with_gas rec gas err x)) ω.
+    <-> forall gas, pre (to_hoare c (mfix_with_gas rec gas x)) ω.
+
+Axiom mfix_post
+  : forall `{MayProvide ix i, Provide2 ix MFIX (RAISE t)} `(c : contract i Ω)
+           `(rec : (t -> impure ix u) -> t -> impure ix u) (ω ω' : Ω)
+            (x : t) (r : u),
+    post (to_hoare c (mfix rec x)) ω r ω'
+    <-> exists gas, post (to_hoare c (mfix_with_gas rec gas x)) ω r ω'.