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 "!".

This chapter starts by presenting the cryptographic constant-time (CCT) discipline, which we statically enforce using a simple type system. This static discipline is, however, not enough to protect cryptographic programs against speculative execution attacks. To secure CCT programs against this more powerful attacker model we additionally use a program transformation called Speculative Load Hardening (SLH). We prove formally that CCT programs protected by SLH achieve speculative constant-time security.

Cryptographic constant-time

Cryptographic constant-time (CCT) is a software countermeasure against cache-based timing attacks, a class of timing side-channel attacks that exploit the latency between cache hits and cache misses to infer cryptographic keys and other secrets. In addition to ensuring program counter security by requiring programmers to not branch on secrets, CCT requires programmers to also not perform memory accesses depending on secrets. While we won't model caches explicitly, this generally implies security against timing attacks exploiting both instruction and data caches.

To model memory accesses that depend on secrets 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 in Imp CCT trivially holds for all PC well-typed programs. 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 CCT secure (since it accesses memory based on secret information):
x <- a[secret]

Adding constant-time conditional and refactoring expressions

But first, we add an b ? e₁ : e₂ conditional expression that executes in constant time (for instance using a special constant-time conditional move instruction). This constant-time conditional will also be used in our SLH countermeasure below.

To avoid making the definitions of arithmetic and boolean expressions mutually inductive, we drop boolean expressions altogether and encode them using arithmetic expressions. Our encoding of bools in terms of nats is similar to that of C, where zero means false, and non-zero means true.

Finally, we refactor the semantics of binary operators in terms of the binop enumeration below, to avoid the duplication in Imp:

We define the semantics of binops directly on nats. We are careful to allow other representations of true (any non-zero number).

Definition not_zero (n : nat) : bool := negb (n =? 0).
Definition bool_to_nat (b : bool) : nat := if b then 1 else 0.

Definition eval_binop (o:binop) (n₁ n₂ : nat) : nat :=
  match o with
  | BinPlus ⇒ n₁ + n₂
  | BinMinus ⇒ n₁ - n₂
  | BinMult ⇒ n₁ × n₂
  | BinEq ⇒ if n₁ =? n₂ then 1 else 0
  | BinLe ⇒ if n₁ <=? n₂ then 1 else 0
  | BinAnd ⇒ bool_to_nat (not_zero n₁ && not_zero n₂)
  | BinImpl ⇒ bool_to_nat (negb (not_zero n₁) || not_zero n₂)
  end.

Inductive aexp : Type :=
  | ANum (n : nat)
  | AId (x : string)
  | ABin (o:binop) (a₁ a₂ : aexp) (* <--- REFACTORED *)
  | ACTIf (b:aexp) (a₁ a₂:aexp). (* <--- NEW *)

We can encode all the previous arithmetic and boolean operations:

Definition APlus := ABin BinPlus.
Definition AMinus := ABin BinMinus.
Definition AMult := ABin BinMult.
Definition BTrue := ANum 1.
Definition BFalse := ANum 0.
Definition BAnd := ABin BinAnd.
Definition BImpl := ABin BinImpl.
Definition BNot b := BImpl b BFalse.
Definition BOr a₁ a₂ := BImpl (BNot a₁) a₂.
Definition BEq := ABin BinEq.
Definition BNeq a₁ a₂ := BNot (BEq a₁ a₂).
Definition BLe := ABin BinLe.
Definition BGt a₁ a₂ := BNot (BLe a₁ a₂).
Definition BLt a₁ a₂ := BGt a₂ a₁.

Hint Unfold eval_binop : core.

The label assigned to the result of a constant-time conditional will simply join the labels of the 3 involved expressions:

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

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

The notations we use for expressions are the same as in Imp, except the notation for be?a₁:a₂ which is new:

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 "'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" := (BLt 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.

Notation "be '?' a₁ ':' a₂" := (ACTIf be a₁ a₂) (* <-- NEW *)
(in custom com at level 20, no associativity).

Adding arrays

Now back to adding array reads and writes to commands:

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) (* <--- NEW *)
     (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) (* <--- NEW *)
     (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). (* <--- NEW *)

