Module RTLofRTLinjectspec

Require Import Utf8.

Require Import
  Coqlib Registers Maps Ast.

Require Import
  Utils Common Transcode
  INJECT RTLinject RTLofRTLinject.

Section TRCODE.

  Variable bi : backend_info.
  Variable c : RTL.code.
  Inductive tr_stmt : statement → node → list reg → node → node → Prop :=
  | Tr_assert cond args nd res exit
    : tr_stmt (Sassume cond args) nd res exit nd
  | Tr_freeperm nd res exit
    : tr_stmt Sfreeperm nd res exit nd
  | Tr_requestperm rp ad args nd res exit
    : tr_stmt (Srequestperm rp ad args) nd res exit nd
  | Tr_release nd res exit
    : tr_stmt Srelease nd res exit nd
  | Tr_skip nd res exit
    : tr_stmt Sskip nd res exit nd
  | Tr_op op args dst ns res exit nd
     (OP: ok_op op)
     (NS: c ! ns = Some (RTL.Iop op (List.map xI args) (xI dst) nd))
    : tr_stmt (Sop op args dst) ns res exit nd
  | Tr_load addr args dst b ns res exit nd
     (NS: c ! ns = Some (RTL.Iload Mint32 addr (List.map xI args) (xI dst) nd))
    : tr_stmt (Sload b addr args dst) ns res exit nd
  | Tr_store addr args src r b ns res exit nd
     (NS: c ! ns = Some (RTL.Istore Mint32 addr (List.map xI args) (xI src) nd))
    : tr_stmt (Sstore r b addr args src) ns res exit nd
  | Tr_seq s1 s2 ns ni res exit nd
     (S1: tr_stmt s1 ns res exit ni)
     (S2: tr_stmt s2 ni res exit nd)
    : tr_stmt (Sseq s1 s2) ns res exit nd
  | Tr_ifthenelse cnd args strue sfalse ns nt nf res exit nd
     (STRUE: tr_stmt strue nt res exit nd)
     (SFALSE: tr_stmt sfalse nf res exit nd)
     (NS: c ! ns = Some (RTL.Icond cnd (List.map xI args) nt nf))
    : tr_stmt (Sifthenelse cnd args strue sfalse) ns res exit nd
  | Tr_while cnd args sbody ns nb res exit nd
     (BODY: tr_stmt sbody nb res exit ns)
     (NS: c ! ns = Some (RTL.Icond cnd (List.map xI args) nb nd))
    : tr_stmt (Swhile cnd args sbody) ns res exit nd
  | Tr_repeat cnd args sbody ns nb res exit nd
     (BODY: tr_stmt sbody nb res exit ns)
     (NS: c ! ns = Some (RTL.Icond (Op.negate_condition cnd) (List.map xI args) nb nd))
    : tr_stmt (Srepeat sbody cnd args) nb res exit nd
  | Tr_atomic b aop args r ns res exit nd
     (NS: c ! ns = Some (RTL.Iatomic aop (List.map xI args) (xI r) nd))
    : tr_stmt (Satomicmem b aop args r) ns res exit nd
  | Tr_fence ns res exit nd r
     (NS: c ! ns = Some (RTL.Ifence nd))
    : tr_stmt (Sfence r) ns res exit nd
  | Tr_abort af msg ns ni res exit nd r
     (NS: c ! ns = Some (RTL.Iop (Op.Ointconst (bi_translate_abort_msg bi msg)) nil xH ni))
     (ABORT: c ! ni = Some (RTL.Icall abort_sig (inr reg (bi_abort bi)) (xH :: nil) xH nd))
    : tr_stmt (Sabort af r msg) ns res exit nd
  | Tr_return_nil exit nd
    : tr_stmt (Sreturn nil) exit nil exit nd
  | Tr_return_cons s srcl t tgtl ni ns nd exit
      (NS: c ! ns = Some (RTL.Iop Op.Omove (xI s :: nil) t exit))
      (RET: tr_stmt (Sreturn srcl) ni tgtl ns nd)
    : tr_stmt (Sreturn (s::srcl)) ni (t::tgtl) exit nd
  | Tr_leak_off l r o res exit nd
      (LEAK: ¬ bi.(bi_show_leak))
    : tr_stmt (Leak l r o) nd res exit nd
  | Tr_leak_on l r o ns ni res exit nd
      (LEAK: bi.(bi_show_leak))
      (NS: c ! ns = Some (RTL.Iop (Op.Ointconst (bi.(bi_translate_leak) l)) nil (xI o) ni))
      (NS': c ! ni = Some (RTL.Icall leak_sig (inr _ bi.(bi_leak)) (xI o::xI r::nil) (xI o) nd))
    : tr_stmt (Leak l r o) ns res exit nd
  .

  Inductive tr_init : node → list reg → list reg → node → Prop :=
  | TrInit_nil n : tr_init n nil nil n
  | TrInit_cons a args p param ns ni nd
    (INIT: tr_init ni args param nd)
    (NS: c ! ns = Some (RTL.Iop Op.Omove (xO a::nil) (xI p) ni))
    : tr_init ns (a::args) (p::param) nd
  .

  Variable pc : node.
  Inductive tr_instr : instruction → Prop :=
  | Tr_inop succ
      (PC: c ! pc = Some (RTL.Inop succ))
    : tr_instr (Inop succ)
  | Tr_iop op args dst succ
      (OKOP: ok_op op)
      (PC: c ! pc = Some (RTL.Iop op (List.map xO args) (xO dst) succ))
    : tr_instr (Iop op args dst succ)
  | Tr_icall sg func args dst succ func'
      (FUNC: func' = match func with inl f => inl _ (xO f) | inr f => inr _ f end)
      (PC: c ! pc = Some (RTL.Icall sg func' (List.map xO args) (xO dst) succ))
    : tr_instr (Icall sg func args dst succ)
  | Tr_ithreadcreate fp arg succ
      (PC: c ! pc = Some (RTL.Ithreadcreate (xO fp) (xO arg) succ))
    : tr_instr (Ithreadcreate fp arg succ)
  | Tr_icond cond args if_so if_not
      (PC: c ! pc = Some (RTL.Icond cond (List.map xO args) if_so if_not))
    : tr_instr (Icond cond args if_so if_not)
  | Tr_ireturn tgt
      (PC: c ! pc = Some (RTL.Ireturn (Some (xO tgt))))
    : tr_instr (Ireturn tgt)
  | Tr_iinject ic args dst succ np nd
      (STMT: tr_stmt ic.(ic_stmt_low) nd (List.map xO dst) succ succ)
      (INIT: tr_init np args ic.(ic_params) nd)
      (PC: c ! pc = Some (RTL.Inop np))
    : tr_instr (Iinject ic args dst succ)
  .

End TRCODE.

Section S.

  Variable bi : backend_info.

  Lemma tr_stmt_incr:
    ∀ s1 s2, state_incr s1 s2 →
    ∀ stmt,
    ∀ res exit nd ns,
    tr_stmt bi s1.(st_code) stmt ns res exit nd →
    tr_stmt bi s2.(st_code) stmt ns res exit nd.

Ltac bind_inv :=
  match goal with
    | [H: bind ?f ?g ?s1 = OK ?y ?s3 ?i |- _] =>
      destruct (bind_inversion _ _ f g y s1 s3 i H) as
          (? & ? & ? & ? & ?Hbind & ?Hbind' );
      clear H
  end.

  Lemma translate_statement_correct stmt :
    ∀ res exit nd,
    ∀ st ns st' p,
    transl_stmt bi res exit stmt nd st = OK ns st' p →
    tr_stmt bi st'.(st_code) stmt ns res exit nd.

  Lemma tr_init_incr:
    ∀ s1 s2, state_incr s1 s2 →
    ∀ ns args param nd,
      tr_init s1.(st_code) ns args param nd →
      tr_init s2.(st_code) ns args param nd.

  Lemma init_stmt_correct :
    ∀ args param nd,
    ∀ s ns s' p,
      init_stmt args param nd s = OK ns s' p →
      tr_init s'.(st_code) ns args param nd.

  Lemma translate_instruction_correct {k i s s' p} :
    translate_instruction bi k i s = OK tt s' p →
    tr_instr bi s'.(st_code) k i.

  Lemma tr_instr_incr:
    ∀ s1 s2, state_incr s1 s2 →
    ∀ k i,
      tr_instr bi s1.(st_code) k i →
      tr_instr bi s2.(st_code) k i.

  Definition match_code c c' : Prop :=
    ∀ k i, c ! k = Some i → tr_instr bi c' k i.

  Lemma translate_code_correct :
    ∀ c z,
    match translate_code bi c z with
      | Errors.OK s =>
        match_code c s.(st_code)
      | Errors.Error _ => True
    end.

End S.