Top.SystemC.Examples

The source of this file can be found on Github.

Examples

This file contains some worked examples in Coq for System C.

As System C is concerned with tracking effectful computation, represented by a block type, we define a base block type S0 that is used to represent some ambient, global effectful operation perhaps for performing I/O.

In System C, we could define S0 using the following:

interface S0 {
  def doSomething(): Int
}

Parameter S0 : btyp.
Parameter S0Wf : wf_btyp empty S0.
Parameter S0Type : btype S0.

Identity on blocks

Here is an example of a function which takes a block argument f of type S0 and boxes it. In System C, we could define this using the following:

def id {f : S0} {
  box f
}

Definition id : blk :=
  blk_babs S0 (stm_ret (exp_box (cset_bvar 0) (blk_bvar 0))).

Naturally, it would have the type {f : S0} => S0 at {f}. You can see this by hovering over id_typ in the following code block.

def show_typ() { val id_typ = id; () }

Definition id_typ : btyp :=
  typ_bfun S0 (typ_capt S0 (cset_bvar 0)).


Lemma id_typing : empty @ {}C ; nil |-blk id ~: id_typ.

Effectful Handlers

Next, we model a simple try-catch expression which simply returns a value. This, written in our language, looks like:

def try_return_immediate() {
  try {
    0
  } with cap : S0 {
    def doSomething() {
      1
    }
  }
}

As our formalism in Coq lacks integers (and other expression values), we model our expressions and expression values in Coq using a base expression type typ_base and a singular inhabitant of that type, namely exp_const.

Definition try_return_immediate_typ :=
  typ_base.
Definition try_return_param_type :=
  typ_base.
Definition try_return_immediate :=
  stm_try {}C try_return_param_type try_return_immediate_typ
     (stm_ret exp_const) (* 0 *)
     (stm_ret exp_const) (* 1 *).

As expected, that try statement returns an Int (in our formalism, a typ_base).

Lemma try_return_immediate_typing : empty @ {}C ; nil |-stm try_return_immediate ~: try_return_immediate_typ.

And naturally, reduces to 0 (exp_const) as the effect is never invoked. As an aside, we assume the existance of three unique, fresh labels, which are used by our reduction semantics to uniquely identify frames on the stack.

Parameter l1 l2 l3 : label.
Axiom l1l2 : l1 ≠ l2.
Axiom l1l3 : l1 ≠ l3.
Axiom l2l3 : l2 ≠ l3.

Now, the try expression then reduces to returning a value directly out of a handler frame.

Lemma try_return_immediate_s1 :
  〈 try_return_immediate | top | nil 〉-->
  〈 (stm_ret exp_const) (* 0 *) |
     (H l1 {}C (stm_ret exp_const) (* 1 *)) :: top |
     (l1, bind_sig try_return_param_type try_return_immediate_typ) :: nil 〉.

...which, by our reduction rules, eliminates the handler frame from the top of the stack.

Lemma try_return_immediate_s2 : ∀ Q,
  〈 (stm_ret exp_const) (* 0 *) | (H l1 {}C (stm_ret exp_const) (* 1 *)) :: top | Q 〉-->
  〈 (stm_ret exp_const) (* 0 *) | top | Q 〉.

Invoking a handler

Similarly, next we model a try statement which actually throws something. In System C, this can be expressed using the following fragment:

def try_return_throw() {
  try {
    cap.doSomething()
  } with cap : S0 {
    def doSomething() {
      0
    }
  }
}

Definition try_return_throw_typ :=
  typ_base.
Definition try_return_throw_param_typ :=
  typ_base.
Definition try_return_throw :=
  stm_try {}C try_return_throw_param_typ try_return_throw_typ
  (stm_perform (blk_bvar 0) exp_const (* () *))
  (stm_ret exp_const (* 0 *)).

Naturally, it still returns an Int/typ_base though.

Lemma try_return_throw_typing : empty @ {}C ; nil |-stm try_return_throw ~: try_return_throw_typ.

The reduction steps for this expression are a bit more complicated. First, a throw statement is reduced in the presence of a matching handler, which shifts evaluation to that handler and unwinds from there.

Lemma try_return_throw_s1 :
  〈 try_return_throw | top | nil 〉-->
  〈 (stm_perform (blk_handler l1) exp_const (* () *)) |
     (H l1 {}C (stm_ret exp_const (* 0 *))) :: top |
     [(l1, bind_sig try_return_throw_param_typ try_return_throw_typ)] 〉.

Lemma try_return_throw_s2 : ∀ Q,
  〈 (stm_perform (blk_handler l1) exp_const (* () *)) | (H l1 {}C (stm_ret exp_const (* 0 *))) :: top | Q 〉-->
  〈throw l1 # exp_const (* () *) | (H l1 {}C (stm_ret exp_const (* 0 *))) :: top • top | Q〉.

