Changeset 2165


Ignore:
Timestamp:
Jul 7, 2012, 3:23:57 AM (5 years ago)
Author:
sacerdot
Message:

Only three daemons left.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Test.ma

    r2164 r2165  
    467467qed.
    468468
     469lemma external_ram_status_of_pseudo_status:
     470 ∀M,cm,s,sigma,policy.
     471  external_ram …
     472   (code_memory_of_pseudo_assembly_program cm sigma policy)
     473   (status_of_pseudo_status M cm s sigma policy) =
     474  external_ram … cm s.
     475 //
     476qed.
     477
     478lemma set_external_ram_status_of_pseudo_status:
     479  ∀M,cm,ps,sigma,policy,ram.
     480    set_external_ram …
     481      (code_memory_of_pseudo_assembly_program cm sigma policy)
     482      (status_of_pseudo_status M cm ps sigma policy)
     483      ram =
     484    status_of_pseudo_status M cm (set_external_ram … cm ps ram) sigma policy.
     485  //
     486qed.
     487
    469488definition map_address_mode_using_internal_pseudo_address_map_ok ≝
    470489 λM,sigma,cm.λs:PreStatus ? cm.λaddr,v,v'.
     
    482501     let register ≝ get_register ?? s [[ false; false; i ]] in
    483502     map_internal_ram_address_using_pseudo_address_map M sigma register v = v'
     503  | EXT_INDIRECT e ⇒
     504     assoc_list_lookup ??
     505      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None … ∧
     506     v = v'
    484507  | _ ⇒ v = v'].
    485508
     
    624647      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
    625648      >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
    626       [
     649      [ cases daemon (*CSC*)
    627650      | >(insert_low_internal_ram_status_of_pseudo_status … v) // <EQ2
    628651        @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % ]
    629 qed.
     652  |5: * #EQ1 #EQ2 <EQ2 >get_register_status_of_pseudo_status
     653      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
     654      >EQ1 normalize nodelta
     655      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status
     656  |6: #EQ <EQ cases daemon (*CSC*)
     657  |7: #EQ <EQ @set_8051_sfr_status_of_pseudo_status cases daemon (*CSC*)
     658  |8: #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
     659  |9: #EQ <EQ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status
     660      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ]
     661qed.
Note: See TracChangeset for help on using the changeset viewer.