Library miniasm

Require Import String.

Notation "'let' 'val' x ':=' t 'in' u" :=
  (match t with
   | Some x => u
   | None => None
   end)
    (at level 200, x ident, t at level 100, u at level 200, only parsing).

Notation "'let' 'val' ( x , y ) ':=' t 'in' u" :=
  (match t with
   | Some (x, y) => u
   | None => None
   end)
    (at level 200, x ident, t at level 100, u at level 200, only parsing).

Notation "'let' 'val' ( x , y , z ) ':=' t 'in' u" :=
  (match t with
   | Some (x, y, z) => u
   | None => None
   end)
    (at level 200, x ident, t at level 100, u at level 200, only parsing).

Notation "'ret' e" := (Some e) (at level 200, only parsing).
Notation "'exit'" := None (at level 200, only parsing).

Notation "e '==?' v" := (e = Some v) (at level 70, only parsing).

Definition var := string.

The mini-language instructions :

Inductive instr :=
| Init : var -> nat -> instr
| Assign : var -> var -> instr
| Addv : var -> var -> instr
| Subv : var -> var -> instr
| Branch : nat -> instr
| Branchif : var -> nat -> instr
| Return : instr.

Open Scope list_scope.
Require Import List.

Definition eq_var x y := if string_dec x y then true else false.

Require Import Arith.
Definition eq_nat x y := x =? y.

Fixpoint assoc_opt {A} {B} (f: A -> A -> bool) (x:A) (l:list (A * B)) : option B :=
  match l with
   | (y,k)::l => if f x y then Some k else assoc_opt f x l
   | nil => None
  end.

Notation assoc_var := (assoc_opt eq_var).
Notation assoc_instr := (assoc_opt eq_nat).
Notation program := (list (nat * instr)).

Fixpoint assign {A} {B} (f: A -> A -> bool) (x:A) (v:B) (l:list (A * B)) : list (A * B) :=
  match l with
  | nil => (x ,v )::l
  | (y,k)::l => if f x y then (y,v )::l else (y,k)::assign f x v l
  end.

Notation assign_var := (assign eq_var).

Definition lifted_plus v w :=
  let val n := v in
  let val m := w in
  ret n + m.

Definition lifted_minus v w :=
  let val n := v in
  let val m := w in
  ret n - m.

Local Open Scope string_scope.

A state is a program * a code pointer * a memory

Definition state : Type := list (nat * instr) * nat * list (var * option nat).

The step function of the mini-language :

Fixpoint step_opt (st : state): option state :=
  match st with
  | (p, pc, m) =>
    match assoc_instr pc p with
    | Some i =>
      match i with
      | Init x n =>
        ret (p, pc + 1, assign_var x (Some n) m)
      | Assign x y =>
        let val w := assoc_var y m in
        ret (p, pc + 1, assign_var x w m)
      | Addv x y =>
        let val v := assoc_var x m in
        let val w := assoc_var y m in
        let k := lifted_plus v w in
        ret (p, pc + 1, assign_var x k m)
      | Subv x y =>
        let val v := assoc_var x m in
        let val w := assoc_var y m in
        let k := lifted_minus v w in
        ret (p, pc + 1, assign_var x k m)
      | Branch n => ret (p, n, m)
      | Branchif x n =>
        let val v := assoc_var x m in
        match v with
        | Some a => if eq_nat a 0 then ret (p, pc + 1, m) else ret (p, n, m)
        | None => exit
        end
      | Return => exit
      end
    | None => exit
    end
  end.

The deterministic small-step semantics of the mini-lang :

Inductive det_sem : state -> state -> Prop :=
| Step_1 : forall p pc m x n,
    assoc_instr pc p ==? (Init x n ) ->
    det_sem (p , pc , m ) (p , pc + 1, assign eq_var x (Some n) m )
| Step_2 : forall p pc m x y w,
    assoc_instr pc p ==? (Assign x y ) ->
    assoc_var y m ==? w ->
    det_sem (p , pc , m ) (p , pc + 1, assign eq_var x w m )