Fixpoint aeval (st : state) (a: aexp) : nat :=
  match a with
  | ANum n ⇒ n
  | AId x ⇒ st x
  | ABin b a₁ a₂ ⇒ eval_binop b (aeval st a₁) (aeval st a₂)
  | <{b ? a₁ : a₂}> ⇒ if not_zero (aeval st b) then aeval st a₁
                           (* ^- NEW -> *) else aeval st a₂
  end.

A couple of obvious lemmas that will be useful in the proofs:

Lemma not_zero_aeval_S : ∀ b n st,
aeval st b = S n →
not_zero (aeval st b) = true.

Proof. intros b n st H. rewrite H. reflexivity. Qed.

Lemma not_zero_aeval_O : ∀ b st,
aeval st b = O →
not_zero (aeval st b) = false.

Proof. intros b st H. rewrite H. reflexivity. Qed.

We also define an array update operation, to be used in the semantics of array writes below:

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

Instrumenting semantics with observations

In addition to the boolean branches, which are observable in the PC security model, for CCT security also the array reads and writes are observable:

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', [OBranch true] ++ os₁)>

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

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

<(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₁ n,
      (aeval st b =? S n ) = true →
      <(st , ast )> =[ c₁ ]=> <(st', ast', os₁ )> →
      <(st , ast )> =[ if b then c₁ else c₂ end ]=> <(st', ast', [OBranch true ] ++ os₁ )>
  | CTE_IfFalse : ∀ st ast st' ast' b c₁ c₂ os₁,
      (aeval st b =? 0) = true →
      <(st , ast )> =[ c₂ ]=> <(st', ast', os₁ )> →
      <(st , ast )> =[ if b then c₁ else c₂ end ]=> <(st', ast', [OBranch false ] ++ os₁ )>
  | 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).

Hint Constructors cteval : core.

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 cct_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 cct_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 cct_insecure_prog_is_not_cct_secure : ∃ P PA ,
  ¬ (cct_secure P PA cct_insecure_prog ).
Proof.
  ∃ (X!-> public; Y!-> secret; _!-> public).
  ∃ (A!-> secret; _!-> public).
  unfold cct_secure, cct_insecure_prog; intros CTSEC.
  remember (Y!-> 1; _ !-> 0) as st₁.
  remember (Y!-> 2; _ !-> 0) as st₂.
  remember (A!-> [1;2;3]; _!-> []) as ast.
  specialize (CTSEC st₁ st₂ ast ast).

  assert (Contra: [OARead A 1] = [OARead A 2]).
  { eapply CTSEC; subst.
    (* public variables equivalent *)
    - 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.
    (* public arrays equivalent *)
    - apply pub_equiv_refl.
    - eapply CTE_ARead; simpl; auto.
    - eapply CTE_ARead; simpl; auto. }

  discriminate.
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 ∈ l" (at level 40).

Inductive aexp_has_label (P:pub_vars) : aexp → label → Prop :=
  | T_Num : ∀ n,
       P ⊢ (ANum n ) \in public
  | T_Id : ∀ X,
       P ⊢ (AId X ) \in (P X )
  | T_Bin : ∀ op a₁ l₁ a₂ l₂,
       P ⊢ a₁ \in l₁ →
       P ⊢ a₂ \in l₂ →
       P ⊢ (ABin op a₁ a₂ ) \in (join l₁ l₂ )
  | T_CTIf : ∀ be l a₁ l₁ a₂ l₂,
       P ⊢ be \in l →
       P ⊢ a₁ \in l₁ →
       P ⊢ a₂ \in l₂ →
       P ⊢ <{ be ? a₁ : a₂ }> \in (join l (join l₁ l₂))

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

Hint Constructors aexp_has_label : core.

