include "common/BackEndOps.ma". include "common/CostLabel.ma". include "common/Registers.ma". include "ASM/I8051.ma". include "common/Graphs.ma". include "utilities/lists.ma". include "common/LabelledObjects.ma". include "ASM/Util.ma". include "basics/lists/listb.ma". include "joint/String.ma". (* Here is the structure of parameter records (downward edges are coercions, the ↓ edges are the only explicitly defined coercions). lin_params and graph_params are simple wrappers of unserialized_params, and the coercions from them to params instantate the missing bits with values for linarized programs and graph programs respectively. lin_params graph_params | \_____ /____ | | / \ | | / ↓ ↓ | | params | | | | | stmt_params | | / unserialized_params unserialized_params : things unrelated to being in graph or linear form stmt_params : adds successor type needed to define statements params : adds type of code and related properties *) (* inductive possible_flows : Type[0] ≝ | Labels : list label → possible_flows | Call : possible_flows. *) inductive argument (T : Type[0]) : Type[0] ≝ | Reg : T → argument T | Imm : Byte → argument T. definition psd_argument ≝ argument register. definition psd_argument_from_reg : register → psd_argument ≝ Reg register. coercion reg_to_psd_argument : ∀r : register.psd_argument ≝ psd_argument_from_reg on _r : register to psd_argument. (* definition psd_argument_from_beval : beval → psd_argument ≝ Imm register. coercion beval_to_psd_argument : ∀b : beval.psd_argument ≝ psd_argument_from_beval on _b : beval to psd_argument. *) definition psd_argument_from_byte : Byte → psd_argument ≝ Imm ?. coercion byte_to_psd_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte on _b : Byte to psd_argument. definition hdw_argument ≝ argument Register. definition hdw_argument_from_reg : Register → hdw_argument ≝ Reg Register. coercion reg_to_hdw_argument : ∀r : Register.hdw_argument ≝ hdw_argument_from_reg on _r : Register to hdw_argument. (* definition hdw_argument_from_beval : beval → hdw_argument ≝ Imm Register. coercion beval_to_hdw_argument : ∀b : beval.hdw_argument ≝ hdw_argument_from_beval on _b : beval to hdw_argument. *) definition hdw_argument_from_byte : Byte → hdw_argument ≝ Imm ?. coercion byte_to_hdw_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte on _b : Byte to hdw_argument. definition byte_of_nat : nat → Byte ≝ bitvector_of_nat 8. definition zero_byte : Byte ≝ bv_zero 8. record unserialized_params : Type[1] ≝ { acc_a_reg: Type[0] (* registers that will eventually need to be A *) ; acc_b_reg: Type[0] (* registers that will eventually need to be B *) ; acc_a_arg: Type[0] (* arguments that will eventually need to be A *) ; acc_b_arg: Type[0] (* arguments that will eventually need to be B *) ; dpl_reg: Type[0] (* low address registers *) ; dph_reg: Type[0] (* high address registers *) ; dpl_arg: Type[0] (* low address registers *) ; dph_arg: Type[0] (* high address registers *) ; snd_arg : Type[0] (* second argument of binary op *) ; pair_move: Type[0] (* argument of move instructions *) ; call_args: Type[0] (* arguments of function calls *) ; call_dest: Type[0] (* possible destination of function computation *) (* other instructions not fitting in the general framework *) ; ext_seq : Type[0] ; ext_seq_labels : ext_seq → list label ; has_tailcalls : bool (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *) ; paramsT : Type[0] }. inductive joint_seq (p:unserialized_params) (globals: list ident): Type[0] ≝ | COMMENT: String → joint_seq p globals | MOVE: pair_move p → joint_seq p globals | POP: acc_a_reg p → joint_seq p globals | PUSH: acc_a_arg p → joint_seq p globals | ADDRESS: ∀i: ident. i ∈ globals → dpl_reg p → dph_reg p → joint_seq p globals | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_seq p globals (* int done with generic move *) (*| INT: generic_reg p → Byte → joint_seq p globals *) | CLEAR_CARRY: joint_seq p globals | SET_CARRY: joint_seq p globals | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals | extension_seq : ext_seq p → joint_seq p globals. definition NOOP ≝ λp,globals.COMMENT p globals EmptyString. notation "r ← a1 .op. a2" with precedence 60 for @{'op2 $op $r $a1 $a2}. notation "r ← . op . a" with precedence 60 for @{'op1 $op $r $a}. notation "r ← a" with precedence 60 for @{'mov $r $a}. (* to be set in individual languages *) notation "❮r, s❯ ← a1 . op . a2" with precedence 55 for @{'opaccs $op $r $s $a1 $a2}. interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2). interpretation "op1" 'op1 op r a = (OP1 ? ? op r a). interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2). coercion extension_seq_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝ extension_seq on _s : ext_seq ? to joint_seq ??. (* inductive joint_branch (p : step_params) : Type[0] ≝ | COND: acc_a_reg p → label → joint_branch p | extension_branch : ext_branch p → joint_branch p.*) (*coercion extension_to_branch : ∀p.∀s : ext_branch p.joint_branch p ≝ extension_branch on _s : ext_branch ? to joint_branch ?.*) inductive joint_step (p : unserialized_params) (globals : list ident) : Type[0] ≝ | COST_LABEL: costlabel → joint_step p globals | CALL: (ident + (dpl_arg p × (dph_arg p))) → call_args p → call_dest p → joint_step p globals | COND: acc_a_reg p → label → joint_step p globals | step_seq : joint_seq p globals → joint_step p globals. coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝ step_seq on _s : joint_seq ?? to joint_step ??. definition step_labels ≝ λp, globals.λs : joint_step p globals. match s with [ step_seq s ⇒ match s with [ extension_seq ext ⇒ ext_seq_labels … ext | _ ⇒ [ ] ] | COND _ l ⇒ [l] | _ ⇒ [ ] ]. definition step_forall_labels : ∀p.∀globals. (label → Prop) → joint_step p globals → Prop ≝ λp,g,P,inst. All … P (step_labels … inst). record stmt_params : Type[1] ≝ { uns_pars :> unserialized_params ; succ : Type[0] ; succ_label : succ → option label ; has_fcond : bool }. inductive joint_fin_step (p: unserialized_params): Type[0] ≝ | GOTO: label → joint_fin_step p | RETURN: joint_fin_step p | TAILCALL : has_tailcalls p → (ident + (dpl_arg p × (dph_arg p))) → call_args p → joint_fin_step p. definition fin_step_labels ≝ λp.λs : joint_fin_step p. match s with [ GOTO l ⇒ [l] | _ ⇒ [ ] ]. inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝ | sequential: joint_step p globals → succ p → joint_statement p globals | final: joint_fin_step p → joint_statement p globals | FCOND: has_fcond p → acc_a_reg p → label → label → joint_statement p globals. coercion fin_step_to_stmt : ∀p : stmt_params.∀globals. ∀s : joint_fin_step p.joint_statement p globals ≝ final on _s : joint_fin_step ? to joint_statement ??. record params : Type[1] ≝ { stmt_pars :> stmt_params ; codeT: list ident → Type[0] ; code_point : Type[0] ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals) ; point_of_label : ∀globals.codeT globals → label → option code_point ; point_of_succ : code_point → succ stmt_pars → code_point }. definition code_has_point ≝ λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false]. (* interpretation "code membership" 'mem p c = (code_has_point ?? c p). *) (* definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt). unification hint 0 ≔ p, globals, code ⊢ point_in_code p globals code ≡ Sig (code_point p) (λpt.bool_to_Prop (code_has_point p globals code pt)). definition stmt_at_safe ≝ λp,globals,code.λpt : point_in_code p globals code. match pt with [ mk_Sig pt' pt_prf ⇒ match stmt_at … code pt' return λx.stmt_at … code pt' = x → ? with [ Some x ⇒ λ_.x | None ⇒ λabs.⊥ ] (refl …) ]. normalize in pt_prf; >abs in pt_prf; // qed. *) definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals) ≝ λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P s. definition forall_statements_i : ∀p : params.∀globals.(code_point p → joint_statement p globals → Prop) → codeT p globals → Prop ≝ λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P pt s. lemma forall_statements_mp : ∀p,globals.modus_ponens ?? (forall_statements p globals). #p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed. lemma forall_statements_i_mp : ∀p,globals.∀P,Q.(∀pt,s.P pt s → Q pt s) → ∀c.forall_statements_i p globals P c → forall_statements_i p globals Q c. #p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed. definition code_has_label ≝ λp,globals,c,l. match point_of_label p globals c l with [ Some pt ⇒ code_has_point … c pt | None ⇒ false ]. definition stmt_explicit_labels : ∀p,globals. joint_statement p globals → list label ≝ λp,globals,stmt. match stmt with [ sequential c _ ⇒ step_labels … c | final c ⇒ fin_step_labels … c | FCOND _ _ l1 l2 ⇒ [l1 ; l2] ]. definition stmt_implicit_label : ∀p,globals.joint_statement p globals → option label ≝ λp,globals,s.match s with [ sequential _ s ⇒ succ_label … s | _ ⇒ None ?]. definition stmt_labels : ∀p : stmt_params.∀globals. joint_statement p globals → list label ≝ λp,g,stmt. (match stmt_implicit_label … stmt with [ Some l ⇒ [l] | None ⇒ [ ] ]) @ stmt_explicit_labels … stmt. definition stmt_forall_labels ≝ λp, globals.λ P : label → Prop.λs : joint_statement p globals. All … P (stmt_labels … s). lemma stmt_forall_labels_explicit : ∀p,globals,P.∀s : joint_statement p globals. stmt_forall_labels … P s → All … P (stmt_explicit_labels … s). #p#globals#P #s whd in ⊢ (% → ?); whd in ⊢ (???% → ?); elim (stmt_implicit_label ???) [2: #next * #_] // qed. lemma stmt_forall_labels_implicit : ∀p,globals,P.∀s : joint_statement p globals. stmt_forall_labels … P s → opt_All … P (stmt_implicit_label … s). #p#globals#P#s whd in ⊢ (% → ?); whd in ⊢ (???% → ?); elim (stmt_implicit_label ???) [ // | #next * #Pnext #_ @Pnext ] qed. definition code_forall_labels ≝ λp,globals,P,c.forall_statements p globals (stmt_forall_labels … P) c. lemma code_forall_labels_mp : ∀p,globals,P,Q.(∀l.P l → Q l) → ∀c.code_forall_labels p globals P c → code_forall_labels … Q c ≝ λp,globals,P,Q,H.forall_statements_mp … (λs. All_mp … H ?). record lin_params : Type[1] ≝ { l_u_pars : unserialized_params }. lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|). #tag #A #lbl #l elim l [*] ** [2: #id] #a #tl #IH [ change with (if (eq_identifier ???) then ? else ?) in match (occurs_exactly_once ????); change with (if (eq_identifier ???) then ? else ?) in match (index_of_label ????); @eq_identifier_elim #Heq normalize nodelta [ #_ normalize / by /] | whd in ⊢ (?%→?%?); ] #H >(index_of_label_from_internal … H) @le_S_S @(IH H) qed. (* mv *) lemma nth_opt_hit_length : ∀A,l,n,x.nth_opt A n l = Some ? x → n < |l|. #A #l elim l normalize [ #n #x #ABS destruct(ABS)] #hd #tl #IH * [2:#n] #x normalize [#H @le_S_S @(IH … H)] /2 by / qed. lemma nth_opt_miss_length : ∀A,l,n.nth_opt A n l = None ? → n ≥ |l|. #A #l elim l [//] #hd #tl #IH * normalize [#ABS destruct(ABS)] #n' #H @le_S_S @(IH … H) qed. lemma nth_opt_safe : ∀A,l,n,prf.nth_opt A n l = Some ? (nth_safe A n l prf). #A #l elim l [ #n #ABS @⊥ /2 by absurd/ | #hd #tl #IH * normalize // ] qed. definition lin_params_to_params ≝ λlp : lin_params. mk_params (mk_stmt_params (l_u_pars lp) unit (λ_.None ?) true) (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals))) (* code_point ≝ *)ℕ (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls) (* point_of_label ≝ *)(λglobals,c,lbl. If occurs_exactly_once ?? lbl c then with prf do return index_of_label ?? lbl c else None ?) (* point_of_succ ≝ *)(λcurrent.λ_.S (current)). coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params on _lp : lin_params to params. lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals. ∀pt.code_has_point … code pt = leb (S pt) (|code|). #lp #globals #code elim code [ #pt % | #hd #tl #IH * [%] #n @IH ]qed. lemma lin_code_has_label : ∀lp : lin_params.∀globals.∀code:codeT lp globals. ∀lbl.code_has_label … code lbl = occurs_exactly_once ?? lbl code. #lp #globals #code #lbl whd in match (code_has_label ????); whd in match (point_of_label ????); elim (true_or_false_Prop (occurs_exactly_once ?? lbl code)) #Heq >Heq normalize nodelta [ >lin_code_has_point @(leb_elim (S ?)) [#_ | #ABS elim(absurd ?? ABS) -ABS @index_of_label_length assumption ]] % qed. record graph_params : Type[1] ≝ { g_u_pars : unserialized_params }. (* One common instantiation of params via Graphs of joint_statements (all languages but LIN) *) definition graph_params_to_params ≝ λgp : graph_params. mk_params (mk_stmt_params (g_u_pars gp) label (Some ?) false) (* codeT ≝ *)(λglobals.graph (joint_statement ? globals)) (* code_point ≝ *)label (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code) (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl) (* point_of_succ ≝ *)(λ_.λlbl.lbl). coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params on _gp : graph_params to params. lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals. ∀pt.code_has_point … code pt = (pt ∈ code). // qed. lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals. ∀lbl.code_has_label … code lbl = (lbl ∈ code). // qed. definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop. λs : joint_statement p globals. match s with [ sequential _ n ⇒ P n | _ ⇒ True ]. definition statement_closed : ∀globals.∀p : params. codeT p globals → code_point p → (joint_statement p globals) → Prop ≝ λglobals,p,code,pt,s. All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧ stmt_forall_succ … (λn.bool_to_Prop (code_has_point … code (point_of_succ ? pt n))) s. definition code_closed : ∀p : params.∀globals. codeT p globals → Prop ≝ λp,globals,code. forall_statements_i … (statement_closed … code) code. record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝ { joint_if_luniverse: universe LabelTag; (*CSC: used only for compilation*) joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*) (* Paolo: if we want this machinery to work for RTLabs too, we will need the following, right? *) (* joint_if_sig: signature; -- dropped in front end *) joint_if_result : call_dest p; joint_if_params : paramsT p; (*CSC: XXXXX stacksize unused for LTL-...*) joint_if_stacksize: nat; joint_if_code : codeT p globals ; joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) (*; joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) *) }. definition code_in_universe : ∀p,globals. codeT p globals → universe LabelTag → Prop ≝ λp,globals,c,u.∀l.code_has_label … c l → fresh_for_univ … l u. lemma memb_to_present : ∀tag,A.∀i : identifier tag.∀m. i ∈ m → present tag A m i. #tag #A #i #m whd in ⊢ (?%→%); cases (lookup tag A m i) [ * | #x #_ % #ABS destruct ] qed. lemma present_to_memb : ∀tag,A.∀i : identifier tag.∀m. present tag A m i → bool_to_Prop (i∈m). #tag #A #i #m whd in ⊢ (%→?%); cases (lookup tag A m i) [ * #ABS cases (ABS (refl …)) | #x #_ % ] qed. lemma graph_code_in_universe_if : ∀p : graph_params.∀globals. ∀c : codeT p globals.∀u.fresh_map_for_univ … c u → code_in_universe … c u ≝ λp,g,c,u,H,l,G.H ? (memb_to_present … G). lemma graph_code_in_universe_only_if : ∀p : graph_params.∀globals. ∀c : codeT p globals.∀u. code_in_universe … c u → fresh_map_for_univ … c u ≝ λp,g,c,u,H,l,G.H ? (present_to_memb … G). include alias "basics/logic.ma". record good_if (p : params) (globals : list ident) (def : joint_internal_function p globals) : Prop ≝ { entry_costed : ∃l,nxt. stmt_at … (joint_if_code … def) (joint_if_entry … def) = Some … (sequential … (COST_LABEL … l) nxt) ; entry_unused : let entry ≝ pi1 … (joint_if_entry … def) in let code ≝ joint_if_code … def in forall_statements_i … (λpt,stmt.stmt_forall_labels … (λlbl.point_of_label … code lbl ≠ Some ? entry) stmt ∧ stmt_forall_succ … (λnxt.point_of_succ … pt nxt ≠ entry) stmt) code ; code_is_closed : code_closed … (joint_if_code … def) ; code_is_in_universe : code_in_universe … (joint_if_code … def) (joint_if_luniverse … def) }. definition joint_closed_internal_function ≝ λp,globals. Σdef : joint_internal_function p globals.good_if … def. unification hint 0 ≔ p,g ⊢ joint_closed_internal_function p g ≡ Sig (joint_internal_function p g) (λdef.good_if … def). definition set_joint_code ≝ λglobals: list ident. λpars: params. λint_fun: joint_internal_function pars globals. λgraph: codeT pars globals. λentry. (*λexit.*) mk_joint_internal_function pars globals (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun) (joint_if_params … int_fun) (joint_if_stacksize … int_fun) graph entry (*exit*). definition set_joint_if_graph ≝ λglobals.λpars : graph_params. λgraph. λp:joint_internal_function pars globals. λentry_prf. (*λexit_prf.*) set_joint_code globals pars p graph (mk_Sig ?? (joint_if_entry ?? p) entry_prf) (*(mk_Sig … (joint_if_exit ?? p) exit_prf)*). definition set_luniverse ≝ λglobals,pars. λp : joint_internal_function globals pars. λluniverse: universe LabelTag. mk_joint_internal_function globals pars luniverse (joint_if_runiverse … p) (joint_if_result … p) (joint_if_params … p) (joint_if_stacksize … p) (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*). definition set_runiverse ≝ λglobals,pars. λp : joint_internal_function globals pars. λruniverse: universe RegisterTag. mk_joint_internal_function globals pars (joint_if_luniverse … p) runiverse (joint_if_result … p) (joint_if_params … p) (joint_if_stacksize … p) (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*). (* Specialized for graph_params *) definition add_graph ≝ λg_pars : graph_params.λglobals.λl:label.λstmt. λp:joint_internal_function g_pars globals. let code ≝ add … (joint_if_code … p) l stmt in mk_joint_internal_function … (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) (joint_if_params … p) (joint_if_stacksize … p) code (pi1 … (joint_if_entry … p)) (*(pi1 … (joint_if_exit … p))*). >graph_code_has_point whd in match code; >mem_set_add @orb_Prop_r elim (joint_if_entry ???) #x #H