csgordon

Setting up MSR's F* Compiler on Windows, for use under Cygwin.

• Download the F* distribution from this page: http://research.microsoft.com/en-us/projects/fstar/
• Install F# (whichever version is appropriate) (I installed F#3.0, but suspect F* is built against 2.0)
• Install F# Powerpack version 2.0 (not the latest version, but this is required; also called FS Powerpack for F# 2.0) from: http://fsharppowerpack.codeplex.com/releases
• Install the F# 2.0 (VS 2010) redistributable runtime from: http://www.microsoft.com/en-us/download/details.aspx?id=13450
• Download the z3 distribution from: http://z3.codeplex.com/releases
• Install Cygwin, if not already done. Make sure make is installed.
• Unpack the F* and z3 distributions.
• Add the F# compiler, runtime, and F# Powerpack bin directories to your Cygwin PATH. I added the following to my .bashrc:

csgordon

Installing F# on Debian

In theory you should be able to install the mono-devel package from Debian, then grab the latest checkout of F#'s Github repository and build. Unfortunately, the most recent versions of Debian's (and Ubuntu's) mono-devel package (3.0.6) include a lovely bug that breaks the F# build (https://bugzilla.xamarin.com/show_bug.cgi?id=10884). Another alternative is installing Debian Sid (unstable branch), where there are currently working F# packages, but installing a whole system from unstable has the sorts of stability issues you might expect, and cherry-picking the right .deb packages from the Debian repositories is unpleasant. There's also the option of using an F# developer's personal repository (https://gist.github.com/tkellogg/5619461), but I don't like adding untrusted sources to my sources.list.

After discovering that Vagrant includes support for a version of Debian Wheezy with F#, I figured out a working, relatively uninvasive approach based on the package

csgordon

open import Data.Nat
open import Data.Fin

module StrictlyPositive where

  -- The following datatype is accepted by Agda, but rejected
  -- by Coq
  data Ty : Set0 -> Set0 where
    c1 : Ty ℕ
    c2 : Ty (Ty ℕ)

csgordon

open import Data.Nat
open import Data.Fin
open import Level
open import Relation.Binary.PropositionalEquality

module LF where

  {- Semantic model primitives -}
  Rℕ : {C : ℕ -> Set} -> (x : ℕ) -> C ℕ.zero -> ((n : ℕ) -> C n -> C (ℕ.suc n)) -> C x
  Rℕ ℕ.zero z s = z

csgordon

data T : Type -> Type where
  c1 : T Nat
  c2 : T (T Nat)

ElimT : (A : Type) -> T A -> A
ElimT _ c1 = 3
ElimT _ c2 = c1

csgordon

Keybase proof

I hereby claim:

• I am csgordon on github.
• I am csgordon (https://keybase.io/csgordon) on keybase.
• I have a public key whose fingerprint is 31DF C618 06FE DE8D D007 7571 5A37 6FB7 4F95 CA41

To claim this, I am signing this object:

csgordon

TeX log appears below

[verbose]: Creating arXiv submission AutoTeX object
[verbose]: *** Using TeX Live 2016 ***
[verbose]: Calling arXiv submission AutoTeX process
[verbose]: TeX/AutoTeX.pm: admin_timeout = minion
[verbose]: <acmart.cls>	is of type 'TeX auxiliary'.
[verbose]: <journalarxiv.bbl>	is of type 'TeX auxiliary'.
[verbose]: <journalarxiv.tex>	is of type 'LATEX2e'.
[verbose]: ~~~~~~~~~~~ Processing file 'journalarxiv.tex'

csgordon

Require Import Utf8.
Require Import Program.
Require Import Arith.
Require Import Ensembles.
Require Import Setoid.
Require Import Relations.
Require Import Morphisms.
Require Import Coq.Classes.Equivalence.

Polymorphic Definition binop (E:Type) := E -> E -> E.

csgordon

module ActorCore {
    class {:extern} ActorRef<Ms> {}
    predicate {:extern} at<T,Ms>(i: ActorRef<Ms>, p:(T ~> bool))
    /* at[i](_) is a modality */
    lemma atImpl<T,M>(c:ActorRef<M>, P:T~>bool, Q:T~>bool)
        requires forall x:T :: P.requires(x) ==> Q.requires(x)
        requires forall x:T :: P.requires(x) ==> P(x) ==> Q(x)
        ensures at(c, P) ==> at(c, Q)
    /* When using the above, Dafny sometimes doesn't notice the precondition holds;
    this variant forces it to look for it. */

csgordon

/*
 * Sample code for the AGERE 2019 paper "Modal Assertions for Actor Correctness" by Colin S. Gordon, DOI 10.1145/3358499.3361221.
  * Note that at the time of this writing, there is an issue (https://github.com/dafny-lang/dafny/issues/359) where this file only verifies from the command line (modulo complains about missing implementations of abstract methods).  Currently, verifying this via the Dafny Visual Studio Code plugin runs into trouble with the higher-order predicates.

 * Last checked with a local build of Dafny commit 8f141e9d05b2dba9de4ba997040df6166c2d168c and Boogie commit bc49937e7ee88e931bbe2dbf779a42612731a8fd
 */

module ActorCore {
    class {:extern} ActorRef<Ms> {}
    predicate {:extern} at<T,Ms>(i: ActorRef<Ms>, p:(T ~> bool))