include "joint/SemanticUtils.ma". include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *) (*CSC: XXXX*) axiom lin_succ_pc: unit → address → address. (*CSC: re-organize to take succ_pc out of lin_more_sem_params to share the following definition between LTL and LIN *) definition lin_more_sem_params: more_sem_params lin_params_ := mk_more_sem_params lin_params_ unit hw_register_env lin_succ_pc hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA) (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB) (λ_.hwreg_store RegisterDPL) (λe.λ_.hwreg_retrieve e RegisterDPL) (λ_.hwreg_store RegisterDPH) (λe.λ_.hwreg_retrieve e RegisterDPH) (λlocals,dest_src. match dest_src with [ from_acc reg ⇒ do v ← hwreg_retrieve locals RegisterA ; hwreg_store reg v locals | to_acc reg ⇒ do v ← hwreg_retrieve locals reg ; hwreg_store RegisterA v locals ]) pointer_of_label. definition lin_sem_params: sem_params ≝ mk_sem_params … lin_more_sem_params. definition lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e. definition lin_pop_frame: list beval → state … lin_sem_params → res (state … lin_sem_params) ≝ λ_.λst. OK … st. definition lin_save_frame: unit → state … lin_sem_params → state … lin_sem_params ≝ λ_.λst.st. definition lin_more_sem_params1 : more_sem_params1 … lin_params1 ≝ mk_more_sem_params1 ? lin_params1 lin_more_sem_params lin_init_locals lin_pop_frame lin_save_frame. (*CSC: XXXXXXXXXX *) axiom lin_fetch_statement: ∀globals. genv … (lin_params globals) → state lin_sem_params → res (pre_lin_statement globals). (*CSC: XXXXX, for is_final only *) axiom lin_fetch_result: state lin_sem_params → res (list beval). (*CSC: XXXX, for external functions only*) axiom lin_fetch_external_args: external_function → state lin_sem_params → res (list val). axiom lin_set_result: list val → state lin_sem_params → res (state lin_sem_params). definition lin_exec_extended: ∀globals. genv globals (lin_params globals) → False → unit → state lin_sem_params → IO io_out io_in (trace × (state lin_sem_params)) ≝ λglobals,ge,abs. ⊥. @abs qed. definition lin_more_sem_params2: ∀globals. more_sem_params2 … (lin_params globals) ≝ λglobals. mk_more_sem_params2 … lin_more_sem_params1 (lin_fetch_statement …) lin_fetch_result lin_fetch_external_args lin_set_result (lin_exec_extended …). definition lin_fullexec ≝ joint_fullexec … (λp. lin_more_sem_params2 (prog_var_names … p)).