| Step_3 : forall p pc m x y v w,
    assoc_instr pc p ==? (Addv x y ) ->
    assoc_var x m ==? v ->
    assoc_var y m ==? w ->
    det_sem (p , pc , m ) (p , pc + 1, assign eq_var x (lifted_plus v w) m )
| Step_4 : forall p pc m x y v w,
    assoc_instr pc p ==? (Subv x y ) ->
    assoc_var x m ==? v ->
    assoc_var y m ==? w ->
    det_sem (p , pc , m ) (p , pc + 1, assign eq_var x (lifted_minus v w) m )
| Step_5 : forall p pc m n,
    assoc_instr pc p ==? (Branch n ) ->
    det_sem (p , pc , m ) (p , n , m )
| Step_6 : forall p pc m x n,
    assoc_instr pc p ==? (Branchif x n ) ->
    assoc_var x m ==? (Some 0) ->
    det_sem (p , pc , m ) (p , pc + 1, m )
| Step_7 : forall p pc m x n k,
    assoc_instr pc p ==? (Branchif x n ) ->
    assoc_var x m ==? (Some (S k)) ->
    det_sem (p , pc , m ) (p , n , m )
.

Proof that the function and the inductive relation are the same :

Lemma step_opt_det_sem : forall s s' , step_opt s = Some s' <-> det_sem s s'.

Some variables values might not be known at compile time : we introduce a non-deterministic semantics for dealing with this

An erased memory is a memory with less known variables (unknown variable = None value) :

Inductive erased : list (var * option nat) -> list (var * option nat) -> Prop :=
| Erased_1: forall x v tl1 tl2,
    erased tl1 tl2 ->
    erased ((x , v ) :: tl1) ((x , v ) :: tl2)
| Erased_2: forall x a tl1 tl2,
    erased tl1 tl2 ->
    erased ((x , Some a ) :: tl1) ((x , None ) :: tl2)
| Erased_3: erased nil nil
.

An erased state contains an erased memory

Inductive state_erased: state -> state -> Prop :=
| State_Erased : forall p pc m1 m2,
erased m1 m2 ->
state_erased (p , pc , m1 ) (p , pc , m2 ).

A (deterministic) run follows the deterministic semantics upto a return instruction

Inductive run: state -> (list state ) -> Prop :=
| Run_1 : forall p pc m,
    assoc_instr pc p ==? Return ->
    run (p , pc , m ) ((p , pc , m )::nil)
| Run_2 : forall st st' r,
    step_opt st ==? st' ->
    run st' r ->
    run st (st ::r)
.

Lemma run_init : forall s s' T , run s (s'::T) -> s = s'.

We use a cost function to compute the cost of a run

First a function giving each instruction a cost

Parameter instr_cost : instr -> nat.

The function that computes the cost associated with a state

Definition step_cost {A} (st: (program * nat * A)) :=
  match st with
  | (p, pc, m) =>
    match assoc_instr pc p with
    | None => None
    | Some i => Some (instr_cost i)
    end
  end.

The cost of a run

Fixpoint cost {A} (r: list (program * nat * A)) :=
  match r with
  | nil => 0
  | (st :: t) =>
    match step_cost st with
    | Some k => k + cost t
    | None => 0
    end
  end.

The cost of a step is the same even with an erased memory

