Changeset 2079 for src/ASM/Assembly.ma

Timestamp:

Jun 14, 2012, 11:45:49 AM (8 years ago)

Author:

sacerdot

Message:

sigma_policy_specification restyled

File:

• src/ASM/Assembly.ma (modified) (2 diffs)

src/ASM/Assembly.ma

@@ -773 +773 @@
   λsigma: Word → Word.
   λpolicy: Word → bool.
+  sigma (zero …) = zero … ∧
   ∀ppc: Word. ∀ppc_ok.
     let instr_list ≝ \snd program in
@@ -780 +781 @@
     let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
     let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
-     sigma (zero …) = zero …
-     ∧
-      (nat_of_bitvector … ppc ≤ |instr_list| →
+     (nat_of_bitvector … ppc ≤ |instr_list| →
        next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction)))
      ∧