Lemma try_return_throw_s3 :
  〈throw l1 # exp_const (* () *) | (H l1 {}C (stm_ret exp_const (* 0 *))) :: top • top |
     [(l1, bind_sig try_return_throw_param_typ try_return_throw_typ)]〉-->
  〈 (stm_ret exp_const (* 0 *)) | top | [(l1, bind_sig try_return_throw_param_typ try_return_throw_typ)] 〉 .

Invoking a handler, redux

This example is a little more complicated. Here, we throw while evaluating a value-binder under the handler block.

def try_apply_throw() {
  try {
    val x = cap.doSomething();
    x
  } with cap : S0 {
    def doSomething() {
      1
    }
  }
}

Definition try_apply_throw_param_typ := typ_base.
Definition try_apply_throw_typ := typ_base.
Definition try_apply_throw :=
  stm_try {}C try_apply_throw_param_typ try_apply_throw_typ
    (stm_val typ_base
      (stm_perform (blk_bvar 0) exp_const (* () *))
      (stm_ret (exp_bvar 0) (* x *)))
    (stm_ret (exp_const) (* 1 *)).

Naturally, it returns an Int/typ_base again.

Lemma try_apply_throw_typing :
  empty @ {}C ; nil |-stm try_apply_throw ~: try_apply_throw_typ.

The reduction steps for this statement are a little more complicated. First, as before, we shift the try statement onto the stack as a handler frame.

Lemma try_apply_throw_s1 :
  〈 try_apply_throw | top | nil 〉-->
  〈 (stm_val typ_base
      (stm_perform (blk_handler l1) exp_const (* () *))
      (stm_ret (exp_bvar 0) (* x *)))
    | (H l1 {}C (stm_ret exp_const (* 1 *))) :: top
    | [(l1, bind_sig try_apply_throw_param_typ try_apply_throw_typ)]
   〉.

Next, we mark that we are evaluating a binding with a K frame.

Lemma try_apply_throw_s2 :
  〈 (stm_val typ_base (stm_perform (blk_handler l1) exp_const (* () *)) (stm_ret (exp_bvar 0) (* x *)))
    | (H l1 {}C (stm_ret exp_const (* 1 *))) :: top
    | [(l1, bind_sig try_apply_throw_param_typ try_apply_throw_typ)]
  〉-->
  〈 (stm_perform (blk_handler l1) exp_const (* () *))
    | (K typ_base (stm_ret (exp_bvar 0) (* x *))) :: ((H l1 {}C (stm_ret exp_const (* 1 *))) :: top)
    | [(l1, bind_sig try_apply_throw_param_typ try_apply_throw_typ)]
  〉.

We throw in the presence of a K frame and a matching H (handler) frame, which causes the K frame to be unwound...

Lemma try_apply_throw_s3 :
  〈 (stm_perform (blk_handler l1) exp_const (* () *))
    | (K typ_base (stm_ret (exp_bvar 0) (* x *))) :: ((H l1 {}C (stm_ret exp_const (* 1 *))) :: top)
    | [(l1, bind_sig try_apply_throw_param_typ try_apply_throw_typ)]
  〉-->
  〈throw l1 # exp_const (* () *)
    | (K typ_base (stm_ret (exp_bvar 0) (* x *))) :: ((H l1 {}C (stm_ret exp_const (* 1 *))) :: top)
    • top
    | [(l1, bind_sig try_apply_throw_param_typ try_apply_throw_typ)]
  〉.

We unwind the stack, building the resumption continuation as we go, denoted by • ...

Lemma try_apply_throw_s4 :
  〈throw l1 # exp_const (* () *)
    | (K typ_base (stm_ret (exp_bvar 0) (* x *))) :: ((H l1 {}C (stm_ret exp_const (* 1 *))) :: top)
    • top
    | [(l1, bind_sig try_apply_throw_param_typ try_apply_throw_typ)]
  〉-->
  〈throw l1 # exp_const (* () *)
    | ((H l1 {}C (stm_ret exp_const (* 1 *))) :: top)
    • (K typ_base (stm_ret (exp_bvar 0) (* x *))) :: top
    | [(l1, bind_sig try_apply_throw_param_typ try_apply_throw_typ)]
  〉.

... and when we get to the matching H frame, we shift it off to evaluate the corresponding handler.

Lemma try_apply_throw_s5 :
  〈throw l1 # exp_const (* () *)
    | ((H l1 {}C (stm_ret exp_const (* 1 *))) :: top)
    • (K typ_base (stm_ret (exp_bvar 0) (* x *))) :: top
    | [(l1, bind_sig try_apply_throw_param_typ try_apply_throw_typ)]
  〉-->
  〈 (stm_ret exp_const (* 1 *))
    | top
    | [(l1, bind_sig try_apply_throw_param_typ try_apply_throw_typ)]
  〉.

