Changeset 2142 for src/ASM

Timestamp:

Jun 29, 2012, 10:09:10 AM (8 years ago)

Author:

sacerdot

Message:

Down to one daemon that requires one lemma (monotonicity of sigma).

File:

• src/ASM/AssemblyProof.ma (modified) (1 diff)

src/ASM/AssemblyProof.ma

@@ -406 +406 @@
     [1: #j #H <load_code_memory_ok
         [ @assembly_ok
-        | cut (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (|assembled|))) ≤ |assembled'|)
-          [ cases sigma_policy_witness #_ #sigma_ok cases daemon
-            (*CSC: True, propagate already proved invariant*)
-          | #LE @(lt_to_le_to_lt … LE)
-            @lt_to_lt_nat_of_bitvector_add
-            [ @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? eq_assembly_1_pseudoinstruction)
-              / by /
-            | @(transitive_le ???? assembly_ok1) change with (? < ?) cases daemon
-              (*CSC: Same as before*)
-            | assumption
-            ]   
+        | cases (le_to_or_lt_eq … assembly_ok1)
+          [ #assembly_ok1'
+            cut (nat_of_bitvector 16 (sigma ppc)+|assembled|≤|assembled'|)
+            [ <assembly_ok3 cases sigma_policy_witness #_ >EQprogram #sigma_ok
+              cases (sigma_ok … ppc_ok) -sigma_ok >eq_fetch_pseudo_instruction
+              #sigma_ok1 #sigma_ok2
+              cases daemon (*CSC: True, apply lemma above + monotonicity of sigma *)
+            | #LE2
+              cut (|assembled| < 2^16)
+               [ @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? eq_assembly_1_pseudoinstruction) / by /] #LTassembled
+              cut (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (|assembled|))) ≤ |assembled'|)
+              [ >nat_of_bitvector_add
+                >nat_of_bitvector_bitvector_of_nat_inverse try assumption
+                @(le_to_lt_to_lt … LE2 assembly_ok1')
+              | #LE @(lt_to_le_to_lt … LE)
+                @lt_to_lt_nat_of_bitvector_add
+                [ @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? eq_assembly_1_pseudoinstruction)
+                  / by /
+                | @(le_to_lt_to_lt ???? assembly_ok1') @LE2
+                | assumption
+                ]
+              ]
+            ]
+          | #assembly_ok1' >assembly_ok1' / by /
           ]
         ]