Lemma step_cost_erased_is_equal : forall s s' , state_erased s s' -> step_cost (s) = step_cost(s').

An erased trace is a run with all its states (more or less) erased

Inductive erased_trace: list state -> list state -> Prop :=
| Erased_Trace_1 :
    erased_trace nil nil
| Erased_Trace_2 : forall st1 st1' T1 T1',
    state_erased st1 st1' ->
    erased_trace T1 T1' ->
    erased_trace (st1 ::T1) (st1'::T1').

The cost of an erased trace is the same as the initial trace

Lemma trace_cost_erased_is_equal : forall T T', erased_trace T T' -> cost(T) = cost(T').

max run cost computes the most expensive cost of an (erased) program : if there is ambiguity as to which branch to take, the max run takes the branch with the greater cost

Inductive max_run_cost : state -> nat -> Prop :=
| Max_Run_Cost_1 : forall p pc m,
    assoc_instr pc p ==? Return ->
    max_run_cost (p , pc , m ) (instr_cost Return)
| Max_Run_Cost_2 : forall st st' c k,
    step_opt st ==? st' ->
    step_cost st ==? c ->
    max_run_cost st' k ->
    max_run_cost st (c + k)
| Max_Run_Cost_3 : forall p pc m x n c k k',
    assoc_instr pc p ==? (Branchif x n ) ->
    assoc_var x m ==? None ->
    step_cost (p , pc , m ) ==? c ->
    max_run_cost (p , pc + 1, m ) k ->
    max_run_cost (p , n , m ) k' ->
    k > k' ->
    max_run_cost (p , pc , m ) (c + k)
| Max_Run_Cost_4 : forall p pc m x n c k k',
    assoc_instr pc p ==? (Branchif x n ) ->
    assoc_var x m ==? None ->
    step_cost (p , pc , m ) ==? c ->
    max_run_cost (p , pc + 1, m ) k ->
    max_run_cost (p , n , m ) k' ->
    k <= k' ->
    max_run_cost (p , pc , m ) (c + k').

Another definition of max run cost

Inductive max_run_cost2 : state -> nat -> Prop :=
| Max_Run_Cost2_1 : forall p pc m,
    assoc_instr pc p ==? Return ->
    max_run_cost2 (p , pc , m ) (instr_cost Return)
| Max_Run_Cost2_2 : forall st st' c k,
    step_opt st ==? st' ->
    step_cost st ==? c ->
    max_run_cost2 st' k ->
    max_run_cost2 st (c + k)
| Max_Run_Cost2_3 : forall p pc m x n c k k',
    assoc_instr pc p ==? (Branchif x n ) ->
    assoc_var x m ==? None ->
    step_cost (p , pc , m ) ==? c ->
    max_run_cost2 (p , pc + 1, m ) k ->
    max_run_cost2 (p , n , m ) k' ->
    max_run_cost2 (p , pc , m ) (c + max k k').

Require Import Omega.

Lemma max_is_max : forall k k' , k > k' -> max k k' = k.

Lemma max_is_max2 : forall k k', k <= k' -> max k k' = k'.

Lemma max_run_max1 : forall s k k' , max_run_cost s k -> k > k' -> max_run_cost s (Init.Nat.max k k') .

Lemma max_run_max2 : forall s k k' , max_run_cost s (k') -> k <= k' -> max_run_cost s (Init.Nat.max k k') .

The two definitions of max run cost are equivalent

Lemma max_run_cost_equiv_max_run_cost2 : forall s k , max_run_cost s k <-> max_run_cost2 s k.
Search (_ <= max _ _).
Search ( ( _ <=? _ ) ).
Qed.

The cost of a step is unique : there is no other identical step with a different cost

Lemma step_cost_is_unique : forall (s:state) k k' , step_cost s = Some k -> step_cost s = Some k' -> k = k'.

The maximum cost is unique : there are no two identical computation of max_run_cost that give different results

Lemma max_run_cost_is_unique : forall s k , max_run_cost s k -> forall k' , max_run_cost s k' -> k = k'.

Every transition in the deterministic semantics exists in the non-deterministic semantics

Lemma embedding : forall s s' , (det_sem s s') -> (nondet_sem s s').

Some useful auxiliary lemmas ...

Erasure is reflexive

The conservation property : if there is a transition s1 ~~> s2 in the non-deterministic semantics, there exists an equivalent transition s1' ~~> s2' with erased memories (ie. s1 --> s1' and s2 --> s2')

Lemma conservation : forall P pc1 pc2 M1 M2 M1' ,
nondet_sem (P ,pc1 ,M1 ) (P ,pc2 ,M2 ) -> erased M1 M1' -> exists M2' , nondet_sem (P ,pc1 ,M1') (P ,pc2 ,M2') /\ erased M2 M2'.

The conservations property holds when going from the deterministic semantics to the nondet :

Lemma post_embedding_conservation : forall P pc1 pc2 M1 M2 M1' ,
det_sem (P ,pc1 ,M1 ) (P ,pc2 ,M2 ) -> erased M1 M1' -> exists M2' , nondet_sem (P ,pc1 ,M1') (P ,pc2 ,M2') /\ erased M2 M2'.

A trace in the non-deterministic semantics :

Inductive trace_nondet: list state -> Prop :=
| Trace_Nondet_1 : forall st,
    trace_nondet (st ::nil)
| Trace_Nondet_2 : forall st1 st2 r,
    (nondet_sem st1 st2 ) ->
    trace_nondet (st2 ::r) ->
    trace_nondet (st1 ::st2 ::r).

A deterministic trace is a non-deterministic trace

Lemma trace_embedding : forall s T , run s T -> trace_nondet (T).

A program doesnt change after erasure of the memory of the state

Lemma program_invariant : forall p1 p2 pc1 pc2 m1 m2,
nondet_sem (p1 ,pc1 ,m1 ) (p2 ,pc2 ,m2 ) -> p1 = p2.

Conservation property for nondet traces

Lemma trace_conservation : forall T s s' ,
    trace_nondet (s ::T) -> state_erased s s' -> exists T' , erased_trace (s ::T) (s'::T') /\ trace_nondet(s'::T').

Lemma post_embedding_trace_conservation : forall T s s' ,
    run s (s ::T) -> state_erased s s' -> exists T', erased_trace (s ::T) (s'::T') /\ trace_nondet (s'::T').

Lemma post_embedding_trace_conservation' : forall T s ,
    run s (T) -> exists T', erased_trace (T) (T') /\ trace_nondet (T').

The final function returns True if the given state is final (i.e. is a Return instr)

Definition final (st : option state) :=
  match st with
  | None => False
  | Some (p, pc, m) => assoc_instr pc p ==? Return
  end.

The last function returns the last state of a trace :

Fixpoint last {A} (l : list A) :=
  match l with
  | nil => None
  | (h :: nil) => Some h
  | (h :: t) => last t
  end.

last doesnt care about the head of a trace :

Lemma last_cons : forall st (r : list state) , r <> nil -> last(st :: r) = last (r).

A normal trace is a trace that ends with a Return instruction :

Definition trace_norm (T : list state) := final(last(T)).

A finite trace is a trace that follows the non deterministic semantics and ends with a return instruction :

Definition trace_finite (T : list state) := final(last(T)) /\ trace_nondet(T).

Obvious lemmas :

Lemma trace_finite_is_trace_nondet : forall T, trace_finite T -> trace_nondet T.

Lemma erased_trace_same_length : forall T T', erased_trace T T' -> length T = length T'.

Lemma trace_nondet_cons : forall T s , T <> nil -> trace_nondet (s ::T) -> trace_nondet T.

Lemma nondet_erased_is_nondet : forall s1 s1' s2 ,
nondet_sem s1 s2 -> state_erased s1 s1' -> exists s2', nondet_sem s1' s2'.

Lemma trace_finite_is_normal : forall T , trace_finite T -> final(last(T)).

A deterministic run finishes with the return instruction, it is thus normal :

Lemma deterministic_is_normal : forall s T ,
run s T -> final (last (T)).

Because the deterministic semantics can be lifted to the non deterministic semantics, a deterministic run is a finite run

Lemma deterministic_is_finite : forall s T,
run s T -> trace_finite T.

A normal run stays normal after erasure of its memory

  Lemma erased_norm_is_norm_aux: forall t t',
      erased_trace t t' ->
      final (last (t)) ->
      final (last (t')).

  Lemma erased_norm_is_norm : forall r,
      final(last(r)) -> forall r', erased_trace r r' -> final (last(r')).

The max run is very close to max run cost but returns the trace of the maximum run of the program, not its cost

  Inductive max_run: state -> (list state ) -> Prop :=
| Max_Run_1 : forall p pc m,
    assoc_instr pc p ==? Return ->
    max_run (p , pc , m ) ((p , pc , m ) :: nil)
| Max_Run_2 : forall st st' r,
    step_opt st ==? st' ->
    max_run st' r ->
    max_run st (st ::r)
| Max_Run_3 : forall p pc m x n r r',
    assoc_instr pc p ==? (Branchif x n ) ->
    assoc_var x m ==? None ->
    max_run (p , pc + 1, m ) r ->
    max_run (p , n , m ) r' ->
    cost r > cost r' ->
    max_run (p , pc , m ) ((p , pc , m ) :: r)
| Max_Run_4 : forall p pc m x n r r',
    assoc_instr pc p ==? (Branchif x n ) ->
    assoc_var x m ==? None ->
    max_run (p , pc + 1, m ) r ->
    max_run (p , n , m ) r' ->
    cost r <= cost r' ->
    max_run (p , pc , m ) ((p , pc , m ) :: r')
.

Useful property : a max run always begins with its the state given as a first parameter :

Lemma max_run_init : forall s s' T , max_run s (s' :: T) -> s = s'.

A max run is a special case of finite run :

Lemma max_run_is_finite : forall s T , max_run s T -> trace_finite T.

Quite obviously, the cost of the max run is the maximum cost of the program :

Lemma max_run_cost_is_max_cost: forall st k, max_run_cost st k -> exists r, max_run st r /\ cost r = k.

Some useful lemmas

Lemma L10: forall (st: state) r, cost (st :: r) >= cost (st :: nil).

Lemma L11: forall (st: state) r r', cost r >= cost r' -> cost (st :: r) >= cost (st :: r').

The max run is finite, thus it is normal :

Lemma max_run_is_normal : forall s T , max_run s T -> final(last(T)).

Auxiliary lemmas

Lemma max_run_init2 : forall s t , max_run s t -> exists t' , t = s ::t'.

Lemma nondet_det_equals : forall s s' s'' , nondet_sem s s' -> step_opt s ==? s'' -> s' = s''.

The max run has a cost that is greater than all the others finite traces :

Lemma max_run_is_max : forall st r, trace_finite (st ::r) -> forall r', max_run st (r') -> (cost (r') >= cost (st ::r)).

The cost of the max run is still greater than other finite traces even when its computed from an erased version of the memories of the traces

Lemma max_run_erased :
  forall m st', max_run st' m ->
                forall st r, trace_finite (st :: r) ->
                             forall r', trace_finite (st' :: r') ->
                                        erased_trace (st :: r) (st' :: r') ->
                                        cost m >= cost (st :: r).

The cost of the max run is greater than other finite traces even when its computed from an erased version of the memory of the beginning state

Lemma max_run_erased_is_max :
  forall m st', max_run st' m ->
                forall st r, trace_finite (st ::r) ->
                             state_erased st st' ->
                             cost m >= cost (st ::r).

The cost computed by max run cost from an erased version of the memory of the beginning state is greater than the cost of every finite trace

Lemma max_run_erased_is_max_cost :
  forall k st', max_run_cost st' k ->
                forall st r, trace_finite (st ::r) ->
                             state_erased st st' ->
                             k >= cost (st ::r).

The cost computed by max run cost from an erased version of the memory of the beginning state is greater than the actuel cost of the program

Theorem max_cost_final :
  forall k st', max_run_cost st' k ->
                forall st r, run st (st ::r) ->
                             state_erased st st' ->
                             k >= cost (st ::r).

The final theorem : k is an upper bound of the cost of the actual execution of the program

Theorem max_cost_final' :
  forall k st', max_run_cost st' k ->
                forall st r, run st (r) ->
                             state_erased st st' ->
                             k >= cost (r).

The theorem as it is shown in the manuscript :

Theorem max_cost_final_rephrased :
  forall k st st' t,
    run st (t) ->
    state_erased st st' ->
    max_run_cost st' k ->
    k >= cost (t).