Changeset 2136 for src/ASM

Timestamp:

Jun 28, 2012, 2:58:54 PM (8 years ago)

Author:

sacerdot

Message:

...

File:

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

src/ASM/AssemblyProof.ma

@@ -405 +405 @@
             (add … (sigma ppc) (bitvector_of_nat … j))))))
     [1: #j #H <load_code_memory_ok
-        [ @assembly_ok cases daemon
+        [ @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) cases daemon
+            | @(transitive_le ???? assembly_ok1) change with (? < ?) cases daemon
+              (*CSC: Same as before*)
             | assumption
             ]