[1168] | 1 | include "joint/Joint.ma". |
---|
[733] | 2 | |
---|
[3255] | 3 | inductive psd_or_hdw : Type[0] ≝ |
---|
| 4 | | PSD: register → psd_or_hdw |
---|
| 5 | | HDW: Register → psd_or_hdw. |
---|
[1161] | 6 | |
---|
[3255] | 7 | definition ertl_hdw_readable : Register → Prop ≝ |
---|
| 8 | λR.match R with |
---|
| 9 | [ RegisterA ⇒ False |
---|
| 10 | | RegisterB ⇒ False |
---|
| 11 | | RegisterDPL ⇒ False |
---|
| 12 | | RegisterDPH ⇒ False |
---|
[3371] | 13 | | RegisterCarry ⇒ False |
---|
[3255] | 14 | | Register04 (* = RegisterST0 *) ⇒ False |
---|
| 15 | | Register05 (* = RegisterST1 *) ⇒ False |
---|
| 16 | | _ ⇒ True |
---|
| 17 | ]. |
---|
[1241] | 18 | |
---|
[3255] | 19 | definition ertl_readable ≝ |
---|
| 20 | λR.match R with |
---|
| 21 | [ HDW R ⇒ ertl_hdw_readable R |
---|
| 22 | | _ ⇒ True |
---|
| 23 | ]. |
---|
[1178] | 24 | |
---|
[3255] | 25 | definition ertl_hdw_writable : Register → Prop ≝ |
---|
| 26 | λR.match R with |
---|
| 27 | [ Register06 (* = RegisterSPL *) ⇒ False |
---|
| 28 | | Register07 (* = RegisterSPH *) ⇒ False |
---|
[3371] | 29 | | RegisterCarry ⇒ False |
---|
[3255] | 30 | | _ ⇒ True |
---|
| 31 | ]. |
---|
| 32 | |
---|
| 33 | definition ertl_writable : psd_or_hdw → Prop ≝ |
---|
| 34 | λR.match R with |
---|
| 35 | [ HDW R ⇒ ertl_hdw_writable R |
---|
| 36 | | _ ⇒ True |
---|
| 37 | ]. |
---|
| 38 | |
---|
| 39 | definition move_dst ≝ Σr : psd_or_hdw.ertl_writable r. |
---|
| 40 | unification hint 0 ≔ ⊢ move_dst ≡ Sig psd_or_hdw (λr.ertl_writable r). |
---|
| 41 | |
---|
| 42 | definition move_src ≝ argument (Σr : psd_or_hdw.ertl_readable r). |
---|
| 43 | |
---|
| 44 | definition move_src_from_reg : |
---|
| 45 | (Σr.ertl_readable r) → move_src ≝ Reg ?. |
---|
| 46 | coercion reg_to_move_src : |
---|
| 47 | ∀r : (Σr : psd_or_hdw.ertl_readable r).move_src ≝ |
---|
| 48 | move_src_from_reg on _r : Sig psd_or_hdw ? to move_src. |
---|
| 49 | |
---|
[2286] | 50 | definition psd_argument_move_src : psd_argument → move_src ≝ |
---|
[3255] | 51 | λarg.match arg return λ_.move_src with |
---|
[2286] | 52 | [ Imm b ⇒ Imm ? b |
---|
| 53 | | Reg r ⇒ Reg ? (PSD r) |
---|
[3255] | 54 | ]. @I qed. |
---|
[2286] | 55 | coercion psd_argument_to_move_src : ∀a:psd_argument.move_src ≝ |
---|
| 56 | psd_argument_move_src on _a : psd_argument to move_src. |
---|
[1248] | 57 | |
---|
[2286] | 58 | inductive ertl_seq : Type[0] ≝ |
---|
| 59 | | ertl_frame_size: register → ertl_seq. |
---|
| 60 | |
---|
| 61 | definition ERTL_uns ≝ mk_unserialized_params |
---|
| 62 | (* acc_a_reg ≝ *) register |
---|
| 63 | (* acc_b_reg ≝ *) register |
---|
| 64 | (* acc_a_arg ≝ *) psd_argument |
---|
| 65 | (* acc_b_arg ≝ *) psd_argument |
---|
| 66 | (* dpl_reg ≝ *) register |
---|
| 67 | (* dph_reg ≝ *) register |
---|
| 68 | (* dpl_arg ≝ *) psd_argument |
---|
| 69 | (* dph_arg ≝ *) psd_argument |
---|
| 70 | (* snd_arg ≝ *) psd_argument |
---|
| 71 | (* pair_move ≝ *) (move_dst × move_src) |
---|
| 72 | (* call_args ≝ *) ℕ |
---|
| 73 | (* call_dest ≝ *) unit |
---|
| 74 | (* ext_seq ≝ *) ertl_seq |
---|
[2563] | 75 | (* ext_seq_labels ≝ *) (λ_.[]) |
---|
[2490] | 76 | (* has_tailcall ≝ *) false |
---|
[3263] | 77 | (* paramsT ≝ *) unit. |
---|
[2286] | 78 | |
---|
[2783] | 79 | definition regs_from_move_dst : move_dst → list register ≝ |
---|
| 80 | λm. match m with [PSD r ⇒ [r] | HDW _ ⇒ [ ] ]. |
---|
| 81 | |
---|
| 82 | definition regs_from_move_src : move_src → list register ≝ |
---|
| 83 | λm. match m with [Imm _ ⇒ [ ] | Reg r ⇒ match r with [PSD r1 ⇒ [r1] | HDW _ ⇒ [ ] ] ]. |
---|
| 84 | |
---|
| 85 | definition ertl_ext_seq_regs : ertl_seq → list register ≝ |
---|
| 86 | λs.match s with [ertl_frame_size r ⇒ [r] | _ ⇒ [ ]]. |
---|
| 87 | |
---|
| 88 | definition ERTL_functs ≝ mk_get_pseudo_reg_functs ERTL_uns |
---|
| 89 | (* acc_a_regs *) (λr.[r]) |
---|
| 90 | (* acc_b_regs *) (λr.[r]) |
---|
| 91 | (* acc_a_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]]) |
---|
| 92 | (* acc_b_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]]) |
---|
| 93 | (* dpl_regs *) (λr.[r]) |
---|
| 94 | (* dph_regs *) (λr.[r]) |
---|
| 95 | (* dpl_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]]) |
---|
| 96 | (* dph_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]]) |
---|
| 97 | (* snd_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]]) |
---|
| 98 | (* pair_move_regs *) (λx.(regs_from_move_dst (\fst x)) @ (regs_from_move_src (\snd x))) |
---|
| 99 | (* f_call_args *) (λ_.[ ]) |
---|
| 100 | (* f_call_dest *) (λ_.[ ]) |
---|
| 101 | (* ext_seq_regs *) ertl_ext_seq_regs |
---|
| 102 | (* params_regs *) (λ_.[ ]). |
---|
| 103 | |
---|
| 104 | definition ERTL ≝ mk_graph_params (mk_uns_params ERTL_uns ERTL_functs). |
---|
[2286] | 105 | definition ertl_program ≝ joint_program ERTL. |
---|
[2946] | 106 | unification hint 0 ≔ ⊢ ertl_program ≡ joint_program ERTL. |
---|
[2286] | 107 | |
---|
| 108 | interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)). |
---|
| 109 | |
---|
| 110 | (* aid unification *) |
---|
| 111 | unification hint 0 ≔ |
---|
| 112 | (*---------------*) ⊢ |
---|
| 113 | pair_move ERTL ≡ move_dst × move_src. |
---|
| 114 | unification hint 0 ≔ |
---|
| 115 | (*---------------*) ⊢ |
---|
| 116 | acc_a_reg ERTL ≡ register. |
---|
| 117 | unification hint 0 ≔ |
---|
| 118 | (*---------------*) ⊢ |
---|
| 119 | acc_b_reg ERTL ≡ register. |
---|
| 120 | unification hint 0 ≔ |
---|
| 121 | (*---------------*) ⊢ |
---|
| 122 | acc_a_arg ERTL ≡ psd_argument. |
---|
| 123 | unification hint 0 ≔ |
---|
| 124 | (*---------------*) ⊢ |
---|
| 125 | acc_b_arg ERTL ≡ psd_argument. |
---|
| 126 | unification hint 0 ≔ |
---|
| 127 | (*---------------*) ⊢ |
---|
| 128 | dpl_reg ERTL ≡ register. |
---|
| 129 | unification hint 0 ≔ |
---|
| 130 | (*---------------*) ⊢ |
---|
| 131 | dph_reg ERTL ≡ register. |
---|
| 132 | unification hint 0 ≔ |
---|
| 133 | (*---------------*) ⊢ |
---|
| 134 | dpl_arg ERTL ≡ psd_argument. |
---|
| 135 | unification hint 0 ≔ |
---|
| 136 | (*---------------*) ⊢ |
---|
| 137 | dph_arg ERTL ≡ psd_argument. |
---|
| 138 | unification hint 0 ≔ |
---|
| 139 | (*---------------*) ⊢ |
---|
| 140 | snd_arg ERTL ≡ psd_argument. |
---|
| 141 | unification hint 0 ≔ |
---|
| 142 | (*---------------*) ⊢ |
---|
| 143 | call_args ERTL ≡ ℕ. |
---|
| 144 | unification hint 0 ≔ |
---|
| 145 | (*---------------*) ⊢ |
---|
| 146 | call_dest ERTL ≡ unit. |
---|
| 147 | |
---|
| 148 | unification hint 0 ≔ |
---|
| 149 | (*---------------*) ⊢ |
---|
| 150 | ext_seq ERTL ≡ ertl_seq. |
---|
| 151 | |
---|
| 152 | coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ERTL ≝ |
---|
| 153 | psd_argument_from_reg |
---|
| 154 | on _r : register to snd_arg ERTL. |
---|
| 155 | coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ERTL ≝ |
---|
| 156 | psd_argument_from_byte |
---|
| 157 | on _b : Byte to snd_arg ERTL. |
---|
| 158 | |
---|
| 159 | definition ertl_seq_joint ≝ extension_seq ERTL. |
---|
| 160 | coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint |
---|
[2946] | 161 | on _s : ertl_seq to joint_seq ERTL ?. |
---|
| 162 | |
---|
[3037] | 163 | definition ERTL_premain : ∀p : ertl_program. |
---|
| 164 | joint_closed_internal_function ERTL (prog_names … p) ≝ |
---|
[2946] | 165 | λp. |
---|
| 166 | let l1 : label ≝ an_identifier … one in |
---|
| 167 | let l2 : label ≝ an_identifier … (p0 one) in |
---|
| 168 | let l3 : label ≝ an_identifier … (p1 one) in |
---|
| 169 | let res ≝ |
---|
[3037] | 170 | mk_joint_internal_function ERTL (prog_names … p) |
---|
[2946] | 171 | (mk_universe … (p0 (p0 one))) |
---|
| 172 | (mk_universe … one) |
---|
[3263] | 173 | it it 0 0 0 (empty_map …) l1 in |
---|
[2946] | 174 | (* todo: args for main? *) |
---|
| 175 | let res ≝ add_graph … l1 |
---|
| 176 | (sequential … (COST_LABEL … (init_cost_label … p)) l2) |
---|
| 177 | res in |
---|
| 178 | let res ≝ add_graph … l2 |
---|
[2952] | 179 | (sequential … (CALL ERTL ? (inl … (prog_main … p)) 0 it) l3) |
---|
[2946] | 180 | res in |
---|
| 181 | let res ≝ add_graph … l3 |
---|
| 182 | (GOTO ? l3) |
---|
| 183 | res in |
---|
| 184 | res. |
---|
| 185 | % |
---|
| 186 | [ ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct |
---|
| 187 | % |
---|
| 188 | [1,3,5: %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct |
---|
| 189 | |2: % |
---|
| 190 | |4,6: % whd in ⊢ (??%%→?); #EQ destruct |
---|
| 191 | ] |
---|
| 192 | | ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I} |
---|
| 193 | | ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); // |
---|
| 194 | | ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I |
---|
| 195 | | %{l2} %{(init_cost_label … p)} % |
---|
| 196 | ] |
---|
[3037] | 197 | qed. |
---|