Changeset 2230 for src

Timestamp:

Jul 23, 2012, 10:35:43 AM (8 years ago)

Author:

sacerdot

Message:

Glue proof maximally simplified or sort of.

File:

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

src/ASM/Policy.ma

@@ -653 +653 @@
    cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
    #lbl #ins % ]
+  lapply (Hfpol3 (nat_of_bitvector ? ppc) ppc_ok) >bitvector_of_nat_inverse_nat_of_bitvector
+  inversion (lookup_opt ????) normalize nodelta [ #Hl #abs cases abs ]
+  * #pc #jl #Hl normalize nodelta
+  inversion (lookup_opt ????) normalize nodelta [ #Hl #abs cases abs ]
+  * #Spc #Sjl #SHL lapply SHL
+  <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative
+  #SHl normalize nodelta #Hcompact
   @conj
-  [ lapply (Hfpol3 (nat_of_bitvector ? ppc) ppc_ok)
-    >bitvector_of_nat_inverse_nat_of_bitvector
-    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
-      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 % ]]
+  [ >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉)
+    >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
+    >add_bitvector_of_nat_plus >Hcompact %
   | (* Basic proof scheme:
        - ppc < |snd program|, hence our instruction is in the program
@@ -676 +674 @@
     elim (le_to_or_lt_eq … Hfpol4) #Hfpc
     [ %1 @(le_to_lt_to_lt … Hfpc) >Hfpol2
-      lapply (Hfpol3 (nat_of_bitvector ? ppc) ppc_ok)
-      >bitvector_of_nat_inverse_nat_of_bitvector
-      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 … Hl 〈0,short_jump〉)
-              #H @(le_to_lt_to_lt … Hfpc) >Hfpol2 @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 … SHl 〈0,short_jump〉) >Hcompact #X @X ]]
+      >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉)
+      >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 … Hl 〈0,short_jump〉)
+          #H @(le_to_lt_to_lt … Hfpc) >Hfpol2 @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 … 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 *)
       elim (le_to_or_lt_eq … (pc_increases (nat_of_bitvector ? ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)))
-      [ lapply (Hfpol3 (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 #Hc
-            >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hpc normalize nodelta
-            >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
-            >nat_of_bitvector_bitvector_of_nat_inverse
-            [2: <Hfpc >Hfpol2 @Hpc ]
-            elim (le_to_or_lt_eq … (pc_increases (S (nat_of_bitvector ? ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)))
-            <Hfpol2 >Hfpc >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #HSpc
-            [ %1 >Hc in HSpc; #X @X
-            | %2 @conj
-              [2: >Hc in HSpc; #X @X
-              | #ppc' #ppc_ok' #Hppc'
+      [ >bitvector_of_nat_inverse_nat_of_bitvector
+        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #Hpc normalize nodelta
+        >nat_of_bitvector_bitvector_of_nat_inverse
+        [2: <Hfpc >Hfpol2 @Hpc ]
+        elim (le_to_or_lt_eq … (pc_increases (S (nat_of_bitvector ? ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)))
+        <Hfpol2 >Hfpc >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) #HSpc
+        [ %1 >Hcompact in HSpc; #X @X
+        | %2 @conj
+          [2: >Hcompact in HSpc; #X @X
+          | #ppc' #ppc_ok' #Hppc'
                 (* S ppc < ppc' < |\snd program| *)
                 (* lookup S ppc = 2^16 *)
@@ -728 +708 @@
                     #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'))
-                    >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >HSpc #Hle1
+                    >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1
                     lapply (pc_increases (nat_of_bitvector ? ppc') (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok') (le_n ?))
                     <Hfpol2 >Hfpc #Hle2
@@ -735 +715 @@
                     >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) #Hxpc
                     lapply (pc_increases (S (nat_of_bitvector ? ppc)) (S (nat_of_bitvector ? ppc')) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … (le_S_S … Hppc')) ppc_ok')
-                    >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >HSpc #Hle1
+                    >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1
                     lapply (pc_increases (S (nat_of_bitvector ? ppc')) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok' (le_n ?))
                     <Hfpol2 >Hfpc #Hle2
@@ -747 +727 @@
                   ]
                 ]
-              ]
-            ]
           ]
         ]
       | >bitvector_of_nat_inverse_nat_of_bitvector
-        <Hfpol2 >Hfpc
-        cases (lookup … ppc fpol 〈0,short_jump〉) #pc #jl normalize nodelta #Hpc %1 >Hpc
+        <Hfpol2 >Hfpc >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #Hpc
+        %1 >Hpc
         >bitvector_of_nat_exp_zero whd in match (nat_of_bitvector ? (zero ?));
         <plus_O_n whd in match instruction_size; normalize nodelta
-        lapply (refl ? (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?))
-        [5: cases (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?) in ⊢ (???% → %);
-          #len #ins #Hass lapply (fst_snd_assembly_1_pseudoinstruction … Hass)
-          #Hli >Hli
-          lapply (assembly1_pseudoinstruction_lt_2_to_16 ??? ppc (λx0.zero 16) ?)
-          [5: >Hass / by /
-          ]
-        ]
+        inversion (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?)
+        #len #ins #Hass lapply (fst_snd_assembly_1_pseudoinstruction … Hass)
+        #Hli >Hli
+        lapply (assembly1_pseudoinstruction_lt_2_to_16 ??? ppc (λx0.zero 16) ?)
+        [5: >Hass / by / ]
       ]
     ]