SpecCTSpeculative Constant-Time

Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From Coq Require Import Strings.String.
From SECF Require Import Maps.
From Coq Require Import Bool.Bool.
From Coq Require Import Arith.Arith.
From Coq Require Import Arith.EqNat.
From Coq Require Import Arith.PeanoNat. Import Nat.
From Coq Require Import Lia.
From Coq Require Import List. Import ListNotations.
Set Default Goal Selector "!".

Cryptographic constant-time

Cryptographic constant-time (CCT) is a software countermeasure against cache-based timing attacks, a class of side-channel attacks that exploit the latency between cache hits and cache misses to retrieve cryptographic keys and other secrets. In addition to ensuring program counter security, CCT requires programmers to not perform memory accesses depending on secrets.

To model this we will make the Imp language more realistic by adding arrays. We need such an extension, since otherwise variable accesses in the original Imp map to memory operations at constant locations, which thus cannot depend on secrets, so CCT trivially holds for all programs in Imp. Array indices on the other hand are computed at runtime, which leads to accessing memory addresses that can depend on secrets, making CCT non-trivial for Imp with arrays.

For instance, here is a simple program that is pc secure (since it does no branches), but not constant-time secure (since it's accesses memory based on secret information):
x <- a[secret]

Constant-time conditional

But first, we extend the arithmetic expressions of Imp with an b ? e₁ : e₂ conditional that executes in constant time (for instance using a special constant-time conditional move instruction). This constant-time conditional will be used in one of our countermeasures below, but it complicates things a bit, since it makes arithmetic and boolean expressions mutually inductive.

Scheme aexp_bexp_ind := Induction for aexp Sort Prop
with bexp_aexp_ind := Induction for bexp Sort Prop.
Combined Scheme aexp_bexp_mutind from aexp_bexp_ind,bexp_aexp_ind.

Typing Constant-time conditional

Typing of arithmetic and boolean expressions will also become mutually inductive.

P⊢b- be ∈ l P ⊢a- a₁ ∈ l₁ P ⊢a- a₂ ∈ l₂	(T_CTIf)

P ⊢a- be?a₁:a₂ ∈ join l (join l₁ l₂)

Definition W : string := "W".
Definition X : string := "X".
Definition Y : string := "Y".
Definition Z : string := "Z".
Definition A : string := "A".
Definition AP : string := "AP".
Definition AS : string := "AS".

Coercion AId : string >-> aexp.
Coercion ANum : nat >-> aexp.

Declare Custom Entry com.
Declare Scope com_scope.

Notation "<{ e }>" := e (at level 0, e custom com at level 99) : com_scope.
Notation "( x )" := x (in custom com, x at level 99) : com_scope.
Notation "x" := x (in custom com at level 0, x constr at level 0) : com_scope.
Notation "f x .. y" := (.. (f x) .. y)
                  (in custom com at level 0, only parsing,
                  f constr at level 0, x constr at level 9,
                  y constr at level 9) : com_scope.
Notation "x + y" := (APlus x y) (in custom com at level 50, left associativity).
Notation "x - y" := (AMinus x y) (in custom com at level 50, left associativity).
Notation "x * y" := (AMult x y) (in custom com at level 40, left associativity).
Notation "be '?' a₁ ':' a₂" := (ACTIf be a₁ a₂)
                 (in custom com at level 20, no associativity).
Notation "'true'" := true (at level 1).
Notation "'true'" := BTrue (in custom com at level 0).
Notation "'false'" := false (at level 1).
Notation "'false'" := BFalse (in custom com at level 0).
Notation "x <= y" := (BLe x y) (in custom com at level 70, no associativity).
Notation "x > y" := (BGt x y) (in custom com at level 70, no associativity).
Notation "x = y" := (BEq x y) (in custom com at level 70, no associativity).
Notation "x <> y" := (BNeq x y) (in custom com at level 70, no associativity).
Notation "x && y" := (BAnd x y) (in custom com at level 80, left associativity).
Notation "'~' b" := (BNot b) (in custom com at level 75, right associativity).

Open Scope com_scope.

Now back to adding arrays

Notation "<{{ e }}>" := e (at level 0, e custom com at level 99) : com_scope.
Notation "( x )" := x (in custom com, x at level 99) : com_scope.
Notation "x" := x (in custom com at level 0, x constr at level 0) : com_scope.
Notation "f x .. y" := (.. (f x) .. y)
                  (in custom com at level 0, only parsing,
                  f constr at level 0, x constr at level 9,
                  y constr at level 9) : com_scope.

Open Scope com_scope.

Notation "'skip'" :=
  Skip (in custom com at level 0) : com_scope.
Notation "x := y" :=
  (Asgn x y)
    (in custom com at level 0, x constr at level 0,
      y custom com at level 85, no associativity) : com_scope.
Notation "x ; y" :=
  (Seq x y)
    (in custom com at level 90, right associativity) : com_scope.
Notation "'if' x 'then' y 'else' z 'end'" :=
  (If x y z)
    (in custom com at level 89, x custom com at level 99,
     y at level 99, z at level 99) : com_scope.
Notation "'while' x 'do' y 'end'" :=
  (While x y)
    (in custom com at level 89, x custom com at level 99, y at level 99) : com_scope.

Notation "x '<-' a '[[' i ']]'" :=
  (ARead x a i)
     (in custom com at level 0, x constr at level 0,
      a at level 85, i custom com at level 85, no associativity) : com_scope.
Notation "a '[' i ']' '<-' e" :=
  (AWrite a i e)
     (in custom com at level 0, a constr at level 0,
      i custom com at level 0, e custom com at level 85,
         no associativity) : com_scope.

Definition state := total_map nat.
Definition astate := total_map (list nat).

Fixpoint aeval (st : state) (a : aexp) : nat :=
  match a with
  | ANum n ⇒ n
  | AId x ⇒ st x
  | <{a₁ + a₂}> ⇒ (aeval st a₁) + (aeval st a₂)
  | <{a₁ - a₂}> ⇒ (aeval st a₁) - (aeval st a₂)
  | <{a₁ × a₂}> ⇒ (aeval st a₁) × (aeval st a₂)
  | <{b ? a₁ : a₂}> ⇒ if beval st b then aeval st a₁
          (* ^- NEW -> *) else aeval st a₂
  end
with beval (st : state) (b : bexp) : bool :=
  match b with
  | <{true }> ⇒ true
  | <{false }> ⇒ false
  | <{a₁ = a₂}> ⇒ (aeval st a₁) =? (aeval st a₂)
  | <{a₁ ≠ a₂}> ⇒ negb ((aeval st a₁) =? (aeval st a₂))
  | <{a₁ ≤ a₂}> ⇒ (aeval st a₁) <=? (aeval st a₂)
  | <{a₁ > a₂}> ⇒ negb ((aeval st a₁) <=? (aeval st a₂))
  | <{¬ b₁}> ⇒ negb (beval st b₁)
  | <{b₁ && b₂}> ⇒ andb (beval st b₁) (beval st b₂)
  end.

Fixpoint upd (i:nat) (ns:list nat) (n:nat) : list nat :=
  match i, ns with
  | 0, _ :: ns' ⇒ n :: ns'
  | S i', _ :: ns' ⇒ upd i' ns' n
  | _, _ ⇒ ns
  end.

Observations

Inductive observation : Type :=
  | OBranch (b : bool)
  | OARead (a : string) (i : nat)
  | OAWrite (a : string) (i : nat).

Definition obs := list observation.

We define an instrumented big-step operational semantics based on these observations.

	(CTE_Skip)

<(st , ast)> =[ skip ]=> <(st, ast, [])>

aeval st e = n	(CTE_Asgn)

<(st, ast)> =[ x := e ]=> <(x !-> n; st, ast, [])>

<(st, ast)> =[ c₁ ]=> <(st', ast', os₁)>
<(st', ast')> =[ c₂ ]=> <(st'', ast'', os₂)>	(CTE_Seq)

<(st, ast)> =[ c₁ ; c₂ ]=> <(st'', ast'', os₂++os₁)>

beval st b = true
<(st, ast)> =[ c₁ ]=> <(st', ast', os₁)>	(* CTE_IfTrue *)

<(st, ast)> =[ if b then c₁ else c₂ end]=> <(st', ast', os₁ ++ [OBranch true])>

beval st b = false
<(st, ast)> =[ c₂ ]=> <(st', ast', os₁)>	(* CTE_IfFalse *)

<(st, ast)> =[ if b then c₁ else c₂ end]=> <(st', ast', os₁ ++ [OBranch false])>

<(st,ast)> =[ if b then c; while b do c end else skip end ]=> <(st', ast', os)>	(* CTE_While *)

<(st,ast)> =[ while b do c end ]=> <(st', ast', os)>

aeval st ie = i
i < length (ast a)	(* CTE_AREad *)

<(st, ast)> =[ x <- a[[ie]] ]=> <(x !-> nth i (ast a) 0; st, ast, [OARead a i])>

aeval st e = n
aeval st ie = i
i < length (ast a)	(* CTE_Write *)

<(st, ast)> =[ a[ie] <- e ]=> <(st, a !-> upd i (ast a) n; ast, [OAWrite a i])>

Reserved Notation
         "'<(' st , ast ')>' '=[' c ']=>' '<(' stt , astt , os ')>'"
         (at level 40, c custom com at level 99,
          st constr, ast constr, stt constr, astt constr at next level).

Inductive cteval : com → state → astate → state → astate → obs → Prop :=
  | CTE_Skip : ∀ st ast,
      <(st , ast )> =[ skip ]=> <(st , ast , [])>
  | CTE_Asgn : ∀ st ast e n x,
      aeval st e = n →
      <(st , ast )> =[ x := e ]=> <(x !-> n; st , ast , [])>
  | CTE_Seq : ∀ c₁ c₂ st ast st' ast' st'' ast'' os₁ os₂,
      <(st , ast )> =[ c₁ ]=> <(st', ast', os₁ )> →
      <(st', ast')> =[ c₂ ]=> <(st'', ast'', os₂ )> →
      <(st , ast )> =[ c₁ ; c₂ ]=> <(st'', ast'', os₂ ++os₁ )>
  | CTE_IfTrue : ∀ st ast st' ast' b c₁ c₂ os₁,
      beval st b = true →
      <(st , ast )> =[ c₁ ]=> <(st', ast', os₁ )> →
      <(st , ast )> =[ if b then c₁ else c₂ end ]=> <(st', ast', os₁ ++ [OBranch true ])>
  | CTE_IfFalse : ∀ st ast st' ast' b c₁ c₂ os₁,
      beval st b = false →
      <(st , ast )> =[ c₂ ]=> <(st', ast', os₁ )> →
      <(st , ast )> =[ if b then c₁ else c₂ end ]=> <(st', ast', os₁ ++ [OBranch false ])>
  | CTE_While : ∀ b st ast st' ast' os c,
      <(st ,ast )> =[ if b then c ; while b do c end else skip end ]=>
        <(st', ast', os )> → (* <^- Nice trick; from small-step semantics *)
      <(st ,ast )> =[ while b do c end ]=> <(st', ast', os )>
  | CTE_ARead : ∀ st ast x a ie i,
      aeval st ie = i →
      i < length (ast a) →
      <(st , ast )> =[ x <- a [[ie ]] ]=> <(x !-> nth i (ast a) 0; st , ast , [OARead a i ])>
  | CTE_Write : ∀ st ast a ie i e n,
      aeval st e = n →
      aeval st ie = i →
      i < length (ast a) →
      <(st , ast )> =[ a [ie ] <- e ]=> <(st , a !-> upd i (ast a) n; ast , [OAWrite a i ])>

  where "<( st , ast )> =[ c ]=> <( stt , astt , os )>" := (cteval c st ast stt astt os).

Constant-time security definition

Definition label := bool.

Definition public : label := true.
Definition secret : label := false.

Definition pub_vars := total_map label.
Definition pub_arrs := total_map label.

Definition pub_equiv (P : total_map label) {X:Type} (s₁ s₂ : total_map X) :=
∀ x:string, P x = true → s₁ x = s₂ x.

Lemma pub_equiv_refl : ∀ {X:Type} (P : total_map label) (s : total_map X),
pub_equiv P s s.
Proof. intros X P s x Hx. reflexivity. Qed.

Lemma pub_equiv_sym : ∀ {X:Type} (P : total_map label) (s₁ s₂ : total_map X),
pub_equiv P s₁ s₂ →
pub_equiv P s₂ s₁.
Proof. unfold pub_equiv. intros X P s₁ s₂ H x Px. rewrite H; auto. Qed.

Lemma pub_equiv_trans : ∀ {X:Type} (P : total_map label) (s₁ s₂ s₃ : total_map X),
  pub_equiv P s₁ s₂ →
  pub_equiv P s₂ s₃ →
  pub_equiv P s₁ s₃.
Proof.
  unfold pub_equiv. intros X P s₁ s₂ s₃ H₁₂ H₂₃ x Px.
  rewrite H₁₂; try rewrite H₂₃; auto.
Qed.

Definition ct_secure P PA c :=
  ∀ st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' os₁ os₂,
    pub_equiv P st₁ st₂ →
    pub_equiv PA ast1 ast2 →
    <(st₁ , ast1 )> =[ c ]=> <(st₁', ast1', os₁ )> →
    <(st₂ , ast2 )> =[ c ]=> <(st₂', ast2', os₂ )> →
    os₁ = os₂.

Example pc secure program that is not constant-time secure

Definition ct_insecure_prog :=
<{{ X <- A [[Y ]] }}> .

(* This program is trivially pc secure, because it does not branch at all.
But it is not constant-time secure, if Y is a secret variable. This is
shown below. *)

Example ct_insecure_prog_is_not_ct_secure : ∃ P PA ,
  ¬ (ct_secure P PA ct_insecure_prog ) .
Proof.
  remember (X!-> public; Y!-> secret; _!-> public) as P.
  remember (A!-> secret; _!-> public) as PA.
  ∃ P. ∃ PA. unfold ct_secure, ct_insecure_prog; intros H.
  remember (Y!-> 1; _ !-> 0) as st₁.
  remember (Y!-> 2; _ !-> 0) as st₂.
  remember (A!-> [1;2;3]; _!-> []) as ast.
  assert (Heval1: <(st₁, ast)> =[ct_insecure_prog ]=> <(X!->2; st₁, ast, [OARead A 1])>).
  { unfold ct_insecure_prog; subst.
    replace (X !-> 2; Y !-> 1; _ !-> 0)
      with (X !-> nth 1 ((A!-> [1;2;3]; _!-> []) A) 0; Y !-> 1; _ !-> 0)
        by (reflexivity).
    eapply CTE_ARead; simpl; auto. }
  assert (Heval2: <(st₂, ast)> =[ct_insecure_prog ]=> <(X!->3; st₂, ast, [OARead A 2])>).
  { unfold ct_insecure_prog; subst.
    replace (X !-> 3; Y !-> 2; _ !-> 0)
      with (X !-> nth 2 ((A!-> [1;2;3]; _!-> []) A) 0; Y !-> 2; _ !-> 0)
        by (reflexivity).
      eapply CTE_ARead; simpl; auto. }
  subst. eapply H in Heval2; eauto.
  - inversion Heval2.
  - intros x Hx. destruct (String.eqb_spec Y x) as [Heq | Hneq].
    + subst. rewrite t_update_neq in Hx; [| discriminate].
      rewrite t_update_eq in Hx. discriminate.
    + do 2 (rewrite t_update_neq; [| assumption]). reflexivity.
  - apply pub_equiv_refl.
Qed.

Type system for cryptographic constant-time programming

Definition join (l₁ l₂ : label) : label := l₁ && l₂.

Lemma join_public : ∀ {l₁ l₂},
join l₁ l₂ = public → l₁ = public ∧ l₂ = public.
Proof. apply andb_prop. Qed.

Definition can_flow (l₁ l₂ : label) : bool := l₁ || negb l₂.

Reserved Notation "P '⊢a-' a ∈ l" (at level 40).
Reserved Notation "P '⊢b-' b ∈ l" (at level 40).

Inductive aexp_has_label (P:pub_vars) : aexp → label → Prop :=
  | T_Num : ∀ n,
       P ⊢a - (ANum n ) \in public
  | T_Id : ∀ X,
       P ⊢a - (AId X ) \in (P X )
  | T_Plus : ∀ a₁ l₁ a₂ l₂,
       P ⊢a - a₁ \in l₁ →
       P ⊢a - a₂ \in l₂ →
       P ⊢a - <{ a₁ + a₂ }> \in (join l₁ l₂ )
  | T_Minus : ∀ a₁ l₁ a₂ l₂,
       P ⊢a - a₁ \in l₁ →
       P ⊢a - a₂ \in l₂ →
       P ⊢a - <{ a₁ - a₂ }> \in (join l₁ l₂ )
  | T_Mult : ∀ a₁ l₁ a₂ l₂,
       P ⊢a - a₁ \in l₁ →
       P ⊢a - a₂ \in l₂ →
       P ⊢a - <{ a₁ × a₂ }> \in (join l₁ l₂ )
  | T_CTIf : ∀ be l a₁ l₁ a₂ l₂,
       P ⊢b - be \in l →
       P ⊢a - a₁ \in l₁ →
       P ⊢a - a₂ \in l₂ →
       P ⊢a - <{ be ? a₁ : a₂ }> \in (join l (join l₁ l₂))

where "P '⊢a-' a '∈' l" := (aexp_has_label P a l)

with bexp_has_label (P:pub_vars) : bexp → label → Prop :=
  | T_True :
       P ⊢b - <{ true }> \in public
  | T_False :
       P ⊢b - <{ false }> \in public
  | T_Eq : ∀ a₁ l₁ a₂ l₂,
       P ⊢a - a₁ \in l₁ →
       P ⊢a - a₂ \in l₂ →
       P ⊢b - <{ a₁ = a₂ }> \in (join l₁ l₂ )
  | T_Neq : ∀ a₁ l₁ a₂ l₂,
       P ⊢a - a₁ \in l₁ →
       P ⊢a - a₂ \in l₂ →
       P ⊢b - <{ a₁ ≠ a₂ }> \in (join l₁ l₂ )
  | T_Le : ∀ a₁ l₁ a₂ l₂,
       P ⊢a - a₁ \in l₁ →
       P ⊢a - a₂ \in l₂ →
       P ⊢b - <{ a₁ ≤ a₂ }> \in (join l₁ l₂ )
  | T_Gt : ∀ a₁ l₁ a₂ l₂,
       P ⊢a - a₁ \in l₁ →
       P ⊢a - a₂ \in l₂ →
       P ⊢b - <{ a₁ > a₂ }> \in (join l₁ l₂ )
  | T_Not : ∀ b l,
       P ⊢b - b \in l →
       P ⊢b - <{ ¬b }> \in l
  | T_And : ∀ b₁ l₁ b₂ l₂,
       P ⊢b - b₁ \in l₁ →
       P ⊢b - b₂ \in l₂ →
       P ⊢b - <{ b₁ && b₂ }> \in (join l₁ l₂ )

where "P '⊢b-' b '∈' l" := (bexp_has_label P b l).

Scheme aexp_bexp_has_label_ind := Induction for aexp_has_label Sort Prop
with bexp_aexp_has_label_ind := Induction for bexp_has_label Sort Prop.
Combined Scheme aexp_bexp_has_label_mutind
from aexp_bexp_has_label_ind,bexp_aexp_has_label_ind.

Theorem noninterferent_aexp_bexp : ∀ P s₁ s₂,
  pub_equiv P s₁ s₂ →
  (∀ a l, P ⊢a - a \in l →
   l = public → aeval s₁ a = aeval s₂ a ) ∧
  (∀ b l, P ⊢b - b \in l →
   l = public → beval s₁ b = beval s₂ b ).
Proof.
  intros P s₁ s₂ Heq. apply (aexp_bexp_has_label_mutind P);
    simpl; intros;
    (repeat match goal with
    | [Heql : join _ _ = public ⊢ _] ⇒
      let G₁ := fresh "G₁" in
      let G₂ := fresh "G₂" in
      destruct (join_public Heql) as [G₁ G₂];
      rewrite G₁ in *; rewrite G₂ in ×
    end); try reflexivity; eauto; firstorder;
    (repeat match goal with
    | [IH : aeval s₁ ?a = aeval s₂ ?a ⊢ _] ⇒ rewrite IH
    end);
    (repeat match goal with
    | [IH : beval s₁ ?b = beval s₂ ?b ⊢ _] ⇒ rewrite IH
    end); reflexivity.
Qed.

Theorem noninterferent_aexp : ∀ {P s₁ s₂ a},
  pub_equiv P s₁ s₂ →
  P ⊢a - a \in public →
  aeval s₁ a = aeval s₂ a.
Proof.
  intros P s₁ s₂ a Heq Ht. remember public as l.
  generalize dependent Heql. generalize dependent l.
  apply noninterferent_aexp_bexp. assumption.
Qed.

Theorem noninterferent_bexp : ∀ {P s₁ s₂ b},
  pub_equiv P s₁ s₂ →
  P ⊢b - b \in public →
  beval s₁ b = beval s₂ b.
Proof.
  intros P s₁ s₂ b Heq Ht. remember public as l.
  generalize dependent Heql. generalize dependent l.
  apply noninterferent_aexp_bexp. assumption.
Qed.

	(CT_Skip)

P ;; PA ⊢ct- skip

P ⊢a- a ∈ l can_flow l (P X) = true	(CT_Asgn)

P ;; PA ⊢ct- X := a

P ;; PA ⊢ct- c₁ P ;; PA ⊢ct- c₂	(CT_Seq)

P ;; PA ⊢ct- c₁;c₂

P ⊢b- b ∈ public P ;; PA ⊢ct- c₁ P ;; PA ⊢ct- c₂	(CT_If)

P ;; PA ⊢ct- if b then c₁ else c₂

P ⊢b- b ∈ public P ⊢ct- c	(CT_While)

P ;; PA ⊢ct- while b then c end

P ⊢a- i ∈ public can_flow (PA a) (P x) = true	(CT_ARead)

P ;; PA ⊢ct- x <- a[[i]]

P ⊢a- i ∈ public P ⊢a- e ∈ l can_flow l (PA a) = true	(CT_AWrite)

P ;; PA ⊢ct- a[i] <- e

Reserved Notation "P ';;' PA '⊢ct-' c" (at level 40).

Inductive ct_well_typed (P:pub_vars) (PA:pub_arrs) : com → Prop :=
  | CT_Skip :
      P ;; PA ⊢ct - <{{ skip }}>
  | CT_Asgn : ∀ X a l,
      P ⊢a - a \in l →
      can_flow l (P X) = true →
      P ;; PA ⊢ct - <{{ X := a }}>
  | CT_Seq : ∀ c₁ c₂,
      P ;; PA ⊢ct - c₁ →
      P ;; PA ⊢ct - c₂ →
      P ;; PA ⊢ct - <{{ c₁ ; c₂ }}>
  | CT_If : ∀ b c₁ c₂,
      P ⊢b - b \in public →
      P ;; PA ⊢ct - c₁ →
      P ;; PA ⊢ct - c₂ →
      P ;; PA ⊢ct - <{{ if b then c₁ else c₂ end }}>
  | CT_While : ∀ b c₁,
      P ⊢b - b \in public →
      P ;; PA ⊢ct - c₁ →
      P ;; PA ⊢ct - <{{ while b do c₁ end }}>
  | CT_ARead : ∀ x a i,
      P ⊢a - i \in public →
      can_flow (PA a) (P x) = true →
      P ;; PA ⊢ct - <{{ x <- a [[i ]] }}>
  | CT_AWrite : ∀ a i e l,
      P ⊢a - i \in public →
      P ⊢a - e \in l →
      can_flow l (PA a) = true →
      P ;; PA ⊢ct - <{{ a [i ] <- e }}>

where "P ;; PA '⊢ct-' c" := (ct_well_typed P PA c).

Final theorems: noninterference and constant-time security

Theorem ct_well_typed_noninterferent :
  ∀ P PA c s₁ s₂ a₁ a₂ s₁' s₂' a₁' a₂' os₁ os₂,
    P ;; PA ⊢ct - c →
    pub_equiv P s₁ s₂ →
    pub_equiv PA a₁ a₂ →
    <(s₁ , a₁ )> =[ c ]=> <(s₁', a₁', os₁ )> →
    <(s₂ , a₂ )> =[ c ]=> <(s₂', a₂', os₂ )> →
    pub_equiv P s₁' s₂' ∧ pub_equiv PA a₁' a₂'.

Proof.
  intros P PA c s₁ s₂ a₁ a₂ s₁' s₂' a₁' a₂' os₁ os₂
    Hwt Heq Haeq Heval1 Heval2.
  generalize dependent s₂'. generalize dependent s₂.
  generalize dependent a₂'. generalize dependent a₂.
  generalize dependent os₂.
  induction Heval1; intros os₂' a₂ Haeq a₂' s₂ Heq s₂' Heval2;
    inversion Heval2; inversion Hwt; subst.
  - split; auto.
  - split; auto.
    intros y Hy. destruct (String.eqb_spec x y) as [Hxy | Hxy].
    + rewrite Hxy. do 2 rewrite t_update_eq.
      eapply noninterferent_aexp; eauto.
      subst. rewrite Hy in H₁₁.
      unfold can_flow in H₁₁. simpl in H₁₁.
      destruct l; try discriminate. auto.
    + do 2 rewrite (t_update_neq _ _ _ _ _ Hxy).
      apply Heq. apply Hy.
  - edestruct IHHeval1_2; eauto.
    + eapply IHHeval1_1; eauto.
    + eapply IHHeval1_1; eauto.
  - eapply IHHeval1; eauto.
  - rewrite (noninterferent_bexp Heq H₁₃) in H.
    rewrite H in H₈. discriminate H₈.
  - rewrite (noninterferent_bexp Heq H₁₃) in H.
    rewrite H in H₈. discriminate H₈.
  - eapply IHHeval1; eassumption.
  - eapply IHHeval1; eauto. repeat constructor; eassumption.
  - (* NEW CASE: ARead *)
    split; eauto.
    erewrite noninterferent_aexp; eauto.
    intros y Hy. destruct (String.eqb_spec x y) as [Hxy | Hxy].
    + rewrite Hxy. do 2 rewrite t_update_eq.
      subst. rewrite Hy in ×.
      rewrite Haeq; eauto. now destruct (PA a).
    + do 2 rewrite (t_update_neq _ _ _ _ _ Hxy).
      apply Heq. apply Hy.
  - (* NEW CASE: AWrite *)
    split; eauto.
    erewrite noninterferent_aexp; eauto.
    intros y Hy.
    destruct (String.eqb_spec a y) as [Hay | Hay].
    + rewrite Hay. do 2 rewrite t_update_eq.
      subst. rewrite Hy in ×.
      rewrite Haeq; eauto.
      erewrite (noninterferent_aexp Heq); eauto. now destruct l.
    + do 2 rewrite (t_update_neq _ _ _ _ _ Hay).
      apply Haeq. apply Hy.
Qed.

Theorem ct_well_typed_ct_secure : ∀ P PA c,
P ;; PA ⊢ct - c →
ct_secure P PA c.

Proof.
  unfold ct_secure.
  intros P PA c Hwt st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' os₁ os₂
    Heq Haeq Heval1 Heval2.
  generalize dependent st₂'. generalize dependent st₂.
  generalize dependent ast2'. generalize dependent ast2.
  generalize dependent os₂.
  induction Heval1; intros os₂' a₂ Haeq a₂' s₂ Heq s₂' Heval2;
    inversion Heval2; inversion Hwt; subst.
  - reflexivity.
  - reflexivity.
  - erewrite IHHeval1_2; [erewrite IHHeval1_1 | | | |];
      try reflexivity; try eassumption.
    + eapply ct_well_typed_noninterferent;
        [ | eassumption | eassumption | eassumption | eassumption ];
        eassumption.
    + eapply ct_well_typed_noninterferent;
        [ | eassumption | eassumption | eassumption | eassumption ];
        eassumption.
  - f_equal. eapply IHHeval1; try eassumption.
  - rewrite (noninterferent_bexp Heq H₁₃) in H.
    rewrite H in H₈. discriminate H₈.
  - rewrite (noninterferent_bexp Heq H₁₃) in H.
    rewrite H in H₈. discriminate H₈.
  - f_equal. eapply IHHeval1; eassumption.
  - eapply IHHeval1; eauto. repeat constructor; eassumption.
  - (* NEW CASE: ARead *)
    f_equal. f_equal. eapply noninterferent_aexp; eassumption.
  - (* NEW CASE: AWrite *)
    f_equal. f_equal. eapply noninterferent_aexp; eassumption.
Qed.

Speculative constant-time

This part is based on the "Spectre Declassified" paper from IEEE SP 2023, just in simplified form.

The observations are the same as above, so we can just reuse them.

Print observation.

We additionally add adversary provided directions to our semantics, which control speculation behavior.

Inductive direction :=
| DStep
| DForce
| DLoad (a : string) (i : nat)
| DStore (a : string) (i : nat).

Definition dirs := list direction.

Reserved Notation
         "'<(' st , ast , b , ds ')>' '=[' c ']=>' '<(' stt , astt , bb , os ')>'"
         (at level 40, c custom com at level 99,
          st constr, ast constr, stt constr, astt constr at next level).

Inductive spec_eval : com → state → astate → bool → dirs →
                             state → astate → bool → obs → Prop :=
  | Spec_Skip : ∀ st ast b,
      <(st , ast , b , [])> =[ skip ]=> <(st , ast , b , [])>
  | Spec_Asgn : ∀ st ast b e n x,
      aeval st e = n →
      <(st , ast , b , [])> =[ x := e ]=> <(x !-> n; st , ast , b , [])>
  | Spec_Seq : ∀ c₁ c₂ st ast b st' ast' b' st'' ast'' b'' os₁ os₂ ds₁ ds₂,
      <(st , ast , b , ds₁ )> =[ c₁ ]=> <(st', ast', b', os₁ )> →
      <(st', ast', b', ds₂ )> =[ c₂ ]=> <(st'', ast'', b'', os₂ )> →
      <(st , ast , b , ds₁ ++ds₂ )> =[ c₁ ; c₂ ]=> <(st'', ast'', b'', os₂ ++os₁ )>
  | Spec_If : ∀ st ast b st' ast' b' be c₁ c₂ os₁ ds,
      <(st , ast , b , ds )> =[ match beval st be with
                       | true ⇒ c₁
                       | false ⇒ c₂ end ]=> <(st', ast', b', os₁ )> →
      <(st , ast , b , DStep :: ds )> =[ if be then c₁ else c₂ end ]=>
        <(st', ast', b', os₁ ++ [OBranch (beval st be)])>
  | Spec_If_F : ∀ st ast b st' ast' b' be c₁ c₂ os₁ ds,
      <(st , ast , true , ds )> =[ match beval st be with
                       | true ⇒ c₂ (* <-- branches swapped *)
                       | false ⇒ c₁ end ]=> <(st', ast', b', os₁ )> →
      <(st , ast , b , DForce :: ds )> =[ if be then c₁ else c₂ end ]=>
        <(st', ast', b', os₁ ++ [OBranch (beval st be)])>
  | Spec_While : ∀ be st ast b ds st' ast' b' os c,
      <(st , ast , b , ds )> =[ if be then c ; while be do c end else skip end ]=>
        <(st', ast', b', os )> →
      <(st , ast , b , ds )> =[ while be do c end ]=> <(st', ast', b', os )>
  | Spec_ARead : ∀ st ast b x a ie i,
      aeval st ie = i →
      i < length (ast a) →
      <(st , ast , b , [DStep ])> =[ x <- a [[ie ]] ]=>
        <(x !-> nth i (ast a) 0; st , ast , b , [OARead a i ])>
  | Spec_ARead_U : ∀ st ast x a ie i a' i',
      aeval st ie = i →
      i ≥ length (ast a) →
      i' < length (ast a') →
      <(st , ast , true , [DLoad a' i'])> =[ x <- a [[ie ]] ]=>
        <(x !-> nth i' (ast a') 0; st , ast , true , [OARead a i ])>
  | Spec_Write : ∀ st ast b a ie i e n,
      aeval st e = n →
      aeval st ie = i →
      i < length (ast a) →
      <(st , ast , b , [DStep ])> =[ a [ie ] <- e ]=>
        <(st , a !-> upd i (ast a) n; ast , b , [OAWrite a i ])>
  | Spec_Write_U : ∀ st ast a ie i e n a' i',
      aeval st e = n →
      aeval st ie = i →
      i ≥ length (ast a) →
      i' < length (ast a') →
      <(st , ast , true , [DStore a' i'])> =[ a [ie ] <- e ]=>
        <(st , a' !-> upd i' (ast a') n; ast , true , [OAWrite a i ])>

  where "<( st , ast , b , ds )> =[ c ]=> <( stt , astt , bb , os )>" :=
    (spec_eval c st ast b ds stt astt bb os).

Speculative constant-time security definition

Definition spec_ct_secure P PA c :=
  ∀ st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' b₁' b₂' os₁ os₂ ds,
    pub_equiv P st₁ st₂ →
    pub_equiv PA ast1 ast2 →
    <(st₁ , ast1 , false , ds )> =[ c ]=> <(st₁', ast1', b₁', os₁ )> →
    <(st₂ , ast2 , false , ds )> =[ c ]=> <(st₂', ast2', b₂', os₂ )> →
    os₁ = os₂.

Example constant-time program that is insecure under speculative execution.

Definition spec_insecure_prog :=
  <{{ if Z ≤ 0 then
        X <- AP [[Z ]];
        if X ≤ 5 then Y := 1 else Y := 0 end
      else skip end }}> .

Example spec_insecure_prog_is_ct_and_spec_insecure :
∃ P PA ,
  P ;; PA ⊢ct - spec_insecure_prog ∧ ¬ (spec_ct_secure P PA spec_insecure_prog ) .
Proof.
  ∃ (X!-> public; Y!-> public; Z!-> public; _ !-> secret).
  ∃ (AP!-> public; AS!-> secret; _ !-> public).
  split; unfold spec_insecure_prog.
  - repeat econstructor;
    replace (public) with (join public public) at 4 by reflexivity;
    repeat constructor.
  - intros H.
    remember (Z!-> 1; _ !-> 0) as st.
    remember (AP!-> [1]; AS!-> [1;3]; _ !-> []) as ast1.
    remember (AP!-> [1]; AS!-> [1;7]; _ !-> []) as ast2.
    remember (DForce :: ([DLoad "AS" 1] ++ [DStep ])) as ds.
    remember (([OBranch true ] ++ [OARead "AP" 1]) ++ [OBranch false ]) as os₁.
    remember (([OBranch false ] ++ [OARead "AP" 1])++ [OBranch false ]) as os₂.
    assert (Heval1:
    <(st, ast1, false , ds )> =[ spec_insecure_prog ]=> <( Y!-> 1; X!-> 3; st, ast1, true , os₁)>).
    { unfold spec_insecure_prog; subst.
      eapply Spec_If_F. eapply Spec_Seq.
      - eapply Spec_ARead_U; simpl; eauto.
      - replace ([OBranch true ]) with ([] ++ [OBranch true ]) by reflexivity.
        eapply Spec_If; simpl. eapply Spec_Asgn; eauto. }
    assert (Heval2:
      <(st, ast2, false , ds )> =[ spec_insecure_prog ]=> <( Y!-> 0; X!-> 7; st, ast2, true , os₂)>).
      { unfold spec_insecure_prog; subst.
        eapply Spec_If_F. eapply Spec_Seq.
        - eapply Spec_ARead_U; simpl; eauto.
        - replace ([OBranch false ]) with ([] ++ [OBranch false ]) by reflexivity.
          eapply Spec_If; simpl. eapply Spec_Asgn; eauto. }
    subst. eapply H in Heval1.
    + eapply Heval1 in Heval2. inversion Heval2.
    + eapply pub_equiv_refl.
    + intros x Hx. destruct (String.eqb_spec "AP" x) as [HeqAP | HneqAP];
      destruct (String.eqb_spec "AS" x) as [HeqAS | HneqAS].
      × subst. do 2 rewrite t_update_eq. reflexivity.
      × subst. do 2 rewrite t_update_eq. reflexivity.
      × subst. rewrite t_update_neq in Hx; [| assumption].
        rewrite t_update_eq in Hx. discriminate.
      × do 4 (rewrite t_update_neq; [| assumption]). reflexivity.
Qed.

Lemma speculation_bit_monotonic : ∀ c s a b ds s' a' b' os,
  <(s , a , b , ds )> =[ c ]=> <(s', a', b', os )> →
  b = true →
  b' = true.
Proof. intros c s a b ds s' a' b' os Heval Hb. induction Heval; eauto. Qed.

Lemma speculation_needs_force : ∀ c s a b ds s' a' b' os,
  <(s , a , b , ds )> =[ c ]=> <(s', a', b', os )> →
  b = false →
  b' = true →
  In DForce ds.
Proof.
  intros c s a b ds s' a' b' os Heval Hb Hb'.
  induction Heval; subst; simpl; eauto; try discriminate.
  apply in_or_app. destruct b'; eauto.
Qed.

Lemma unsafe_access_needs_speculation : ∀ c s a b ds s' a' b' os ax i,
  <(s , a , b , ds )> =[ c ]=> <(s', a', b', os )> →
  In (DLoad ax i) ds ∨ In (DStore ax i) ds →
  b = true ∨ In DForce ds.
Proof.
  intros c s a b ds s' a' b' os ax i Heval Hin.
  induction Heval; simpl in *; try tauto; try (firstorder; discriminate).
  - destruct Hin as [Hin | Hin].
    + apply in_app_or in Hin. destruct Hin as [Hin | Hin].
      × specialize (IHHeval1 (or_introl _ Hin)). destruct IHHeval1; try tauto.
        right. apply in_or_app. tauto.
      × specialize (IHHeval2 (or_introl _ Hin)). destruct IHHeval2; try tauto.
        { destruct b eqn:Eq; try tauto.
          (* slightly more interesting case, the rest very boring *)
          right. apply speculation_needs_force in Heval1; [| reflexivity|assumption].
          apply in_or_app. tauto. }
        { right. apply in_or_app. tauto. }
    + (* very symmetric, mostly copy paste *)
      apply in_app_or in Hin. destruct Hin as [Hin | Hin].
      × specialize (IHHeval1 (or_intror _ Hin)). destruct IHHeval1; try tauto.
        right. apply in_or_app. tauto.
      × specialize (IHHeval2 (or_intror _ Hin)). destruct IHHeval2; try tauto.
        { destruct b eqn:Eq; try tauto.
          right. apply speculation_needs_force in Heval1; [| reflexivity|assumption].
          apply in_or_app. tauto. }
        { right. apply in_or_app. tauto. }
Qed.

We can recover sequential execution from spec_eval if there is no speculation, so all directives are DStep and speculation flag starts false.

Definition seq_spec_eval (c :com) (st :state) (ast :astate)
    (st' :state) (ast' :astate) (os :obs) : Prop :=
  ∃ ds , (∀ d, In d ds → d = DStep ) ∧
    <(st , ast , false , ds )> =[ c ]=> <(st', ast', false , os )>.

(* Sequential execution is equivalent to constant-time evaluation, i.e. cteval. *)

Lemma cteval_equiv_seq_spec_eval : ∀ c st ast st' ast' os,
  seq_spec_eval c st ast st' ast' os ↔ <(st , ast )> =[ c ]=> <(st', ast', os )> .
Proof.
  intros c st ast st' ast' os. unfold seq_spec_eval. split; intros H.
  - (* -> *)
    destruct H as [ds [Hstep Heval] ].
    induction Heval; try (now econstructor; eauto).
    + (* Spec_Seq *) eapply CTE_Seq.
      × eapply IHHeval1. intros d HdIn.
        assert (L: In d ds₁ ∨ In d ds₂) by (left; assumption).
        eapply in_or_app in L. eapply Hstep in L. assumption.
      × eapply IHHeval2. intros d HdIn.
        assert (L: In d ds₁ ∨ In d ds₂) by (right; assumption).
        eapply in_or_app in L. eapply Hstep in L. assumption.
    + (* Spec_If *) destruct (beval st be) eqn:Eqbe.
      × eapply CTE_IfTrue; [assumption |].
        eapply IHHeval. intros d HdIn.
        apply (in_cons DStep d) in HdIn. apply Hstep in HdIn. assumption.
      × eapply CTE_IfFalse; [assumption |].
        eapply IHHeval. intros d HdIn.
        apply (in_cons DStep d) in HdIn. apply Hstep in HdIn. assumption.
    + (* Spec_IF_F; contra *) exfalso.
      assert (L: ~(DForce = DStep )) by discriminate. apply L.
      apply (Hstep DForce). apply in_eq.
    + (* Spec_ARead_U; contra *) exfalso.
      assert (L: ~(DLoad a' i' = DStep )) by discriminate. apply L.
      apply (Hstep (DLoad a' i')). apply in_eq.
    + (* Spec_AWrite_U; contra *) exfalso.
      assert (L: ~(DStore a' i' = DStep )) by discriminate. apply L.
      apply (Hstep (DStore a' i')). apply in_eq.
  - (* <- *)
    induction H.
    + (* CTE_Skip *)
      ∃ []; split; [| eapply Spec_Skip].
      simpl. intros d Contra; destruct Contra.
    + (* CTE_Asgn *)
      ∃ []; split; [| eapply Spec_Asgn; assumption].
      simpl. intros d Contra; destruct Contra.
    + (* CTE_Seq *)
      destruct IHcteval1 as [ds₁ [Hds1 Heval1] ].
      destruct IHcteval2 as [ds₂ [Hds2 Heval2] ].
      ∃ (ds₁ ++ ds₂). split; [| eapply Spec_Seq; eassumption].
      intros d HdIn. apply in_app_or in HdIn. destruct HdIn as [Hin1 | Hin2].
      × apply Hds1 in Hin1. assumption.
      × apply Hds2 in Hin2. assumption.
    + (* CTE_IfTrue *)
      destruct IHcteval as [ds [Hds Heval] ]. ∃ (DStep :: ds). split.
      × intros d HdIn. apply in_inv in HdIn.
        destruct HdIn as [Heq | HIn]; [symmetry; assumption | apply Hds; assumption].
      × rewrite <- H. eapply Spec_If. rewrite H; simpl. assumption.
    + (* CTE_IfFalse *)
      destruct IHcteval as [ds [Hds Heval] ]. ∃ (DStep :: ds). split.
      × intros d HdIn. apply in_inv in HdIn.
        destruct HdIn as [Heq | HIn]; [symmetry; assumption | apply Hds; assumption].
      × rewrite <- H. eapply Spec_If. rewrite H; simpl. assumption.
    + (* CTE_While *)
      destruct IHcteval as [ds [Hds Heval] ]. ∃ ds.
      split; [assumption |]. eapply Spec_While; assumption.
    + (* CTE_ARead *)
      ∃ [DStep ]. split.
      × simpl. intros d HdIn. destruct HdIn as [Heq | Contra]; [| destruct Contra].
        symmetry. assumption.
      × eapply Spec_ARead; assumption.
    + (* CTE_AWrite *)
      ∃ [DStep ]. split.
      × simpl. intros d HdIn. destruct HdIn as [Heq | Contra]; [| destruct Contra].
        symmetry. assumption.
      × eapply Spec_Write; assumption.
Qed.

Lemma ct_well_typed_seq_spec_eval_ct_secure :
  ∀ P PA c st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' os₁ os₂,
    P ;; PA ⊢ct - c →
    pub_equiv P st₁ st₂ →
    pub_equiv PA ast1 ast2 →
    seq_spec_eval c st₁ ast1 st₁' ast1' os₁ →
    seq_spec_eval c st₂ ast2 st₂' ast2' os₂ →
    os₁ = os₂.
Proof.
  intros P PA c st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' os₁ os₂ Hwt
    HP HPA Heval1 Heval2.
  apply cteval_equiv_seq_spec_eval in Heval1, Heval2.
  apply ct_well_typed_ct_secure in Hwt. eapply Hwt; eauto.
Qed.

Selective SLH transformation that we will show enforces speculative constant-time security.

Fixpoint sel_slh (P:pub_vars) (c:com) :=
  (match c with
  | <{{skip }}> ⇒ <{{skip }}>
  | <{{x := e}}> ⇒ <{{x := e}}>
  | <{{c₁; c₂}}> ⇒ <{{ sel_slh P c₁; sel_slh P c₂}}>
  | <{{if be then c₁ else c₂ end }}> ⇒
      <{{if be then "b" := (be ? "b" : 1); sel_slh P c₁
               else "b" := (be ? 1 : "b"); sel_slh P c₂ end }}>
  | <{{while be do c end }}> ⇒
      <{{while be do "b" := (be ? "b" : 1); sel_slh P c end ;
         "b" := (be ? 1 : "b")}}>
  | <{{x <- a[[i]]}}> ⇒
      if P x then <{{x <- a[[i]]; x := ("b" = 1) ? 0 : x}}>
             else <{{x <- a[[i]]}}>
  | <{{a[i] <- e}}> ⇒ <{{a[i] <- e}}>
  end)%string.

To prove this transformation secure, Spectre Declassified uses an idealized semantics, capturing selective speculative load hardening more abstractly.

Reserved Notation
         "P '⊢' '<(' st , ast , b , ds ')>' '=[' c ']=>' '<(' stt , astt , bb , os ')>'"
         (at level 40, c custom com at level 99,
          st constr, ast constr, stt constr, astt constr at next level).

Inductive ideal_eval (P:pub_vars) :
    com → state → astate → bool → dirs →
           state → astate → bool → obs → Prop :=
  | Ideal_Skip : ∀ st ast b,
      P ⊢ <(st , ast , b , [])> =[ skip ]=> <(st , ast , b , [])>
  | Ideal_Asgn : ∀ st ast b e n x,
      aeval st e = n →
      P ⊢ <(st , ast , b , [])> =[ x := e ]=> <(x !-> n; st , ast , b , [])>
  | Ideal_Seq : ∀ c₁ c₂ st ast b st' ast' b' st'' ast'' b'' os₁ os₂ ds₁ ds₂,
      P ⊢ <(st , ast , b , ds₁ )> =[ c₁ ]=> <(st', ast', b', os₁ )> →
      P ⊢ <(st', ast', b', ds₂ )> =[ c₂ ]=> <(st'', ast'', b'', os₂ )> →
      P ⊢ <(st , ast , b , ds₁ ++ds₂ )> =[ c₁ ; c₂ ]=> <(st'', ast'', b'', os₂ ++os₁ )>
  | Ideal_If : ∀ st ast b st' ast' b' be c₁ c₂ os₁ ds,
      P ⊢ <(st , ast , b , ds )> =[ match beval st be with
                                 | true ⇒ c₁
                                 | false ⇒ c₂ end ]=> <(st', ast', b', os₁ )> →
      P ⊢ <(st , ast , b , DStep :: ds )> =[ if be then c₁ else c₂ end ]=>
        <(st', ast', b', os₁ ++[OBranch (beval st be)])>
  | Ideal_If_F : ∀ st ast b st' ast' b' be c₁ c₂ os₁ ds,
      P ⊢ <(st , ast , true , ds )> =[ match beval st be with
                                    | true ⇒ c₂ (* <-- branches swapped *)
                                    | false ⇒ c₁ end ]=> <(st', ast', b', os₁ )> →
      P ⊢ <(st , ast , b , DForce :: ds )> =[ if be then c₁ else c₂ end ]=>
        <(st', ast', b', os₁ ++[OBranch (beval st be)])>
  | Ideal_While : ∀ be st ast b ds st' ast' b' os c,
      P ⊢ <(st , ast , b , ds )> =[ if be then c ; while be do c end else skip end ]=>
        <(st', ast', b', os )> →
      P ⊢ <(st , ast , b , ds )> =[ while be do c end ]=> <(st', ast', b', os )>
  | Ideal_ARead : ∀ st ast b x a ie i,
      aeval st ie = i →
      i < length (ast a) →
      P ⊢ <(st , ast , b , [DStep ])> =[ x <- a [[ie ]] ]=>
        <(x !-> if b && P x then 0 else nth i (ast a) 0; st , ast , b , [OARead a i ])>
  | Ideal_ARead_U : ∀ st ast x a ie i a' i',
      aeval st ie = i →
      i ≥ length (ast a) →
      i' < length (ast a') →
      P ⊢ <(st , ast , true , [DLoad a' i'])> =[ x <- a [[ie ]] ]=>
        <(x !-> if P x then 0 else nth i' (ast a') 0; st , ast , true , [OARead a i ])>
  | Ideal_Write : ∀ st ast b a ie i e n,
      aeval st e = n →
      aeval st ie = i →
      i < length (ast a) →
      P ⊢ <(st , ast , b , [DStep ])> =[ a [ie ] <- e ]=>
        <(st , a !-> upd i (ast a) n; ast , b , [OAWrite a i ])>
  | Ideal_Write_U : ∀ st ast a ie i e n a' i',
      aeval st e = n →
      aeval st ie = i →
      i ≥ length (ast a) →
      i' < length (ast a') →
      P ⊢ <(st , ast , true , [DStore a' i'])> =[ a [ie ] <- e ]=>
        <(st , a' !-> upd i' (ast a') n; ast , true , [OAWrite a i ])>

  where "P ⊢ <( st , ast , b , ds )> =[ c ]=> <( stt , astt , bb , os )>" :=
    (ideal_eval P c st ast b ds stt astt bb os).

(* We show that on sequential executions this is equivalent to seq_spec_eval *)

Lemma seq_eval_ideal_eval_ind1 : ∀ P c s a b ds s' a' b' os,
  (∀ d : direction, In d ds → d = DStep ) →
  <( s , a , b , ds )> =[ c ]=> <( s', a', b', os )> →
  b = false →
  b' = false →
  P ⊢ <( s , a , b , ds )> =[ c ]=> <( s', a', b', os )>.
Proof.
  intros P c s a b ds s' a' b' os Hds H Eb Eb'.
  induction H; try constructor; eauto.
  - (* Seq *)
    assert(b' = false).
    { destruct b' eqn:Eqb'; [| reflexivity].
      apply speculation_needs_force in H; try tauto.
      assert (contra : DForce = DStep).
      { apply Hds. apply in_or_app. left. assumption. }
      inversion contra. }
    eapply Ideal_Seq.
    × apply IHspec_eval1; eauto using in_or_app.
    × apply IHspec_eval2; eauto using in_or_app.
  - (* If *) simpl in Hds; eauto.
  - (* If_F *) simpl in Hds.
    assert (contra : DForce = DStep). { apply Hds. left. reflexivity. }
    inversion contra.
  - (* ARead *)
    destruct b eqn:Eqb; [discriminate |].
    replace (x !-> nth i (ast a) 0; st)
      with (x !-> if b && P x then 0 else nth i (ast a) 0; st)
        by (rewrite Eqb; simpl; reflexivity).
    rewrite <- Eqb. eapply Ideal_ARead; eauto.
  - (* AREad_U *) discriminate.
Qed.

Lemma speculation_needs_force_ideal : ∀ P c s a b ds s' a' b' os,
  P ⊢ <(s , a , b , ds )> =[ c ]=> <(s', a', b', os )> →
  b = false →
  b' = true →
  In DForce ds.
Proof.
  intros P c s a b ds s' a' b' os Heval Hb Hb'.
  induction Heval; subst; simpl; eauto; try discriminate.
  apply in_or_app. destruct b'; eauto.
Qed.

Lemma seq_eval_ideal_eval_ind2 : ∀ P c s a b ds s' a' b' os,
  (∀ d : direction, In d ds → d = DStep ) →
  P ⊢ <( s , a , b , ds )> =[ c ]=> <( s', a', b', os )> →
  b = false →
  b' = false →
  <( s , a , b , ds )> =[ c ]=> <( s', a', b', os )>.
Proof. (* proof really the same as gen1 *)
  intros P c s a b ds s' a' b' os Hds H Eb Eb'.
  induction H; try constructor; eauto.
  - (* Seq *)
    assert(b' = false).
    { destruct b' eqn:Eqb'; [| reflexivity].
      apply speculation_needs_force_ideal in H; try tauto.
      assert (contra : DForce = DStep).
      { apply Hds. apply in_or_app. left. assumption. }
      inversion contra. }
    eapply Spec_Seq.
    × apply IHideal_eval1; eauto using in_or_app.
    × apply IHideal_eval2; eauto using in_or_app.
  - (* IF *) simpl in Hds; eauto.
  - (* If_F *) simpl in Hds.
    assert (contra : DForce = DStep). { apply Hds. left. reflexivity. }
    inversion contra.
  - (* ARead *)
    destruct b eqn:Eqb; [discriminate |]; simpl.
    eapply Spec_ARead; eauto.
  - discriminate.
Qed.

Definition seq_ideal_eval (P:pub_vars) (c:com) (s:state) (a:astate)
    (s':state) (a':astate) (os:obs) : Prop :=
  ∃ ds , (∀ d, In d ds → d = DStep ) ∧
    P ⊢ <(s , a , false , ds )> =[ c ]=> <(s', a', false , os )>.

Lemma seq_spec_eval_ideal_eval : ∀ P c s a s' a' os,
  seq_spec_eval c s a s' a' os ↔
  seq_ideal_eval P c s a s' a' os.
Proof.
  intros P c s a s' a' os. unfold seq_spec_eval, seq_ideal_eval.
  split; intros [ds [Hds H] ]; ∃ ds; (split; [ apply Hds |]).
  - apply seq_eval_ideal_eval_ind1; eauto.
  - eapply seq_eval_ideal_eval_ind2; eauto.
Qed.

Let's now prove that the idealized semantics does enforce speculative constant-time

Definition prefix {X:Type} (xs ys : list X) : Prop :=
∃ zs , xs ++ zs = ys.

Lemma prefix_refl : ∀ {X:Type} {ds : list X},
prefix ds ds.
Proof. intros X ds. ∃ []. apply app_nil_r. Qed.

Lemma prefix_nil : ∀ {X:Type} (ds : list X),
prefix [] ds.
Proof. intros X ds. unfold prefix. eexists. simpl. reflexivity. Qed.

Lemma prefix_heads_and_tails : ∀ {X:Type} (h₁ h₂ : X) (t₁ t₂ : list X),
  prefix (h₁ ::t₁) (h₂ ::t₂) → h₁ = h₂ ∧ prefix t₁ t₂.
Proof.
  intros X h₁ h₂ t₁ t₂. unfold prefix. intros Hpre.
  destruct Hpre as [zs Hpre]; simpl in Hpre.
  inversion Hpre; subst. eauto.
Qed.

Lemma prefix_heads : ∀ {X:Type} (h₁ h₂ : X) (t₁ t₂ : list X),
prefix (h₁ ::t₁) (h₂ ::t₂) → h₁ = h₂.
Proof.
intros X h₁ h₂ t₁ t₂ H. apply prefix_heads_and_tails in H; tauto.
Qed.

Lemma prefix_or_heads : ∀ {X:Type} (x y : X) (xs ys : list X),
  prefix (x :: xs) (y :: ys) ∨ prefix (y :: ys) (x :: xs) →
  x = y.
Proof.
  intros X x y xs ys H.
  destruct H as [H | H]; apply prefix_heads in H; congruence.
Qed.

Lemma prefix_cons : ∀ {X:Type} (d :X) (ds₁ ds₂: list X),
prefix ds₁ ds₂ ↔
prefix (d ::ds₁) (d ::ds₂).
Proof.
  intros X d ds₁ ds₂. split; [unfold prefix| ]; intros H.
  - destruct H; subst.
    eexists; simpl; eauto.
  - apply prefix_heads_and_tails in H. destruct H as [_ H]. assumption.
Qed.

Lemma prefix_app : ∀ {X:Type} {ds₁ ds₂ ds₀ ds₃ : list X},
  prefix (ds₁ ++ ds₂) (ds₀ ++ ds₃) →
  prefix ds₁ ds₀ ∨ prefix ds₀ ds₁.
Proof.
  intros X ds₁. induction ds₁ as [| d₁ ds₁' IH]; intros ds₂ ds₀ ds₃ H.
  - left. apply prefix_nil.
  - destruct ds₀ as [| d₀ ds₀'] eqn:D₀.
    + right. apply prefix_nil.
    + simpl in H; apply prefix_heads_and_tails in H.
      destruct H as [Heq Hpre]; subst.
      apply IH in Hpre; destruct Hpre; [left | right];
      apply prefix_cons; assumption.
Qed.

Lemma prefix_append_front : ∀ {X:Type} {ds₁ ds₂ ds₃ : list X},
  prefix (ds₁ ++ ds₂) (ds₁ ++ ds₃) →
  prefix ds₂ ds₃.
Proof.
  intros X ds₁. induction ds₁ as [| d₁ ds₁' IH]; intros ds₂ ds₃ H.
  - auto.
  - simpl in H; apply prefix_cons in H. apply IH in H. assumption.
Qed.

Lemma app_eq_prefix : ∀ {X:Type} {ds₁ ds₂ ds₁' ds₂' : list X},
  ds₁ ++ ds₂ = ds₁' ++ ds₂' →
  prefix ds₁ ds₁' ∨ prefix ds₁' ds₁.
Proof.
  intros X ds₁. induction ds₁ as [| h₁ t₁ IH]; intros ds₂ ds₁' ds₂' H.
  - left. apply prefix_nil.
  - destruct ds₁' as [| h₁' t₁'] eqn:D₁'.
    + right. apply prefix_nil.
    + simpl in H; inversion H; subst.
      apply IH in H₂. destruct H₂ as [HL | HR];
      [left | right]; apply prefix_cons; auto.
Qed.

Ltac split4 := split; [|split; [| split] ].

Lemma pub_equiv_update_public : ∀ P {A:Type}
    (t₁ t₂ : total_map A) (X :string) (a₁ a₂ :A),
  pub_equiv P t₁ t₂ →
  P X = public →
  a₁ = a₂ →
  pub_equiv P (X!-> a₁; t₁) (X!-> a₂; t₂).
Proof.
  intros P A t₁ t₂ X a₁ a₂ Hequiv Hpub Ha1a₂ x Hx.
  destruct (String.eqb_spec X x) as [Heq | Hneq].
  - subst. do 2 rewrite t_update_eq. reflexivity.
  - do 2 (rewrite t_update_neq;[| auto]). eapply Hequiv; eauto.
Qed.

Lemma pub_equiv_update_secret : ∀ P {A:Type}
    (t₁ t₂ : total_map A) (X :string) (a₁ a₂ :A),
  pub_equiv P t₁ t₂ →
  P X = secret →
  pub_equiv P (X!-> a₁; t₁) (X!-> a₂; t₂).
Proof.
  intros P A t₁ t₂ X a₁ a₂ Hequiv Hsec x Hx.
  destruct (String.eqb_spec X x) as [Heq | Hneq].
  - subst. rewrite Hsec in Hx. discriminate.
  - do 2 (rewrite t_update_neq;[| auto]). eapply Hequiv; eauto.
Qed.

Lemma ct_well_typed_ideal_noninterferent_general :
  ∀ P PA c st₁ st₂ ast1 ast2 b st₁' st₂' ast1' ast2' b₁' b₂' os₁ os₂ ds₁ ds₂,
    P ;; PA ⊢ct - c →
    pub_equiv P st₁ st₂ →
    (b = false → pub_equiv PA ast1 ast2 ) →
    (prefix ds₁ ds₂ ∨ prefix ds₂ ds₁ ) → (* <- interesting generalization *)
    P ⊢ <(st₁ , ast1 , b , ds₁ )> =[ c ]=> <(st₁', ast1', b₁', os₁ )> →
    P ⊢ <(st₂ , ast2 , b , ds₂ )> =[ c ]=> <(st₂', ast2', b₂', os₂ )> →
    pub_equiv P st₁' st₂' ∧ b₁' = b₂' ∧
      (b₁' = false → pub_equiv PA ast1' ast2') ∧
      ds₁ = ds₂. (* <- interesting generalization *)
Proof.
  intros P PA c st₁ st₂ ast1 ast2 b st₁' st₂' ast1' ast2' b₁' b₂' os₁ os₂ ds₁ ds₂
    Hwt Heq Haeq Hds Heval1 Heval2.
  generalize dependent st₂'. generalize dependent st₂.
  generalize dependent ast2'. generalize dependent ast2.
  generalize dependent os₂. generalize dependent b₂'.
  generalize dependent ds₂.
  induction Heval1; intros ds2X Hds b₂' os₂' a₂ Haeq a₂' s₂ Heq s₂' Heval2;
    inversion Heval2; inversion Hwt; subst.
  - (* Skip *) auto.
  - (* Asgn *) split4; auto.
    destruct (P x) eqn:EqPx.
    + eapply pub_equiv_update_public; eauto.
      eapply noninterferent_aexp; eauto.
      destruct l; [auto | simpl in H₁₄; discriminate].
    + eapply pub_equiv_update_secret; eauto.
  - (* Seq *)
    destruct Hds as [Hpre | Hpre]; apply prefix_app in Hpre as Hds1.
    + (* prefix (ds₁ ++ ds₂) (ds₀ ++ ds₃) *)
      eapply IHHeval1_1 in Hds1; eauto.
      destruct Hds1 as [ Hstates [Hbits [Hastates Hdirections] ] ]. subst.
      eapply prefix_append_front in Hpre as Hds2.
      eapply IHHeval1_2 in H₁₄; eauto. firstorder. subst. reflexivity.
    + (* prefix (ds₀ ++ ds₃) (ds₁ ++ ds₂) *)
      eapply IHHeval1_1 with (ds₂:=ds₀) in H₁₃; eauto; [| tauto].
      destruct H₁₃ as [ Hstates [Hbits [Hastates Hdirections] ] ]. subst.
      eapply prefix_append_front in Hpre as Hds2.
      eapply IHHeval1_2 in H₁₄; eauto. firstorder; subst; reflexivity.
  - (* If *)
    assert(G : P ;; PA ⊢ct - (if beval st be then c₁ else c₂)).
    { destruct (beval st be); assumption. }
    assert(Gds : prefix ds ds₀ ∨ prefix ds₀ ds).
    { destruct Hds as [Hds | Hds]; apply prefix_cons in Hds; tauto. }
    erewrite noninterferent_bexp in H₁₀.
    + specialize (IHHeval1 G _ Gds _ _ _ Haeq _ _ Heq _ H₁₀).
      firstorder; congruence.
    + apply pub_equiv_sym. eassumption.
    + eassumption.
  - (* IF; contra *)
    apply prefix_or_heads in Hds; inversion Hds.
  - (* IF; contra *)
     apply prefix_or_heads in Hds; inversion Hds.
  - (* If_F; analog to If *)
    assert(G : P ;; PA ⊢ct - (if beval st be then c₂ else c₁)).
    { destruct (beval st be); assumption. }
    assert(Gds : prefix ds ds₀ ∨ prefix ds₀ ds).
    { destruct Hds as [Hds | Hds]; apply prefix_cons in Hds; tauto. }
    erewrite noninterferent_bexp in H₁₀.
    + assert(GG: true = false → pub_equiv PA ast a₂). (* <- only difference *)
      { intro Hc. discriminate. }
      specialize (IHHeval1 G _ Gds _ _ _ GG _ _ Heq _ H₁₀).
      firstorder; congruence.
    + apply pub_equiv_sym. eassumption.
    + eassumption.
  - (* While *) eapply IHHeval1; try eassumption. repeat constructor; eassumption.
  - (* ARead *) split4; eauto.
    destruct (P x) eqn:EqPx; simpl.
    + eapply pub_equiv_update_public; eauto.
      destruct b₂' eqn:Eqb2'; simpl; [reflexivity |].
      unfold can_flow in H₁₈. eapply orb_true_iff in H₁₈.
      destruct H₁₈ as [Hapub | Contra]; [| simpl in Contra; discriminate].
      eapply Haeq in Hapub; [| reflexivity]. rewrite Hapub.
      eapply noninterferent_aexp in Heq; eauto. rewrite Heq.
      reflexivity.
    + eapply pub_equiv_update_secret; eauto.
  - (* ARead_U *) split4; eauto.
    + destruct (P x) eqn:EqPx.
      × simpl. eapply pub_equiv_update_public; eauto.
      × eapply pub_equiv_update_secret; eauto.
    + apply prefix_or_heads in Hds. inversion Hds.
  - (* ARead *) split4; eauto.
    + destruct (P x) eqn:EqPx.
      × eapply pub_equiv_update_public; eauto.
      × eapply pub_equiv_update_secret; eauto.
    + apply prefix_or_heads in Hds. inversion Hds.
  - (* Aread_U *) split4; eauto.
    + destruct (P x) eqn:EqPx.
      × eapply pub_equiv_update_public; eauto.
      × eapply pub_equiv_update_secret; eauto.
    + apply prefix_or_heads in Hds. inversion Hds. reflexivity.
  - (* Write *) split4; eauto. intro Hb₂'.
    destruct (PA a) eqn:EqPAa.
    + eapply pub_equiv_update_public; eauto.
      destruct l eqn:Eql.
      × eapply noninterferent_aexp in H₁₉, H₂₀; eauto. rewrite H₁₉, H₂₀.
        apply Haeq in Hb₂'. apply Hb₂' in EqPAa. rewrite EqPAa. reflexivity.
      × simpl in H₂₁. discriminate.
    + eapply pub_equiv_update_secret; eauto.
  - (* Write_U; contra *) apply prefix_or_heads in Hds. inversion Hds.
  - (* Write; contra *) apply prefix_or_heads in Hds. inversion Hds.
  - (* Write_U; contra *) split4; eauto.
    + intro contra. discriminate contra.
    + apply prefix_or_heads in Hds. inversion Hds. reflexivity.
Qed.

Lemma ct_well_typed_ideal_noninterferent :
  ∀ P PA c s₁ s₂ a₁ a₂ b s₁' s₂' a₁' a₂' b₁' b₂' os₁ os₂ ds,
    P ;; PA ⊢ct - c →
    pub_equiv P s₁ s₂ →
    (b = false → pub_equiv PA a₁ a₂ ) →
    P ⊢ <(s₁ , a₁ , b , ds )> =[ c ]=> <(s₁', a₁', b₁', os₁ )> →
    P ⊢ <(s₂ , a₂ , b , ds )> =[ c ]=> <(s₂', a₂', b₂', os₂ )> →
    pub_equiv P s₁' s₂' ∧ b₁' = b₂' ∧ (b₁' = false → pub_equiv PA a₁' a₂').
Proof.
  intros P PA c s₁ s₂ a₁ a₂ b s₁' s₂' a₁' a₂' b₁' b₂' os₁ os₂ ds
    Hwt Heq Haeq Heval1 Heval2.
  eapply ct_well_typed_ideal_noninterferent_general in Heval2; eauto; try tauto.
  left. apply prefix_refl.
Qed.

This corollary (used below) also follows from noninterferent_general

Corollary aux : ∀ P PA s₁ s₂ a₁ a₂ b ds₁ ds₂ c st₁ st₂ ast1 ast2 b₁ b₂ os₁ os₂ ds₁' ds₂',
  ds₂ ++ ds₂' = ds₁ ++ ds₁' →
  P ;; PA ⊢ct - c →
  pub_equiv P s₁ s₂ →
  (b = false → pub_equiv PA a₁ a₂ ) →
  P ⊢ <(s₁ , a₁ , b , ds₁ )> =[ c ]=> <(st₁ , ast1 , b₁ , os₁ )> →
  P ⊢ <(s₂ , a₂ , b , ds₂ )> =[ c ]=> <(st₂ , ast2 , b₂ , os₂ )> →
  ds₁ = ds₂ ∧ ds₁' = ds₂'.
Proof.
  intros P PA s₁ s₂ a₁ a₂ b ds₁ ds₂ c st₁ st₂ ast1 ast2 b₁ b₂ os₁ os₂ ds₁' ds₂'
    Hds Hwt Heq Haeq Heval1 Heval2.
  pose proof Hds as H.
  symmetry in H.
  apply app_eq_prefix in H.
  eapply ct_well_typed_ideal_noninterferent_general in H;
    [ | | | | apply Heval1 | apply Heval2]; try eassumption.
  - destruct H as [ _ [ _ [ _ H] ] ]. subst. split; [reflexivity|].
    apply app_inv_head in Hds. congruence.
Qed.

Theorem ideal_spec_ct_secure :
  ∀ P PA c s₁ s₂ a₁ a₂ b s₁' s₂' a₁' a₂' b₁' b₂' os₁ os₂ ds,
    P ;; PA ⊢ct - c →
    pub_equiv P s₁ s₂ →
    (b = false → pub_equiv PA a₁ a₂ ) →
    P ⊢ <(s₁ , a₁ , b , ds )> =[ c ]=> <(s₁', a₁', b₁', os₁ )> →
    P ⊢ <(s₂ , a₂ , b , ds )> =[ c ]=> <(s₂', a₂', b₂', os₂ )> →
    os₁ = os₂.
Proof.
  intros P PA c s₁ s₂ a₁ a₂ b s₁' s₂' a₁' a₂' b₁' b₂' os₁ os₂ ds
    Hwt Heq Haeq Heval1 Heval2.
  generalize dependent s₂'. generalize dependent s₂.
  generalize dependent a₂'. generalize dependent a₂.
  generalize dependent os₂. generalize dependent b₂'.
  induction Heval1; intros b₂' os₂' a₂ Haeq a₂' s₂ Heq s₂' Heval2;
    inversion Heval2; inversion Hwt; subst.
  - (* Skip *) reflexivity.
  - (* Skip *) reflexivity.
  - (* Seq *) eapply aux in H₁; [| | | | apply Heval1_1 | apply H₅ ]; eauto.
    destruct H₁ as [H₁ H₁']. subst.
    assert(NI₁ : pub_equiv P st' st'0 ∧ b' = b'0 ∧ (b' = false → pub_equiv PA ast' ast'0)).
    { eapply ct_well_typed_ideal_noninterferent; [ | | | eassumption | eassumption]; eauto. }
    destruct NI₁ as [NI1eq [NIb NIaeq] ]. subst.
    erewrite IHHeval1_2; [erewrite IHHeval1_1 | | | |];
      try reflexivity; try eassumption.
  - (* If *) f_equal.
    + eapply IHHeval1; try eassumption; try (destruct (beval st be); eassumption).
      erewrite noninterferent_bexp; eassumption.
    + f_equal. eapply noninterferent_bexp in Heq; [| eassumption].
      rewrite Heq. reflexivity.
  - (*If_F *) f_equal.
    + eapply IHHeval1; try eassumption; try (destruct (beval st be); eassumption).
      × intro contra. discriminate contra.
      × erewrite noninterferent_bexp; eassumption.
    + f_equal. eapply noninterferent_bexp in Heq; [| eassumption].
      rewrite Heq. reflexivity.
  - eapply IHHeval1; eauto. repeat constructor; eassumption.
  - (* ARead *) f_equal. f_equal. eapply noninterferent_aexp; eassumption.
  - (* ARead_U *) f_equal. f_equal. eapply noninterferent_aexp; eassumption.
  - (* AWrite *) f_equal. f_equal. eapply noninterferent_aexp; eassumption.
  - (* AWrite *) f_equal. f_equal. eapply noninterferent_aexp; eassumption.
Qed.

We now prove that the idealized semantics is equivalent to sel_slh transformation (Lemma 6 and the more precise Lemma 7).

All results about sel_slh below assume that the original c doesn't already use the variable "b" needed by the sel_slh translation.

Fixpoint a_unused (x:string) (a:aexp) : Prop :=
  match a with
  | ANum n ⇒ True
  | AId y ⇒ y ≠ x
  | <{a₁ + a₂}>
  | <{a₁ - a₂}>
  | <{a₁ × a₂}> ⇒ a_unused x a₁ ∧ a_unused x a₂
  | <{b ? a₁ : a₂}> ⇒ b_unused x b ∧ a_unused x a₁ ∧ a_unused x a₂
  end
with b_unused (x:string) (b:bexp) : Prop :=
  match b with
  | <{true }>
  | <{false }> ⇒ True
  | <{a₁ = a₂}>
  | <{a₁ ≠ a₂}>
  | <{a₁ ≤ a₂}>
  | <{a₁ > a₂}> ⇒ a_unused x a₁ ∧ a_unused x a₂
  | <{¬ b₁}> ⇒ b_unused x b₁
  | <{b₁ && b₂}> ⇒ b_unused x b₁ ∧ b_unused x b₂
  end.

Fixpoint unused (x:string) (c:com) : Prop :=
  match c with
  | <{{skip }}> ⇒ True
  | <{{y := e}}> ⇒ y ≠ x ∧ a_unused x e
  | <{{c₁; c₂}}> ⇒ unused x c₁ ∧ unused x c₂
  | <{{if be then c₁ else c₂ end }}> ⇒
      b_unused x be ∧ unused x c₁ ∧ unused x c₂
  | <{{while be do c end }}> ⇒ b_unused x be ∧ unused x c
  | <{{y <- a[[i]]}}> ⇒ y ≠ x ∧ a_unused x i
  | <{{a[i] <- e}}> ⇒ a_unused x i ∧ a_unused x e
  end.

Open Scope string_scope.

As a warm-up we prove that sel_slh properly updates the variable "b".

Proving this by induction on com or spec_eval leads to induction hypotheses, that are not strong enough to prove the While or Spec_While case. Therefore we will prove it by induction on the program size (prog_size) of a tupel (c :com) and (ds :dirs).

Fixpoint com_size (c :com) :nat :=
  match c with
  | <{{ c₁; c₂ }}> ⇒ 1 + (com_size c₁) + (com_size c₂)
  | <{{ if be then ct else cf end }}> ⇒ 1 + max (com_size ct) (com_size cf)
  | <{{ while be do cw end }}> ⇒ 3 + (com_size cw)
  | _ ⇒ 1
  end.

Definition prog_size (c :com) (ds :dirs) :nat := com_size c + length ds.

The induction principle on prog_size

Axiom prog_size_ind :
  ∀ P : com → dirs → Prop,
  (∀ c ds,
    ( ∀ c' ds',
      prog_size c' ds' < prog_size c ds →
      P c' ds') → P c ds ) →
  (∀ c ds, P c ds ).

The proof of sel_slh_flag

Lemma prog_size_monotonic: ∀ c₁ ds₁ c₂ ds₂,
  (com_size c₁ < com_size c₂ ∧ length ds₁ ≤ length ds₂ ) ∨
  (com_size c₁ ≤ com_size c₂ ∧ length ds₁ < length ds₂ ) →
  prog_size c₁ ds₁ < prog_size c₂ ds₂.
Proof.
  intros c₁ ds₁ c₂ ds₂ [ [Hcom Hdir] | [Hcom Hdir] ];
  unfold prog_size; lia.
Qed.

Based on the Lemma prog_size_monotonic we can build a tactic to solve the subgoals in the form of prog_size c' ds' < prog_size c ds, which will be produced by prog_size_ind.

Ltac prog_size_auto :=
  try ( apply prog_size_monotonic; left; split; simpl;
        [| repeat rewrite app_length]; lia );
  try ( apply prog_size_monotonic; right; split; simpl;
        [| repeat rewrite app_length]; lia);
  try ( apply prog_size_monotonic; left; split; simpl;
        [auto | repeat rewrite app_length; lia] ).

To properly apply prog_size_ind, we need to state sel_slh_flag as a proposition of type com → dirs → Prop. Therefore we define the following:

Definition sel_slh_flag_prop (c :com) (ds :dirs) :Prop :=
  ∀ P st ast (b:bool) st' ast' (b':bool) os,
  unused "b" c →
  st "b" = (if b then 1 else 0) →
  <(st , ast , b , ds )> =[ sel_slh P c ]=> <(st', ast', b', os )> →
  st' "b" = (if b' then 1 else 0).

Lemma sel_slh_flag : ∀ c ds,
  sel_slh_flag_prop c ds.
Proof.
  eapply prog_size_ind. unfold sel_slh_flag_prop.
  intros c ds IH P st ast b st' ast' b' os Hunused Hstb Heval.
  destruct c; simpl in *; try (now inversion Heval; subst; eauto).
  - (* Asgn *)
    inversion Heval; subst. rewrite t_update_neq; tauto.
  - (* Seq *)
    inversion Heval; subst; clear Heval.
    apply IH in H₁; try tauto.
    + apply IH in H₁₀; try tauto. prog_size_auto.
    + prog_size_auto.
  - (* IF *)
    inversion Heval; subst; clear Heval.
    + (* Spec_If *)
      destruct (beval st be) eqn:Eqnbe.
      × inversion H₁₀; subst; clear H₁₀.
        inversion H₁; subst; clear H₁.
        apply IH in H₁₁; try tauto.
        { prog_size_auto. }
        { rewrite t_update_eq. simpl. rewrite Eqnbe. assumption. }
      × (* analog to true case *)
        inversion H₁₀; subst; clear H₁₀.
        inversion H₁; subst; clear H₁.
        apply IH in H₁₁; try tauto.
        { prog_size_auto. }
        { rewrite t_update_eq. simpl. rewrite Eqnbe. assumption. }
    + (* Spec_If_F; analog to Spec_If case *)
      destruct (beval st be) eqn:Eqnbe.
      × inversion H₁₀; subst; clear H₁₀.
        inversion H₁; subst; clear H₁.
        apply IH in H₁₁; try tauto.
        { prog_size_auto. }
        { rewrite t_update_eq. simpl. rewrite Eqnbe. reflexivity. }
      × inversion H₁₀; subst; clear H₁₀.
        inversion H₁; subst; clear H₁.
        apply IH in H₁₁; try tauto.
        { prog_size_auto. }
        { rewrite t_update_eq. simpl. rewrite Eqnbe. reflexivity. }
  - (* While *)
      inversion Heval; subst; clear Heval.
      inversion H₁; subst; clear H₁.
      inversion H₁₁; subst; clear H₁₁.
      + (* non-speculative *)
        destruct (beval st be) eqn:Eqnbe.
        × inversion H₁₂; subst; clear H₁₂.
          assert(Hwhile: <(st'1, ast'1, b'1, (ds₀ ++ ds₂)%list)>
              =[ sel_slh P <{{while be do c end }}> ]=> <(st', ast', b', (os₂++os₃)%list)> ).
          { simpl. eapply Spec_Seq; eassumption. }
          apply IH in Hwhile; eauto.
          { prog_size_auto. }
          { clear Hwhile; clear H₁₁.
            inversion H₁; subst; clear H₁.
            inversion H₂; subst; clear H₂. simpl in H₁₂.
            apply IH in H₁₂; try tauto.
            - prog_size_auto.
            - rewrite t_update_eq, Eqnbe; simpl. assumption. }
        × inversion H₁₂; subst; clear H₁₂.
          inversion H₁₀; subst; simpl.
          rewrite t_update_eq, Eqnbe; simpl. assumption.
      + (* speculative; analog to non_speculative case *)
        destruct (beval st be) eqn:Eqnbe.
        × inversion H₁₂; subst; clear H₁₂.
          inversion H₁₀; subst; simpl.
          rewrite t_update_eq, Eqnbe; simpl. reflexivity.
        × inversion H₁₂; subst; clear H₁₂.
          assert(Hwhile: <(st'1, ast'1, b'1, (ds₀ ++ ds₂)%list)>
              =[sel_slh P <{{while be do c end }}>]=> <(st', ast', b', (os₂++os₃)%list )>).
          { simpl. eapply Spec_Seq; eassumption. }
          apply IH in Hwhile; eauto.
          { prog_size_auto. }
          { clear Hwhile; clear H₁₁.
            inversion H₁; subst; clear H₁.
            inversion H₂; subst; clear H₂. simpl in H₁₂.
            apply IH in H₁₂; try tauto.
            - prog_size_auto.
            - rewrite t_update_eq, Eqnbe; simpl. reflexivity. }
  - (* ARead *)
    destruct (P x) eqn:Eqnbe.
    + inversion Heval; subst; clear Heval.
      inversion H₁₀; subst; clear H₁₀.
      rewrite t_update_neq; [| tauto].
      inversion H₁; subst;
      try (rewrite t_update_neq; [assumption| tauto]).
    + inversion Heval; subst;
      try (rewrite t_update_neq; [assumption| tauto]).
Qed.

We now prove that sel_slh implies the ideal semantics.

Lemma aeval_beval_unused_update : ∀ X st n,
  (∀ ae, a_unused X ae →
    aeval (X !-> n; st) ae = aeval st ae ) ∧
  (∀ be, b_unused X be →
    beval (X !-> n; st) be = beval st be ).
Proof.
  intros X st n. apply aexp_bexp_mutind; intros;
  simpl in *; try reflexivity;
  try (
    rewrite H; [| tauto]; rewrite H₀; [| tauto]; reflexivity
  ).
  - rewrite t_update_neq; eauto.
  - rewrite H; [| tauto]. rewrite H₀; [| tauto]. rewrite H₁; [| tauto].
    reflexivity.
  - rewrite H; auto.
Qed.

Lemma aeval_unused_update : ∀ X st ae n,
a_unused X ae →
aeval (X !-> n; st) ae = aeval st ae.
Proof. intros X st ae n. apply aeval_beval_unused_update. Qed.

Lemma beval_unused_update : ∀ X st be n,
b_unused X be →
beval (X !-> n; st) be = beval st be.
Proof. intros X st be n. apply aeval_beval_unused_update. Qed.

Lemma ideal_unused_overwrite: ∀ P st ast b ds c st' ast' b' os X n,
  unused X c →
  P ⊢ <(st , ast , b , ds )> =[ c ]=> <(st', ast', b', os )> →
  P ⊢ <(X !-> n; st , ast , b , ds )> =[ c ]=> <(X !-> n; st', ast', b', os )>.
Proof.
  intros P st ast b ds c st' ast' b' os X n Hu H.
  induction H; simpl in Hu.
  - (* Skip *) econstructor.
  - (* Asgn *)
    rewrite t_update_permute; [| tauto].
    econstructor. rewrite aeval_unused_update; tauto.
  - (* Seq *)
    econstructor.
    + apply IHideal_eval1; tauto.
    + apply IHideal_eval2; tauto.
  - (* If *)
    rewrite <- beval_unused_update with (X:=X) (n:=n); [| tauto].
    econstructor.
    rewrite beval_unused_update; [ | tauto].
    destruct ( beval st be) eqn:D; apply IHideal_eval; tauto.
  - (* If_F *)
    rewrite <- beval_unused_update with (X:=X) (n:=n); [| tauto].
    econstructor.
    rewrite beval_unused_update; [ | tauto].
    destruct ( beval st be) eqn:D; apply IHideal_eval; tauto.
  - (* While *)
    econstructor. apply IHideal_eval. simpl; tauto.
  - (* ARead *)
    rewrite t_update_permute; [| tauto]. econstructor; [ | assumption].
    rewrite aeval_unused_update; tauto.
  - (* ARead_U *)
    rewrite t_update_permute; [| tauto]. econstructor; try assumption.
    rewrite aeval_unused_update; tauto.
  - (* AWrite *)
    econstructor; try assumption.
    + rewrite aeval_unused_update; tauto.
    + rewrite aeval_unused_update; tauto.
  - (* AWrite_U *)
    econstructor; try assumption.
    + rewrite aeval_unused_update; tauto.
    + rewrite aeval_unused_update; tauto.
Qed.

Lemma ideal_unused_update : ∀ P st ast b ds c st' ast' b' os X n,
  unused X c →
  P ⊢ <(X !-> n; st , ast , b , ds )> =[ c ]=> <(X !-> n; st', ast', b', os )> →
  P ⊢ <(st , ast , b , ds )> =[ c ]=> <(X !-> st X; st', ast', b', os )>.
Proof.
  intros P st ast b ds c st' ast' b' os X n Hu Heval.
  eapply ideal_unused_overwrite with (X:=X) (n:=(st X)) in Heval; [| assumption].
  do 2 rewrite t_update_shadow in Heval. rewrite t_update_same in Heval. assumption.
Qed.

Lemma ideal_unused_update_rev : ∀ P st ast b ds c st' ast' b' os X n,
  unused X c →
  P ⊢ <(st , ast , b , ds )> =[ c ]=> <(X!-> st X; st', ast', b', os )> →
  P ⊢ <(X !-> n; st , ast , b , ds )> =[ c ]=> <(X !-> n; st', ast', b', os )>.
Proof.
  intros P st ast b ds c st' ast' b' os X n Hu H.
  eapply ideal_unused_overwrite in H; [| eassumption].
  rewrite t_update_shadow in H. eassumption.
Qed.

Definition sel_slh_ideal_prop (c: com) (ds :dirs) :Prop :=
  ∀ P st ast (b: bool) st' ast' b' os,
    unused "b" c →
    st "b" = (if b then 1 else 0) →
    <(st , ast , b , ds )> =[ sel_slh P c ]=> <(st', ast', b', os )> →
    P ⊢ <(st , ast , b , ds )> =[ c ]=> <("b" !-> st "b"; st', ast', b', os )>.

Lemma sel_slh_ideal : ∀ c ds,
  sel_slh_ideal_prop c ds.
Proof.
  apply prog_size_ind. unfold sel_slh_ideal_prop.
  intros c ds IH P st ast b st' ast' b' os Hunused Hstb Heval.
  destruct c; simpl in *; inversion Heval; subst; clear Heval;
  try (destruct (P x); discriminate).
  - (* Skip *)
    rewrite t_update_same. apply Ideal_Skip.
  - (* Asgn *)
    rewrite t_update_permute; [| tauto].
    rewrite t_update_same.
    constructor. reflexivity.
  - (* Seq *)
    eapply Ideal_Seq.
    + apply IH in H₁; try tauto.
      × eassumption.
      × prog_size_auto.
    + apply sel_slh_flag in H₁ as Hstb'0; try tauto.
      apply IH in H₁₀; try tauto.
      × eapply ideal_unused_update_rev; try tauto.
      × prog_size_auto.
  (* IF *)
  - (* non-speculative *)
    destruct (beval st be) eqn:Eqnbe; inversion H₁₀;
    inversion H₁; subst; clear H₁₀; clear H₁; simpl in ×.
    + apply IH in H₁₁; try tauto.
      × replace (OBranch true) with (OBranch (beval st be))
          by (rewrite <- Eqnbe; reflexivity).
        apply Ideal_If. rewrite Eqnbe.
        rewrite Eqnbe in H₁₁. rewrite t_update_same in H₁₁.
        rewrite app_nil_r. apply H₁₁.
      × prog_size_auto.
      × rewrite t_update_eq. rewrite Eqnbe. assumption.
    + (* analog to true case *)
      apply IH in H₁₁; try tauto.
      × replace (OBranch false) with (OBranch (beval st be))
          by (rewrite <- Eqnbe; reflexivity).
        apply Ideal_If. rewrite Eqnbe. rewrite Eqnbe in H₁₁.
        rewrite t_update_same in H₁₁. rewrite app_nil_r.
        apply H₁₁.
      × prog_size_auto.
      × rewrite t_update_eq. rewrite Eqnbe. assumption.
  - (* speculative *)
    destruct (beval st be) eqn:Eqnbe; inversion H₁₀; inversion H₁;
    subst; simpl in *; clear H₁₀; clear H₁; rewrite Eqnbe in H₁₁.
    + replace (OBranch true) with (OBranch (beval st be))
         by (rewrite <- Eqnbe; reflexivity).
      apply Ideal_If_F. rewrite Eqnbe. apply IH in H₁₁; try tauto.
      × rewrite t_update_eq in H₁₁.
        apply ideal_unused_update in H₁₁; try tauto.
        rewrite app_nil_r. apply H₁₁.
      × prog_size_auto.
    + (* analog to true case *)
      replace (OBranch false) with (OBranch (beval st be))
        by (rewrite <- Eqnbe; reflexivity).
      apply Ideal_If_F. rewrite Eqnbe. apply IH in H₁₁; try tauto.
      × rewrite t_update_eq in H₁₁.
        apply ideal_unused_update in H₁₁; try tauto.
        rewrite app_nil_r. apply H₁₁.
      × prog_size_auto.
  - (* While *)
    eapply Ideal_While.
    inversion H₁; subst; clear H₁.
    inversion H₁₁; subst; clear H₁₁; simpl in ×.
    + (* non-speculative *)
      assert(Lnil: os₂ = [] ∧ ds₂ = []).
      { inversion H₁₀; subst; eauto. }
      destruct Lnil; subst; simpl.
      apply Ideal_If.
      destruct (beval st be) eqn:Eqnbe.
      × inversion H₁₂; subst; clear H₁₂.
        inversion H₁; subst; clear H₁.
        inversion H₂; subst; clear H₂; simpl in ×.
        assert(Hwhile: <(st'1, ast'1, b'1, ds₂)>
          =[ sel_slh P <{{while be do c end }}> ]=> <(st', ast', b', os₂)> ).
        { simpl. replace ds₂ with (ds₂ ++ [])%list by (rewrite app_nil_r; reflexivity).
          replace os₂ with ([] ++ os₂)%list by reflexivity.
          eapply Spec_Seq; eassumption. }
        do 2 rewrite app_nil_r. eapply Ideal_Seq.
        { rewrite Eqnbe in H₁₃. rewrite t_update_same in H₁₃.
          apply IH in H₁₃; try tauto.
          - eassumption.
          - prog_size_auto. }
        { apply IH in Hwhile; auto.
          - eapply ideal_unused_update_rev; eauto.
          - prog_size_auto.
          - apply sel_slh_flag in H₁₃; try tauto.
            rewrite t_update_eq. rewrite Eqnbe. assumption. }
      × inversion H₁₂; subst; clear H₁₂.
        inversion H₁₀; subst; clear H₁₀; simpl in ×.
        rewrite Eqnbe. do 2 rewrite t_update_same.
        apply Ideal_Skip.
    + (* speculative; analog to non_speculative *)
      assert(Lnil: os₂ = [] ∧ ds₂ = []).
      { inversion H₁₀; subst; eauto. }
      destruct Lnil; subst; simpl.
      apply Ideal_If_F.
      destruct (beval st be) eqn:Eqnbe.
      × inversion H₁₂; subst; clear H₁₂.
        inversion H₁₀; subst; clear H₁₀; simpl in ×.
        rewrite Eqnbe. rewrite t_update_shadow. rewrite t_update_same.
        apply Ideal_Skip.
      × inversion H₁₂; subst; clear H₁₂.
        inversion H₁; subst; clear H₁.
        inversion H₂; subst; clear H₂; simpl in ×.
        assert(Hwhile: <(st'1, ast'1, b'1, ds₂)>
          =[ sel_slh P <{{while be do c end }}> ]=> <(st', ast', b', os₂)> ).
        { simpl. replace ds₂ with (ds₂ ++ [])%list by (rewrite app_nil_r; reflexivity).
          replace os₂ with ([] ++ os₂)%list by reflexivity.
          eapply Spec_Seq; eassumption. }
        do 2 rewrite app_nil_r. eapply Ideal_Seq.
        { rewrite Eqnbe in H₁₃.
          apply IH in H₁₃; try tauto.
          - rewrite t_update_eq in H₁₃.
            apply ideal_unused_update in H₁₃; [| tauto].
            eassumption.
          - prog_size_auto. }
        { apply IH in Hwhile; auto.
          - rewrite Eqnbe in H₁₃.
            apply IH in H₁₃; try tauto.
            + apply ideal_unused_update_rev; eauto.
            + prog_size_auto.
          - prog_size_auto.
          - apply sel_slh_flag in H₁₃; try tauto.
            rewrite Eqnbe. rewrite t_update_eq. reflexivity. }
  (* ARead *)
  - (* Spec_ARead; public *)
    destruct (P x) eqn:Heq; try discriminate H.
    injection H; intros; subst; clear H.
    inversion H₁; clear H₁; subst. repeat rewrite <- app_nil_end in ×.
    inversion H₀; clear H₀; subst; simpl in ×.
    × (* Ideal_ARead *)
      rewrite t_update_neq; [| tauto]. rewrite Hstb.
      rewrite t_update_shadow. rewrite t_update_permute; [| tauto].
      rewrite t_update_eq. simpl.
      rewrite <- Hstb at 1. rewrite t_update_same.
      replace ((if b' then 1 else 0) =? 1)%nat with (b' && P x)
        by (rewrite Heq; destruct b'; simpl; reflexivity).
       eapply Ideal_ARead; eauto.
    × (* Ideal_ARead_U *)
      rewrite t_update_neq; [| tauto]. rewrite Hstb.
      rewrite t_update_shadow. rewrite t_update_permute; [| tauto].
      simpl. rewrite <- Hstb at 1. rewrite t_update_same.
      replace (x !-> 0; st) with (x !-> if P x then 0 else nth i' (ast' a') 0; st)
        by (rewrite Heq; reflexivity).
      eapply Ideal_ARead_U; eauto.
  - (* Spec_ARead; secret*)
    destruct (P x) eqn:Heq; try discriminate H. inversion H; clear H; subst.
    rewrite t_update_permute; [| tauto]. rewrite t_update_same.
    replace (x !-> nth (aeval st i) (ast' a) 0; st)
      with (x !-> if b' && P x then 0 else nth (aeval st i) (ast' a) 0; st)
        by (rewrite Heq; destruct b'; reflexivity).
    eapply Ideal_ARead; eauto.
  - (* Spec_Read_U *)
    destruct (P x) eqn:Heq; try discriminate H. inversion H; clear H; subst.
    rewrite t_update_permute; [| tauto]. rewrite t_update_same.
    replace (x !-> nth i' (ast' a') 0; st)
      with (x !-> if P x then 0 else nth i' (ast' a') 0; st)
        by (rewrite Heq; reflexivity).
    eapply Ideal_ARead_U; eauto.
  (* AWrite *)
  - (* Spec_Write *)
    rewrite t_update_same. apply Ideal_Write; tauto.
  - (* Spec_Write_U *)
    rewrite t_update_same. apply Ideal_Write_U; tauto.
Qed.

Finally, we use this to prove spec_ct_secure for sel_slh.

Theorem sel_slh_spec_ct_secure :
  ∀ P PA c st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' b₁' b₂' os₁ os₂ ds,
    P ;; PA ⊢ct - c →
    unused "b" c →
    st₁ "b" = 0 →
    st₂ "b" = 0 →
    pub_equiv P st₁ st₂ →
    pub_equiv PA ast1 ast2 →
    <(st₁ , ast1 , false , ds )> =[ sel_slh P c ]=> <(st₁', ast1', b₁', os₁ )> →
    <(st₂ , ast2 , false , ds )> =[ sel_slh P c ]=> <(st₂', ast2', b₂', os₂ )> →
    os₁ = os₂.
Proof.
  intros P PA c st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' b₁' b₂' os₁ os₂ ds
    Hwt Hunused Hs1b Hs2b Hequiv Haequiv Heval1 Heval2.
  eapply sel_slh_ideal in Heval1; try assumption.
  eapply sel_slh_ideal in Heval2; try assumption.
  eapply ideal_spec_ct_secure; eauto.
Qed.

Speculative constant-time interpreter

Module SpecCTInterpreter.

Since the construction of directions for proofs of examples is very time consuming, we want to have an alternative. This alternative is an interpreter which, if it is sound can be used to easily proof examples.

Definition prog_st : Type := state × astate × bool × dirs × obs.

Inductive output_st (A : Type): Type :=
| OST_Error : output_st A
| OST_OutOfFuel : output_st A
| OST_Finished : A → prog_st → output_st A.

Definition evaluator (A : Type): Type := prog_st → (output_st A ).
Definition interpreter : Type := evaluator unit.

Definition ret {A : Type} (value : A) : evaluator A :=
fun (pst: prog_st) ⇒ OST_Finished A value pst.

Definition bind {A : Type} {B : Type} (e : evaluator A) (f : A → evaluator B): evaluator B :=
  fun (pst: prog_st) ⇒
    match e pst with
    | OST_Finished _ value (st', ast', b', ds', os₁) ⇒
        match (f value) (st', ast', b', ds', os₁) with
        | OST_Finished _ value (st'', ast'', b'', ds'', os₂) ⇒
            OST_Finished B value (st'', ast'', b'', ds'', os₂)
        | ret ⇒ ret
        end
    | OST_Error _ ⇒ OST_Error B
    | OST_OutOfFuel _ ⇒ OST_OutOfFuel B
    end.

Notation "e >>= f" := (bind e f) (at level 58, left associativity).
Notation "e >> f" := (bind e (fun _ ⇒ f)) (at level 58, left associativity).

Funtions for execution of com instructions

Definition finish : interpreter := ret tt.

Definition get_var (name : string): evaluator nat :=
  fun (pst : prog_st) ⇒
    let
      '(st, _, _, _, _) := pst
    in
      ret (st name) pst.

Definition set_var (name : string) (value : nat) : interpreter :=
  fun (pst: prog_st) ⇒
    let
      '(st, ast, b, ds, os) := pst
    in
      let
        new_st := (name !-> value; st)
      in
        finish (new_st , ast, b, ds, os).

Definition get_arr (name : string): evaluator (list nat) :=
  fun (pst: prog_st) ⇒
    let
      '(_, ast, _, _, _) := pst
    in
      ret (ast name) pst.

Definition set_arr (name : string) (value : list nat) : interpreter :=
  fun (pst : prog_st) ⇒
    let '(st, ast, b, ds, os) := pst in
    let new_ast := (name !-> value ; ast) in
    finish (st, new_ast , b, ds, os).

Definition start_speculating : interpreter :=
  fun (pst : prog_st) ⇒
    let '(st, ast, _, ds, os) := pst in
    finish (st, ast, true , ds, os).

Definition is_speculating : evaluator bool :=
  fun (pst : prog_st) ⇒
    let '(_, _, b, _, _) := pst in
    ret b pst.

Definition eval_aexp (a : aexp) : evaluator nat :=
  fun (pst: prog_st) ⇒
    let '(st, _, _, _, _) := pst in
    let v := aeval st a in
    ret v pst.

Definition eval_bexp (be : bexp) : evaluator bool :=
  fun (pst : prog_st) ⇒
    let '(st, _, _, _, _) := pst in
    let v := beval st be in
    ret v pst.

Definition raise_error : interpreter :=
fun _ ⇒ OST_Error unit.

Definition observe (o : observation) : interpreter :=
  fun (pst : prog_st) ⇒
    let '(st, ast, b, ds, os) := pst in
    OST_Finished unit tt (st, ast, b, ds, (o :: os)%list).

Definition fetch_direction : evaluator (option direction) :=
  fun (pst : prog_st) ⇒
    let '(st, ast, b, ds, os) := pst in
    match ds with
    | d::ds' ⇒
        ret (Some d) (st, ast, b, ds', os)
    | [] ⇒ ret None (st, ast, b, [], os)
    end.

The speculative constant-time interpreter

Fixpoint spec_eval_engine_aux (fuel : nat) (c : com) : interpreter :=
  match fuel with
  | O ⇒ fun _ ⇒ OST_OutOfFuel unit
  | S fuel ⇒
    match c with
    | <{ skip }> ⇒ finish
    | <{ x := e }> ⇒ eval_aexp e >>= fun v ⇒ set_var x v
    | <{ c₁ ; c₂ }> ⇒
        spec_eval_engine_aux fuel c₁ >>
        spec_eval_engine_aux fuel c₂
    | <{ if be then ct else cf end }> ⇒
        eval_bexp be >>= fun bool_value ⇒ observe (OBranch bool_value) >> fetch_direction >>=
        fun dop ⇒
          match dop with
          | Some DStep ⇒
              if bool_value then spec_eval_engine_aux fuel ct
              else spec_eval_engine_aux fuel cf
          | Some DForce ⇒
              start_speculating >>
              if bool_value then spec_eval_engine_aux fuel cf
              else spec_eval_engine_aux fuel ct
          | _ ⇒ raise_error
          end
    | <{ while be do c end }> ⇒
        spec_eval_engine_aux fuel <{if be then c ; while be do c end else skip end }>
    | <{ x <- a[[ie]] }> ⇒
        eval_aexp ie >>= fun i ⇒ observe (OARead a i) >> get_arr a >>=
        fun arr_a ⇒ is_speculating >>= fun b ⇒ fetch_direction >>=
        fun dop ⇒
          match dop with
          | Some DStep ⇒
              if (i <? List.length arr_a)%nat then set_var x (nth i arr_a 0)
              else raise_error
          | Some (DLoad a' i') ⇒
              get_arr a' >>= fun arr_a' ⇒
                if negb (i <? List.length arr_a)%nat && (i' <? List.length arr_a')%nat && b then
                  set_var x (nth i' arr_a' 0)
                else raise_error
          | _ ⇒ raise_error
          end
    | <{ a[ie] <- e }> ⇒
        eval_aexp ie >>= fun i ⇒ observe (OAWrite a i) >> get_arr a >>=
        fun arr_a ⇒ eval_aexp e >>= fun n ⇒ is_speculating >>= fun b ⇒ fetch_direction >>=
        fun dop ⇒
          match dop with
          | Some DStep ⇒
              if (i <? List.length arr_a)%nat then set_arr a (upd i arr_a n)
              else raise_error
          | Some (DStore a' i') ⇒
              get_arr a' >>= fun arr_a' ⇒
                if negb (i <? List.length arr_a)%nat && (i' <? List.length arr_a')%nat && b then
                  set_arr a' (upd i' arr_a' n)
                else raise_error
          | _ ⇒ raise_error
          end
    end
end.

(* In principle, could also define spec_eval_engine without fuel,
   but in practice it's quite complicated: *)
(* Program Fixpoint spec_eval_engine_aux (fuel : nat) (c : com) (ds : dirs) :  *)
(*   state * astate * bool -> ds':dirs{length ds' <= length ds} * output_st {measure (com_size c + length ds)} *)
(* ... *)
(*     | <{ c₁ ; c₂ }> => *)
(*         let '(ds', k) := spec_eval_engine_aux ds c₁ in *)
(*         k >> spec_eval_engine_aux ds' c₂ *)

Definition compute_fuel (c :com) (ds :dirs) :=
  match ds with
  | [] ⇒ com_size c
  | _ ⇒ length ds × com_size c
  end.

Definition spec_eval_engine (c : com) (st : state) (ast : astate) (b : bool) (ds : dirs)
      : option (state × astate × bool × obs) :=
    match spec_eval_engine_aux (compute_fuel c ds) c (st , ast , b , ds , []) with
    | OST_Finished _ _ (st', ast', b', ds', os) ⇒
        if ((length ds') =? 0)%nat then Some (st', ast', b', os)
        else None
    | _ ⇒ None
    end.

Soundness of the interpreter

Lemma ltb_reflect : ∀ n m :nat,
reflect (n < m) (n <? m)%nat.
Proof.
intros n m. apply iff_reflect. rewrite ltb_lt. reflexivity.
Qed.

Lemma eqb_reflect: ∀ n m :nat,
reflect (n = m ) (n =? m)%nat.
Proof.
intros n m. apply iff_reflect. rewrite eqb_eq. reflexivity.
Qed.

Lemma spec_eval_engine_aux_sound : ∀ n c st ast b ds os st' ast' b' ds' os' u,
  spec_eval_engine_aux n c (st , ast , b , ds , os )
    = OST_Finished unit u (st', ast', b', ds', os') →
  (∃ dsn osn ,
  (dsn ++ds')%list = ds ∧ (osn ++os)%list = os' ∧
      <(st , ast , b , dsn )> =[ c ]=> <(st', ast', b', osn )> ).
Proof.
  induction n as [| n' IH]; intros c st ast b ds os st' ast' b' ds' os' u Haux;
  simpl in Haux; [discriminate |].
  destruct c as [| X e | c₁ c₂ | be ct cf | be cw | X a ie | a ie e ] eqn:Eqnc;
  unfold ">>=" in Haux; simpl in Haux.
  - (* Skip *)
    inversion Haux; subst.
    ∃ []; ∃ []; split;[| split]; try reflexivity.
    apply Spec_Skip.
  - (* Asgn *)
    simpl in Haux. inversion Haux; subst.
    ∃ []; ∃ []; split;[| split]; try reflexivity.
    apply Spec_Asgn. reflexivity.
  - destruct (spec_eval_engine_aux _ c₁ _) eqn:Hc₁;
    try discriminate; simpl in Haux.
    destruct p as [ [ [ [stm astm] bm] dsm] osm]; simpl in Haux.
    destruct (spec_eval_engine_aux _ c₂ _) eqn:Hc₂;
    try discriminate; simpl in Haux.
    destruct p as [ [ [ [stt astt] bt] dst] ost]; simpl in Haux.
    apply IH in Hc₁. destruct Hc₁ as [ds₁ [ os₁ [Hds1 [Hos1 Heval1] ] ] ].
    apply IH in Hc₂. destruct Hc₂ as [ds₂ [ os₂ [Hds2 [Hos2 Heval2] ] ] ].
    inversion Haux; subst. ∃ (ds₁++ds₂)%list; ∃ (os₂++os₁)%list;
    split; [| split].
    + rewrite <- app_assoc. reflexivity.
    + rewrite <- app_assoc. reflexivity.
    + eapply Spec_Seq; eauto.
  - (* IF *)
    destruct ds as [| d ds_tl] eqn:Eqnds; simpl in Haux; try discriminate.
    destruct d eqn:Eqnd; try discriminate; simpl in Haux.
    + (* DStep *)
      destruct (beval st be) eqn:Eqnbe.
      × destruct (spec_eval_engine_aux _ ct _ ) eqn:Hct; try discriminate; simpl in Haux.
        destruct p as [ [ [ [stt astt] bt] dst] ost]; simpl in Haux.
        inversion Haux; subst. apply IH in Hct.
        destruct Hct as [dst [ ost [Hds [Hos Heval] ] ] ].
        ∃ (DStep :: dst); ∃ (ost++[OBranch true ])%list; split;[| split].
        { simpl. rewrite Hds. reflexivity. }
        { rewrite <- app_assoc. simpl. rewrite Hos. reflexivity. }
        { rewrite <- Eqnbe. apply Spec_If. rewrite Eqnbe. apply Heval. }
      × destruct (spec_eval_engine_aux _ cf _ ) eqn:Hcf; try discriminate; simpl in Haux.
        destruct p as [ [ [ [stt astt] bt] dst] ost]; simpl in Haux.
        inversion Haux; subst. apply IH in Hcf.
        destruct Hcf as [dst [ ost [Hds [Hos Heval] ] ] ].
        ∃ (DStep :: dst); ∃ (ost++[OBranch false ])%list; split;[| split].
        { simpl. rewrite Hds. reflexivity. }
        { rewrite <- app_assoc. simpl. rewrite Hos. reflexivity. }
        { rewrite <- Eqnbe. apply Spec_If. rewrite Eqnbe. apply Heval. }
    + (* DForce *)
      destruct (beval st be) eqn:Eqnbe.
      × destruct (spec_eval_engine_aux _ cf _ ) eqn:Hcf; try discriminate; simpl in Haux.
        destruct p as [ [ [ [stt astt] bt] dst] ost]; simpl in Haux.
        inversion Haux; subst. apply IH in Hcf.
        destruct Hcf as [dst [ ost [Hds [Hos Heval] ] ] ].
        ∃ (DForce :: dst); ∃ (ost++[OBranch true ])%list; split;[| split].
        { simpl. rewrite Hds. reflexivity. }
        { rewrite <- app_assoc. simpl. rewrite Hos. reflexivity. }
        { rewrite <- Eqnbe. apply Spec_If_F. rewrite Eqnbe. apply Heval. }
      × destruct (spec_eval_engine_aux _ ct _ ) eqn:Hct; try discriminate; simpl in Haux.
        destruct p as [ [ [ [stt astt] bt] dst] ost]; simpl in Haux.
        inversion Haux; subst. apply IH in Hct.
        destruct Hct as [dst [ ost [Hds [Hos Heval] ] ] ].
        ∃ (DForce :: dst); ∃ (ost++[OBranch false ])%list; split;[| split].
        { simpl. rewrite Hds. reflexivity. }
        { rewrite <- app_assoc. simpl. rewrite Hos. reflexivity. }
        { rewrite <- Eqnbe. apply Spec_If_F. rewrite Eqnbe. apply Heval. }
  - (* While *)
    apply IH in Haux. destruct Haux as [dst [ ost [Hds [Hos Heval] ] ] ].
    ∃ dst; ∃ ost; split; [| split]; eauto.
    apply Spec_While. apply Heval.
  - (* ARead *)
    destruct ds as [| d ds_tl] eqn:Eqnds; simpl in Haux; try discriminate.
    destruct d eqn:Eqnd; try discriminate; simpl in Haux.
    + (* DStep *)
      destruct (aeval st ie <? Datatypes.length (ast a))%nat eqn:Eqnindex; try discriminate.
      destruct (observe (OARead a (aeval st ie)) (st, ast, b, ds_tl, os)) eqn:Eqbobs; try discriminate;
      simpl in Haux. inversion Haux; subst.
      eexists [DStep ]; eexists [OARead a (aeval st ie)]; split;[| split]; try reflexivity.
      eapply Spec_ARead; eauto. destruct (ltb_reflect (aeval st ie) (length (ast' a))) as [Hlt | Hgeq].
      × apply Hlt.
      × discriminate.
    + (* DForce *)
      destruct (negb (aeval st ie <? Datatypes.length (ast a))%nat) eqn:Eqnindex1;
      destruct ((i <? Datatypes.length (ast a₀))%nat) eqn:Eqnindex2;
      destruct b eqn:Eqnb; try discriminate; simpl in Haux. inversion Haux; subst.
      eexists [DLoad a₀ i ]; eexists [OARead a (aeval st ie)]; split;[| split]; try reflexivity.
      eapply Spec_ARead_U; eauto.
      × destruct (ltb_reflect (aeval st ie) (length (ast' a))) as [Hlt | Hgeq].
        { discriminate. }
        { apply not_lt in Hgeq. apply Hgeq. }
      × destruct (ltb_reflect i (length (ast' a₀))) as [Hlt | Hgeq].
        { apply Hlt. }
        { discriminate. }
  - (* AWrite *)
  destruct ds as [| d ds_tl] eqn:Eqnds; simpl in Haux; try discriminate.
  destruct d eqn:Eqnd; try discriminate; simpl in Haux.
  + (* DStep *)
    destruct ((aeval st ie <? Datatypes.length (ast a))%nat) eqn:Eqnindex; try discriminate.
    destruct (observe (OAWrite a (aeval st ie)) (st, ast, b, ds_tl, os)) eqn:Eqbobs; try discriminate;
    simpl in Haux. inversion Haux; subst.
    eexists [DStep ]; eexists [OAWrite a (aeval st' ie)]; split;[| split]; try reflexivity.
    eapply Spec_Write; eauto. destruct (ltb_reflect (aeval st' ie) (length (ast a))) as [Hlt | Hgeq].
    × apply Hlt.
    × discriminate.
  + (* DForce *)
    destruct (negb (aeval st ie <? Datatypes.length (ast a))%nat) eqn:Eqnindex1;
    destruct (i <? Datatypes.length (ast a₀))%nat eqn:Eqnindex2;
    destruct b eqn:Eqnb; try discriminate; simpl in Haux. inversion Haux; subst.
    eexists [DStore a₀ i]; eexists [OAWrite a (aeval st' ie)]; split;[| split]; try reflexivity.
    eapply Spec_Write_U; eauto.
    × destruct (ltb_reflect (aeval st' ie) (length (ast a))) as [Hlt | Hgeq].
      { discriminate. }
      { apply not_lt in Hgeq. apply Hgeq. }
    × destruct (ltb_reflect i (length (ast a₀))) as [Hlt | Hgeq].
      { apply Hlt. }
      { discriminate. }
Qed.

Theorem spec_eval_engine_sound: ∀ c st ast b ds st' ast' b' os',
  spec_eval_engine c st ast b ds = Some (st', ast', b', os') →
  <(st , ast , b , ds )> =[ c ]=> <(st', ast', b', os')> .
Proof.
  intros c st ast b ds st' ast' b' os' Hengine.
  unfold spec_eval_engine in Hengine.
  destruct (spec_eval_engine_aux _ c _) eqn:Eqnaux;
  try discriminate. destruct p as [ [ [ [stt astt] bt] dst] ost].
  destruct ((Datatypes.length dst =? 0)%nat) eqn:Eqnds; try discriminate.
  apply spec_eval_engine_aux_sound in Eqnaux.
  destruct Eqnaux as [dsn [osn [Hdsn [Hosn Heval] ] ] ].
  inversion Hengine; subst. rewrite app_nil_r.
  destruct (eqb_reflect (length dst) 0) as [Heq | Hneq].
  + apply length_zero_iff_nil in Heq. rewrite Heq. rewrite app_nil_r. apply Heval.
  + discriminate.
Qed.

Definition spec_insecure_prog_2 :=
  <{{ X := 0;
      Y := 0;
      while Y ≤ 2 do
        Z <- AP [[Y ]];
        X := X + Z ;
        Y := Y + 1
      end ;
      if X ≤ 42 then W := 1 else W := 0 end }}> .

Example spec_insecure_prog_2_is_ct_and_spec_insecure :
  ∃ P PA ,
    P ;; PA ⊢ct - spec_insecure_prog_2 ∧ ¬ (spec_ct_secure P PA spec_insecure_prog_2 ) .
Proof.
  ∃ (X!-> public; Y!-> public; Z!-> public; _ !-> secret).
  ∃ (AP!-> public; AS!-> secret; _ !-> public).
  split; unfold spec_insecure_prog.
  - repeat econstructor;
    replace (public) with (join public public) at 4 by reflexivity;
    repeat constructor.
  - remember (_ !-> 0) as st.
    remember (AP!-> [1;2;3]; AS!-> [40;41;42;43]; _ !-> []) as ast1.
    remember (AP!-> [1;2;3]; AS!-> [4;5;6;7]; _ !-> []) as ast2.
    remember ([DStep ; DStep ; DStep ; DStep ; DStep ; DStep ; DForce ; DLoad AS 3; DStep ; DStep ]) as ds.
    intros Hsecure.
    assert (L: ∃ stt1 astt1 bt₁ os₁ stt2 astt2 bt₂ os₂ ,
      <(st, ast1, false , ds )> =[ spec_insecure_prog_2 ]=> <( stt1 , astt1 , bt₁ , os₁ )> ∧
      <(st, ast2, false , ds )> =[ spec_insecure_prog_2 ]=> <( stt2 , astt2 , bt₂ , os₂ )> ∧
      os₁ ≠ os₂ ).
    { eexists; eexists; eexists; eexists; eexists; eexists; eexists; eexists.
      split; [| split].
      - apply spec_eval_engine_sound. unfold spec_insecure_prog_2, spec_eval_engine;
        subst; simpl; reflexivity.
      - apply spec_eval_engine_sound. unfold spec_insecure_prog_2, spec_eval_engine;
        subst; simpl; reflexivity.
      - intros Contra; inversion Contra. }
    destruct L as [stt1 [astt1 [bt₁ [os₁ [stt2 [astt2 [bt₂ [os₂ [Heval1 [Heval2 Hneq] ] ] ] ] ] ] ] ] ].
    eapply Hsecure in Heval1; eauto.
    + apply pub_equiv_refl.
    + intros x Hx. destruct (String.eqb_spec "AP" x) as [HeqAP | HneqAP];
      destruct (String.eqb_spec "AS" x) as [HeqAS | HneqAS].
      × subst. do 2 rewrite t_update_eq. reflexivity.
      × subst. do 2 rewrite t_update_eq. reflexivity.
      × subst. rewrite t_update_neq in Hx; [| assumption].
        rewrite t_update_eq in Hx. discriminate.
      × subst. do 4 (rewrite t_update_neq; [| assumption]). reflexivity.
Qed.

End SpecCTInterpreter.

(* 2024-07-26 15:44 *)