Top.SystemC.Soundness

The source of this file can be found on Github.

Soundness

The proof of soundness is split the following aspects:

• Substitution. See file SystemC.Substitution. For instance etyping_through_subst_ee shows that substituting an expression in an expression preserves expression-typing, and styping_through_subst_bs shows that substituting a block into a statement preserves statement-typing).
• Plugging. Lemma 3.6 in the paper is proven (in a variation) by unwind_step.
• Preservation. We show type preservation of reducing statements (preservation_stmt) and machine states (preservation_step).
• Progress. We show type progress for statements (progress_stmt) and machine states (progress_step).

Context Plugging

This helper lemma is important: it says that given a continuation and some variable x, plugging the variable in the position of the hole is well-typed.

This lemma roughly corresponds to Lemma 3.6 in the paper.

Lemma unwind_step : ∀ L Q x C T1 T2 k,
  wf_vtyp empty T1 →
  wf_cap empty C →
  C ; Q |-cnt k ~: T1 ~> T2 →
  x `notin` L →
  [(x, bind_val T1)] @ C ; Q |-stm (plug k x) ~: T2.

Helper lemma showing that plug doesn't introduce binders.

Lemma plugging : ∀ (x : atom) k C Q T1 T2,
  C ; Q |-cnt k ~: T1 ~> T2 →
  open_es (plug k 0) x = plug k x.

Preservation

As discussed in SystemC.Definitions, the operational semantics of SystemC is mechanized as an abstract machine, separating redexes that depend on the evaulation context from those that do not.

In consequence, the preservation Theorem 3.4 from the paper, maps to two separate theorems in the mechanization:

• preservation_stmt shows that reducing statement regardless of the context preserves the type.
• preservation_step shows that stepping from one state to another preserves the typability of the machine state.

Furthermore, the pure reductions for expressions (preservation_expr) and blocks (preservation_block) also preserve types, correspondingly.

Lemma preservation_block : ∀ E R Q b b' S1,
  btyping E R Q b S1 →
  bred b b' →
  btyping E R Q b' S1.

Lemma preservation_expr : ∀ E Q b b' S1,
  etyping E Q b S1 →
  ered b b' →
  etyping E Q b' S1.

Lemma preservation_stmt : ∀ E R Q s s' T,
  styping E R Q s T →
  sred s s' →
  styping E R Q s' T.

Lemma preservation_step : ∀ s1 s2,
  typing_state s1 →
  s1 --> s2 →
  typing_state s2.

Progress

Like with preservation, we have two lemmas for progress:

• progress_stmt shows that a well-typed statement can take a step.
• progress_step shows that a well-typed machine can take a step.

Canonical forms

We start by proving the usual canonical forms lemmas.

Lemma canonical_form_tabs : ∀ e T R Q,
  bvalue e →
  btyping empty R Q e (typ_tfun T) →
  ∃ e1, e = blk_tabs e1.

Lemma canonical_form_vabs : ∀ e U1 U2 R Q,
  bvalue e →
  btyping empty R Q e (typ_vfun U1 U2) →
  ∃ V, ∃ e1, e = blk_vabs V e1.

Lemma canonical_form_babs : ∀ e U1 U2 R Q,
  bvalue e →
  btyping empty R Q e (typ_bfun U1 U2) →
  ∃ V, ∃ e1, e = blk_babs V e1.

Lemma canonical_form_box : ∀ e R Q C,
  evalue e →
  etyping empty Q e (typ_capt R C) →
  ∃ s, e = exp_box C s.

Note that due to the slightly different representation of capability-types, we also have canonical forms for those

Lemma canonical_form_exc : ∀ b R Q T1 T,
  bvalue b →
  empty @ R ; Q |-blk b ~: (typ_eff T1 T) →
  ∃ l, b = blk_handler l ∧ Signatures.binds l (bind_sig T1 T) Q.

Progress

Lemma progress_block : ∀ b S1 R Q,
  empty @ R ; Q |-blk b ~: S1 →
  bvalue b ∨ ∃ b', b -->b b'.

Lemma progress_expr : ∀ Q e T,
  empty ; Q |-exp e ~: T →
  evalue e ∨ ∃ e', e -->e e'.

Lemma progress_stmt : ∀ s T R Q,
  empty @ R ; Q |-stm s ~: T →
  machine_redex s ∨ ∃ s', s -->s s'.

Lemma progress_step : ∀ s1,
  typing_state s1 →
  done s1 ∨ ∃ s2, s1 --> s2.