Changeset 1882 for src/ASM


Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (8 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r1522 r1882  
    22include "common/Identifiers.ma".
    33include "common/CostLabel.ma".
     4include "common/LabelledObjects.ma".
    45
    56axiom ASMTag : String.
     
    203204  | Mov: [[dptr]] → Identifier → pseudo_instruction.
    204205
    205 definition labelled_instruction ≝ option Identifier × pseudo_instruction.
     206definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction.
    206207definition preamble ≝ (identifier_map SymbolTag nat) × (list (Identifier × Word)).
    207208definition assembly_program ≝ list instruction.
  • src/ASM/Status.ma

    r1666 r1882  
    510510  λac: option Bit.
    511511  λov: Bit.
    512     let old_cy ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) O ? in
    513     let old_ac ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 1 ? in
    514     let old_fo ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 2 ? in
    515     let old_rs1 ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 3 ? in
    516     let old_rs0 ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 4 ? in
    517     let old_ov ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 5 ? in
    518     let old_ud ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 6 ? in
    519     let old_p ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 7 ? in
     512    let sfr_psw ≝ get_8051_sfr ?? s SFR_PSW in
     513    let old_cy ≝ get_index_v ?? sfr_psw O ? in
     514    let old_ac ≝ get_index_v ?? sfr_psw 1 ? in
     515    let old_fo ≝ get_index_v ?? sfr_psw 2 ? in
     516    let old_rs1 ≝ get_index_v ?? sfr_psw 3 ? in
     517    let old_rs0 ≝ get_index_v ?? sfr_psw 4 ? in
     518    let old_ov ≝ get_index_v ?? sfr_psw 5 ? in
     519    let old_ud ≝ get_index_v ?? sfr_psw 6 ? in
     520    let old_p ≝ get_index_v ?? sfr_psw 7 ? in
    520521    let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in
    521522      set_8051_sfr ?? s SFR_PSW
     
    11281129qed.
    11291130
    1130 definition instruction_matches_identifier ≝
    1131   λy: Identifier.
    1132   λx: labelled_instruction.
    1133     match \fst x with
    1134     [ None ⇒ false
    1135     | Some x ⇒ eq_identifier ? x y
    1136     ].
    1137 
    1138 let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝
    1139  match l with
    1140   [ nil ⇒ true
    1141   | cons hd tl ⇒ notb (instruction_matches_identifier id hd) ∧ does_not_occur id tl].
    1142 
    1143 lemma does_not_occur_None:
    1144  ∀id,i,list_instr.
    1145   does_not_occur id (list_instr@[〈None …,i〉]) =
    1146   does_not_occur id list_instr.
    1147  #id #i #list_instr elim list_instr
    1148   [ % | #hd #tl #IH whd in ⊢ (??%%); >IH %]
    1149 qed.
    1150 
    1151 lemma does_not_occur_Some:
    1152  ∀id,id',i,list_instr.
    1153   eq_identifier ? id' id = false →
    1154    does_not_occur id (list_instr@[〈Some ? id',i〉]) =
    1155     does_not_occur id list_instr.
    1156  #id #id' #i #list_instr elim list_instr
    1157   [ #H normalize in H ⊢ %; >H %
    1158   | * #x #i' #tl #IH #H whd in ⊢ (??%%); >(IH H) %]
    1159 qed.
    1160 
    1161 lemma does_not_occur_absurd:
    1162  ∀id,i,list_instr.
    1163   does_not_occur id (list_instr@[〈Some ? id,i〉]) = false.
    1164  #id #i #list_instr elim list_instr
    1165   [ normalize change with (if (if eq_identifier ??? then ? else ?) then ? else ? = ?)
    1166     >eq_identifier_refl %
    1167   | * #x #i' #tl #IH whd in ⊢ (??%%); >IH cases (notb ?) %]
    1168 qed.
    1169 
    1170 
    1171 let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
    1172  match l with
    1173   [ nil ⇒ false
    1174   | cons hd tl ⇒
    1175      if instruction_matches_identifier id hd then
    1176       does_not_occur id tl
    1177      else
    1178       occurs_exactly_once id tl ].
    1179 
    1180 lemma occurs_exactly_once_None:
    1181  ∀id,i,list_instr.
    1182   occurs_exactly_once id (list_instr@[〈None …,i〉]) =
    1183   occurs_exactly_once id list_instr.
    1184  #id #i #list_instr elim list_instr
    1185   [ % | #hd #tl #IH whd in ⊢ (??%%); >IH >does_not_occur_None %]
    1186 qed.
    1187 
    1188 lemma occurs_exactly_once_Some:
    1189  ∀id,id',i,prefix.
    1190   occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_identifier ? id' id ∨ occurs_exactly_once id prefix.
    1191  #id #id' #i #prefix elim prefix
    1192   [ whd in ⊢ (?% → ?);
    1193     change with (eq_identifier ? id' id) in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
    1194     @eq_identifier_elim normalize nodelta; /2/
    1195   | *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
    1196     cases he; normalize nodelta
    1197      [ #H @ (IH H)
    1198      | #x whd in ⊢ (? → ?(??%)); change with (eq_identifier ? x id) in match (instruction_matches_identifier ??);
    1199        @eq_identifier_elim #E normalize nodelta
    1200        [ destruct @eq_identifier_elim normalize nodelta;
    1201         /2/ #H >does_not_occur_Some /2/
    1202        | #H @IH @H]]]
    1203 qed.
    1204 
    1205 lemma occurs_exactly_once_Some_stronger:
    1206   ∀id,id',i,prefix.
    1207     occurs_exactly_once id (prefix@[〈Some ? id',i〉]) →
    1208     (eq_identifier ? id' id ∧ does_not_occur id prefix) ∨
    1209     (¬eq_identifier ? id' id ∧ occurs_exactly_once id prefix).
    1210  #id #id' #i #prefix elim prefix
    1211  [ whd in ⊢ (?% → ?); change with (eq_identifier ???) in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?);
    1212    @eq_identifier_elim #E
    1213   [ normalize //
    1214   | normalize #H @⊥ @H 
    1215   ]
    1216  | *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
    1217    cases he; normalize nodelta
    1218    [ #H @ (IH H)
    1219    | #x @eq_identifier_elim #Heq
    1220      [ @eq_identifier_elim normalize nodelta
    1221        [ #H >H >does_not_occur_absurd #Hf @⊥ @Hf
    1222        | #H >(does_not_occur_Some)
    1223          [ #H2 whd in match (does_not_occur ??);
    1224            change with (eq_identifier ???) in match (instruction_matches_identifier ??);
    1225            >Heq >eq_identifier_refl normalize nodelta
    1226            @orb_elim normalize nodelta whd in match (occurs_exactly_once ??);
    1227            change with (eq_identifier ???) in match (instruction_matches_identifier ??);
    1228            >eq_identifier_refl
    1229            normalize nodelta @H2 
    1230          | /2/
    1231          ]
    1232        ]
    1233      | normalize nodelta #H lapply (IH H) -IH -H;
    1234        @eq_identifier_elim #Heq2
    1235        #Hor @orb_elim
    1236        [ <Heq2 in Hor; #Hor normalize in Hor;
    1237          whd in match (does_not_occur ??); change with (eq_identifier ???) in match (instruction_matches_identifier ??);
    1238          >eq_identifier_false // normalize nodelta
    1239          cases (does_not_occur id' tl) in Hor; normalize nodelta //
    1240        | normalize nodelta whd in match (occurs_exactly_once ??);
    1241          change with (eq_identifier ???) in match (instruction_matches_identifier ??);
    1242          >eq_identifier_false //
    1243        ]
    1244      ] 
    1245    ]
    1246  ]
    1247 qed.   
    1248 
    1249 let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
    1250   match l with
    1251   [ nil ⇒ ?
    1252   | cons hd tl ⇒
    1253     if pred hd then
    1254       acc
    1255     else
    1256       index_of_internal A pred tl (S acc)
    1257   ].
    1258   cases not_implemented.
    1259 qed.
    1260 
    1261 
    1262 definition index_of ≝
    1263   λA.
    1264   λeq.
    1265   λl.
    1266     index_of_internal A eq l 0.
    1267 
    1268 lemma index_of_internal_None: ∀i,id,instr_list,n.
    1269  occurs_exactly_once id (instr_list@[〈None …,i〉]) →
    1270   index_of_internal ? (instruction_matches_identifier id) instr_list n =
    1271    index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
    1272  #i #id #instr_list elim instr_list
    1273   [ #n #abs whd in abs; cases abs
    1274   | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?);
    1275     cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%);
    1276     [ #H %
    1277     | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %;
    1278       [ #_ % | #abs cases abs ]]]
    1279 qed.
    1280 
    1281 lemma index_of_internal_Some_miss: ∀i,id,id'.
    1282  eq_identifier ? id' id = false →
    1283  ∀instr_list,n.
    1284  occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
    1285   index_of_internal ? (instruction_matches_identifier id) instr_list n =
    1286    index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n.
    1287  #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ
    1288  change with (occurs_exactly_once ?? → ?) generalize in match n; -n -H; elim instr_list
    1289   [ #n #abs cases abs
    1290   | #hd #tl #IH #n whd in ⊢ (?% → ??%%); cases (instruction_matches_identifier id hd) normalize nodelta;
    1291     [ // | #K @IH //]]
    1292 qed.
    1293 
    1294 lemma index_of_internal_Some_hit: ∀i,id.
    1295  ∀instr_list,n.
    1296   occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
    1297    index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id,i〉]) n
    1298   = |instr_list| + n.
    1299  #i #id #instr_list elim instr_list
    1300   [ #n #_ whd in ⊢ (??%%); change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl %
    1301   | #hd #tl #IH #n whd in ⊢ (?% → ??%%); cases (instruction_matches_identifier id hd) normalize nodelta;
    1302     [ >does_not_occur_absurd #abs cases abs | #H >plus_n_Sm applyS (IH (S n)) //]]
    1303 qed.
    1304 
    13051131definition address_of_word_labels_code_mem ≝
    1306   λcode_mem.
     1132  λcode_mem : list labelled_instruction.
    13071133  λid: Identifier.
    1308     bitvector_of_nat 16 (index_of ? (instruction_matches_identifier id) code_mem).
     1134    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem).
    13091135
    13101136lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
    1311  occurs_exactly_once id (instr_list@[〈None …,i〉]) →
     1137 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
    13121138  address_of_word_labels_code_mem instr_list id =
    13131139  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
    13141140 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
    1315  >(index_of_internal_None H) %
     1141 >(index_of_internal_None ?????? H) %
    13161142qed.
    13171143
    13181144lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
    13191145 eq_identifier ? id' id = false →
    1320   occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
     1146  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
    13211147   address_of_word_labels_code_mem instr_list id =
    13221148   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
    13231149 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
    1324  >(index_of_internal_Some_miss H) [ @refl | // ]
     1150 >(index_of_internal_Some_miss ???????? H) [ @refl | // ]
    13251151qed.
    13261152
    13271153lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
    1328   occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
     1154  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
    13291155   address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
    13301156   = bitvector_of_nat … (|instr_list|).
    13311157 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
    1332  >(index_of_internal_Some_hit H) <plus_n_O @refl
     1158 >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl
    13331159qed.
    13341160
  • src/ASM/Util.ma

    r1811 r1882  
    1212notation "⊥" with precedence 90
    1313  for @{ match ? in False with [ ] }.
     14notation "Ⓧ" with precedence 90
     15  for @{ λabs.match abs in False with [ ] }.
     16
    1417
    1518definition ltb ≝
     
    561564    foldr ? ? (append ?) [ ] l.
    562565
    563 let rec rev (A: Type[0]) (l: list A) on l ≝
    564   match l with
    565   [ nil ⇒ nil A
    566   | cons hd tl ⇒ (rev A tl) @ [ hd ]
    567   ].
     566(* redirecting to library reverse *)
     567definition rev ≝ reverse.
    568568
    569569lemma append_length:
     
    594594  elim L
    595595  [ normalize >append_nil %
    596   | #HD #TL #IH
    597     normalize >IH
     596  | #HD #TL normalize #IH
     597    >rev_append_def
     598    >rev_append_def
     599    >rev_append_def
     600    >append_nil
     601    normalize
     602    >IH
    598603    @associative_append
    599604  ]
     
    607612  elim L
    608613  [ %
    609   | #HD #TL #IH
    610     normalize
     614  | #HD #TL normalize #IH
     615    >rev_append_def
    611616    >(append_length A (rev A TL) [HD])
    612     normalize /2/
     617    normalize /2 by /
    613618  ]
    614619qed.
     
    834839coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
    835840
     841lemma bool_as_Prop_to_eq : ∀b : bool. b → b = true.
     842**%
     843qed.
     844
     845(* with this you can use prf : b with b : bool with rewriting
     846   >prf rewrites b as true *)
     847coercion bool_to_Prop_to_eq : ∀b : bool.∀prf : b.b = true
     848 ≝ bool_as_Prop_to_eq on _prf : bool_to_Prop ? to (? = true).
     849
     850lemma andb_Prop : ∀b,d : bool.b → d → b∧d.
     851#b #d #btrue #dtrue >btrue >dtrue %
     852qed.
     853
     854lemma andb_Prop_true : ∀b,d : bool. (b∧d) → And (bool_to_Prop b) (bool_to_Prop d).
     855#b #d #bdtrue elim (andb_true … bdtrue) #btrue #dtrue >btrue >dtrue % %
     856qed.
     857
     858lemma orb_Prop_l : ∀b,d : bool.b → b∨d.
     859#b #d #btrue >btrue %
     860qed.
     861
     862lemma orb_Prop_r : ∀b,d : bool.d → b∨d.
     863#b #d #dtrue >dtrue elim b %
     864qed.
     865
     866lemma orb_Prop_true : ∀b,d : bool. (b∨d) → Or (bool_to_Prop b) (bool_to_Prop d).
     867#b #d #bdtrue elim (orb_true_l … bdtrue) #xtrue >xtrue [%1 | %2] %
     868qed.
     869
     870lemma notb_Prop : ∀b : bool. Not (bool_to_Prop b) → notb b.
     871* * #H [@H % | %]
     872qed.
     873
    836874lemma eq_false_to_notb: ∀b. b = false → ¬ b.
    837  *; /2/
    838 qed.
     875 *; /2 by eq_true_false, I/
     876qed.
     877
     878lemma not_b_to_eq_false : ∀b : bool. Not (bool_to_Prop b) → b = false.
     879** #H [elim (H ?) % | %]
     880qed.
     881
     882(* with this you can use prf : ¬b with b : bool with rewriting
     883   >prf rewrites b as false *)
     884coercion not_bool_to_Prop_to_eq : ∀b : bool.∀prf : Not (bool_to_Prop b).b = false
     885 ≝ not_b_to_eq_false on _prf : Not (bool_to_Prop ?) to (? = false).
     886
     887
     888lemma true_or_false_Prop : ∀b : bool.Or (bool_to_Prop b) (¬(bool_to_Prop b)).
     889* [%1 % | %2 % *]
     890qed.
     891
     892lemma eq_true_to_b : ∀b. b = true → b.
     893#b #btrue >btrue %
     894qed.
     895
     896definition if_then_else_safe : ∀A : Type[0].∀b : bool.(b → A) → (¬(bool_to_Prop b) → A) → A ≝
     897  λA,b,f,g.
     898  match b return λx.match x with [true ⇒ bool_to_Prop b | false ⇒ ¬bool_to_Prop b] → A with
     899  [ true ⇒ f
     900  | false ⇒ g
     901  ] ?. elim b % *
     902qed.
     903
     904notation > "'If' b 'then' 'with' ident prf1 'do' f 'else' 'with' ident prf2 'do' g" with precedence 46 for
     905  @{'if_then_else_safe $b (λ${ident prf1}.$f) (λ${ident prf2}.$g)}.
     906notation > "'If' b 'then' 'with' ident prf1 : ty1 'do' f 'else' 'with' ident prf2 : ty2 'do' g" with precedence 46 for
     907  @{'if_then_else_safe $b (λ${ident prf1}:$ty1.$f) (λ${ident prf2}:$ty2.$g)}.
     908notation > "'If' b 'then' f 'else' 'with' ident prf2 'do' g" with precedence 46 for
     909  @{'if_then_else_safe $b (λ_.$f) (λ${ident prf2}.$g)}.
     910notation > "'If' b 'then' f 'else' 'with' ident prf2 : ty2 'do' g" with precedence 46 for
     911  @{'if_then_else_safe $b (λ_.$f) (λ${ident prf2}:$ty2.$g)}.
     912notation > "'If' b 'then' 'with' ident prf1 'do' f 'else' g" with precedence 46 for
     913  @{'if_then_else_safe $b (λ${ident prf1}.$f) (λ_.$g)}.
     914notation > "'If' b 'then' 'with' ident prf1 : ty1 'do' f 'else' g" with precedence 46 for
     915  @{'if_then_else_safe $b (λ${ident prf1}:$ty1.$f) (λ_.$g)}.
     916
     917notation < "hvbox('If' \nbsp b \nbsp 'then' \nbsp break 'with' \nbsp ident prf1 : ty1 \nbsp 'do' \nbsp break f \nbsp break 'else' \nbsp break 'with' \nbsp ident prf2 : ty2 \nbsp 'do' \nbsp break g)" with precedence 46 for
     918  @{'if_then_else_safe $b (λ${ident prf1}:$ty1.$f) (λ${ident prf2}:$ty2.$g)}.
     919notation < "hvbox('If' \nbsp b \nbsp 'then' \nbsp break f \nbsp break 'else' \nbsp break 'with' \nbsp ident prf2 : ty2 \nbsp 'do' \nbsp break g)" with precedence 46 for
     920  @{'if_then_else_safe $b (λ_:$ty1.$f) (λ${ident prf2}:$ty2.$g)}.
     921notation < "hvbox('If' \nbsp b \nbsp 'then' \nbsp break 'with' \nbsp ident prf1 : ty1 \nbsp 'do' \nbsp break f \nbsp break 'else' \nbsp break g)" with precedence 46 for
     922  @{'if_then_else_safe $b (λ${ident prf1}:$ty1.$f) (λ_:$ty2.$g)}.
     923 
     924interpretation "dependent if then else" 'if_then_else_safe b f g = (if_then_else_safe ? b f g).
    839925
    840926lemma length_append:
Note: See TracChangeset for help on using the changeset viewer.