Qcert.Translation.TCAMPtoNRA

Section TCAMPtoNRA.

Auxiliary definitions and lemmas for the types corresponding to the encoding of input/output(s) of Patterns in the NRA

  Context {m:basic_model}.

  Definition pat_context_type tconst tbind tpid : rtype :=
    Rec Closed (("PBIND",tbind ) :: ("PCONST",tconst ) :: ("PDATA",tpid ) :: nil) (eq_refl _).

  Definition pat_wrap_a1_type tconst tbind tpid : rtype :=
    Rec Closed (("PBIND",tbind ) :: ("PCONST",tconst ) :: ("a1",tpid ) :: nil) (eq_refl _).

  Lemma ATpat_match {n τin τout} :
    n ▷ τin >=> τ out →
    pat_match n ▷ τin >=> Coll τ out.

  Lemma ATpat_match_inv {n τin τout} :
    pat_match n ▷ τin >=> τ out →
    ∃ τout', τ out = Coll τ out' ∧ n ▷ τin >=> τ out'.

  Lemma ATpat_match_invcoll {n τin τout} :
    pat_match n ▷ τin >=> Coll τ out →
    n ▷ τin >=> τ out .

Auxiliary lemmas specific to some of the NRA expressions used in the translation

  Lemma ATdot {p s τin τ pf τout k}:
    p ▷ τin >=> Rec k τ pf →
    tdot τ s = Some τ out →
    AUnop (ADot s) p ▷ τin >=> τ out.

  Lemma ATdot_inv {p s τin τout}:
    AUnop (ADot s) p ▷ τin >=> τ out →
    ∃ τ pf k,
      p ▷ τin >=> Rec k τ pf ∧
      tdot τ s = Some τ out.

  Lemma ATpat_data τc τ τin :
    pat_data ▷ pat_context_type τ c τ τin >=> τin.

  Lemma ATunnest_two (s1 s2:string) (op:nra) τin τ₁ pf1 τs τrem pf2 :
    op ▷ τin >=> (Coll (Rec Closed τ ₁ pf1)) →
    tdot τ ₁ s1 = Some (Coll τ s) →
    τ rem = (rremove (rec_concat_sort τ ₁ ((s2 ,τ s )::nil)) s1 ) →
    unnest_two s1 s2 op ▷
               τin >=> Coll (Rec Closed τ rem pf2).

  Lemma Coll_proj1 τ :
    proj1_sig (Coll τ) = Coll₀ (proj1_sig τ).

  Lemma ATunnest_two_inv {s1 s2:string} {op:nra} {τin τout} :
    unnest_two s1 s2 op ▷ τin >=> Coll τ out →
    ∃ τ₁ pf1 τs pf2,
    op ▷ τin >=> (Coll (Rec Closed τ ₁ pf1)) ∧
    tdot τ ₁ s1 = Some (Coll τ s) ∧
    τ out = Rec Closed (rremove (rec_concat_sort τ ₁ ((s2 ,τ s )::nil)) s1) pf2.

Main lemma for the type preservation of the translation.

Some corollaries of the main Lemma

Section dedicated to the reverse direction for type preservation

  Lemma ATaid_inv {τin τout} :
    AID ▷ τin >=> τ out → τin = τ out.

  Lemma UIP_refl_dec
        {A:Type}
        (dec:∀ x y:A, {x = y } + {x ≠ y })
        {x:A}
        (p1:x = x) : p1 = eq_refl x.

  Lemma nra_of_pat_type_form_output_weak p τin τout :
    nra_of_pat p ▷ τin >=> τ out →
    ∃ τout',τ out = Coll τ out'.

  Theorem nra_of_pat_type_form_output p τin τout :
    nra_of_pat p ▷ τin >=> τ out →
    {τout' | τ out = Coll τout'}.

  Lemma nra_of_pat_top_type_form_output_weak p c τin τout :
    nra_of_pat_top c p ▷ τin >=> τ out →
    ∃ τout', τ out = Coll τ out'.

  Theorem nra_of_pat_top_type_form_output p c τin τout :
    nra_of_pat_top c p ▷ τin >=> τ out →
    {τout' | τ out = Coll τout'}.

Theorem 7.4: Pattern<->NRA. Final iff Theorem of type preservation for the translation from Patterns to NRA

End TCAMPtoNRA.