Changeset 1014 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 21, 2011, 2:02:37 AM (8 years ago)
Author:
sacerdot
Message:

The main theorem is completely broken (again).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r998 r1014  
    785785definition expand_pseudo_instruction:
    786786 ∀program:pseudo_assembly_program.∀pol: policy program.
    787   ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc,pi.
     787  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
    788788  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
    789789  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
    790   \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
     790  let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
    791791  pc = sigma program pol ppc →
    792792  Σres:list instruction. Some … res = expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi
    793 ≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,pi,prf1,prf2,prf3,prf4.
    794    match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi with
     793≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,prf1,prf2,prf3.
     794   match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) (\fst (fetch_pseudo_instruction (\snd program) ppc)) with
    795795    [ None ⇒ let dummy ≝ [ ] in dummy
    796796    | Some res ⇒ res ].
Note: See TracChangeset for help on using the changeset viewer.