Theorem noninterferent_aexp : ∀ {P s₁ s₂ a},
  pub_equiv P s₁ s₂ →
  P ⊢ a \in public →
  aeval s₁ a = aeval s₂ a.
Proof.
  intros P s₁ s₂ a Heq Ht. remember public as l.
  generalize dependent Heql.
  induction Ht; simpl; intros.
  - reflexivity.
  - eapply Heq; auto.
  - eapply join_public in Heql.
    destruct Heql as [HP₁ HP₂]. subst.
    rewrite IHHt1, IHHt2; reflexivity.
  - eapply join_public in Heql.
    destruct Heql as [HP HP']. subst.
    eapply join_public in HP'.
    destruct HP' as [HP₁ HP₂]. subst.
    rewrite IHHt1, IHHt2, IHHt3; reflexivity.
Qed.

	(CCT_Skip)

P ;; PA ⊢ct- skip

P ⊢ a ∈ l can_flow l (P X) = true	(CCT_Asgn)

P ;; PA ⊢ct- X := a

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

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

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

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

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

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

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

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

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

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

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

Inductive cct_well_typed (P:pub_vars) (PA:pub_arrs) : com → Prop :=
  | CCT_Skip :
      P ;; PA ⊢ct - <{{ skip }}>
  | CCT_Asgn : ∀ X a l,
      P ⊢ a \in l →
      can_flow l (P X) = true →
      P ;; PA ⊢ct - <{{ X := a }}>
  | CCT_Seq : ∀ c₁ c₂,
      P ;; PA ⊢ct - c₁ →
      P ;; PA ⊢ct - c₂ →
      P ;; PA ⊢ct - <{{ c₁ ; c₂ }}>
  | CCT_If : ∀ b c₁ c₂,
      P ⊢ b \in public →
      P ;; PA ⊢ct - c₁ →
      P ;; PA ⊢ct - c₂ →
      P ;; PA ⊢ct - <{{ if b then c₁ else c₂ end }}>
  | CCT_While : ∀ b c₁,
      P ⊢ b \in public →
      P ;; PA ⊢ct - c₁ →
      P ;; PA ⊢ct - <{{ while b do c₁ end }}>
  | CCT_ARead : ∀ x a i,
      P ⊢ i \in public →
      can_flow (PA a) (P x) = true →
      P ;; PA ⊢ct - <{{ x <- a [[i ]] }}>
  | CCT_AWrite : ∀ a i e l,
      P ⊢ i \in public →
      P ⊢ e \in l →
      can_flow l (PA a) = true →
      P ;; PA ⊢ct - <{{ a [i ] <- e }}>

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

Hint Constructors cct_well_typed : core.

Final theorems: noninterference and constant-time security

Theorem cct_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.
  (* Most cases are the similar as for pc_well_typed *)
  - 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_aexp Heq H₁₃) in H.
    rewrite eqb_eq in H, H₈. rewrite H in H₈. discriminate H₈.
  - rewrite (noninterferent_aexp Heq H₁₃) in H.
    rewrite eqb_eq in H, H₈. rewrite H in H₈. discriminate H₈.
  - eapply IHHeval1; eassumption.
  - eapply IHHeval1; eauto.
  - (* 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 cct_well_typed_secure : ∀ P PA c,
P ;; PA ⊢ct - c →
cct_secure P PA c.

Proof.
  unfold cct_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.
  (* Most cases are the similar as for pc_well_typed *)
  - reflexivity.
  - reflexivity.
  - erewrite IHHeval1_2; [erewrite IHHeval1_1 | | | |];
      try reflexivity; try eassumption.
    + eapply cct_well_typed_noninterferent with (c:=c₁); eauto.
    + eapply cct_well_typed_noninterferent with (c:=c₁); eauto.
  - rewrite (noninterferent_aexp Heq H₁₃) in H.
    rewrite eqb_eq in H, H₈.
    rewrite H in H₈. inversion H₈. subst.
    f_equal. eapply IHHeval1; try eassumption.
  - rewrite (noninterferent_aexp Heq H₁₃) in H.
    rewrite eqb_eq in H, H₈.
    rewrite H₈ in H. discriminate H.
  - rewrite (noninterferent_aexp Heq H₁₃) in H.
    rewrite eqb_eq in H, H₈.
    rewrite H in H₈. discriminate H₈.
  - f_equal. eapply IHHeval1; eassumption.
  - eapply IHHeval1; eauto.
  - (* 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 aeval st be with
                       | O ⇒ c₂
                       | S _ ⇒ c₁ end ]=> <(st', ast', b', os₁ )> →
      <(st , ast , b , DStep :: ds )> =[ if be then c₁ else c₂ end ]=>
        <(st', ast', b', [OBranch (not_zero (aeval st be))] ++ os₁ )>
  | Spec_If_F : ∀ st ast b st' ast' b' be c₁ c₂ os₁ ds,
      <(st , ast , true , ds )> =[ match aeval st be with
                       | O ⇒ c₁ (* <-- branches swapped *)
                       | S _ ⇒ c₂ end ]=> <(st', ast', b', os₁ )> →
      <(st , ast , b , DForce :: ds )> =[ if be then c₁ else c₂ end ]=>
        <(st', ast', b', [OBranch (not_zero (aeval st be))] ++ os₁ )>
  | 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).

Hint Constructors spec_eval : core.

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 CCT programs that are insecure under speculative execution

Definition spec_insecure_prog :=
  <{{ if Z < 1 then (* where 1 is the size of AP, but this can mispeculate *)
        X <- AP [[Z ]]; (* loads secret to public variable X
                         using a speculatively out of bounds access *)
        if X ≤ 5 then Y := 1 else Y := 0 end (* speculatively leak X *)
      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. admit. - intros Hcs.
    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 false ] ++ ([OARead "AP" 1]) ++ [OBranch true ])) 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 Hcs 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.
Admitted.

Here is a more realistic example

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 }}> .

This example is formalized at the end of the file.

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.

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 )>.

