diff options
Diffstat (limited to 'proof.tex')
-rw-r--r-- | proof.tex | 29 |
1 files changed, 19 insertions, 10 deletions
@@ -27,8 +27,10 @@ As HTL is quite different to RTL, this first translation is the most involved tr \begin{figure} \centering \begin{minted}{coq} -Inductive match_states : RTL.state -> HTL.state -> Prop := -| match_state : forall asa asr sf f sp sp' rs mem m st res +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)) @@ -36,17 +38,24 @@ Inductive match_states : RTL.state -> HTL.state -> Prop := (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) + (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_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). + forall f m m0 (TF : tr_module f m), + match_states + (RTL.Callstate nil (AST.Internal f) nil m0) + (HTL.Callstate nil m nil). \end{minted} \caption{\texttt{match\_states} predicate used to match an RTL state to the equivalent HTL state.}\label{fig:match_states} \end{figure} |