Lemmas on the CoLiS language

Syntactic sugar

module SyntacticSugar
  use import base.Syntax
  use import base.CommonSemantics
  use import base.Semantics
  use import mystrings.String

Not (!)

  function tneg (t: term) : term =
    TIf t TFalse TTrue

  lemma evalt_neg : forall t gamma sigma b b' gamma'.
    eval_term t gamma sigma b gamma' ->
    b' = (match b with BNormal True -> BNormal False | BNormal False | BFatal -> BNormal True | _ -> b end) ->
    eval_term (tneg t) gamma sigma b' gamma'

  lemma nofatal_neg : forall t gamma sigma b gamma'.
    eval_term (tneg t) gamma sigma b gamma' ->
    b <> BFatal

  lemma symproj_neg : forall t gamma sigma b gamma'.
    eval_term (tneg t) gamma sigma b gamma'
    <-> eval_term (tneg (tneg (tneg t))) gamma sigma b gamma'

And (&&)

  function tconj (t_1 t_2: term) : term =
    TIf t_1 t_2 TFalse

  lemma evalt_conj_true : forall t_1 t_2 gamma gamma_1 gamma_2 sigma_1 sigma_2 b_2.
    eval_term t_1 gamma sigma_1 (BNormal True) gamma_1 ->
    eval_term t_2 gamma_1 sigma_2 b_2 gamma_2 ->
    eval_term (tconj t_1 t_2) gamma (concat sigma_1 sigma_2) b_2 gamma_2

  lemma evalt_conj_false : forall t_1 t_2 gamma gamma_1 sigma_1 b_1.
    eval_term t_1 gamma sigma_1 b_1 gamma_1 ->
    (match b_1 with BNormal False | BFatal -> true | _ -> false end) ->
    eval_term (tconj t_1 t_2) gamma sigma_1 (BNormal False) gamma_1

  lemma evalt_conj_transmit : forall t_1 t_2 gamma gamma_1 sigma_1 b_1.
    eval_term t_1 gamma sigma_1 b_1 gamma_1 ->
    (match b_1 with BNormal _ | BFatal -> false | _ -> true end) ->
    eval_term (tconj t_1 t_2) gamma sigma_1 b_1 gamma_1

  lemma associative_conj : forall t_1 t_2 t_3 gamma sigma b gamma'.
    eval_term (tconj (tconj t_1 t_2) t_3) gamma sigma b gamma'
    <-> eval_term (tconj t_1 (tconj t_2 t_3)) gamma sigma b gamma'

Or (||)

  function tdisj (t_1 t_2: term) : term =
    TIf t_1 TTrue t_2

  lemma evalt_disj_true : forall t_1 t_2 gamma gamma_1 sigma_1.
    eval_term t_1 gamma sigma_1 (BNormal True) gamma_1 ->
    eval_term (tdisj t_1 t_2) gamma sigma_1 (BNormal True) gamma_1

  lemma evalt_disj_false : forall t_1 t_2 gamma gamma_1 gamma_2 sigma_1 sigma_2 b_1 b_2.
    eval_term t_1 gamma sigma_1 b_1 gamma_1 ->
    (match b_1 with BNormal False | BFatal -> true | _ -> false end) ->
    eval_term t_2 gamma_1 sigma_2 b_2 gamma_2 ->
    eval_term (tdisj t_1 t_2) gamma (concat sigma_1 sigma_2) b_2 gamma_2

  lemma evalt_disj_transmit : forall t_1 t_2 gamma gamma_1 sigma_1 b_1.
    eval_term t_1 gamma sigma_1 b_1 gamma_1 ->
    (match b_1 with BNormal _ | BFatal -> false | _ -> true end) ->
    eval_term (tdisj t_1 t_2) gamma sigma_1 b_1 gamma_1

  lemma associative_disj : forall t_1 t_2 t_3 gamma sigma b gamma'.
    eval_term (tdisj (tdisj t_1 t_2) t_3) gamma sigma b gamma'
    <-> eval_term (tdisj t_1 (tdisj t_2 t_3)) gamma sigma b gamma'

While

  function twhile (t_1 t_2: term) : term =
    TIf t_1 (TDoWhile t_2 t_1) TTrue

end

Simple facts