(* We prove that this new definition for sequential execution is equivalent to
the old one, 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 (aeval st be) eqn:Eqbe.
      × eapply CTE_IfFalse; [rewrite Eqbe; simpl; reflexivity |].
        eapply IHHeval. intros d HdIn.
        apply (in_cons DStep d) in HdIn. apply Hstep in HdIn. assumption.
      × eapply CTE_IfTrue; [rewrite Eqbe; simpl; eapply eqb_refl |].
        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 eqb_eq in H. erewrite <- not_zero_aeval_S; [| eassumption].
        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 eqb_eq in H. erewrite <- not_zero_aeval_O; [| eassumption].
        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 cct_well_typed_secure in Hwt. eapply Hwt; eauto.
Qed.

Selective SLH transformation

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

Definition msf : string := "msf".

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 msf := (be ? msf : 1); sel_slh P c₁
               else msf := (be ? 1 : msf ); sel_slh P c₂ end }}>
  | <{{while be do c end }}> ⇒
      <{{while be do msf := (be ? msf : 1); sel_slh P c end ;
         msf := (be ? 1 : msf )}}>
  | <{{x <- a[[i]]}}> ⇒
      if P x then <{{x <- a[[i]]; x := (msf = 1) ? 0 : x}}>
             else <{{x <- a[[i]]}}>
  | <{{a[i] <- e}}> ⇒ <{{a[i] <- e}}>
  end.

Ideal semantics definition

