(*
 * Copyright (c) Facebook, Inc. and its affiliates.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree.
 *)

(* Proofs about llvm to llair translation *)

open HolKernel boolLib bossLib Parse;
open listTheory arithmeticTheory pred_setTheory finite_mapTheory wordsTheory integer_wordTheory;
open settingsTheory miscTheory llvmTheory llairTheory llair_propTheory llvm_to_llairTheory;

new_theory "llvm_to_llair_prop";

numLib.prefer_num ();

Inductive v_rel:
  (∀w. v_rel (FlatV (PtrV w)) (FlatV (IntV (w2i w) pointer_size))) ∧
  (∀w. v_rel (FlatV (W1V w)) (FlatV (IntV (w2i w) 1))) ∧
  (∀w. v_rel (FlatV (W8V w)) (FlatV (IntV (w2i w) 8))) ∧
  (∀w. v_rel (FlatV (W32V w)) (FlatV (IntV (w2i w) 32))) ∧
  (∀w. v_rel (FlatV (W64V w)) (FlatV (IntV (w2i w) 64))) ∧
  (∀vs1 vs2.
    list_rel v_rel vs1 vs2
    ⇒
    v_rel (AggV vs1) (AggV vs2))
End

(* Define when an LLVM state is related to a llair one. Parameterised over a
 * relation on program counters, which chould be generated by the
 * transformation. It is not trivial because the translation cuts up blocks at
 * function calls and for remiving phi nodes.
 *
 * Also parameterised on a map for locals relating LLVM registers to llair
 * expressions that compute the value in that register. This corresponds to part
 * of the translation's state.
 *)
