Changeset 1882 for src/ASM/Status.ma

Timestamp:

Apr 6, 2012, 8:02:10 PM (9 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

File:

• src/ASM/Status.ma (modified) (2 diffs)

src/ASM/Status.ma

@@ -510 +510 @@
   λac: option Bit.
   λov: Bit.
-    let old_cy ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) O ? in
-    let old_ac ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 1 ? in
-    let old_fo ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 2 ? in
-    let old_rs1 ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 3 ? in
-    let old_rs0 ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 4 ? in
-    let old_ov ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 5 ? in
-    let old_ud ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 6 ? in
-    let old_p ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 7 ? in
+    let sfr_psw ≝ get_8051_sfr ?? s SFR_PSW in
+    let old_cy ≝ get_index_v ?? sfr_psw O ? in
+    let old_ac ≝ get_index_v ?? sfr_psw 1 ? in
+    let old_fo ≝ get_index_v ?? sfr_psw 2 ? in
+    let old_rs1 ≝ get_index_v ?? sfr_psw 3 ? in
+    let old_rs0 ≝ get_index_v ?? sfr_psw 4 ? in
+    let old_ov ≝ get_index_v ?? sfr_psw 5 ? in
+    let old_ud ≝ get_index_v ?? sfr_psw 6 ? in
+    let old_p ≝ get_index_v ?? sfr_psw 7 ? in
     let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in
       set_8051_sfr ?? s SFR_PSW
@@ -1128 +1129 @@
 qed.
 