To prove this transformation secure, Spectre Declassified uses an ideal semantics, capturing selective speculative load hardening more abstractly. The proof effort is decomposed into: 1. a speculative constant-time proof for the ideal semantics; 2. a compiler correctness proof for the sel_slh transformation taking source programs which are executed using the ideal semantics to target programs executed using the speculative semantics.

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 aeval st be with
                                 | O ⇒ c₂
                                 | S _ ⇒ c₁ end ]=> <(st', ast', b', os₁ )> →
      P ⊢ <(st , ast , b , DStep :: ds )> =[ if be then c₁ else c₂ end ]=>
        <(st', ast', b', [OBranch (not_zero (aeval st be))] ++ os₁ )>
  | Ideal_If_F : ∀ st ast b st' ast' b' be c₁ c₂ os₁ ds,
      P ⊢ <(st , ast , true , ds )> =[ match aeval st be with
                                    | O ⇒ c₁ (* <-- branches swapped *)
                                    | S _ ⇒ c₂ end ]=> <(st', ast', b', os₁ )> →
      P ⊢ <(st , ast , b , DForce :: ds )> =[ if be then c₁ else c₂ end ]=>
        <(st', ast', b', [OBranch (not_zero (aeval st be))] ++ os₁ )>
  | 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).

Hint Constructors ideal_eval : core.

Ideal semantics enforces speculative constant-time

Let's now prove that the ideal semantics does enforce speculative constant-time. As in the proofs we did before for constant-time and pc security, we rely on a proof of noninterference. For our ideal semantics this noninterference proof is very interesting.

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 - (match aeval st be with
                             | O ⇒ c₂
                             | S _ ⇒ c₁
                             end)).
    { destruct (aeval st be); assumption. }
    assert(Gds : prefix ds ds₀ ∨ prefix ds₀ ds).
    { destruct Hds as [Hds | Hds]; apply prefix_cons in Hds; tauto. }
    erewrite noninterferent_aexp 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 - (match aeval st be with
                             | O ⇒ c₁
                             | S _ ⇒ c₂
                             end)).
    { destruct (aeval st be); assumption. }
    assert(Gds : prefix ds ds₀ ∨ prefix ds₀ ds).
    { destruct Hds as [Hds | Hds]; apply prefix_cons in Hds; tauto. }
    erewrite noninterferent_aexp 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 in the sequence case) 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.
    + f_equal. eapply noninterferent_aexp in Heq; [| eassumption].
      rewrite Heq. reflexivity.
    + eapply IHHeval1; try eassumption; try (destruct (aeval st be); eassumption).
      erewrite (noninterferent_aexp Heq H₁₄); eassumption.
  - (* If_F *)
    f_equal.
    + f_equal. eapply noninterferent_aexp in Heq; [| eassumption].
      rewrite Heq. reflexivity.
    + eapply IHHeval1; try eassumption; try (destruct (aeval st be); eassumption).
      × intro contra. discriminate contra.
      × erewrite noninterferent_aexp; eassumption.
  - (* While *) eapply IHHeval1; eauto.
  - (* 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.

Correctness of sel_slh as a compiler from ideal to speculative semantics

We now prove that the ideal semantics correctly captures the programs produced by sel_slh when executed using the speculative semantics. We phrase this as a backwards compiler correctness proof for sel_slh.

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

Fixpoint a_unused (x:string) (a:aexp) : Prop :=
  match a with
  | ANum n ⇒ True
  | AId y ⇒ y ≠ x
  | ABin _ a₁ a₂ ⇒ a_unused x a₁ ∧ a_unused x a₂
  | <{b ? a₁ : a₂}> ⇒ a_unused x b ∧ a_unused x a₁ ∧ a_unused x a₂
  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 }}> ⇒
      a_unused x be ∧ unused x c₁ ∧ unused x c₂
  | <{{while be do c end }}> ⇒ a_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.

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

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 size of a the pair of the (c:com) and the (ds:dirs).

Fixpoint com_size (c :com) :nat :=
  match c with
  | <{{ c₁; c₂ }}> ⇒ 1 + (com_size c₁) + (com_size c₂)
  (* For conditionals the maximum of both branches is tighter, but a
     looser bound based on blindly "counting all constructors"
     (commented here) works just as well, and is easier to explain on
     paper *)
  | <{{ if be then ct else cf end }}> ⇒ 1 + max (com_size ct) (com_size cf)
  (* | <{{ if be then ct else cf end }}> => 1 + (com_size ct) + (com_size cf) *)
  | <{{ while be do cw end }}> ⇒ 1 + (com_size cw)
  | <{{ skip }}> ⇒ 1
  | _ ⇒ 1
  end.

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

