Changeset 827


Ignore:
Timestamp:
May 24, 2011, 1:26:43 PM (8 years ago)
Author:
sacerdot
Message:

The preamble is now part of the PseudoStatus?.

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r826 r827  
    2828qed.
    2929
    30 theorem assembly_meets_specification:
     30axiom assembly_meets_specification:
    3131  ∀pseudo_assembly_program.
    3232    match assembly pseudo_assembly_program with
     
    3636        assembly_specification ? pseudo_assembly_program (load_code_memory code_mem)
    3737    ].
     38cases not_implemented (*
    3839  # PROGRAM
    3940  [ cases PROGRAM
     
    5253    ]
    5354  | cases not_implemented
    54   ]
     55  ] *)
     56qed.
     57
     58definition status_of_pseudo_status: PseudoStatus → option Status ≝
     59 λps.
     60  match assembly (code_memory ? ps) with
     61   [ None ⇒ None …
     62   | Some p ⇒
     63      let cm ≝ load_code_memory (\fst p) in
     64      let pc ≝ ? in
     65       Some …
     66        (mk_PreStatus (BitVectorTrie Byte 16)
     67          cm
     68          (low_internal_ram … ps)
     69          (high_internal_ram … ps)
     70          (external_ram … ps)
     71          pc
     72          (special_function_registers_8051 … ps)
     73          (special_function_registers_8052 … ps)
     74          (p1_latch … ps)
     75          (p3_latch … ps)
     76          (clock … ps)) ].
     77
     78lemma foo:
     79 ∀ticks_of.
     80 ∀ps: PseudoStatus.
     81  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
     82  let s'' ≝ status_of_pseudo_status ps' in
     83  let s ≝ status_of_pseudo_status ps in
     84  let s' ≝ execute_1 s in
     85   s = s''.
  • src/ASM/Interpret.ma

    r825 r827  
    675675  λps: PseudoStatus.
    676676  λid: Identifier.
    677     address_of_word_labels_code_mem (code_memory ? ps) id.
     677    address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.
    678678
    679679definition execute_1_pseudo_instruction: (Word → nat) → PseudoStatus → PseudoStatus ≝
    680680  λticks_of.
    681681  λs.
    682   let 〈instr, pc〉 ≝ fetch_pseudo_instruction (code_memory ? s) (program_counter ? s) in
     682  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
    683683  let ticks ≝ ticks_of (program_counter ? s) in
    684684  let s ≝ set_clock ? s (clock ? s + ticks) in
  • src/ASM/Status.ma

    r821 r827  
    104104
    105105definition Status ≝ PreStatus (BitVectorTrie Byte 16).
    106 definition PseudoStatus ≝ PreStatus (list labelled_instruction).
     106definition PseudoStatus ≝ PreStatus (pseudo_assembly_program).
    107107
    108108lemma sfr8051_index_19:
Note: See TracChangeset for help on using the changeset viewer.