Changeset 2123


Ignore:
Timestamp:
Jun 27, 2012, 4:04:14 PM (5 years ago)
Author:
boender
Message:
Location:
src/ASM
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2032 r2123  
    450450definition assembly_program ≝ list instruction.
    451451definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).
     452
     453(* labels & instructions *)
     454definition instruction_has_label ≝
     455  λid: Identifier.
     456  λi.
     457  match i with
     458  [ Jmp j ⇒ j = id
     459  | Call j ⇒ j = id
     460  | Instruction instr ⇒
     461    match instr with
     462    [ JC j ⇒ j = id
     463    | JNC j ⇒ j = id
     464    | JZ j ⇒ j = id
     465    | JNZ j ⇒ j = id
     466    | JB _ j ⇒ j = id
     467    | JBC _ j ⇒ j = id
     468    | DJNZ _ j ⇒ j = id
     469    | CJNE _ j ⇒ j = id
     470    | _ ⇒ False
     471    ]
     472  | _ ⇒ False
     473  ].
  • src/ASM/AssemblyProofSplitSplit.ma

    r2122 r2123  
    11include "ASM/AssemblyProofSplit.ma".
    22include "common/LabelledObjects.ma".
    3 
    4 definition instruction_has_label ≝
    5   λid: Identifier.
    6   λi.
    7   match i with
    8   [ Jmp j ⇒ j = id
    9   | Call j ⇒ j = id
    10   | Instruction instr ⇒
    11     match instr with
    12     [ JC j ⇒ j = id
    13     | JNC j ⇒ j = id
    14     | JZ j ⇒ j = id
    15     | JNZ j ⇒ j = id
    16     | JB _ j ⇒ j = id
    17     | JBC _ j ⇒ j = id
    18     | DJNZ _ j ⇒ j = id
    19     | CJNE _ j ⇒ j = id
    20     | _ ⇒ False
    21     ]
    22   | _ ⇒ False
    23   ].
    24  
    25 
    26 definition is_well_labelled_p ≝
    27   λinstr_list.
    28   ∀id: Identifier.
    29   ∀ppc. ∀ppc_ok.
    30   ∀i.
    31     fetch_pseudo_instruction instr_list ppc ppc_ok = i →
    32       instruction_has_label id (\fst i) →
    33         occurs_exactly_once ASMTag pseudo_instruction id instr_list.
    343
    354lemma short_jump_cond_ok:
  • src/ASM/Status.ma

    r2119 r2123  
    11451145qed.
    11461146
     1147definition is_well_labelled_p ≝
     1148  λinstr_list.
     1149  ∀id: Identifier.
     1150  ∀ppc. ∀ppc_ok.
     1151  ∀i.
     1152    fetch_pseudo_instruction instr_list ppc ppc_ok = i →
     1153      instruction_has_label id (\fst i) →
     1154        occurs_exactly_once ASMTag pseudo_instruction id instr_list.
     1155
    11471156definition address_of_word_labels_code_mem ≝
    11481157  λcode_mem : list labelled_instruction.
  • src/ASM/Util.ma

    r2111 r2123  
    14941494coercion not_neq_None : ∀A.∀a : option A.∀prf : ¬a≠None ?.a = None ? ≝
    14951495  not_neq_None_to_eq on _prf : ¬?≠None ? to ? = None ?.
     1496 
     1497lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.
     1498  #a #b / by refl/
     1499qed.
     1500
     1501lemma nth_last: ∀A,a,l.
     1502  nth (|l|) A l a = a.
     1503 #A #a #l elim l
     1504 [ / by /
     1505 | #h #t #Hind whd in match (nth ????); whd in match (tail ??); @Hind
     1506 ]
     1507qed.
     1508
     1509
     1510lemma minus_zero_to_le: ∀n,m:ℕ.n - m = 0 → n ≤ m.
     1511 #n
     1512 elim n
     1513 [ #m #_ @le_O_n
     1514 | #n' #Hind #m cases m
     1515   [ #H -n whd in match (minus ??) in H; >H @le_n
     1516   | #m' -m #H whd in match (minus ??) in H; @le_S_S @Hind @H
     1517   ]
     1518 ]
     1519qed.
     1520
     1521lemma plus_zero_zero: ∀n,m:ℕ.n + m = 0 → m = 0.
     1522 #n #m #Hn @sym_eq @le_n_O_to_eq <Hn >commutative_plus @le_plus_n_r
     1523qed.
     1524
     1525(* this can probably be done more simply somewhere *)
     1526lemma not_true_is_false:
     1527  ∀b:bool.b ≠ true → b = false.
     1528 #b cases b
     1529 [ #H @⊥ @(absurd ?? H) @refl
     1530 | #H @refl
     1531 ]
     1532qed.
Note: See TracChangeset for help on using the changeset viewer.