The induction principle on size

Check measure_induction.

Lemma size_ind :
  ∀ P : com → dirs → Prop,
  (∀ c ds,
    ( ∀ c' ds',
      size c' ds' < size c ds →
      P c' ds') → P c ds ) →
  (∀ c ds, P c ds ).
Proof.
  intros.
  remember (fun c_ds ⇒ P (fst c_ds) (snd c_ds)) as P'.
  replace (P c ds) with (P' (c, ds)) by now rewrite HeqP'.
  eapply measure_induction with (f:=fun c_ds ⇒ size (fst c_ds) (snd c_ds)). intros. rewrite HeqP'.
  apply H. intros.
  remember (c', ds') as c_ds'.
  replace (P c' ds') with (P' c_ds') by now rewrite Heqc_ds', HeqP'.
  apply H₀. now rewrite Heqc_ds'.
Qed.

The proof of sel_slh_flag

Lemma 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₂ ) →
  size c₁ ds₁ < size c₂ ds₂.
Proof.
  intros c₁ ds₁ c₂ ds₂ [ [Hcom Hdir] | [Hcom Hdir] ];
  unfold size; lia.
Qed.

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

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

To properly apply 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 msf c →
  st msf = (if b then 1 else 0) →
  <(st , ast , b , ds )> =[ sel_slh P c ]=> <(st', ast', b', os )> →
  st' msf = (if b' then 1 else 0).

Lemma sel_slh_flag : ∀ c ds,
  sel_slh_flag_prop c ds.
