Changeset 911


Ignore:
Timestamp:
Jun 9, 2011, 10:38:21 AM (8 years ago)
Author:
sacerdot
Message:

Type of set_code_memory generalized.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r909 r911  
    15231523qed.
    15241524*)
     1525
     1526axiom execute_1_pseudo_instruction_preserves_code_memory:
     1527 ∀ticks_of,ps.
     1528  code_memory … (execute_1_pseudo_instruction ticks_of ps) = code_memory … ps.
     1529
    15251530(*
    15261531lemma execute_code_memory_unchanged:
     
    15761581  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
    15771582  let s' ≝ execute_1 s in
    1578    s = s'']].
     1583   s' = s'']].
    15791584 #ticks_of #ps
    1580  whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     1585 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ λ_.%])
     1586 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ λ_.match % with [ _ ⇒ ? | _ ⇒ ? ]])
     1587 >execute_1_pseudo_instruction_preserves_code_memory
    15811588 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
     1589 change with (? (set_code_memory ?? ps (load_code_memory (\fst 〈cm,costs〉))) = ?)
    15821590 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
    15831591 generalize in match (sig2 … (execute_1_pseudo_instruction' ticks_of ps))
  • src/ASM/Status.ma

    r843 r911  
    305305               
    306306definition set_code_memory ≝
    307   λM: Type[0].
    308   λs: PreStatus M.
    309   λr: M.
     307  λM,M': Type[0].
     308  λs: PreStatus M.
     309  λr: M'.
    310310    let old_low_internal_ram ≝ low_internal_ram ? s in
    311311    let old_high_internal_ram ≝ high_internal_ram ? s in
     
    317317    let old_p3_latch ≝ p3_latch ? s in
    318318    let old_clock ≝ clock ? s in
    319       mk_PreStatus M r
     319      mk_PreStatus M' r
    320320                old_low_internal_ram
    321321                old_high_internal_ram
     
    10761076 λl.
    10771077 λstatus.
    1078    set_code_memory ? status (load_code_memory l).
     1078   set_code_memory (BitVectorTrie Word 16) ? status (load_code_memory l).
    10791079
    10801080definition fetch_pseudo_instruction: list labelled_instruction → Word → (pseudo_instruction × Word) ≝
Note: See TracChangeset for help on using the changeset viewer.