Changeset 2111 for src

Timestamp:

Jun 26, 2012, 5:30:41 PM (8 years ago)

Author:

sacerdot

Message:

Cleanup: lemmas/theorems/axioms moved to the right places.

Location:

src

Files:

• ASM/Arithmetic.ma (modified) (2 diffs)
• ASM/Assembly.ma (modified) (3 diffs)
• ASM/AssemblyProof.ma (modified) (4 diffs)
• ASM/Status.ma (modified) (1 diff)
• ASM/Util.ma (modified) (1 diff)
• common/Identifiers.ma (modified) (1 diff)

src/ASM/Arithmetic.ma

@@ -189 +189 @@
   ∀b: BitVector n.
     bitvector_of_nat n (nat_of_bitvector n b) = b.
+
+axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n.
 
 lemma nat_of_bitvector_aux_injective:
@@ -689 +691 @@
     add … l r = add … r l.
 
+axiom nat_of_bitvector_add:
+ ∀n,v1,v2.
+  nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n →
+   nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.
+
 example add_SO:
   ∀n: nat.

src/ASM/Assembly.ma

@@ -581 +581 @@
     \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i).
 
-(*CSC: move elsewhere *)
-lemma nth_safe_append:
- ∀A,l,n,n_ok.
-  ∃pre,suff.
-   (pre @ [nth_safe A n l n_ok]) @ suff = l.
-#A #l elim l normalize
- [ #n #abs cases (absurd ? abs (not_le_Sn_O ?))
- | #hd #tl #IH #n cases n normalize
-   [ #_ %{[]} /2/
-   | #m #m_ok cases (IH m ?)
-     [ #pre * #suff #EQ %{(hd::pre)} %{suff} <EQ in ⊢ (???%); % | skip ]]
-qed.
-
-lemma fetch_pseudo_instruction_vsplit:
- ∀instr_list,ppc,ppc_ok.
-  ∃pre,suff,lbl.
-   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.
-#instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);
-cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}
-lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta
-#EQ %{lbl0} @EQ
-qed.
-
-axiom eqb_succ_injective_Pos:
-  ∀l, r: Pos.
-    eqb (succ l) (succ r) = true → eqb l r = true.
-
-lemma eqb_true_to_refl_Pos:
-  ∀l, r: Pos.
-    eqb l r = true → l = r.
-  #l #r @(pos_elim2 … l r)
-  [1:
-    #r cases r
-    [1:
-      #_ %
-    |2,3:
-      #l normalize in ⊢ (% → ?); #absurd destruct(absurd)
-    ]
-  |2:
-    #l cases l
-    [1:
-      normalize in ⊢ (% → ?); #absurd destruct(absurd)
-    |2,3:
-      #l' normalize in ⊢ (% → ?); #absurd destruct(absurd)
-    ]
-  |3:
-    #l #r #inductive_hypothesis #relevant @eq_f
-    @inductive_hypothesis @eqb_succ_injective_Pos
-    assumption
-  ]
-qed.
-
-lemma eq_identifier_eq:
-  ∀tag: String.
-  ∀l.
-  ∀r.
-    eq_identifier tag l r = true → l = r.
-  #tag #l #r cases l cases r
-  #pos_l #pos_r
-  cases pos_l cases pos_r
-  [1:
-    #_ %
-  |2,3,4,7:
-    #p1_l normalize in ⊢ (% → ?);
-    #absurd destruct(absurd)
-  |5,9:
-    #p1_l #p1_r normalize in ⊢ (% → ?);
-    #relevant
-    >(eqb_true_to_refl_Pos … relevant) %
-  |*:
-    #p_l #p_r normalize in ⊢ (% → ?);
-    #absurd destruct(absurd)
-  ]
-qed.
-
-axiom neq_identifier_neq:
-  ∀tag: String.
-  ∀l, r: identifier tag.
-    eq_identifier tag l r = false → (l = r → False).
   
 (* label_map: identifier ↦ pseudo program counter *)
@@ -772 +693 @@
 qed.
 
-
-(*CSC: move elsewhere; practically equal to shift_nth_safe but for commutation
-  of addition. One of the two lemmas should disappear. *)
-lemma nth_safe_prepend:
- ∀A,l1,l2,j.∀H:j<|l2|.∀K:|l1|+j<|(l1@l2)|.
-  nth_safe A j l2 H =nth_safe A (|l1|+j) (l1@l2) K.
- #A #l1 #l2 #j #H >commutative_plus @shift_nth_safe
-qed.
-
-lemma nth_safe_cons:
- ∀A,hd,tl,l2,j,j_ok,Sj_ok.
-  nth_safe A j (tl@l2) j_ok =nth_safe A (1+j) (hd::tl@l2) Sj_ok.
-//
-qed.
-
-lemma eq_nth_safe_proof_irrelevant:
- ∀A,l,i,i_ok,i_ok'.
-  nth_safe A l i i_ok = nth_safe A l i i_ok'.
-#A #l #i #i_ok #i_ok' %
-qed.
-
-(*CSC: move elsewhere *)
-axiom nat_of_bitvector_add:
- ∀n,v1,v2.
-  nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n →
-   nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.
-
-(*CSC: move elsewhere *)
-lemma fetch_pseudo_instruction_append:
- ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'.
-  let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
-  fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
-  〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
- #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
- cut (|l1| + nat_of_bitvector … ppc < 2^16)
- [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]
- -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
- >nat_of_bitvector_bitvector_of_nat_inverse try assumption
- [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ] 
- #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
- #lbl #instr normalize nodelta >add_associative %
-qed.
-
 definition sigma_policy_specification ≝
   λprogram: pseudo_assembly_program.
@@ -832 +710 @@
       (  (nat_of_bitvector … ppc < |instr_list| → nat_of_bitvector … pc < nat_of_bitvector … next_pc)
        ∨ (nat_of_bitvector … ppc = |instr_list| → next_pc = (zero …))).
-
-(*CSC: Move elsewhere *)
-axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n.
 
 definition assembly:

src/ASM/AssemblyProof.ma

@@ -3 +3 @@
 include "ASM/StatusProofs.ma".
 include alias "arithmetics/nat.ma".
-
-definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
-  λP.
-    P true ∧ P false.
- 
-let rec bitvector_elim_prop_internal
-  (n: nat) (P: BitVector n → Prop) (m: nat)
-    on m:
-      m ≤ n → BitVector (n - m) → Prop ≝
-  match m return λm. m ≤ n → BitVector (n - m) → Prop with
-  [ O    ⇒ λprf1. λprefix. P ?
-  | S n' ⇒ λprf2. λprefix.
-      bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' …)
-  ].
-  try applyS prefix
-  try (@le_S_to_le assumption)
-  letin res ≝ (bit ::: prefix)
-  <minus_S_S >minus_Sn_m
-  assumption
-qed.
-
-definition bitvector_elim_prop ≝
-  λn: nat.
-  λP: BitVector n → Prop.
-    bitvector_elim_prop_internal n P n ? ?.
-  try @le_n
-  <minus_n_n @[[ ]]
-qed.
-
-lemma bool_eq_internal_eq:
-  ∀b, c.
-    (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c.
-  #b #c
-  cases b cases c normalize nodelta
-  try (#_ % @I)
-  #assm destruct %
-qed.
 
 definition bit_elim: ∀P: bool → bool. bool ≝
@@ -62 +25 @@
   try @le_n
   <minus_n_n @[[]]
-qed.
-
-lemma mem_middle_vector:
-  ∀A: Type[0].
-  ∀m, o: nat.
-  ∀eq: A → A → bool.
-  ∀reflex: ∀a. eq a a = true.
-  ∀p: Vector A m.
-  ∀a: A.
-  ∀r: Vector A o.
-    mem A eq ? (p@@(a:::r)) a = true.
-  #A #m #o #eq #reflex #p #a
-  elim p try (normalize >reflex #H %)
-  #m' #hd #tl #inductive_hypothesis
-  normalize
-  cases (eq ??) normalize nodelta
-  try (#irrelevant %)
-  @inductive_hypothesis
 qed.
 
@@ -136 +81 @@
   cases v try %
   #n' #hd #tl %
-qed.
-
-corollary subvector_hd_tl:
-  ∀A: Type[0].
-  ∀o: nat.
-  ∀eq: A → A → bool.
-  ∀refl: ∀a. eq a a = true.
-  ∀h: A.
-  ∀v: Vector A o.
-    bool_to_Prop (subvector_with A ? ? eq v (h ::: v)).
-  #A #o #eq #reflex #h #v
-  >(vector_cons_append … h v)
-  <(vector_cons_empty … ([[h]] @@ v))
-  @(subvector_multiple_append … eq reflex [[ ]] v ? [[h]])
 qed.
 
@@ -236 +167 @@
   ]
 qed.
-
-definition product_elim ≝
-  λm, n: nat.
-  λv: Vector addressing_mode_tag (S m).
-  λq: Vector addressing_mode_tag (S n).
-  λP: (v × q) → bool.
-    list_addressing_mode_tags_elim ? v (λx. list_addressing_mode_tags_elim ? q (λy. P 〈x, y〉)).
-
-definition union_elim ≝ 
-  λA, B: Type[0].
-  λelimA: (A → bool) → bool.
-  λelimB: (B → bool) → bool.
-  λelimU: A ⊎ B → bool.
-    elimA (λa. elimB (λb. elimU (inl ? ? a) ∧ elimU (inr ? ? b))).
-
-(*                           
-definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
-  λP.
-    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADD ? ACC_A addr)) ∧
-    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADDC ? ACC_A addr)) ∧
-    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (SUBB ? ACC_A addr)) ∧
-    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ; dptr ]] (λaddr. P (INC ? addr)) ∧
-    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (DEC ? addr)) ∧
-    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧
-    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧
-    list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
-    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧
-    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧
-    P (DA ? ACC_A) ∧
-    bitvector_elim 8 (λr. P (JC ? (RELATIVE r))) ∧
-    bitvector_elim 8 (λr. P (JNC ? (RELATIVE r))) ∧
-    bitvector_elim 8 (λr. P (JZ ? (RELATIVE r))) ∧
-    bitvector_elim 8 (λr. P (JNZ ? (RELATIVE r))) ∧
-    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JB ? (BIT_ADDR b) (RELATIVE r))))) ∧
-    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JNB ? (BIT_ADDR b) (RELATIVE r))))) ∧
-    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JBC ? (BIT_ADDR b) (RELATIVE r))))) ∧
-    list_addressing_mode_tags_elim ? [[ registr; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
-    P (RL ? ACC_A) ∧
-    P (RLC ? ACC_A) ∧
-    P (RR ? ACC_A) ∧
-    P (RRC ? ACC_A) ∧
-    P (SWAP ? ACC_A) ∧
-    P (RET ?) ∧
-    P (RETI ?) ∧
-    P (NOP ?) ∧
-    bit_elim (λb. P (XCHD ? ACC_A (INDIRECT b))) ∧
-    list_addressing_mode_tags_elim ? [[ carry; bit_addr ]] (λaddr. P (SETB ? addr)) ∧
-    bitvector_elim 8 (λaddr. P (PUSH ? (DIRECT addr))) ∧
-    bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))) ∧
-    union_elim ? ? (product_elim ? ? [[ acc_a ]] [[ direct; data ]])
-                   (product_elim ? ? [[ registr; indirect ]] [[ data ]])
-                   (λd. bitvector_elim 8 (λb. P (CJNE ? d (RELATIVE b)))) ∧
-    list_addressing_mode_tags_elim ? [[ registr; direct; indirect ]] (λaddr. P (XCH ? ACC_A addr)) ∧
-    union_elim ? ? (product_elim ? ? [[acc_a]] [[ data ; registr ; direct ; indirect ]])
-                   (product_elim ? ? [[direct]] [[ acc_a ; data ]])
-                   (λd. P (XRL ? d)) ∧
-    union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]]) 
-                                   (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
-                   (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
-                   (λd. P (ANL ? d)) ∧
-    union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; data ; direct ; indirect ]]) 
-                                   (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
-                   (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
-                   (λd. P (ORL ? d)) ∧
-    union_elim ? ? (product_elim ? ? [[acc_a]] [[ ext_indirect ; ext_indirect_dptr ]])
-                   (product_elim ? ? [[ ext_indirect ; ext_indirect_dptr ]] [[acc_a]])
-                   (λd. P (MOVX ? d)) ∧
-    union_elim ? ? (
-      union_elim ? ? (
-        union_elim ? ? (
-          union_elim ? ? (
-            union_elim ? ?  (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
-                            (product_elim ? ? [[ registr ; indirect ]] [[ acc_a ; direct ; data ]]))
-                            (product_elim ? ? [[direct]] [[ acc_a ; registr ; direct ; indirect ; data ]]))
-                            (product_elim ? ? [[dptr]] [[data16]]))
-                            (product_elim ? ? [[carry]] [[bit_addr]]))
-                            (product_elim ? ? [[bit_addr]] [[carry]])
-                            (λd. P (MOV ? d)).
-  %
-qed.
-  
-definition instruction_elim: ∀P: instruction → bool. bool ≝
-  λP. (*
-    bitvector_elim 11 (λx. P (ACALL (ADDR11 x))) ∧
-    bitvector_elim 16 (λx. P (LCALL (ADDR16 x))) ∧
-    bitvector_elim 11 (λx. P (AJMP (ADDR11 x))) ∧
-    bitvector_elim 16 (λx. P (LJMP (ADDR16 x))) ∧ *)
-    bitvector_elim 8 (λx. P (SJMP (RELATIVE x))). (*  ∧
-    P (JMP INDIRECT_DPTR) ∧
-    list_addressing_mode_tags_elim ? [[ acc_dptr; acc_pc ]] (λa. P (MOVC ACC_A a)) ∧
-    preinstruction_elim (λp. P (RealInstruction p)). *)
-  %
-qed.
-
-
-axiom instruction_elim_complete:
- ∀P. instruction_elim P = true → ∀i. P i = true.
-*)
-(*definition eq_instruction ≝
-  λi, j: instruction.
-    true.*)
 
 definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝

src/ASM/Status.ma

@@ -1130 +1130 @@
 qed.
 
+lemma fetch_pseudo_instruction_vsplit:
+ ∀instr_list,ppc,ppc_ok.
+  ∃pre,suff,lbl.
+   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.
+#instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);
+cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}
+lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta
+#EQ %{lbl0} @EQ
+qed.
+
+lemma fetch_pseudo_instruction_append:
+ ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'.
+  let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
+  fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
+  〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
+ #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
+ cut (|l1| + nat_of_bitvector … ppc < 2^16)
+ [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]
+ -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
+ >nat_of_bitvector_bitvector_of_nat_inverse try assumption
+ [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ] 
+ #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
+ #lbl #instr normalize nodelta >add_associative %
+qed.
+
 definition address_of_word_labels_code_mem ≝
   λcode_mem : list labelled_instruction.

src/ASM/Util.ma

@@ -253 +253 @@
 qed.
 
+(*CSC: practically equal to shift_nth_safe but for commutation
+  of addition. One of the two lemmas should disappear. *)
+lemma nth_safe_prepend:
+ ∀A,l1,l2,j.∀H:j<|l2|.∀K:|l1|+j<|(l1@l2)|.
+  nth_safe A j l2 H =nth_safe A (|l1|+j) (l1@l2) K.
+ #A #l1 #l2 #j #H >commutative_plus @shift_nth_safe
+qed.
+
+lemma nth_safe_cons:
+ ∀A,hd,tl,l2,j,j_ok,Sj_ok.
+  nth_safe A j (tl@l2) j_ok =nth_safe A (1+j) (hd::tl@l2) Sj_ok.
+//
+qed.
+
+lemma eq_nth_safe_proof_irrelevant:
+ ∀A,l,i,i_ok,i_ok'.
+  nth_safe A l i i_ok = nth_safe A l i i_ok'.
+#A #l #i #i_ok #i_ok' %
+qed.
+
+lemma nth_safe_append:
+ ∀A,l,n,n_ok.
+  ∃pre,suff.
+   (pre @ [nth_safe A n l n_ok]) @ suff = l.
+#A #l elim l normalize
+ [ #n #abs cases (absurd ? abs (not_le_Sn_O ?))
+ | #hd #tl #IH #n cases n normalize
+   [ #_ %{[]} /2/
+   | #m #m_ok cases (IH m ?)
+     [ #pre * #suff #EQ %{(hd::pre)} %{suff} <EQ in ⊢ (???%); % | skip ]]
+qed.
 
 definition last_safe ≝

src/common/Identifiers.ma

@@ -80 +80 @@
 @(eqb_elim x y P) [ /2 by / | * #H @F % #E destruct /2 by / ]
 qed.
+
+lemma eq_identifier_eq:
+  ∀tag: String.
+  ∀l.
+  ∀r.
+    eq_identifier tag l r = true → l = r.
+  #tag #l #r cases l cases r
+  #pos_l #pos_r
+  cases pos_l cases pos_r
+  [1:
+    #_ %
+  |2,3,4,7:
+    #p1_l normalize in ⊢ (% → ?);
+    #absurd destruct(absurd)
+  |5,9:
+    #p1_l #p1_r normalize in ⊢ (% → ?);
+    #relevant lapply (eqb_true_to_eq … relevant) #EQ >EQ %
+  |*:
+    #p_l #p_r normalize in ⊢ (% → ?);
+    #absurd destruct(absurd)
+  ]
+qed.
+
+axiom neq_identifier_neq:
+  ∀tag: String.
+  ∀l, r: identifier tag.
+    eq_identifier tag l r = false → (l = r → False).
 
 include "basics/deqsets.ma".