Definition state_rel_def:
  state_rel pc_rel emap (s:llvm$state) (s':llair$state) ⇔
    pc_rel s.ip s'.bp ∧
    (* Unmapped registers in LLVM are unmapped in llair too *)
    (∀r. flookup s.locals r = None ⇒ flookup emap r = None) ∧
    (* Mapped LLVM registers have a related value in the emap (after
     * evaluating) *)
    (∀r v. flookup s.locals r = Some v ⇒
      ∃v' e.
        v_rel v.value v' ∧
        flookup emap r = Some e ∧ eval_exp s' e v') ∧
    erase_tags s.heap = s'.heap
End

Theorem translate_arg_correct:
  ∀s a v pc_rel emap s'.
  state_rel pc_rel emap s s' ∧
  eval s a = Some v
  ⇒
  ∃v'. eval_exp s' (translate_arg emap a) v' ∧ v_rel v.value v'
Proof
  Cases_on `a` >> rw [eval_def, translate_arg_def]
  >- cheat >>
  CASE_TAC >> fs [PULL_EXISTS, state_rel_def] >>
  res_tac >> rfs [] >> metis_tac []
QED

Theorem translate_constant_correct_lem:
  (∀c s pc_rel emap s' (g : glob_var |-> β # word64).
   state_rel pc_rel emap s s'
   ⇒
   ∃v'. eval_exp s' (translate_const c) v' ∧ v_rel (eval_const g c) v') ∧
  (∀(cs : (ty # const) list) s pc_rel emap s' (g : glob_var |-> β # word64).
   state_rel pc_rel emap s s'
   ⇒
   ∃v'. list_rel (eval_exp s') (map (translate_const o snd) cs) v' ∧ list_rel v_rel (map (eval_const g o snd) cs) v') ∧
  (∀(tc : ty # const) s pc_rel emap s' (g : glob_var |-> β # word64).
   state_rel pc_rel emap s s'
   ⇒
   ∃v'. eval_exp s' (translate_const (snd tc)) v' ∧ v_rel (eval_const g (snd tc)) v')
Proof
  ho_match_mp_tac const_induction >> rw [translate_const_def] >>
  simp [Once eval_exp_cases, eval_const_def]
  >- (
    Cases_on `s` >> simp [eval_const_def, translate_size_def, v_rel_cases] >>
    metis_tac [truncate_2comp_i2w_w2i, dimindex_1, dimindex_8, dimindex_32, dimindex_64])
  >- (
    simp [v_rel_cases, PULL_EXISTS, MAP_MAP_o] >>
    fs [combinTheory.o_DEF, pairTheory.LAMBDA_PROD] >>
    metis_tac [])
  >- (
    simp [v_rel_cases, PULL_EXISTS, MAP_MAP_o] >>
    fs [combinTheory.o_DEF, pairTheory.LAMBDA_PROD] >>
    metis_tac [])
  >- cheat
  >- cheat
  >- cheat
  >- cheat
QED

Theorem translate_constant_correct:
  ∀c s pc_rel emap s' g.
   state_rel pc_rel emap s s'
   ⇒
   ∃v'. eval_exp s' (translate_const c) v' ∧ v_rel (eval_const g c) v'
Proof
  metis_tac [translate_constant_correct_lem]
QED

Theorem restricted_i2w_11:
  ∀i (w:'a word). INT_MIN (:'a) ≤ i ∧ i ≤ INT_MAX (:'a) ⇒ (i2w i : 'a word) = i2w (w2i w) ⇒ i = w2i w
Proof
  rw [i2w_def]
  >- (
    Cases_on `n2w (Num (-i)) = INT_MINw` >>
    rw [w2i_neg, w2i_INT_MINw] >>
    fs [word_L_def] >>
    `?j. 0 ≤ j ∧ i = -j` by intLib.COOPER_TAC >>
    rw [] >>
    fs [] >>
    `INT_MIN (:'a) < dimword (:'a)` by metis_tac [INT_MIN_LT_DIMWORD] >>
    `Num j MOD dimword (:'a) = Num j`
    by (irule LESS_MOD >> intLib.COOPER_TAC) >>
    fs []
    >- intLib.COOPER_TAC
    >- (
      `Num j < INT_MIN (:'a)` by intLib.COOPER_TAC >>
      fs [w2i_n2w_pos, integerTheory.INT_OF_NUM]))
  >- (
    fs [GSYM INT_MAX, INT_MAX_def] >>
    `Num i < INT_MIN (:'a)` by intLib.COOPER_TAC >>
    rw [w2i_n2w_pos, integerTheory.INT_OF_NUM] >>
    intLib.COOPER_TAC)
QED

Theorem translate_extract_correct:
  ∀pc_rel emap s1 s1' a v v1' e1' cs ns result.
    state_rel pc_rel emap s1 s1' ∧
    map (λci. signed_v_to_num (eval_const s1.globals ci)) cs = map Some ns ∧
    extract_value v ns = Some result ∧
    eval_exp s1' e1' v1' ∧
    v_rel v v1'
    ⇒
    ∃v2'.
      eval_exp s1' (foldl (λe c. Select e (translate_const c)) e1' cs) v2' ∧
      v_rel result v2'
Proof
  Induct_on `cs` >> rw [] >> fs [extract_value_def]
  >- metis_tac [] >>
  first_x_assum irule >>
  Cases_on `ns` >> fs [] >>
  qmatch_goalsub_rename_tac `translate_const c` >>
  `?v2'. eval_exp s1' (translate_const c) v2' ∧ v_rel (eval_const s1.globals c) v2'`
  by metis_tac [translate_constant_correct] >>
  Cases_on `v` >> fs [extract_value_def] >>
  qpat_x_assum `v_rel (AggV _) _` mp_tac >>
  simp [Once v_rel_cases] >> rw [] >>
  simp [Once eval_exp_cases, PULL_EXISTS] >>
  fs [LIST_REL_EL_EQN] >>
  qmatch_assum_rename_tac `_ = map Some is` >>
  Cases_on `eval_const s1.globals c` >> fs [signed_v_to_num_def, signed_v_to_int_def] >> rw [] >>
  `?i. v2' = FlatV i` by fs [v_rel_cases] >> fs [] >>
  qmatch_assum_rename_tac `option_join _ = Some x` >>
  `?size. i = IntV (&x) size` suffices_by metis_tac [] >> rw [] >>
  qpat_x_assum `v_rel _ _` mp_tac >>
  simp [v_rel_cases] >> rw [] >> fs [signed_v_to_int_def] >> rw [] >>
  intLib.COOPER_TAC
QED

Theorem translate_update_correct:
  ∀pc_rel emap s1 s1' a v1 v1' v2 v2' e2 e2' e1' cs ns result.
    state_rel pc_rel emap s1 s1' ∧
    map (λci. signed_v_to_num (eval_const s1.globals ci)) cs = map Some ns ∧
    insert_value v1 v2 ns = Some result ∧
    eval_exp s1' e1' v1' ∧
    v_rel v1 v1' ∧
    eval_exp s1' e2' v2' ∧
    v_rel v2 v2'
    ⇒
    ∃v3'.
      eval_exp s1' (translate_updatevalue e1' e2' cs) v3' ∧
      v_rel result v3'
Proof
  Induct_on `cs` >> rw [] >> fs [insert_value_def, translate_updatevalue_def]
  >- metis_tac [] >>
  simp [Once eval_exp_cases, PULL_EXISTS] >>
  Cases_on `ns` >> fs [] >>
  Cases_on `v1` >> fs [insert_value_def] >>
  rename [`insert_value (el x _) _ ns`] >>
  Cases_on `insert_value (el x l) v2 ns` >> fs [] >> rw [] >>
  qpat_x_assum `v_rel (AggV _) _` mp_tac >> simp [Once v_rel_cases] >> rw [] >>
  simp [v_rel_cases] >>
  qmatch_goalsub_rename_tac `translate_const c` >>
  qexists_tac `vs2` >> simp [] >>
  `?v4'. eval_exp s1' (translate_const c) v4' ∧ v_rel (eval_const s1.globals c) v4'`
  by metis_tac [translate_constant_correct] >>
  `?idx_size. v4' = FlatV (IntV (&x) idx_size)`
  by (
    pop_assum mp_tac >> simp [Once v_rel_cases] >>
    rw [] >> fs [signed_v_to_num_def, signed_v_to_int_def] >>
    intLib.COOPER_TAC) >>
  first_x_assum drule >>
  disch_then drule >>
  disch_then drule >>
  disch_then (qspecl_then [`el x vs2`, `v2'`, `e2'`, `Select e1' (translate_const c)`] mp_tac) >>
  simp [Once eval_exp_cases] >>
  metis_tac [EVERY2_LUPDATE_same, LIST_REL_LENGTH, LIST_REL_EL_EQN]
QED

Theorem translate_instr_to_exp_correct:
  ∀emap instr r t s1 s1'.
    classify_instr instr = Exp r t ∧
    state_rel pc_rel emap s1 s1'
    ⇒
    (∀s2. step_instr prog s1 instr s2 ⇒
      (∃v pv. eval_exp s1' (translate_instr_to_exp emap instr) v ∧
              flookup s2.locals r = Some pv ∧ v_rel pv.value v))
Proof
  recInduct translate_instr_to_exp_ind >>
  simp [translate_instr_to_exp_def, classify_instr_def] >>
  conj_tac
  >- ( (* Sub *)
    rw [step_instr_cases, Once eval_exp_cases, do_sub_def, PULL_EXISTS] >>
    simp [inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
    simp [v_rel_cases, PULL_EXISTS] >>
    first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
    disch_then drule >>
    first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
    disch_then drule >>
    BasicProvers.EVERY_CASE_TAC >> fs [translate_ty_def, translate_size_def] >>
    rfs [v_rel_cases] >>
    pairarg_tac >> fs [] >>
    fs [pairTheory.PAIR_MAP, wordsTheory.FST_ADD_WITH_CARRY] >>
    qmatch_goalsub_abbrev_tac `eval_exp _ _ (FlatV (IntV i1 _))` >> strip_tac >>
    qmatch_goalsub_abbrev_tac `eval_exp _ _ (FlatV (IntV i2 _))` >> strip_tac >>
    qexists_tac `i1` >> qexists_tac `i2` >> simp [] >>
    unabbrev_all_tac >>
    rw []
    >- (
      irule restricted_i2w_11 >> simp [word_sub_i2w] >>
      `dimindex (:1) = 1` by rw [] >>
      drule truncate_2comp_i2w_w2i >>
      rw [word_sub_i2w] >>
      metis_tac [w2i_ge, w2i_le, SIMP_CONV (srw_ss()) [] ``INT_MIN (:1)``,
                 SIMP_CONV (srw_ss()) [] ``INT_MAX (:1)``])
    >- (
      irule restricted_i2w_11 >> simp [word_sub_i2w] >>
      `dimindex (:8) = 8` by rw [] >>
      drule truncate_2comp_i2w_w2i >>
      rw [word_sub_i2w] >>
      metis_tac [w2i_ge, w2i_le, SIMP_CONV (srw_ss()) [] ``INT_MIN (:8)``,
                 SIMP_CONV (srw_ss()) [] ``INT_MAX (:8)``])
    >- (
      irule restricted_i2w_11 >> simp [word_sub_i2w] >>
      `dimindex (:32) = 32` by rw [] >>
      drule truncate_2comp_i2w_w2i >>
      rw [word_sub_i2w] >>
      metis_tac [w2i_ge, w2i_le, SIMP_CONV (srw_ss()) [] ``INT_MIN (:32)``,
                 SIMP_CONV (srw_ss()) [] ``INT_MAX (:32)``])
    >- (
      irule restricted_i2w_11 >> simp [word_sub_i2w] >>
      `dimindex (:64) = 64` by rw [] >>
      drule truncate_2comp_i2w_w2i >>
      rw [word_sub_i2w] >>
      metis_tac [w2i_ge, w2i_le, SIMP_CONV (srw_ss()) [] ``INT_MIN (:64)``,
                 SIMP_CONV (srw_ss()) [] ``INT_MAX (:64)``])) >>
  conj_tac
  >- (
    rw [step_instr_cases] >>
    simp [inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
    metis_tac [translate_arg_correct, translate_extract_correct]) >>
  conj_tac
  >- (
    rw [step_instr_cases] >>
    simp [inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
    metis_tac [translate_arg_correct, translate_update_correct]) >>
  cheat
QED

export_theory ();