Changeset 838


Ignore:
Timestamp:
May 25, 2011, 12:08:24 PM (8 years ago)
Author:
sacerdot
Message:

Restored.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r835 r838  
    1111  ].
    1212
    13 (*
     13axiom sigma: pseudo_assembly_program → Word → Word.
     14
    1415definition assembly_specification:
    15   ∀sigma: Word → Word. ∀assembly_program: pseudo_assembly_program.
     16  ∀assembly_program: pseudo_assembly_program.
    1617  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
    17   λsigma.
    1818  λpseudo_assembly_program.
    1919  λcode_mem.
     
    2121      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
    2222      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
    23       let address_of ≝ ? in
    24       let labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x) in
    25       let datalabels ≝ λx. sigma (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
    26       let pre_assembled ≝ assembly_1_pseudoinstruction labels datalabels address_of 〈None ?, pre_instr〉 in
    27         encoding_check code_mem pc (sigma pre_new_pc) pre_assembled.
    28       cases not_implemented
    29 qed.
     23      let labels ≝ λx. sigma pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
     24      let datalabels ≝ λx. sigma pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
     25      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
     26       (sigma pseudo_assembly_program pc) labels datalabels pre_instr in
     27      match pre_assembled with
     28       [ None ⇒ True
     29       | Some pc_code ⇒
     30          let 〈new_pc,code〉 ≝ pc_code in
     31           encoding_check code_mem pc (sigma pseudo_assembly_program pre_new_pc) code ].
    3032
    3133axiom assembly_meets_specification:
     
    3537    | Some code_mem_cost ⇒
    3638      let 〈code_mem, cost〉 ≝ code_mem_cost in
    37         assembly_specification ? pseudo_assembly_program (load_code_memory code_mem)
     39        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
    3840    ].
    39 cases not_implemented (*
     41(*
    4042  # PROGRAM
    4143  [ cases PROGRAM
     
    5557  | cases not_implemented
    5658  ] *)
    57 qed.
    58 *)
    59 
    60 axiom sigma: pseudo_assembly_program → Word → Word.
    61 
    62 (*
     59
    6360definition status_of_pseudo_status: PseudoStatus → option Status ≝
    6461 λps.
     
    8178           (p3_latch … ps)
    8279           (clock … ps)) ].
    83 *)
    84 
     80           
    8581(* RUSSEL **)
    8682
Note: See TracChangeset for help on using the changeset viewer.