(* Xavier Leroy's solution to List-machine benchmark,
     with proofs (and some auxiliary lemmas) deleted. *)

(*** Library ***)

Require Import Maps.

(*** Machine specification ***)

(** Abstract syntax of machine code **)

Definition var: Set := positive.
Definition var_eq: forall (v1 v2: var), {v1=v2} + {v1<>v2} := peq.
Definition V (n: nat) : var := P_of_succ_nat n.

Definition label: Set := positive.
Definition label_eq: forall (l1 l2: label), {l1=l2} + {l1<>l2} := peq.
Definition L (n: nat) : label := P_of_succ_nat n.

Inductive instr: Set :=
  | instr_jump: label -> instr
  | instr_branch_if_nil: var -> label -> instr
  | instr_fetch_field: var -> nat -> var -> instr
  | instr_cons: var -> var -> var -> instr
  | instr_halt: instr
  | instr_seq: instr -> instr -> instr.

Infix "::" := instr_seq (at level 60, right associativity).

Inductive program: Set :=
  | prog_end: program
  | prog_block: label -> instr -> program -> program.

Fixpoint program_lookup (p: program) (l: label) {struct p} : option instr :=
  match p with
  | prog_end => None
  | prog_block l' i p' =>
      if label_eq l' l then Some i else program_lookup p' l
  end.

(** Run-time values and environments **)

Inductive value: Set :=
  | value_nil: value
  | value_cons: value -> value -> value.

Definition store := map value.
Definition store_empty : store := empty value.

(** Execution of machine code **)

