wip(feature): Provide the means to work with diverging computations

_CoqProject

@@ -3,6 +3,7 @@
 -Q _build/default/theories/Core FreeSpec.Core
 -Q _build/default/theories/Exec FreeSpec.Exec
 -Q _build/default/theories/FFI FreeSpec.FFI
+-Q _build/default/theories/Contribs FreeSpec.Contribs
 -arg -init-file
 -arg build.v
 
@@ -66,6 +67,10 @@ _build/default/theories/FFI/ML.v
 _build/default/theories/Exec/Eval.v
 _build/default/theories/Exec/Exec.v
 
+_build/default/theories/Contribs/Raise.v
+_build/default/theories/Contribs/MFix.v
+_build/default/theories/Contribs/MFixFacts.v
+
 _build/default/examples/airlock.v
 _build/default/examples/smram.v
 _build/default/examples/heap.v

examples/dune

@@ -1,4 +1,4 @@
 (coq.theory
   (name FreeSpec.Example)
-  (theories FreeSpec.Core FreeSpec.FFI FreeSpec.Exec)
+  (theories FreeSpec.Core FreeSpec.FFI FreeSpec.Exec FreeSpec.Contribs)
   (flags -init-file build.v))

examples/loop.v

@@ -0,0 +1,76 @@
+(* This Source Code Form is subject to the terms of the Mozilla Public
+ * License, v. 2.0. If a copy of the MPL was not distributed with this
+ * file, You can obtain one at https://mozilla.org/MPL/2.0/. *)
+
+(* Copyright (C) 2021 Nomadic Labs *)
+
+From FreeSpec.Core Require Import Core CoreFacts.
+From FreeSpec.Contribs Require Import Raise MFix MFixFacts.
+
+Inductive PICK : interface :=
+| Pick (x : nat) : PICK unit.
+
+Definition pick `{Provide ix PICK} (x : nat) : impure ix unit :=
+  request (Pick x).
+
+Module const_call.
+  (* Our goal is to prove that [forever_pick x] only calls [Pick x]
+     and nothing else. *)
+  Definition forever_pick `{Provide2 ix PICK MFIX} (x : nat)
+    : impure ix False :=
+    mfix (fun rec x => pick x ;; rec x) x.
+
+  Inductive pick_caller_obligation (x : nat)
+    : unit -> forall (a : Type), PICK a -> Prop :=
+  | pick_caller : pick_caller_obligation x tt unit (Pick x).
+
+  Hint Constructors pick_caller_obligation : loop.
+
+  Definition pick_me (x : nat) : contract PICK unit :=
+    {| witness_update := fun _ _ _ _ => tt
+     ; caller_obligation := pick_caller_obligation x
+     ; callee_obligation := no_callee_obligation
+    |}.
+
+  Lemma forever_trustworthy `{StrictProvide3 ix PICK MFIX (RAISE nat)} (x : nat)
+    : pre (to_hoare (ix:=ix) (pick_me x) (forever_pick x)) tt.
+
+  Proof.
+    apply mfix_pre.
+    induction gas.
+    + prove impure.
+    + prove impure with loop.
+  Qed.
+End const_call.
+
+Module inc_call.
+  (* This time, we prove [forever_pick x] first calles [Pick x], then
+     [Pick (x+1)], and so forth. *)
+  Definition forever_pick `{Provide2 ix PICK MFIX} (x : nat)
+    : impure ix False :=
+    mfix (fun rec x => pick x ;; rec (x + 1)%nat) x.
+
+  Inductive pick_caller_obligation (x : nat)
+    : forall (a : Type), PICK a -> Prop :=
+  | pick_caller : pick_caller_obligation x unit (Pick x).
+
+  Hint Constructors pick_caller_obligation : loop.
+
+  Definition pick_me : contract PICK nat :=
+    {| witness_update := fun x _ _ _ => (x+1)%nat
+     ; caller_obligation := pick_caller_obligation
+     ; callee_obligation := no_callee_obligation
+    |}.
+
+  Lemma forever_trustworthy `{StrictProvide3 ix PICK MFIX (RAISE nat)} (x : nat)
+    : pre (to_hoare (ix:=ix) pick_me (forever_pick x)) x.
+
+  Proof.
+    apply mfix_pre.
+    intros gas.
+    revert x.
+    induction gas; intros x.
+    + prove impure.
+    + prove impure with loop.
+  Qed.
+End inc_call.

theories/Contribs/MFix.v

@@ -0,0 +1,155 @@
+(* This Source Code Form is subject to the terms of the Mozilla Public
+ * License, v. 2.0. If a copy of the MPL was not distributed with this
+ * file, You can obtain one at https://mozilla.org/MPL/2.0/. *)
+
+(* Copyright (C) 2021 Nomadic Labs *)
+
+From ExtLib Require Import MonadFix Monad.
+From FreeSpec.Core Require Import Impure.
+From FreeSpec.Contribs Require Import Raise.
+Import MonadLetNotation.
+
+(** Diverging computations are an open problem in FreeSpec since the
+    beginning, due to the use of an inductive datatype to define
+    [impure].  
+
+    Turning [impure] into a coinductive type could be achieved, but it
+    would mean [run_impure] would have to compute the trace of an
+    execution rather than its result.
+
+    Another approach is to consider the act of diverging is an effect
+    that we can encode as an effect.  Regardless of its feasability,
+    this approach has the nice benefit to force developers to “mark”
+    their diverging functions as such.
+
+    Diverging as an effect is not a novel idea.  It is usually encoded
+    by the [mfix] monadic operator, whose type is:
+
+<<
+mfix : ((t -> m u) -> t -> m u) -> t -> m u
+>>
+
+    In FreeSpec, [mfix] can be encoded as follows:
+  
+<<
+Inductive MFIX (i : interface) : interface :=
+| MFix {t u} (rec : (t -> impure i u) -> t -> impure i u) (x : t) : MFIX i u.
+  
+Arguments MFix [i t u].
+>>
+  
+    Here we see [MFIX] is not like the [interface] types we have
+    previously defined in FreeSpec, in that its primitive takes an
+    [impure] function as one of its arguments.  As a consequence,
+    [MFIX] needs to be parameterized by an interface itself, making it
+    a “higher-order interface.”
+  
+    This poses many challenges. For instance, how should we define
+    [mfix] (the helper to use [MFix])? 
+  
+    There most natural candidate is
+  
+<<
+  Definition mfix `{Provide ix (MFIX ix')} {u t}
+      (rec : (t -> impure ix' u) -> t -> impure ix' u) (x : t)
+    : impure ix u :=
+    request (MFix rec x).
+>>
+  
+    As far as we can tell as of now, does not “break” the reasoning
+    framework of FreeSpec… Meaning you should be able to use the
+    reasoning framework of FreeSpec.  Unfortunately, un practice it is
+    really counter-intuitive to use.
+  
+    Can you infer the behavior of the following program?
+  
+<<
+Definition inc_nth
+   `{Provide ix (MFIX ix'), Provide ix (STORE nat), Provide ix' (STORE nat)}
+    (n : nat)
+  : impure ix nat :=
+  put 0%nat;; (* (1) *)
+  mfix (fun rec _ =>
+          let* count := get in (* (2) *)
+          if (Nat.eqb count n)%nat
+          then local n
+          else put (count + 1)%nat;; rec tt) tt.
+>>
+  
+    Because [ix] and [ix'] are two separate interfaces, the effect of
+    [put 0] (see (1)) is not correlated to the effect of [get] (see
+    (2)).
+  
+    That is, we need [ix] and [ix'] to be the same interface, for the
+    effect of the [STORE] to be correlated.  We can specify it by
+    defining only one interface.
+  
+<<
+Definition inc_nth'
+   `{Provide ix (MFIX ix), Provide ix (STORE nat)}
+    (n : nat)
+  : impure ix nat :=
+  put 0%nat;; (* (1) *)
+  mfix (fun rec _ =>
+          let* count := get in (* (2) *)
+          if (Nat.eqb count n)%nat
+          then local n
+          else put (count + 1)%nat;; rec tt) tt.
+>>
+
+    There are many problems with this definition, though.  Firstly, we
+    are not sure such a [ix] exists, and we know better than to reason
+    with empty types.  Secondly, this breaks the main assumption upon
+    which FreeSpec reasoning framework is built: interfaces are
+    independent from each other.  A call of [STORE] primitives cannot
+    alter the semantics of [MFIX]… but somehow, a call to [MFix] can
+    alter the semantics of [STORE].  FreeSpec is not equiped to deal
+    with this setting.
+
+    Interfaces are a rendez-vous point for two software components.
+    Diverging is a local behavior, one which cannot be observed by
+    another.  As a consequence, implementing this effect as a
+    constructor of an interface feels forced.
+
+    However, we like the idea of marking a function to advertize its
+    potentially diverging behavior.  To that end, we introduce an
+    axiomatized [LOOP] interface. *)
+
+Axiom MFIX : interface.
+
+(** But this time, rather than defining [mfix] as a primitive, we
+    axiomatized it. *)
+
+Axiom mfix
+  : forall `{Provide ix MFIX} {t u},
+    ((t -> impure ix u) -> t -> impure ix u) -> t -> impure ix u.
+
+(*
+Instance MonadFix_impure `{Provide ix MFIX} : MonadFix (impure ix) :=
+  { mfix := @impure_mfix ix _ _ }.
+*)
+
+(** And we equip this axiomatized definition with an equation. *)
+
+Axiom mfix_equation
+  : forall `{Provide ix MFIX} {t u}
+           (rec : (t -> impure ix u) -> t -> impure ix u)
+           (x : t),
+    mfix rec x = rec (mfix rec) x.
+
+Definition repeat `{Provide ix MFIX} `(h : t -> impure ix (t + u)) (x : t)
+  : impure ix u :=
+  mfix (fun rec x => let* res := h x in
+                     match res with
+                     | inl x => rec x
+                     | inr x => ret x
+                     end) x.
+
+Fixpoint repeat_gas `{Provide ix MFix} `(h : t -> impure ix (t + u)) (x : t) (gas : nat)
+  : impure ix (option u) :=
+  let* res := h x in
+  match gas, res with
+  | _, inr x => ret (Some x)
+  | S n, inl x => repeat_gas h x n
+  | O, _ => ret None
+  end.

theories/Contribs/MFixFacts.v

@@ -0,0 +1,35 @@
+(* This Source Code Form is subject to the terms of the Mozilla Public
+ * License, v. 2.0. If a copy of the MPL was not distributed with this
+ * file, You can obtain one at https://mozilla.org/MPL/2.0/. *)
+
+(* Copyright (C) 2021 Nomadic Labs *)
+
+From FreeSpec.Core Require Import Core CoreFacts.
+From FreeSpec.Contribs Require Import Raise MFix.
+
+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 x
+  | S n => rec (mfix_with_gas rec n) x
+  end.
+
+(*
+Axiom mfix_pre
+  : forall `{MayProvide ix i, StrictProvide2 ix MFIX (RAISE t),
+             ! Distinguish ix (RAISE t) i, ! Distinguish ix MFIX i}
+           `(c : contract i Ω)
+           `(rec : (t -> impure ix u) -> t -> impure ix u) (ω : Ω) (x : t),
+    pre (to_hoare c (mfix rec x)) ω
+    <-> forall gas, pre (to_hoare c (mfix_with_gas rec gas x)) ω.
+
+Axiom mfix_post
+  : forall `{MayProvide ix i, StrictProvide2 ix MFIX (RAISE t),
+             ! Distinguish ix (RAISE t) i, ! Distinguish ix MFIX i}
+           `(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 ω'.
+*)

theories/Contribs/Raise.v

@@ -0,0 +1,42 @@
+(* This Source Code Form is subject to the terms of the Mozilla Public
+ * License, v. 2.0. If a copy of the MPL was not distributed with this
+ * file, You can obtain one at https://mozilla.org/MPL/2.0/. *)
+
+(* Copyright (C) 2021 Nomadic Labs *)
+
+From FreeSpec.Core Require Import Core.
+From FreeSpec.FFI Require Import FFI.
+From CoqFFI Require Import Interface.
+
+Class MonadRaise (α : Type) (m : Type -> Type) :=
+  { raise {β} : α -> m β }.
+
+Arguments raise [α m MonadRaise β] _.
+
+Inductive RAISE (α : Type) : interface :=
+| Raise {β} : α -> RAISE α β.
+
+Arguments Raise [α β] _.
+
+Definition inj_raise `{Inject (RAISE α) m} (β : Type) (x : α) : m β :=
+  inject (Raise x).
+
+Instance inj_Raise `{Inject (RAISE α) m} : MonadRaise α m :=
+  { raise := inj_raise }.
+
+Fixpoint with_abort `(p : impure (ix + RAISE β) α)
+  : impure ix (α + β) :=
+  match p with
+  | request_then (in_right (Raise x)) _ => local (inr x)
+  | request_then (in_left p) k => request_then p (fun x => with_abort (k x))
+  | local x => local (inl x)
+  end.
+
+Definition try_or `{Monad m, Inject (RAISE α) m} `(p : m (β + α))
+  : m β :=
+  let* x := p in
+  match x with
+  | inl x => ret x
+  | inr err => raise err
+  end.
+

theories/Contribs/dune

@@ -0,0 +1,5 @@
+(coq.theory
+  (package coq-freespec-contribs)
+  (name FreeSpec.Contribs)
+  (theories FreeSpec.Core FreeSpec.FFI)
+  (flags -init-file ../../build.v))