Proof.
  eapply 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. size_auto.
    + size_auto.
  - (* IF *)
    inversion Heval; subst; clear Heval.
    + (* Spec_If *)
      destruct (aeval st be) eqn:Eqnbe.
      × inversion H₁₀; subst; clear H₁₀.
        inversion H₁; subst; clear H₁.
        apply IH in H₁₁; try tauto.
        { 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₁₁.
        { auto. }
        { size_auto. }
        { tauto. }
        { rewrite t_update_eq. simpl. rewrite Eqnbe. assumption. }
    + (* Spec_If_F; analog to Spec_If case *)
      destruct (aeval st be) eqn:Eqnbe.
      × inversion H₁₀; subst; clear H₁₀.
        inversion H₁; subst; clear H₁.
        apply IH in H₁₁; try tauto.
        { size_auto. }
        { rewrite t_update_eq. simpl. rewrite Eqnbe. simpl. reflexivity. }
      × inversion H₁₀; subst; clear H₁₀.
        inversion H₁; subst; clear H₁.
        apply IH in H₁₁; try tauto.
        { size_auto. }
        { rewrite t_update_eq. simpl. rewrite Eqnbe. simpl. reflexivity. }
  - (* While *)
      inversion Heval; subst; clear Heval.
      inversion H₁; subst; clear H₁.
      inversion H₁₁; subst; clear H₁₁.
      + (* non-speculative *)
        destruct (aeval st be) eqn:Eqnbe.
        × inversion H₁₂; subst; clear H₁₂.
          inversion H₁₀; subst; simpl.
          rewrite t_update_eq, Eqnbe; simpl. assumption.
        × 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.
          { 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.
            - size_auto.
            - rewrite t_update_eq, Eqnbe; simpl. assumption. }
      + (* speculative; analog to non_speculative case *)
        destruct (aeval 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.
          { 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.
            - size_auto.
            - rewrite t_update_eq, Eqnbe; simpl. reflexivity. }
        × inversion H₁₂; subst; clear H₁₂.
          inversion H₁₀; subst; simpl.
          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 need a few more lemmas before we prove backwards compiler correctness

Lemma aeval_unused_update : ∀ X st n,
  (∀ ae, a_unused X ae →
    aeval (X !-> n; st) ae = aeval st ae).
Proof.
  intros X st n. induction ae; intros; simpl in *; try reflexivity.
  - rewrite t_update_neq; eauto.
  - destruct H.
    rewrite IHae1; [| tauto]. rewrite IHae2; [| tauto].
    reflexivity.
  - destruct H. destruct H₀.
    rewrite IHae1, IHae2, IHae3; auto.
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 <- aeval_unused_update with (X:=X) (n:=n); [| tauto].
    econstructor.
    rewrite aeval_unused_update; [ | tauto].
    destruct (aeval st be) eqn:D; apply IHideal_eval; tauto.
  - (* If_F *)
    rewrite <- aeval_unused_update with (X:=X) (n:=n); [| tauto].
    econstructor.
    rewrite aeval_unused_update; [ | tauto].
    destruct (aeval 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.

Finally the backwards compiler correctness proof

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

Lemma sel_slh_ideal : ∀ c ds,
  sel_slh_ideal_prop c ds.
Proof.
  apply 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.
      × 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.
      × size_auto.
  (* IF *)
  - (* non-speculative *)
    destruct (aeval st be) eqn:Eqnbe; inversion H₁₀;
    inversion H₁; subst; clear H₁₀; clear H₁; simpl in ×.
    + apply IH in H₁₁; try tauto.
      × rewrite <- Eqnbe. apply Ideal_If. rewrite Eqnbe in ×.
        rewrite t_update_same in H₁₁. apply H₁₁.
      × size_auto.
      × rewrite t_update_eq. rewrite Eqnbe. assumption.
    + (* analog to false case *)
      apply IH in H₁₁; try tauto.
      × rewrite <- Eqnbe. apply Ideal_If. rewrite Eqnbe in ×.
        rewrite t_update_same in H₁₁. apply H₁₁.
      × size_auto.
      × rewrite t_update_eq. rewrite Eqnbe. assumption.
  - (* speculative *)
    destruct (aeval st be) eqn:Eqnbe; inversion H₁₀; inversion H₁;
    subst; simpl in *; clear H₁₀; clear H₁; rewrite Eqnbe in H₁₁.
    + rewrite <- Eqnbe. 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.
      × size_auto.
    + (* analog to false case *)
      rewrite <- Eqnbe. 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.
      × 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 (aeval st be) eqn:Eqnbe.
      × inversion H₁₂; subst; clear H₁₂.
        inversion H₁₀; subst; clear H₁₀; simpl in ×.
        rewrite Eqnbe. do 2 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 (rewrite app_nil_r; 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.
          - size_auto. }
        { apply IH in Hwhile; auto.
          - eapply ideal_unused_update_rev; eauto.
          - size_auto.
          - apply sel_slh_flag in H₁₃; try tauto.
            rewrite t_update_eq. rewrite Eqnbe. assumption. }
    + (* speculative; analog to non_speculative *)
      assert(Lnil: os₂ = [] ∧ ds₂ = []).
      { inversion H₁₀; subst; eauto. }
      destruct Lnil; subst; simpl.
      apply Ideal_If_F.
      destruct (aeval 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 (rewrite app_nil_r; 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.
          - size_auto. }
        { apply IH in Hwhile; auto.
          - rewrite Eqnbe in H₁₃.
            apply IH in H₁₃; try tauto.
            + apply ideal_unused_update_rev; eauto.
            + size_auto.
          - size_auto.
          - apply sel_slh_flag in H₁₃; try tauto.
            rewrite Eqnbe. rewrite t_update_eq. reflexivity. }
      × 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.
  (* ARead *)
  - (* Spec_ARead; public *)
    destruct (P x) eqn:Heq; try discriminate H.
    injection H; intros; subst; clear H.
    inversion H₁; clear H₁; subst. rewrite <- app_nil_r 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).
      replace (not_zero (if b' && P x then 1 else 0)) with (b' && P x)
        by (destruct (b' && P x); 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.

Speculative constant-time security for sel_slh

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 msf c →
    st₁ msf = 0 →
    st₂ msf = 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.

Monadic interpreter for speculative semantics (optional)

Module SpecCTInterpreter.

Since manually constructing directions for the proofs of examples is very time consuming, we introduce a sound monadic interpreter, which can be used to simplify the proofs of the 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).

Helper functions for individual 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 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, (os ++ [o ])%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 actual speculative 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_aexp be >>= fun bool_value ⇒
          observe (OBranch (not_zero bool_value)) >> fetch_direction >>=
        fun dop ⇒
          match dop with
          | Some DStep ⇒
              if not_zero bool_value then spec_eval_engine_aux fuel ct
              else spec_eval_engine_aux fuel cf
          | Some DForce ⇒
              start_speculating >>
              if not_zero 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.

Definition compute_fuel (c :com) (ds :dirs) : nat :=
  (* Reducing the fuel in the base cases of com_size does not break
     any proofs, but some of the tests below need a bit more to finish
     reducing (adding 2 is enough) *)
  2 +
    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 ∧ (os ++osn)%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].
    + reflexivity.
    + rewrite app_nil_r. reflexivity.
    + apply Spec_Skip.
  - (* Asgn *)
    simpl in Haux. inversion Haux; subst.
    ∃ []; ∃ []; split;[| split].
    + reflexivity.
    + rewrite app_nil_r. 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 (aeval st be) eqn:Eqnbe.
      × unfold obs, dirs, not_zero in Haux. simpl in Haux.
        destruct (spec_eval_engine_aux n' cf (st, ast, b, ds_tl, (os ++ [OBranch false ])%list)) 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); ∃ ([OBranch false ]++ost)%list; split;[| split].
        { simpl. rewrite Hds. reflexivity. }
        { rewrite app_assoc. rewrite Hos. reflexivity. }
        { erewrite <- not_zero_aeval_O; [| eassumption].
          apply Spec_If. rewrite Eqnbe. apply Heval. }
      × unfold obs, dirs, not_zero in Haux. simpl in Haux.
        destruct (spec_eval_engine_aux n' ct (st, ast, b, ds_tl, (os ++ [OBranch true ])%list)) 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); ∃ ([OBranch true ]++ost)%list; split;[| split].
        { simpl. rewrite Hds. reflexivity. }
        { rewrite app_assoc. rewrite Hos. reflexivity. }
        { erewrite <- not_zero_aeval_S; [| eassumption].
          apply Spec_If. rewrite Eqnbe. apply Heval. }
    + (* DForce *)
      destruct (aeval st be) eqn:Eqnbe.
      × unfold obs, dirs, not_zero in Haux. simpl in Haux.
        destruct (spec_eval_engine_aux n' ct (st, ast, true , ds_tl, (os ++ [OBranch false ])%list)) 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); ∃ ([OBranch false ]++ost)%list; split;[| split].
        { simpl. rewrite Hds. reflexivity. }
        { rewrite app_assoc. rewrite Hos. reflexivity. }
        { erewrite <- not_zero_aeval_O; [| eassumption].
          apply Spec_If_F. rewrite Eqnbe. apply Heval. }
      × unfold obs, dirs, not_zero in Haux. simpl in Haux.
        destruct (spec_eval_engine_aux n' cf (st, ast, true , ds_tl, (os ++ [OBranch true ])%list)) 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); ∃ ([OBranch true ]++ost)%list; split;[| split].
        { simpl. rewrite Hds. reflexivity. }
        { rewrite app_assoc. rewrite Hos. reflexivity. }
        { erewrite <- not_zero_aeval_S; [| eassumption].
          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.
  - (* 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_l.
  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.

Back to showing that our example is not speculative constant-time

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.

(* 2025-06-28 11:27 *)