Inductive step: program -> store -> instr -> store -> instr -> Prop :=

  | step_seq: forall p r i1 i2 i3,
    (*----------------------------------------------------*)
      step p r ((i1 :: i2) :: i3) r (i1 :: i2 :: i3)

  | step_fetch_field_0: forall p r v1 v2 i a0 a1,
      r#v1 = Some (value_cons a0 a1) ->
    (*----------------------------------------------------*)
      step p r (instr_fetch_field v1 0 v2 :: i) (r#v2 <- a0) i

  | step_fetch_field_1: forall p r v1 v2 i a0 a1,
      r#v1 = Some (value_cons a0 a1) ->
    (*----------------------------------------------------*)
      step p r (instr_fetch_field v1 1 v2 :: i) (r#v2 <- a1) i

  | step_cons: forall p r v1 v2 v3 i a1 a2,
      r#v1 = Some a1 ->
      r#v2 = Some a2 ->
    (*----------------------------------------------------*)
      step p r (instr_cons v1 v2 v3 :: i) (r#v3 <- (value_cons a1 a2)) i

  | step_branch_not_taken: forall p r v l i a1 a2,
      r#v = Some (value_cons a1 a2) ->
    (*----------------------------------------------------*)
      step p r (instr_branch_if_nil v l :: i) r i

  | step_branch_taken: forall p r v l i i',
      r#v = Some value_nil ->
      program_lookup p l = Some i' ->
    (*----------------------------------------------------*)
      step p r (instr_branch_if_nil v l :: i) r i'

  | step_jump: forall p r l i',
      program_lookup p l = Some i' ->
    (*----------------------------------------------------*)
      step p r (instr_jump l) r i'.

Inductive run: program -> store -> instr -> Prop :=

  | run_halt: forall p r,
    (*----------------------------------------------------*)
      run p r instr_halt

  | run_step: forall p r i r' i',
      step p r i r' i' -> run p r' i' ->
    (*----------------------------------------------------*)
      run p r i.

Inductive run_prog : program -> Prop :=
  | run_prog_intro: forall p i,
      program_lookup p (L 0) = Some i ->
      run p (store_empty#1 <- value_nil) i ->
    (*----------------------------------------------------*)
      run_prog p.

Hint Resolve step_seq step_fetch_field_0 step_fetch_field_1
  step_cons step_branch_not_taken step_branch_taken
  step_jump run_halt run_step run_prog_intro: exec.

(*** Types ***)

Inductive ty: Set :=
  | ty_nil: ty
  | ty_list: ty -> ty
  | ty_listcons: ty -> ty.

Inductive subtype: ty -> ty -> Prop :=
  | subtype_refl: forall t,
      subtype t t
  | subtype_nil: forall t,
      subtype ty_nil (ty_list t)
  | subtype_list: forall t t',
      subtype t t' ->
      subtype (ty_list t) (ty_list t')
  | subtype_listcons: forall t t',
      subtype t t' ->
      subtype (ty_listcons t) (ty_listcons t')
  | subtype_listmixed: forall t t',
      subtype t t' ->
      subtype (ty_listcons t) (ty_list t').


Hint Resolve subtype_refl subtype_nil subtype_list
             subtype_listcons subtype_listmixed: typing.

Fixpoint lub (s t: ty) {struct s}: ty :=
  match s, t with
  | ty_nil, ty_nil => ty_nil
  | ty_nil, ty_list t1 => ty_list t1
  | ty_nil, ty_listcons t1 => ty_list t1
  | ty_list s1, ty_nil => ty_list s1
  | ty_list s1, ty_list t1 => ty_list (lub s1 t1)
  | ty_list s1, ty_listcons t1 => ty_list (lub s1 t1)
  | ty_listcons s1, ty_nil => ty_list s1
  | ty_listcons s1, ty_list t1 => ty_list (lub s1 t1)
  | ty_listcons s1, ty_listcons t1 => ty_listcons (lub s1 t1)
  end.

Definition env : Set := map ty.
Definition env_empty : env := empty ty.

Definition env_sub (vt1 vt2: env) : Prop :=
  forall v t2,
  vt2#v = Some t2 -> exists t1, vt1#v = Some t1 /\ subtype t1 t2.

Definition program_typing : Set := map env.
Definition program_typing_empty : program_typing := empty env.

Inductive check_instr: program_typing -> env -> instr -> env -> Prop :=

  | check_instr_seq: forall pt e e' e'' i1 i2,
      check_instr pt e i1 e' ->
      check_instr pt e' i2 e'' ->
    (*----------------------------------------------------*)
      check_instr pt e (i1 :: i2) e''

  | check_instr_branch_list: forall pt e v l t e1,
      e#v = Some (ty_list t) ->
      pt#l = Some e1 ->
      env_sub (e#v <- ty_nil) e1 ->
    (*----------------------------------------------------*)
      check_instr pt e (instr_branch_if_nil v l) (e#v <- (ty_listcons t))

  | check_instr_branch_listcons: forall pt e v l t,
      e#v = Some (ty_listcons t) ->
    (*----------------------------------------------------*)
      check_instr pt e (instr_branch_if_nil v l) e

  | check_instr_branch_nil: forall pt e v l e1,
      e#v = Some (ty_nil) ->
      pt#l = Some e1 ->
      env_sub e e1 ->
    (*----------------------------------------------------*)
      check_instr pt e (instr_branch_if_nil v l) e

  | check_instr_fetch_0: forall pt e v1 v2 t,
      e#v1 = Some (ty_listcons t) ->
    (*----------------------------------------------------*)
      check_instr pt e (instr_fetch_field v1 0 v2) (e#v2 <- t)

  | check_instr_fetch_1: forall pt e v1 v2 t,
      e#v1 = Some (ty_listcons t) ->
    (*----------------------------------------------------*)
      check_instr pt e (instr_fetch_field v1 1 v2) (e#v2 <- (ty_list t))

  | check_instr_cons: forall pt e v1 v2 v3 t1 t2 t3,
      e#v1 = Some t1 ->
      e#v2 = Some t2 ->
      lub (ty_list t1) t2 = (ty_list t3) ->
    (*----------------------------------------------------*)
      check_instr pt e (instr_cons v1 v2 v3) (e#v3 <- (ty_listcons t3)).

Inductive check_block: program_typing -> env -> instr -> Prop :=

  | check_block_halt: forall pt e,
    (*----------------------------------------------------*)
      check_block pt e instr_halt

  | check_block_seq: forall pt e i1 i2 e',
      check_instr pt e i1 e' ->
      check_block pt e' i2 ->
    (*----------------------------------------------------*)
      check_block pt e (i1 :: i2)

  | check_block_jump: forall pt e l e1,
      pt#l = Some e1 ->
      env_sub e e1 ->
    (*----------------------------------------------------*)
      check_block pt e (instr_jump l).


Inductive check_blocks: program_typing -> program -> Prop :=
  | check_blocks_empty: forall pt,
      check_blocks pt prog_end
  | check_blocks_label: forall pt lbl i p e,
      pt#lbl = Some e ->
      check_block pt e i ->
      check_blocks pt p ->
      check_blocks pt (prog_block lbl i p).

Definition typing_dom_match (pt: program_typing) (p: program) : Prop :=
  forall lbl e,
  pt#lbl = Some e -> exists i, program_lookup p lbl = Some i.

Definition env_0 : env := env_empty#(V 0) <- ty_nil.

Inductive check_program: program_typing -> program -> Prop :=
  | check_program_intro: forall pt p,
      pt#(L 0) = Some env_0 ->
      check_blocks pt p ->
      typing_dom_match pt p ->
      check_program pt p.

Hint Resolve check_instr_seq check_instr_branch_list
  check_instr_branch_listcons check_instr_branch_nil
  check_instr_fetch_0 check_instr_fetch_1 check_instr_cons
  check_block_halt check_block_seq check_block_jump: typing.

(*** Proof of type safety ***)

(* Correctness of lub *)

Lemma lub_comm:
  forall t1 t2, lub t2 t1 = lub t1 t2.
Proof.
  induction t1; destruct t2; simpl; auto; rewrite IHt1; auto.
Qed.

Lemma lub_subtype_left:
  forall t1 t2, subtype t1 (lub t1 t2).
Proof.
  induction t1; destruct t2; simpl; auto with typing.
Qed.

Lemma lub_subtype_right:
  forall t1 t2, subtype t2 (lub t1 t2).
Admitted.

Lemma lub_idem:
  forall t, lub t t = t.
Admitted.

Lemma lub_of_subtype:
  forall t1 t2, subtype t1 t2 -> lub t2 t1 = t2.
Admitted.

Lemma lub_least:
  forall t1 t3, subtype t1 t3 ->
  forall t2 (S: subtype t2 t3), subtype (lub t1 t2) t3.
Admitted.

(* Agreement between values and types *)

Inductive value_has_ty: value -> ty -> Prop :=
  | value_has_ty_nil_nil:
      value_has_ty value_nil ty_nil
  | value_has_ty_nil_list: forall t,
      value_has_ty value_nil (ty_list t)
  | value_has_ty_cons_listcons: forall v1 v2 t,
      value_has_ty v1 t ->
      value_has_ty v2 (ty_list t) ->
      value_has_ty (value_cons v1 v2) (ty_listcons t)
  | value_has_ty_cons_list: forall v1 v2 t,
      value_has_ty v1 t ->
      value_has_ty v2 (ty_list t) ->
      value_has_ty (value_cons v1 v2) (ty_list t).

Hint Resolve value_has_ty_nil_nil value_has_ty_nil_list
             value_has_ty_cons_listcons value_has_ty_cons_list: typing.

(* Agreement between variable environment and variable typing *)

Definition store_has_ty (s: store) (e: env) : Prop :=
  forall r t,
  e#r = Some t -> exists v, s#r = Some v /\ value_has_ty v t.

Lemma var_set_type:
  forall s e v t r,
  store_has_ty s e ->
  value_has_ty v t ->
  store_has_ty (s#r <- v) (e#r <- t).
Proof.
  intros; red; intros r' t'.
  repeat rewrite get_set. case (peq r r'); intros.
  exists v; split. auto. replace t' with t. auto. congruence.
  apply H; auto.
Qed. 

Lemma var_set_type_refine:
  forall s e v t r,
  store_has_ty s e ->
  s#r = Some v ->
  value_has_ty v t ->
  store_has_ty s (e#r <- t).
Admitted.

Lemma store_has_ty_empty:
  store_has_ty store_empty env_empty.
Admitted.

(* Lemma store_lookup_has_ty: ... *)

(* Subtyping and value-type agreement *)

Lemma subsumption:
  forall v t1, value_has_ty v t1 ->
  forall t2, subtype t1 t2 -> value_has_ty v t2.
Proof.
  induction 1; intros.
  inversion H; auto with typing.
Admitted.


(* Subject reduction *)

Lemma preservation:
  forall p s1 i1 s2 i2,
  step p s1 i1 s2 i2 ->
  forall pt e1
    (CHKPROG: check_program pt p)
    (STORETY: store_has_ty s1 e1)
    (CHKBLOCK: check_block pt e1 i1),
  exists e2, store_has_ty s2 e2 /\ check_block pt e2 i2.
Admitted.

(* Progress *)

Inductive step_or_halt: program -> store -> instr -> Prop :=
  | step_or_halt_step: forall p r i r' i',
      step p r i r' i' -> step_or_halt p r i
  | step_or_halt_halt: forall p r,
      step_or_halt p r instr_halt.

Lemma progress:
  forall pt e i,
  check_block pt e i ->
  forall p s,
  check_program pt p ->
  store_has_ty s e ->
  step_or_halt p s i.
Admitted.

(* Safety property *)

Inductive run_prog_finite: program -> store -> instr -> Prop :=
  | run_prog_finite_start: forall p i,
      program_lookup p (L 0) = Some i ->
      run_prog_finite p (store_empty#(V 0) <- value_nil) i
  | run_prog_finite_step: forall p r i r' i',
      step p r i r' i' ->
      run_prog_finite p r i ->
      run_prog_finite p r' i'.

Theorem safety:
  forall p s i pt,
  check_program pt p ->
  run_prog_finite p s i ->
  step_or_halt p s i.
Admitted.

(*** Type-checking algorithm ***)

Require Import Bool.

Fixpoint check_subtype (t1 t2: ty) {struct t1} : bool :=
  match t1, t2 with
  | ty_nil, ty_nil => true
  | ty_nil, ty_list t1 => true
  | ty_nil, ty_listcons t1 => false
  | ty_list s1, ty_nil => false
  | ty_list s1, ty_list t1 => check_subtype s1 t1
  | ty_list s1, ty_listcons t1 => false
  | ty_listcons s1, ty_nil => false
  | ty_listcons s1, ty_list t1 => check_subtype s1 t1
  | ty_listcons s1, ty_listcons t1 => check_subtype s1 t1
  end.

Lemma check_subtype_correct:
  forall t1 t2, check_subtype t1 t2 = true -> subtype t1 t2.
Admitted.

Definition check_env_binding_sub (t: ty) (ot: option ty) :=
  match ot with
  | None => false
  | Some t' => check_subtype t' t
  end.

Definition check_env_sub (e1 e2: env) : bool :=
  map_forall2 ty ty check_env_binding_sub e2 e1.

Lemma check_env_sub_correct:
  forall e1 e2, check_env_sub e1 e2 = true -> env_sub e1 e2.
Admitted.
    
Definition typecheck_branch (pt: program_typing) (vt: env) (l: label): bool :=
  match pt#l with
  | None => false
  | Some vt' => check_env_sub vt vt'
  end.

Lemma typecheck_branch_correct:
  forall pt vt l,
  typecheck_branch pt vt l = true ->
  exists vt', pt#l = Some vt' /\ env_sub vt vt'.
Admitted.

Fixpoint typecheck_instr (pt: program_typing) (e: env) (i: instr)
                         {struct i}: option env :=
  match i with
  | i1 :: i2 =>
      match typecheck_instr pt e i1 with
      | None => None
      | Some e1 => typecheck_instr pt e1 i2
      end
  | instr_branch_if_nil v l =>
      match e#v with
      | None => None
      | Some (ty_list t) =>
          if typecheck_branch pt (e#v <- ty_nil) l
          then Some (e#v <- (ty_listcons t))
          else None
      | Some (ty_listcons t) =>
          Some e
      | Some ty_nil =>
          if typecheck_branch pt e l
          then Some e
          else None
      end
  | instr_fetch_field v1 0 v2 =>
      match e#v1 with
      | Some (ty_listcons t) => Some (e#v2 <- t)
      | _ => None
      end
  | instr_fetch_field v1 1 v2 =>
      match e#v1 with
      | Some (ty_listcons t) => Some (e#v2 <- (ty_list t))
      | _ => None
      end
  | instr_cons v1 v2 v3 =>
      match e#v1, e#v2 with
      | Some t1, Some t2 =>
          match lub (ty_list t1) t2 with
          | ty_list t3 => Some (e#v3 <- (ty_listcons t3))
          | _ => None
          end
      | _, _ => None
      end
  | _ =>
      None
  end.

Lemma typecheck_instr_correct:
  forall pt i e e',
  typecheck_instr pt e i = Some e' ->
  check_instr pt e i e'.
Admitted.

Fixpoint typecheck_block (pt: program_typing) (e: env) (i: instr)
                         {struct i}: bool :=
  match i with
  | instr_halt => true
  | i1 :: i2 =>
      match typecheck_instr pt e i1 with
      | None => false
      | Some e1 => typecheck_block pt e1 i2
      end
  | instr_jump l =>
      typecheck_branch pt e l
  | _ => false
  end.

Lemma typecheck_block_correct:
  forall pt i e,
  typecheck_block pt e i = true ->
  check_block pt e i.
Admitted.

Fixpoint typecheck_blocks (pt: program_typing) (p: program) 
         {struct p}: bool :=
  match p with
  | prog_end => true
  | prog_block lbl i p' =>
      match pt#lbl with
      | None => false
      | Some e => typecheck_block pt e i && typecheck_blocks pt p'
      end
  end.

Lemma typecheck_blocks_correct:
  forall pt p,
  typecheck_blocks pt p = true ->
  check_blocks pt p.
Admitted.

Fixpoint label_map (p: program) : map instr :=
  match p with
  | prog_end => empty instr
  | prog_block lbl i p => (label_map p)#lbl <- i
  end.

Definition typecheck_typing_dom_match (pt: program_typing) (p: program) : bool :=
  map_forall2 env instr
    (fun e opt_i => match opt_i with None => false | Some _ => true end)
    pt (label_map p).

Lemma typecheck_typing_dom_match_correct:
  forall pt p,
  typecheck_typing_dom_match pt p = true ->
  typing_dom_match pt p.
Admitted.

Lemma type_eq_dec:
  forall (t1 t2: ty), {t1=t2} + {t1<>t2}.
Proof.
  decide equality. 
Defined.

Lemma env_eq_dec:
  forall (v1 v2: env), {v1=v2} + {v1<>v2}.
Proof.
  exact (map_eq _ type_eq_dec).
Defined.

Lemma program_typing_eq_dec:
  forall (p1 p2: program_typing), {p1=p2} + {p1<>p2}.
Proof.
  exact (map_eq _ env_eq_dec).
Defined.

Definition typecheck_typing_0 (pt: program_typing) : bool :=
  match pt#(L 0) with
  | None => false
  | Some vt => if env_eq_dec vt env_0 then true else false
  end.

Definition typecheck_program (pt: program_typing) (p: program) : bool :=
  typecheck_blocks pt p
  && typecheck_typing_0 pt
  && typecheck_typing_dom_match pt p.

Lemma typecheck_program_correct:
  forall pt p,
  typecheck_program pt p = true -> check_program pt p.
Admitted.

(* Completeness of the algorithm *)

Lemma check_subtype_refl:
  forall t, check_subtype t t = true.
Proof.
  induction t; simpl; auto.
Qed.

Lemma check_subtype_complete:
  forall t1 t2, subtype t1 t2 -> check_subtype t1 t2 = true.
Admitted.

Lemma check_env_sub_complete:
  forall e1 e2, env_sub e1 e2 -> check_env_sub e1 e2 = true.
Admitted.

Lemma typecheck_instr_complete:
  forall pt e i e', check_instr pt e i e' -> typecheck_instr pt e i = Some e'.
Admitted.

Lemma typecheck_program_complete:
  forall pt p, check_program pt p -> typecheck_program pt p = true.
Admitted.

(*** The sample program ***)

Open Scope positive_scope.

Definition psample :=
  prog_block (L 0)
    (instr_cons (V 0) (V 0) (V 1) ::
     instr_cons (V 0) (V 1) (V 1) :: 
     instr_cons (V 0) (V 1) (V 1) ::
     instr_jump (L 1))
 (prog_block (L 1)
    (instr_branch_if_nil (V 1) (L 2) ::
     instr_fetch_field (V 1) 1 (V 1) ::
     instr_branch_if_nil (V 1) (L 2) ::
     instr_jump (L 1))
 (prog_block (L 2)
    instr_halt
  prog_end)).

Definition envsample0 : env :=
  env_empty#(V 0) <- ty_nil.
Definition envsample1 : env := 
  (env_empty#(V 0) <- ty_nil)#(V 1) <- (ty_list ty_nil).
Definition envsample2 : env :=
  env_empty.

Definition ptsample : program_typing :=
  ((program_typing_empty#(L 0) <- envsample0)
                        #(L 1) <- envsample1)
                        #(L 2) <- envsample2.

Inductive outcome: Set :=
  | Finished: store -> outcome
  | Timeout: store -> instr -> outcome
  | Stuck: store -> instr -> outcome
  | No_entry_point: outcome.

Fixpoint exec (p: program) (s: store) (i: instr) (n: nat) {struct n} : outcome :=
  match n with
  | O => Timeout s i
  | S m =>
      match i with
      | (i1 :: i2) :: i3 =>
           exec p s (i1 :: i2 :: i3) m
      | instr_fetch_field v1 0 v2 :: i' =>
           match s#v1 with
           | Some (value_cons a0 a1) =>
               exec p (s#v2 <- a0) i' m
           | _ => Stuck s i
           end
      | instr_fetch_field v1 1 v2 :: i' =>
           match s#v1 with
           | Some (value_cons a0 a1) =>
               exec p (s#v2 <- a1) i' m
           | _ => Stuck s i
           end
      | instr_cons v1 v2 v3 :: i' =>
           match s#v1, s#v2 with
           | Some a1, Some a2 =>
               exec p (s#v3 <- (value_cons a1 a2)) i' m
           | _, _ =>
               Stuck s i
           end
      | instr_branch_if_nil v l :: i' =>
           match s#v with
           | Some (value_cons a1 a2) =>
               exec p s i' m
           | Some value_nil =>
               match program_lookup p l with
               | Some i'' =>
                   exec p s i'' m
               | None => Stuck s i
               end
           | _ => Stuck s i
           end
      | instr_jump l =>
           match program_lookup p l with
           | Some i' =>
               exec p s i' m
           | _ => Stuck s i
           end
      | instr_halt =>
           Finished s
      | _ => Stuck s i
      end
  end.

Definition exec_prog (p: program) (n: nat): outcome :=
  match program_lookup p (L 0) with
  | None => No_entry_point 
  | Some i => exec p (store_empty#(V 0) <- value_nil) i n
  end.

Hint Resolve run_halt run_step run_prog_intro: exec.

Lemma exec_correct:
  forall p sfinal n s i,
  exec p s i n = Finished sfinal -> run p s i.
Admitted.

Lemma exec_prog_correct:
  forall p sfinal n, exec_prog p n = Finished sfinal -> run_prog p.
Admitted.

Eval compute in (exec_prog psample 20%nat).

Transparent lub.

Eval compute in (typecheck_program ptsample psample).