Not so usefull simple facts, just here to show that we can play with the language.

module SimpleFacts
  use import base.Syntax
  use import base.Semantics

  lemma idempotent_process : forall t gamma sigma b gamma'.
    eval_term (TProcess (TProcess t)) gamma sigma b gamma'
    <-> eval_term (TProcess t) gamma sigma b gamma'

  lemma associative_pipe : forall t_1 t_2 t_3 gamma sigma b gamma'.
    eval_term (TPipe (TPipe t_1 t_2) t_3) gamma sigma b gamma'
    <-> eval_term (TPipe t_1 (TPipe t_2 t_3)) gamma sigma b gamma'
end

Equivalences

(* module SemanticEquivalences *)
(*   use import base.Syntax *)
(*   use import base.CommonSemantics *)
(*   use base.Semantics as S *)
(*   use base.SemanticsWithDepth as SWD *)

(*   lemma impl_eval_term : *)
(*     forall t g s b g'. *)
(*     S.eval_term t g s b g' -> *)
(*     exists d. SWD.eval_term t g s b g' d *)

(*   lemma impl_eval_term_tcall : *)
(*     forall l g s b g'. *)
(*     S.eval_term_tcall l g s b g' -> *)
(*     exists d. SWD.eval_term l g s b g' d *)

(*   lemma impl *)

(*   (\* Other direction *\) *)

(*   lemma impl2_eval_term : *)
(*     forall t g s b g' d. *)
(*     SWD.eval_term t g s b g' d -> *)
(*     S.eval_term t g s b g' d *)

(* end *)

module FunctionnalSemanticsWithSkeleton
  use import list.List
  use import mystrings.String
  use import skeleton.Skeleton

  use import base.Syntax
  use import base.CommonSemantics
  use import base.SemanticsWithSkeleton

  let rec lemma functionnal_semantics (sk': skeleton)
    ensures {
       (forall t g s' b' g'. eval_term t g s' b' g' sk' ->
        forall s'2 b'2 g'2 sk'2. eval_term t g s'2 b'2 g'2 sk'2 ->
        s' = s'2 /\ b' = b'2 /\ g' = g'2 /\ sk' = sk'2)

    /\ (forall l g s' b' g'. eval_term_tcall l g s' b' g' sk' ->
        forall s'2 b'2 g'2 sk'2. eval_term_tcall l g s'2 b'2 g'2 sk'2 ->
	s' = s'2 /\ b' = b'2 /\ g' = g'2 /\ sk' = sk'2)

    /\ (forall x_s l t g s' b' g'. eval_term_tfor x_s l t g s' b' g' sk' ->
        forall s'2 b'2 g'2 sk'2. eval_term_tfor x_s l t g s'2 b'2 g'2 sk'2 ->
	s' = s'2 /\ b' = b'2 /\ g' = g'2 /\ sk' = sk'2)

    /\ (forall s g s' b' g'. eval_sexpr s g s' b' g' sk' ->
        forall s'2 b'2 g'2 sk'2. eval_sexpr s g s'2 b'2 g'2 sk'2 ->
	s' = s'2 /\ b' = b'2 /\ g' = g'2 /\ sk' = sk'2)

    /\ (forall s g s' b' g'. eval_sexpr_opt s g s' b' g' sk' ->
        forall s'2 b'2 g'2 sk'2. eval_sexpr_opt s g s'2 b'2 g'2 sk'2 ->
	s' = s'2 /\ b' = b'2 /\ g' = g'2 /\ sk' = sk'2)

    /\ (forall s g s' b' g'. eval_sfrag_opt s g s' b' g' sk' ->
        forall s'2 b'2 g'2 sk'2. eval_sfrag_opt s g s'2 b'2 g'2 sk'2 ->
	s' = s'2 /\ b' = b'2 /\ g' = g'2 /\ sk' = sk'2)

    /\ (forall s g s' b' g'. eval_lexpr s g s' b' g' sk' ->
        forall s'2 b'2 g'2 sk'2. eval_lexpr s g s'2 b'2 g'2 sk'2 ->
	s' = s'2 /\ b' = b'2 /\ g' = g'2 /\ sk' = sk'2)

    /\ (forall s g s' b' g'. eval_lexpr_opt s g s' b' g' sk' ->
        forall s'2 b'2 g'2 sk'2. eval_lexpr_opt s g s'2 b'2 g'2 sk'2 ->
	s' = s'2 /\ b' = b'2 /\ g' = g'2 /\ sk' = sk'2)

    /\ (forall s g s' b' g'. eval_lfrag_opt s g s' b' g' sk' ->
        forall s'2 b'2 g'2 sk'2. eval_lfrag_opt s g s'2 b'2 g'2 sk'2 ->
	s' = s'2 /\ b' = b'2 /\ g' = g'2 /\ sk' = sk'2)
    }
    variant { sk' }
  =
    match sk' with
    | S0 -> ()
    | S1 sk1 ->
      functionnal_semantics sk1

    | S2 sk1 sk2 ->
      functionnal_semantics sk1;
      functionnal_semantics sk2

    | S3 sk1 sk2 sk3 ->
      functionnal_semantics sk1;
      functionnal_semantics sk2;
      functionnal_semantics sk3
    end

  lemma func_eval_term :
    forall t g s1 b1 g1 sk1 s2 b2 g2 sk2.
    eval_term t g s1 b1 g1 sk1 ->
    eval_term t g s2 b2 g2 sk2 ->
    s1 = s2 /\ b1 = b2 /\ g1 = g2 /\ sk1 = sk2

  lemma func_eval_term_tcall :
    forall l g s1 b1 g1 sk1 s2 b2 g2 sk2.
    eval_term_tcall l g s1 b1 g1 sk1 ->
    eval_term_tcall l g s2 b2 g2 sk2 ->
    s1 = s2 /\ b1 = b2 /\ g1 = g2 /\ sk1 = sk2

  lemma func_eval_term_tfor :
    forall x_s l t g s1 b1 g1 sk1 s2 b2 g2 sk2.
    eval_term_tfor x_s l t g s1 b1 g1 sk1 ->
    eval_term_tfor x_s l t g s2 b2 g2 sk2 ->
    s1 = s2 /\ b1 = b2 /\ g1 = g2 /\ sk1 = sk2

  lemma func_eval_sexpr :
    forall s g s1 b1 g1 sk1 s2 b2 g2 sk2.
    eval_sexpr s g s1 b1 g1 sk1 ->
    eval_sexpr s g s2 b2 g2 sk2 ->
    s1 = s2 /\ b1 = b2 /\ g1 = g2 /\ sk1 = sk2

  lemma func_eval_sexpr_opt :
    forall s g s1 b1 g1 sk1 s2 b2 g2 sk2.
    eval_sexpr_opt s g s1 b1 g1 sk1 ->
    eval_sexpr_opt s g s2 b2 g2 sk2 ->
    s1 = s2 /\ b1 = b2 /\ g1 = g2 /\ sk1 = sk2

  lemma func_eval_sfrag_opt :
    forall f g s1 b1 g1 sk1 s2 b2 g2 sk2.
    eval_sfrag_opt f g s1 b1 g1 sk1 ->
    eval_sfrag_opt f g s2 b2 g2 sk2 ->
    s1 = s2 /\ b1 = b2 /\ g1 = g2 /\ sk1 = sk2

  lemma func_eval_lexpr :
    forall l g s1 b1 g1 sk1 s2 b2 g2 sk2.
    eval_lexpr l g s1 b1 g1 sk1 ->
    eval_lexpr l g s2 b2 g2 sk2 ->
    s1 = s2 /\ b1 = b2 /\ g1 = g2 /\ sk1 = sk2

  lemma func_eval_lexpr_opt :
    forall l g s1 b1 g1 sk1 s2 b2 g2 sk2.
    eval_lexpr_opt l g s1 b1 g1 sk1 ->
    eval_lexpr_opt l g s2 b2 g2 sk2 ->
    s1 = s2 /\ b1 = b2 /\ g1 = g2 /\ sk1 = sk2

  lemma func_eval_lfrag_opt :
    forall f g s1 b1 g1 sk1 s2 b2 g2 sk2.
    eval_lfrag_opt f g s1 b1 g1 sk1 ->
    eval_lfrag_opt f g s2 b2 g2 sk2 ->
    s1 = s2 /\ b1 = b2 /\ g1 = g2 /\ sk1 = sk2
end