Changeset 2228

Timestamp:

Jul 20, 2012, 9:10:21 PM (9 years ago)

Author:

sacerdot

Message:

Further proof reduction.

File:

• src/ASM/Policy.ma (modified) (5 diffs)

src/ASM/Policy.ma

@@ -647 +647 @@
 [ lapply (proj1 ?? (proj1 ?? (proj1 ?? Hfpol))) cases (bvt_lookup ??? fpol 〈0,short_jump〉)
   #x #y #Hx normalize nodelta >Hx / by refl/
-| #ppc #ppc_ok normalize nodelta @conj
+| #ppc #ppc_ok normalize nodelta
+  >(?:\fst (fetch_pseudo_instruction (pi1 … (\snd program)) ppc ppc_ok) =
+       \snd (nth (nat_of_bitvector … ppc) ? (\snd program) 〈None ?, Comment []〉))
+  [2: whd in match fetch_pseudo_instruction; normalize nodelta
+   >(nth_safe_nth … 〈None ?, Comment []〉)
+   cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
+   #lbl #ins % ]
+  @conj
   [ lapply ((proj2 ?? (proj1 ?? Hfpol)) (nat_of_bitvector ? ppc) ppc_ok)
     >bitvector_of_nat_inverse_nat_of_bitvector
-    lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %);
-    [ #Hl normalize nodelta #abs cases abs
-    | #x cases x -x #pc #jl #Hl normalize nodelta <add_bitvector_of_nat_Sm
+    inversion (lookup_opt ????) normalize nodelta
+    [ #Hl #abs cases abs
+    | * #pc #jl #Hl normalize nodelta <add_bitvector_of_nat_Sm
       >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative
-      lapply (refl ? (lookup_opt … (add ? ppc (bitvector_of_nat ? 1)) fpol))
-      cases (lookup_opt … (add ? ppc (bitvector_of_nat ? 1)) fpol) in ⊢ (???% → %);
-      [ #Hl normalize nodelta #abs cases abs
-      | #x cases x -x #Spc #Sjl #SHl normalize nodelta #Hcompact
+      inversion (lookup_opt ????) normalize nodelta
+      [ #_ #abs cases abs
+      | * #Spc #Sjl #SHl normalize nodelta #Hcompact
         >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta
         >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
-        >add_bitvector_of_nat_plus >Hcompact @eq_f @eq_f @eq_f
-        whd in match (fetch_pseudo_instruction ???); >nth_safe_nth
-        [ cases (nth ? labelled_instruction ??) |2: skip] normalize nodelta // ]]
+        >add_bitvector_of_nat_plus >Hcompact % ]]
   | (* Basic proof scheme:
        - ppc < |snd program|, hence our instruction is in the program
@@ -675 +679 @@
       lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc) ppc_ok)
       >bitvector_of_nat_inverse_nat_of_bitvector
-      lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %);
-      [ normalize nodelta #_ #abs cases abs
-      | #x cases x -x #pc #jl #EQ normalize nodelta
-        lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol))
-        cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol) in ⊢ (???% → %);
-        [ normalize nodelta #_ #abs cases abs
-        | #x cases x -x #Spc #Sjl #SEQ normalize nodelta       
-          #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
+      inversion (lookup_opt ????) normalize nodelta
+      [ #_ #abs cases abs
+      | * #pc #jl #Hl normalize nodelta
+        inversion (lookup_opt ????) normalize nodelta
+        [ #_ #abs cases abs
+        | * #Spc #Sjl #SHl normalize nodelta #Hcompact       
+          >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
           >nat_of_bitvector_bitvector_of_nat_inverse
           [2: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
-              >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
+              >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
               #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H ]
           lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
-          >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >H -H #H @(transitive_le … H)
-          cut (∀x,y. x=y → x ≤ y) [ #x #y * %] #eq_to_leq @eq_to_leq @eq_f @eq_f
-          whd in match (fetch_pseudo_instruction ???); >nth_safe_nth
-          [ cases (nth ? labelled_instruction ??) |2: skip] normalize nodelta // ]]
+          >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) >Hcompact #X @X ]]
     | (* the program is of length 2^16 and ppc is followed by only zero-size instructions
        * until the end of the program *)
@@ -712 +712 @@
             [ <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
               >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #HSpc %1
-              >Hc in HSpc;
-              whd in match create_label_map;
-              whd in match fetch_pseudo_instruction; normalize nodelta
-              >(nth_safe_nth … 〈None ?, Comment []〉)
-              cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
-              #lbl #ins normalize nodelta #X @X 
+              >Hc in HSpc; #X @X
             | <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
               >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #Hspc %2 @conj
-              [ #ppc' #ppc_ok' #Hppc' 
+              [2: >Hc in Hspc; #X @X
+              | #ppc' #ppc_ok' #Hppc' 
                 (* S ppc < ppc' < |\snd program| *)
                 (* lookup S ppc = 2^16 *)
@@ -727 +723 @@
                 lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc') ppc_ok')
                 >bitvector_of_nat_inverse_nat_of_bitvector
-                lapply (refl ? (lookup_opt … ppc' fpol))
-                cases (lookup_opt … ppc' fpol) in ⊢ (???% → %);
-                [ normalize nodelta #_ #abs cases abs
-                | normalize nodelta #x cases x -x #xpc #xjl #XEQ normalize nodelta
-                  lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc'))) fpol))
-                  cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc'))) fpol) in ⊢ (???% → %);
-                  [ normalize nodelta #_ #abs cases abs
-                  | normalize nodelta #x cases x -x #Sxpc #Sxjl #SXEQ normalize nodelta
+                inversion (lookup_opt ????) normalize nodelta
+                [ #_ #abs cases abs
+                | * #xpc #xjl #XEQ normalize nodelta
+                  inversion (lookup_opt ????) normalize nodelta
+                  [ #_ #abs cases abs
+                  | * #Sxpc #Sxjl #SXEQ normalize nodelta
                     #Hpcompact
                     lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (\snd program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok'))
@@ -756 +750 @@
                   ]
                 ]
-              | >Hc in Hspc;
-                whd in match create_label_map;
-                whd in match fetch_pseudo_instruction; normalize nodelta
-                >(nth_safe_nth … 〈None ?, Comment []〉)
-                cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
-                 #lbl #ins normalize nodelta 
-                whd in match instruction_size;
-                whd in match assembly_1_pseudoinstruction;
-                whd in match expand_pseudo_instruction; normalize nodelta 
-                <add_bitvector_of_nat_Sm in SEQ; >bitvector_of_nat_inverse_nat_of_bitvector
-                >add_commutative #SEQ cases ins
-                [2,3,6: #x [3: #y] normalize nodelta #H @H
-                |4,5: #x normalize nodelta
-                  >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
-                  >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
-                  cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
-                  #lpc #ljl normalize nodelta #H @H
-                |1: #pi normalize nodelta #X @X
-                ]
               ]
             ]