vericert.hls.HTLgenproof
#[local] Hint Resolve Smallstep.forward_simulation_plus : htlproof.
#[local] Hint Resolve AssocMap.gss : htlproof.
#[local] Hint Resolve AssocMap.gso : htlproof.
#[local] Hint Unfold find_assocmap AssocMapExt.get_default : htlproof.
Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop :=
match_assocmap : forall f rs am,
(forall r, Ple r (RTL.max_reg_function f) ->
val_value_lessdef (Registers.Regmap.get r rs) am#r) ->
match_assocmaps f rs am.
#[local] Hint Constructors match_assocmaps : htlproof.
Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
forall st asa asr res,
s = HTL.State res m st asa asr ->
asa!(m.(HTL.mod_st)) = Some (posToValue st).
#[local] Hint Unfold state_st_wf : htlproof.
Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) :
Verilog.assocmap_arr -> Prop :=
| match_arr : forall asa stack,
asa ! (m.(HTL.mod_ram).(ram_mem)) = Some stack /\
stack.(arr_length) = Z.to_nat (f.(RTL.fn_stacksize) / 4) /\
(forall ptr,
0 <= ptr < Z.of_nat m.(HTL.mod_ram).(ram_size) ->
opt_val_value_lessdef (Mem.loadv AST.Mint32 mem
(Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))))
(Option.default (NToValue 0)
(Option.join (array_get_error (Z.to_nat ptr) stack)))) ->
match_arrs m f sp mem asa.
Definition stack_based (v : Values.val) (sp : Values.block) : Prop :=
match v with
| Values.Vptr sp' off => sp' = sp
| _ => True
end.
Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop :=
forall r, stack_based (Registers.Regmap.get r rs) sp.
Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z)
(sp : Values.val) : Prop :=
forall ptr,
0 <= ptr < (stack_length / 4) ->
stack_based (Option.default
Values.Vundef
(Mem.loadv AST.Mint32 m
(Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr)))))
spb.
Definition stack_bounds (sp : Values.val) (hi : Z) (m : mem) : Prop :=
forall ptr v,
hi <= ptr <= Integers.Ptrofs.max_unsigned ->
Z.modulo ptr 4 = 0 ->
Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) = None /\
Mem.storev AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) v = None.
Inductive match_frames : list RTL.stackframe -> list HTL.stackframe -> Prop :=
| match_frames_nil :
match_frames nil nil.
Inductive match_constants : HTL.module -> assocmap -> Prop :=
match_constant :
forall m asr,
asr!(HTL.mod_reset m) = Some (ZToValue 0) ->
asr!(HTL.mod_finish m) = Some (ZToValue 0) ->
match_constants m asr.
Inductive match_states : RTL.state -> HTL.state -> Prop :=
| match_state : forall asa asr sf f sp sp' rs mem m st res
(MASSOC : match_assocmaps f rs asr)
(TF : tr_module f m)
(WF : state_st_wf m (HTL.State res m st asr asa))
(MF : match_frames sf res)
(MARR : match_arrs m f sp mem asa)
(SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0))
(RSBP : reg_stack_based_pointers sp' rs)
(ASBP : arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp)
(BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem)
(CONST : match_constants m asr),
match_states (RTL.State sf f sp st rs mem)
(HTL.State res m st asr asa)
| match_returnstate :
forall
v v' stack mem res
(MF : match_frames stack res),
val_value_lessdef v v' ->
match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res v')
| match_initial_call :
forall f m m0
(TF : tr_module f m),
match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil).
#[local] Hint Constructors match_states : htlproof.
Definition match_prog (p: RTL.program) (tp: HTL.program) :=
Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\
main_is_internal p = true.
Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program):
TransfLink (fun (p1: RTL.program) (p2: HTL.program) => match_prog p1 p2).
Definition match_prog' (p: RTL.program) (tp: HTL.program) :=
Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp.
Lemma match_prog_matches :
forall p tp, match_prog p tp -> match_prog' p tp.
Lemma transf_program_match:
forall p tp, HTLgen.transl_program p = Errors.OK tp -> match_prog p tp.
Lemma regs_lessdef_add_greater :
forall f rs1 rs2 n v,
Plt (RTL.max_reg_function f) n ->
match_assocmaps f rs1 rs2 ->
match_assocmaps f rs1 (AssocMap.set n v rs2).
#[local] Hint Resolve regs_lessdef_add_greater : htlproof.
Lemma regs_lessdef_add_match :
forall f rs am r v v',
val_value_lessdef v v' ->
match_assocmaps f rs am ->
match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.set r v' am).
#[local] Hint Resolve regs_lessdef_add_match : htlproof.
Lemma list_combine_none :
forall n l,
length l = n ->
list_combine Verilog.merge_cell (list_repeat None n) l = l.
Lemma combine_none :
forall n a,
a.(arr_length) = n ->
arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a.
Lemma list_combine_lookup_first :
forall l1 l2 n,
length l1 = length l2 ->
nth_error l1 n = Some None ->
nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n.
Lemma combine_lookup_first :
forall a1 a2 n,
a1.(arr_length) = a2.(arr_length) ->
array_get_error n a1 = Some None ->
array_get_error n (combine Verilog.merge_cell a1 a2) = array_get_error n a2.
Lemma list_combine_lookup_second :
forall l1 l2 n x,
length l1 = length l2 ->
nth_error l1 n = Some (Some x) ->
nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x).
Lemma combine_lookup_second :
forall a1 a2 n x,
a1.(arr_length) = a2.(arr_length) ->
array_get_error n a1 = Some (Some x) ->
array_get_error n (combine Verilog.merge_cell a1 a2) = Some (Some x).
Lemma init_reg_assoc_empty :
forall f l,
match_assocmaps f (RTL.init_regs nil l) (HTL.init_regs nil l).
Lemma arr_lookup_some:
forall (z : Z) (r0 : Registers.reg) (r : Verilog.reg) (asr : assocmap) (asa : Verilog.assocmap_arr)
(stack : Array (option value)) (H5 : asa ! r = Some stack) n,
exists x, Verilog.arr_assocmap_lookup asa r n = Some x.
#[local] Hint Resolve arr_lookup_some : htlproof.
Section CORRECTNESS.
Variable prog : RTL.program.
Variable tprog : HTL.program.
Hypothesis TRANSL : match_prog prog tprog.
Lemma TRANSL' :
Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog.
Let ge : RTL.genv := Globalenvs.Genv.globalenv prog.
Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog.
Lemma symbols_preserved:
forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Lemma function_ptr_translated:
forall (b: Values.block) (f: RTL.fundef),
Genv.find_funct_ptr ge b = Some f ->
exists tf,
Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf.
Lemma functions_translated:
forall (v: Values.val) (f: RTL.fundef),
Genv.find_funct ge v = Some f ->
exists tf,
Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf.
Lemma senv_preserved:
Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
#[local] Hint Resolve senv_preserved : htlproof.
Lemma ptrofs_inj :
forall a b,
Ptrofs.unsigned a = Ptrofs.unsigned b -> a = b.
Lemma op_stack_based :
forall F V sp v m args rs op ge pc' res0 pc f e fin rtrn st stk,
tr_instr fin rtrn st stk (RTL.Iop op args res0 pc')
(Verilog.Vnonblock (Verilog.Vvar res0) e)
(state_goto st pc') ->
reg_stack_based_pointers sp rs ->
(RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') ->
@Op.eval_operation F V ge (Values.Vptr sp Ptrofs.zero) op
(map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v ->
stack_based v sp.
Lemma int_inj :
forall x y,
Int.unsigned x = Int.unsigned y ->
x = y.
Lemma eval_cond_correct :
forall stk f sp pc rs m res ml st asr asa e b f' s s' args i cond,
match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
(forall v, In v args -> Ple v (RTL.max_reg_function f)) ->
Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b ->
translate_condition cond args s = OK e s' i ->
Verilog.expr_runp f' asr asa e (boolToValue b).
Lemma eval_cond_correct' :
forall e stk f sp pc rs m res ml st asr asa v f' s s' args i cond,
match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
(forall v, In v args -> Ple v (RTL.max_reg_function f)) ->
Values.Val.of_optbool None = v ->
translate_condition cond args s = OK e s' i ->
exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'.
Lemma eval_correct_Oshrximm :
forall s sp rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st n,
match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
(RTL.fn_code f) ! pc = Some (RTL.Iop (Op.Oshrximm n) args res0 pc') ->
Op.eval_operation ge sp (Op.Oshrximm n)
(List.map (fun r : BinNums.positive =>
Registers.Regmap.get r rs) args) m = Some v ->
translate_instr (Op.Oshrximm n) args s = OK e s' i ->
exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'.
Lemma eval_correct :
forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st,
match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
(RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') ->
Op.eval_operation ge sp op
(List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v ->
translate_instr op args s = OK e s' i ->
exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'.
The proof of semantic preservation for the translation of instructions
is a simulation argument based on diagrams of the following form:
The precondition and postcondition is that that should hold is match_assocmaps rs assoc.
match_states
code st rs ------------------------- State m st assoc
|| |
|| |
|| |
\/ v
code st rs' ------------------------ State m st assoc'
match_states
where tr_code c data control fin rtrn st is assumed to hold.
Definition transl_instr_prop (instr : RTL.instruction) : Prop :=
forall m asr asa fin rtrn st stmt trans res,
tr_instr fin rtrn st (m.(HTL.mod_ram).(ram_mem)) instr stmt trans ->
exists asr' asa',
HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa').
Lemma transl_inop_correct:
forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive)
(rs : RTL.regset) (m : mem) (pc' : RTL.node),
(RTL.fn_code f) ! pc = Some (RTL.Inop pc') ->
forall R1 : HTL.state,
match_states (RTL.State s f sp pc rs m) R1 ->
exists R2 : HTL.state,
Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2.
Theorem transf_program_correct:
Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog).
End CORRECTNESS.