-definition instruction_matches_identifier ≝
-  λy: Identifier.
-  λx: labelled_instruction.
-    match \fst x with
-    [ None ⇒ false
-    | Some x ⇒ eq_identifier ? x y
-    ].
-
-let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝
- match l with
-  [ nil ⇒ true
-  | cons hd tl ⇒ notb (instruction_matches_identifier id hd) ∧ does_not_occur id tl].
-
-lemma does_not_occur_None:
- ∀id,i,list_instr.
-  does_not_occur id (list_instr@[〈None …,i〉]) =
-  does_not_occur id list_instr.
- #id #i #list_instr elim list_instr
-  [ % | #hd #tl #IH whd in ⊢ (??%%); >IH %]
-qed.
-
-lemma does_not_occur_Some:
- ∀id,id',i,list_instr.
-  eq_identifier ? id' id = false →
-   does_not_occur id (list_instr@[〈Some ? id',i〉]) =
-    does_not_occur id list_instr.
- #id #id' #i #list_instr elim list_instr
-  [ #H normalize in H ⊢ %; >H %
-  | * #x #i' #tl #IH #H whd in ⊢ (??%%); >(IH H) %]
-qed.
-
-lemma does_not_occur_absurd:
- ∀id,i,list_instr.
-  does_not_occur id (list_instr@[〈Some ? id,i〉]) = false.
- #id #i #list_instr elim list_instr
-  [ normalize change with (if (if eq_identifier ??? then ? else ?) then ? else ? = ?)
-    >eq_identifier_refl %
-  | * #x #i' #tl #IH whd in ⊢ (??%%); >IH cases (notb ?) %]
-qed.
-
-
-let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
- match l with
-  [ nil ⇒ false
-  | cons hd tl ⇒
-     if instruction_matches_identifier id hd then
-      does_not_occur id tl
-     else
-      occurs_exactly_once id tl ].
-
-lemma occurs_exactly_once_None:
- ∀id,i,list_instr.
-  occurs_exactly_once id (list_instr@[〈None …,i〉]) =
-  occurs_exactly_once id list_instr.
- #id #i #list_instr elim list_instr
-  [ % | #hd #tl #IH whd in ⊢ (??%%); >IH >does_not_occur_None %]
-qed.
-
-lemma occurs_exactly_once_Some:
- ∀id,id',i,prefix.
-  occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_identifier ? id' id ∨ occurs_exactly_once id prefix.
- #id #id' #i #prefix elim prefix
-  [ whd in ⊢ (?% → ?);
-    change with (eq_identifier ? id' id) in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
-    @eq_identifier_elim normalize nodelta; /2/
-  | *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
-    cases he; normalize nodelta
-     [ #H @ (IH H)
-     | #x whd in ⊢ (? → ?(??%)); change with (eq_identifier ? x id) in match (instruction_matches_identifier ??);
-       @eq_identifier_elim #E normalize nodelta
-       [ destruct @eq_identifier_elim normalize nodelta;
-        /2/ #H >does_not_occur_Some /2/
-       | #H @IH @H]]]
-qed.
-
-lemma occurs_exactly_once_Some_stronger:
-  ∀id,id',i,prefix.
-    occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → 
-    (eq_identifier ? id' id ∧ does_not_occur id prefix) ∨
-    (¬eq_identifier ? id' id ∧ occurs_exactly_once id prefix).
- #id #id' #i #prefix elim prefix
- [ whd in ⊢ (?% → ?); change with (eq_identifier ???) in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?);
-   @eq_identifier_elim #E
-  [ normalize //
-  | normalize #H @⊥ @H  
-  ]
- | *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
-   cases he; normalize nodelta
-   [ #H @ (IH H)
-   | #x @eq_identifier_elim #Heq
-     [ @eq_identifier_elim normalize nodelta
-       [ #H >H >does_not_occur_absurd #Hf @⊥ @Hf
-       | #H >(does_not_occur_Some)
-         [ #H2 whd in match (does_not_occur ??);
-           change with (eq_identifier ???) in match (instruction_matches_identifier ??);
-           >Heq >eq_identifier_refl normalize nodelta
-           @orb_elim normalize nodelta whd in match (occurs_exactly_once ??);
-           change with (eq_identifier ???) in match (instruction_matches_identifier ??);
-           >eq_identifier_refl
-           normalize nodelta @H2  
-         | /2/
-         ]
-       ]
-     | normalize nodelta #H lapply (IH H) -IH -H;
-       @eq_identifier_elim #Heq2
-       #Hor @orb_elim
-       [ <Heq2 in Hor; #Hor normalize in Hor;
-         whd in match (does_not_occur ??); change with (eq_identifier ???) in match (instruction_matches_identifier ??);
-         >eq_identifier_false // normalize nodelta
-         cases (does_not_occur id' tl) in Hor; normalize nodelta //
-       | normalize nodelta whd in match (occurs_exactly_once ??);
-         change with (eq_identifier ???) in match (instruction_matches_identifier ??);
-         >eq_identifier_false //
-       ] 
-     ]  
-   ]
- ]
-qed.   
-
-let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
-  match l with
-  [ nil ⇒ ?
-  | cons hd tl ⇒
-    if pred hd then
-      acc
-    else
-      index_of_internal A pred tl (S acc)
-  ].
-  cases not_implemented.
-qed.
-
-
-definition index_of ≝
-  λA.
-  λeq.
-  λl.
-    index_of_internal A eq l 0.
-
-lemma index_of_internal_None: ∀i,id,instr_list,n.
- occurs_exactly_once id (instr_list@[〈None …,i〉]) →
-  index_of_internal ? (instruction_matches_identifier id) instr_list n =
-   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
- #i #id #instr_list elim instr_list
-  [ #n #abs whd in abs; cases abs
-  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?);
-    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%);
-    [ #H %
-    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %;
-      [ #_ % | #abs cases abs ]]]
-qed.
-
-lemma index_of_internal_Some_miss: ∀i,id,id'.
- eq_identifier ? id' id = false →
- ∀instr_list,n.
- occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
-  index_of_internal ? (instruction_matches_identifier id) instr_list n =
-   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n.
- #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ
- change with (occurs_exactly_once ?? → ?) generalize in match n; -n -H; elim instr_list
-  [ #n #abs cases abs
-  | #hd #tl #IH #n whd in ⊢ (?% → ??%%); cases (instruction_matches_identifier id hd) normalize nodelta;
-    [ // | #K @IH //]]
-qed.
-
-lemma index_of_internal_Some_hit: ∀i,id.
- ∀instr_list,n.
-  occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
-   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id,i〉]) n
-  = |instr_list| + n.
- #i #id #instr_list elim instr_list
-  [ #n #_ whd in ⊢ (??%%); change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl %
-  | #hd #tl #IH #n whd in ⊢ (?% → ??%%); cases (instruction_matches_identifier id hd) normalize nodelta;
-    [ >does_not_occur_absurd #abs cases abs | #H >plus_n_Sm applyS (IH (S n)) //]]
-qed.
-
 definition address_of_word_labels_code_mem ≝
-  λcode_mem.
+  λcode_mem : list labelled_instruction.
   λid: Identifier.
-    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier id) code_mem).
+    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem).
 
 lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
- occurs_exactly_once id (instr_list@[〈None …,i〉]) →
+ occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
   address_of_word_labels_code_mem instr_list id =
   address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
  #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
- >(index_of_internal_None … H) %
+ >(index_of_internal_None ?????? H) %
 qed.
 
 lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
  eq_identifier ? id' id = false →
-  occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
+  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
    address_of_word_labels_code_mem instr_list id =
    address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
  #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
- >(index_of_internal_Some_miss … H) [ @refl | // ]
+ >(index_of_internal_Some_miss ???????? H) [ @refl | // ]
 qed.
 
 lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
-  occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
+  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
    address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
    = bitvector_of_nat … (|instr_list|).
  #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
- >(index_of_internal_Some_hit … H) <plus_n_O @refl
+ >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl
 qed.