vericert.hls.Veriloggenproof

Definition match_prog (prog : HTL.program) (tprog : Verilog.program) :=
  match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog.

Lemma transf_program_match:
  forall prog, match_prog prog (transl_program prog).

Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop :=
| match_stack :
    forall res m pc reg_assoc arr_assoc hstk vstk,
      match_stacks hstk vstk ->
      match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk)
                   (Stackframe res (transl_module m) pc
                                       reg_assoc arr_assoc :: vstk)
| match_stack_nil : match_stacks nil nil.

Inductive match_states : HTL.state -> state -> Prop :=
| match_state :
    forall m st reg_assoc arr_assoc hstk vstk,
      match_stacks hstk vstk ->
      match_states (HTL.State hstk m st reg_assoc arr_assoc)
                   (State vstk (transl_module m) st reg_assoc arr_assoc)
| match_returnstate :
    forall v hstk vstk,
      match_stacks hstk vstk ->
      match_states (HTL.Returnstate hstk v) (Returnstate vstk v)
| match_initial_call :
    forall m,
      match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil).

Lemma Vlit_inj :
  forall a b, Vlit a = Vlit b -> a = b.

Lemma posToValue_inj :
  forall a b,
    0 <= Z.pos a <= Int.max_unsigned ->
    0 <= Z.pos b <= Int.max_unsigned ->
    posToValue a = posToValue b ->
    a = b.

Lemma valueToPos_inj :
  forall a b,
    0 < Int.unsigned a ->
    0 < Int.unsigned b ->
    valueToPos a = valueToPos b ->
    a = b.

Lemma unsigned_posToValue_le :
  forall p,
    Z.pos p <= Int.max_unsigned ->
    0 < Int.unsigned (posToValue p).

Lemma transl_list_fun_fst :
  forall p1 p2 a b,
    0 <= Z.pos p1 <= Int.max_unsigned ->
    0 <= Z.pos p2 <= Int.max_unsigned ->
    transl_list_fun (p1, a) = transl_list_fun (p2, b) ->
    (p1, a) = (p2, b).

Lemma Zle_relax :
  forall p q r,
  p < q <= r ->
  p <= q <= r.
#[local] Hint Resolve Zle_relax : verilogproof.

Lemma transl_in :
  forall l p,
  0 <= Z.pos p <= Int.max_unsigned ->
  (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
  In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) ->
  In p (map fst l).

Lemma transl_notin :
  forall l p,
    0 <= Z.pos p <= Int.max_unsigned ->
    (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
    ~ In p (List.map fst l) -> ~ In (Vlit (posToValue p)) (List.map fst (transl_list l)).

Lemma transl_norepet :
  forall l,
    (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
    list_norepet (List.map fst l) -> list_norepet (List.map fst (transl_list l)).

Lemma transl_list_correct :
  forall l v ev f asr asa asrn asan asr' asa' asrn' asan',
    (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
    list_norepet (List.map fst l) ->
    asr!ev = Some v ->
    (forall p s,
        In (p, s) l ->
        v = posToValue p ->
        stmnt_runp f
                   {| assoc_blocking := asr; assoc_nonblocking := asrn |}
                   {| assoc_blocking := asa; assoc_nonblocking := asan |}
                   s
                   {| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
                   {| assoc_blocking := asa'; assoc_nonblocking := asan' |} ->
        stmnt_runp f
                   {| assoc_blocking := asr; assoc_nonblocking := asrn |}
                   {| assoc_blocking := asa; assoc_nonblocking := asan |}
                   (Vcase (Vvar ev) (list_to_stmnt (transl_list l)) (Some Vskip))
                   {| assoc_blocking := asr'; assoc_nonblocking := asrn' |}
                   {| assoc_blocking := asa'; assoc_nonblocking := asan' |}).
#[local] Hint Resolve transl_list_correct : verilogproof.

Lemma pc_wf :
  forall A m p v,
  (forall p0, In p0 (List.map fst (@AssocMap.elements A m)) -> 0 < Z.pos p0 <= Int.max_unsigned) ->
  m!p = Some v ->
  0 <= Z.pos p <= Int.max_unsigned.

Lemma mis_stepp_decl :
  forall l asr asa f,
    mis_stepp f asr asa (map Vdeclaration l) asr asa.
#[local] Hint Resolve mis_stepp_decl : verilogproof.

Lemma mis_stepp_negedge_decl :
  forall l asr asa f,
    mis_stepp_negedge f asr asa (map Vdeclaration l) asr asa.
#[local] Hint Resolve mis_stepp_negedge_decl : verilogproof.

Lemma mod_entrypoint_equiv m : mod_entrypoint (transl_module m) = HTL.mod_entrypoint m.

Lemma mod_st_equiv m : mod_st (transl_module m) = HTL.mod_st m.

Section CORRECTNESS.

  Variable prog: HTL.program.
  Variable tprog: program.

  Hypothesis TRANSL : match_prog prog tprog.

  Let ge : HTL.genv := Globalenvs.Genv.globalenv prog.
  Let tge : genv := Globalenvs.Genv.globalenv tprog.


  Theorem transf_program_correct:
    forward_simulation (HTL.semantics prog) (Verilog.semantics tprog).

End CORRECTNESS.