Capability threading

Here is a more complicated example, which threads and returns a capability through try/handle frames.

def cap_return() {
  try {
    interface S1 {
      def doSomethingElse(): Unit => Int at {cap}
    }

    val thunk = 
      try {
        def f() {
          cap.doSomething()
        }
        f
      } with cap2 : S1 {
        def doSomethingElse() {
          def g() {
            0
          }
          box {cap} g
        }
      };
    thunk()
  } with cap : S0 {
    def doSomething() {
      0
    }
  }
}

Definition cap_return_tm :=
  (* try { ... *)
  (stm_try {}C typ_base typ_base
          (* val thunk = ... *)
          (stm_val (typ_capt (typ_vfun typ_base typ_base) (cset_bvar 0))
                    (* try { ... *)
                    (stm_try (cset_bvar 0) typ_base typ_base
                             (* def f() { ... *)
                             (stm_def (cset_bvar 1) (typ_vfun typ_base typ_base)
                                      (* cap.doSomething() *)
                                      (blk_vabs typ_base (stm_perform (blk_bvar 1) exp_const))
                             (*} f *)
                                      (stm_ret (exp_box (cset_bvar 2)
                                                        (blk_bvar 0))))
                    (*} with cap2 : S1 { *)
                             (stm_ret (exp_box (cset_bvar 1)
                                               (blk_vabs typ_base (stm_ret exp_const)))))
                    (*}; thunk() *)
                    (stm_vapp (blk_unbox (exp_bvar 0)) exp_const))
  (*} with cap : S0 { ... *)
           (stm_ret exp_const)).
  (*}*)

Naturally, it is also well-typed.

Lemma cap_return_typing0 : ∃ T,
  (styping nil {}C nil
           cap_return_tm
           T).

Desugaring block definitions

Definitions can be desugared at some cost into block applications and boxes. Note that we insert an unbox to work around System C's automatic box inferencing.

def using_def {c : S0} {
  def C() {
    c.doSomething();
    0
  }
  // body here...
  0
}

def sugar_def {c : S0} {
  (unbox {(C : () => Int at {c}) => 
    // body here
    0})
  (box {() => c.doSomething(); 0})
}

Definition sugar_def (C : cap) (S1 : btyp) (b : blk) (s : stm) : stm :=
  (stm_vapp (blk_vabs (typ_capt S1 C) s) (exp_box C b)).

Definition sugar_var (x : atom) : blk :=
    (blk_unbox (exp_fvar x)).

Lemma sugar_def_typing : ∀ L E R b s (C : cap) Q S1 T2,
  R |= C →
  wf_cap E C →
  wf_cap E R →
  E @ C ; Q |-blk b ~: S1 →
  (∀ x : atom, x `notin` L →
    ([(x, bind_val (typ_capt S1 C))] ++ E) @ R ; Q |-stm (open_es s x) ~: T2) →
  E @ R ; Q |-stm (sugar_def C S1 b s) ~: T2.

Lemma sugar_var_typing : ∀ E R f S1 C,
  wf_env E →
  wf_cap E R →
  R |= C →
  binds f (bind_val (typ_capt S1 C)) E →
  E @ R ; nil |-blk (sugar_var f) ~: S1.

Local Mutable State

Finally, we formalize an example which models local, bounded mutable state.

interface ExampleCounter {
  def tick() : Int
}

def handleTick {prog : {() => Int} => Int} : Int {
  val stateFun = try {
    val res = prog {() => counter.tick()};
    box { prog } {(s : Int) => res}
  } with counter : ExampleCounter {
    def tick() {
      box { prog } {(s : Int) => (unbox resume(s))(s + 1)}
    }
  };
  (unbox stateFun)(0)
}

Definition handle_tick_term :=
  blk_babs (typ_bfun (typ_eff typ_base typ_base) typ_base)
    (stm_val
      (typ_capt (typ_vfun typ_base typ_base) (cset_bvar 0))
      (stm_try (cset_bvar 0) typ_base typ_base
        (stm_val typ_base (stm_bapp (blk_bvar 1) (cset_bvar 0) (blk_bvar 0))
          (stm_ret (exp_box (cset_bvar 1) (blk_vabs typ_base (stm_ret (exp_bvar 1))))))
        (stm_val
          (typ_capt (typ_vfun typ_base typ_base) (cset_bvar 1))
          (stm_vapp (blk_bvar 0) (exp_bvar 0))
          (stm_ret
            (exp_box (cset_bvar 1)
              (blk_vabs typ_base (stm_vapp (blk_unbox (exp_bvar 1))
                (exp_bvar 0)))))))
      (stm_vapp (blk_unbox (exp_bvar 0)) exp_const)).
Lemma handle_tick_term_typing :
  ∃ T, empty @ {}C ; nil |-blk handle_tick_term ~: T.