Changeset 3075


Ignore:
Timestamp:
Apr 2, 2013, 7:59:07 PM (4 years ago)
Author:
mckinna
Message:

Apologies for late folding in of old changes which were left over from earlier partial commits; hopefully no clash with paolo's recent commits

Cleaned up treatment of get_*_flag from SFR_PSW

Streamlined lots of typechecking constraints in favour of \ldots/?

Removed daemons by proving many of the clock_set_* lemmas, mostly Russell-style; but should these be moved to StatusProofs?*.ma?

Further streamlining possible: lots of vsplit 1 7 redundancy when dealing with the internal_memory space of the processor.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r3066 r3075  
    33(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    44
     5include "basics/russell.ma".
     6
    57include "ASM/ASM.ma". (* includes "ASM/BitVectorTrie.ma".*)
    68include "ASM/Arithmetic.ma".
    7 (*include "ASM/BitVectorTrie.ma".*)
    8 include "basics/russell.ma".
    99
    1010definition Time ≝ nat.
     
    251251qed.
    252252
     253lemma clock_set_8051_sfr:
     254    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀i,b.
     255        clock … code_memory s = clock … code_memory (set_8051_sfr M code_memory s i b).
     256  #M #code_memory #s #i #b //
     257qed.
     258
    253259definition set_8052_sfr ≝
    254260  λM: Type[0].
     
    282288qed.
    283289
     290lemma clock_set_8052_sfr:
     291    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀i,b.
     292        clock … code_memory s = clock … code_memory (set_8052_sfr M code_memory s i b).
     293  #M #code_memory #s #i #b //
     294qed.
     295
    284296definition set_program_counter ≝
    285297  λM: Type[0].
     
    355367                old_clock.
    356368               
     369definition update_low_internal_ram ≝
     370  λM: Type[0].
     371  λcode_memory:M.
     372  λs: PreStatus M code_memory.
     373  λaddr,v.
     374  let old_low_internal_ram ≝ low_internal_ram ?? s in
     375  let new_low_internal_ram ≝ insert ?? addr v old_low_internal_ram in
     376      set_low_internal_ram … s new_low_internal_ram.
     377           
     378lemma clock_set_low_internal_ram:
     379    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀r.
     380        clock … code_memory s = clock … code_memory (set_low_internal_ram M code_memory s r).
     381  #M #code_memory #s #r //
     382qed.
     383
     384lemma clock_update_low_internal_ram:
     385    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀addr,v.
     386        clock … code_memory s = clock … code_memory (update_low_internal_ram M code_memory s addr v).
     387  #M #code_memory #s #addr #v //
     388qed.
     389
    357390definition set_high_internal_ram ≝
    358391  λM: Type[0].
     
    380413                old_clock.
    381414               
     415definition update_high_internal_ram ≝
     416  λM: Type[0].
     417  λcode_memory:M.
     418  λs: PreStatus M code_memory.
     419  λaddr,v.
     420  let old_high_internal_ram ≝ high_internal_ram ?? s in
     421  let new_high_internal_ram ≝ insert ?? addr v old_high_internal_ram in
     422      set_high_internal_ram … s new_high_internal_ram.
     423
     424lemma clock_set_high_internal_ram:
     425    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀r: BitVectorTrie Byte 7.
     426        clock … code_memory s = clock … code_memory (set_high_internal_ram M code_memory s r).
     427  #M #code_memory #s #r //
     428qed.
     429
     430lemma clock_update_high_internal_ram:
     431    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀addr,v.
     432        clock … code_memory s = clock … code_memory (update_high_internal_ram M code_memory s addr v).
     433  #M #code_memory #s #addr #v //
     434qed.
     435
    382436definition set_external_ram ≝
    383437  λM: Type[0].
     
    404458                old_clock.
    405459               
     460definition update_external_ram ≝
     461  λM: Type[0].
     462  λcode_memory:M.
     463  λs: PreStatus M code_memory.
     464  λaddr,v.
     465  let old_external_ram ≝ external_ram ?? s in
     466  let new_external_ram ≝ insert ?? addr v old_external_ram in
     467      set_external_ram … s new_external_ram.
     468
     469lemma clock_set_external_ram:
     470    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀r: BitVectorTrie Byte 16.
     471        clock … code_memory s = clock … code_memory (set_external_ram M code_memory s r).
     472  #M #code_memory #s #r //
     473qed.
     474
     475lemma clock_update_external_ram:
     476    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀addr: Word. ∀v: Byte.
     477        clock … code_memory s = clock … code_memory (update_external_ram M code_memory s addr v).
     478  #M #code_memory #s #addr #v //
     479qed.
     480
     481definition get_psw_flags ≝
     482  λM: Type[0].
     483  λcode_memory:M.
     484  λs: PreStatus M code_memory.
     485  λflag.
     486  λflag_ok: flag < ?.       
     487    let psw ≝ get_8051_sfr … s SFR_PSW in
     488      get_index_v bool ? psw flag flag_ok.
     489               
    406490definition get_cy_flag ≝
    407491  λM: Type[0].
    408492  λcode_memory:M.
    409493  λs: PreStatus M code_memory.
    410     let sfr ≝ special_function_registers_8051 ?? s in
    411     let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    412       get_index_v bool 8 psw O ?.
    413     normalize
    414     @ (le_S_S ? ?)
    415     [ @ le_O_n
    416     | repeat (@ (le_S_S));
    417       //
    418     ]
     494    get_psw_flags … s 0 ?. //
    419495qed.
    420496
     
    423499  λcode_memory:M.
    424500  λs: PreStatus M code_memory.
    425     let sfr ≝ special_function_registers_8051 ?? s in
    426     let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    427       get_index_v bool 8 psw 1 ?.
    428     normalize
    429     repeat (@ (le_S_S ? ?))
    430     @ le_O_n
     501    get_psw_flags … s 1 ?. //
    431502qed.
    432503
     
    435506  λcode_memory:M.
    436507  λs: PreStatus M code_memory.
    437     let sfr ≝ special_function_registers_8051 ?? s in
    438     let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    439       get_index_v bool 8 psw 2 ?.
    440     normalize
    441     repeat (@ (le_S_S ? ?))
    442     @ le_O_n
     508    get_psw_flags … s 2 ?. //
    443509qed.
    444510
     
    447513  λcode_memory:M.
    448514  λs: PreStatus M code_memory.
    449     let sfr ≝ special_function_registers_8051 ?? s in
    450     let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    451       get_index_v bool 8 psw 3 ?.
    452     normalize
    453     repeat (@ (le_S_S ? ?))
    454     @ le_O_n
     515    get_psw_flags … s 3 ?. //
    455516qed.
    456517
     
    459520  λcode_memory:M.
    460521  λs: PreStatus M code_memory.
    461     let sfr ≝ special_function_registers_8051 ?? s in
    462     let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    463       get_index_v bool 8 psw 4 ?.
    464     normalize
    465     repeat (@ (le_S_S ? ?))
    466     @ le_O_n
     522    get_psw_flags … s 4 ?. //
    467523qed.
    468524
     
    471527  λcode_memory:M.
    472528  λs: PreStatus M code_memory.
    473     let sfr ≝ special_function_registers_8051 ?? s in
    474     let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    475       get_index_v bool 8 psw 5 ?.
    476     normalize
    477     repeat (@ (le_S_S ? ?))
    478     @ le_O_n
     529    get_psw_flags … s 5 ?. //
    479530qed.
    480531
     
    483534  λcode_memory:M.
    484535  λs: PreStatus M code_memory.
    485     let sfr ≝ special_function_registers_8051 ?? s in
    486     let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    487       get_index_v bool 8 psw 6 ?.
    488     normalize
    489     repeat (@ (le_S_S ? ?))
    490     @ le_O_n
     536    get_psw_flags … s 6 ?. //
    491537qed.
    492538
     
    495541  λcode_memory:M.
    496542  λs: PreStatus M code_memory.
    497     let sfr ≝ special_function_registers_8051 ?? s in
    498     let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    499       get_index_v bool 8 psw 7 ?.
    500     normalize
    501     repeat (@ (le_S_S ? ?))
    502     @ le_O_n
     543    get_psw_flags … s 7 ?. //
    503544qed.
    504545
     
    510551  λac: option Bit.
    511552  λov: Bit.
    512     let sfr_psw ≝ get_8051_sfr ?? s SFR_PSW in
    513     let old_cy ≝ get_index_v ?? sfr_psw O ? in
    514     let old_ac ≝ get_index_v ?? sfr_psw 1 ? in
    515     let old_fo ≝ get_index_v ?? sfr_psw 2 ? in
    516     let old_rs1 ≝ get_index_v ?? sfr_psw 3 ? in
    517     let old_rs0 ≝ get_index_v ?? sfr_psw 4 ? in
    518     let old_ov ≝ get_index_v ?? sfr_psw 5 ? in
    519     let old_ud ≝ get_index_v ?? sfr_psw 6 ? in
    520     let old_p ≝ get_index_v ?? sfr_psw 7 ? in
     553    (*let sfr_psw ≝ get_8051_sfr ?? s SFR_PSW in *)
     554    let old_cy ≝ get_cy_flag ?? s (* get_index_v ?? sfr_psw O ?*) in
     555    let old_ac ≝ get_ac_flag ?? s (* get_index_v ?? sfr_psw 1 ?*) in
     556    let old_fo ≝ get_fo_flag ?? s (* get_index_v ?? sfr_psw 2 ?*) in
     557    let old_rs1 ≝ get_rs1_flag ?? s (* get_index_v ?? sfr_psw 3 ?*) in
     558    let old_rs0 ≝ get_rs0_flag ?? s (* get_index_v ?? sfr_psw 4 ?*) in
     559    let old_ov ≝ get_ov_flag ?? s (* get_index_v ?? sfr_psw 5 ?*) in
     560    let old_ud ≝ get_ud_flag ?? s (* get_index_v ?? sfr_psw 6 ?*) in
     561    let old_p ≝ get_p_flag ?? s (* get_index_v ?? sfr_psw 7 ?*) in
    521562    let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in
    522563      set_8051_sfr ?? s SFR_PSW
    523564      [[ cy ; new_ac ; old_fo ; old_rs1 ;
    524565         old_rs0 ; ov ; old_ud ; old_p ]].
    525     [1,2,3,4,5,6,7,8:
    526        normalize
    527        repeat (@ le_S_S)
    528        @ le_O_n
    529     ]
    530 qed.
    531566
    532567definition initialise_status ≝
    533568  λM: Type[0].
    534569  λcode_mem: M.
    535   let status ≝ mk_PreStatus M code_mem                    (* Code mem. *)
    536                          (Stub Byte 7)                      (* Low mem.  *)
    537                          (Stub Byte 7)                      (* High mem. *)
    538                          (Stub Byte 16)                    (* Ext mem.  *)
    539                          (zero 16)                         (* PC.       *)
    540                          (replicate Byte 19 (zero 8)) (* 8051 SFR. *)
    541                          (replicate Byte 5 (zero 8))     (* 8052 SFR. *)
    542                          (zero 8)                           (* P1 latch. *)
    543                          (zero 8)                           (* P3 latch. *)
    544                          O                                      (* Clock.    *)
     570  let status ≝ mk_PreStatus M code_mem                 (* Code mem. *)
     571                         (Stub )                      (* Low mem.  *)
     572                         (Stub )                      (* High mem. *)
     573                         (Stub …)                      (* Ext mem.  *)
     574                         (zero ?)                      (* PC.       *)
     575                         (replicate … (zero ?))        (* 8051 SFR. *)
     576                         (replicate … (zero ?))        (* 8052 SFR. *)
     577                         (zero ?)                      (* P1 latch. *)
     578                         (zero ?)                      (* P3 latch. *)
     579                         O                             (* Clock.    *)
    545580  in
    546     set_8051_sfr ?? status SFR_SP (bitvector_of_nat 8 7).
     581    set_8051_sfr ?? status SFR_SP (bitvector_of_nat ? 7).
    547582 
    548 
    549583definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝
    550584  λb: Byte.
     
    634668  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
    635669  cases (sfr_of_Byte ?)
    636   [1:
     670  [1: 
    637671    normalize nodelta cases not_implemented
    638   |2:
    639     * * normalize nodelta %
     672  |2: 
     673    * * %
    640674  ]
    641675qed.
     
    661695    let c ≝ get_index_v … r 1 ? in
    662696    let d ≝ get_index_v … r 2 ? in
     697(* JHM: redundant bit-twiddling, once you have get_*_flag helpers
    663698    let 〈 un, ln 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
    664     let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in
     699    let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in
     700*)
     701    let r1 ≝ get_rs1_flag ?? s in
     702    let r0 ≝ get_rs0_flag ?? s in
    665703    let offset ≝
    666704      if ¬r1 ∧ ¬r0 then
     
    674712    in
    675713      bitvector_of_nat 7 (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
    676   [1,2,3,4,5:
    677     normalize
    678     repeat (@ le_S_S)
    679     @ le_O_n;
    680   ]
     714  //
    681715qed.
    682716
     
    687721  λr: BitVector 3.
    688722    let address ≝ bit_address_of_register … s r in
    689       lookup ?? address (low_internal_ram … s) (zero 8).
    690      
     723      lookup ?? address (low_internal_ram … s) (zero ?).
     724
    691725definition set_register ≝
    692726  λM: Type[0].
     
    696730  λv: Byte.
    697731    let address ≝ bit_address_of_register … s r in
     732    (*     
    698733    let old_low_internal_ram ≝ low_internal_ram ?? s in
    699734    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
    700735      set_low_internal_ram … s new_low_internal_ram.
     736    *)
     737    update_low_internal_ram … s address v.
    701738     
    702 definition read_from_internal_ram ≝
     739definition read_from_external_ram ≝
     740  λM: Type[0].
     741  λcode_memory:M.
     742  λs: PreStatus M code_memory.
     743  λaddr: Word.
     744    lookup ?? addr (external_ram … s) (zero ?).
     745
     746definition read_from_internal_ram ≝ (* JHM: lots of 7bits+HI/Lo vs. 8bit redundancy throughout *)
    703747  λM: Type[0].
    704748  λcode_memory:M.
     
    712756        (low_internal_ram ?? s)
    713757    in
    714       lookup … seven_bits memory (zero 8).
     758      lookup … seven_bits memory (zero ?).
    715759
    716760definition read_at_stack_pointer ≝
     
    718762  λcode_memory:M.
    719763  λs: PreStatus M code_memory.
    720     read_from_internal_ram M code_memory s (get_8051_sfr ?? s SFR_SP).
     764    read_from_internal_ram s (get_8051_sfr ?? s SFR_SP).
    721765
    722766definition write_at_stack_pointer ≝
     
    726770  λv: Byte.
    727771    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr ?? s SFR_SP) in
    728       if head' … 0 bit_one then
     772      if head' … bit_one then
     773      (*
    729774        let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
    730775          set_high_internal_ram ?? s memory
     776      *)
     777        update_high_internal_ram … s seven_bits v
    731778      else
     779      (*
    732780        let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
    733781          set_low_internal_ram ?? s memory.
     782      *)
     783        update_low_internal_ram … s seven_bits v.
    734784
    735785definition set_arg_16': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → Σs':PreStatus M code_memory. clock ?? s = clock ?? s' ≝
     
    763813      | ACC_DPTR ⇒ λ_:True.
    764814        let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
    765         let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
     815        let big_acc ≝ (zero ?) @@ (get_8051_sfr … s SFR_ACC_A) in
    766816        add … big_acc dptr
    767817      | _ ⇒ Ⓧ
     
    784834        λext_indirect_dptr: True.
    785835          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
    786             lookup ? 16 address (external_ram ?? s) (zero 8)
     836            read_from_external_ram … s address
    787837      | EXT_INDIRECT e ⇒
    788838        λext_indirect: True.
    789839          let address ≝ get_register ?? s [[ false; false; e ]]  in
    790           let padded_address ≝ pad 8 8 address in
    791             lookup ? 16 padded_address (external_ram ?? s) (zero 8)
     840          let padded_address ≝ pad 8 ? address in
     841            read_from_external_ram … s padded_address
    792842      | ACC_DPTR ⇒
    793843        λacc_dptr: True.
    794844          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
    795           let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
     845          let padded_acc ≝ pad 8 ? (get_8051_sfr ?? s SFR_ACC_A) in
    796846          let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
    797             lookup ? 16 address (external_ram ?? s) (zero 8)
     847            read_from_external_ram … s address
    798848      | ACC_PC ⇒
    799849        λacc_pc: True.
    800           let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
     850          let padded_acc ≝ pad 8 ? (get_8051_sfr ?? s SFR_ACC_A) in
    801851          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
    802             lookup ? 16 address (external_ram ?? s) (zero 8)
    803       | DIRECT d ⇒
     852            read_from_external_ram … s address
     853      | DIRECT d ⇒ (* JHM: simplify false branch with read_from_internal_ram *)
    804854        λdirect: True.
    805855          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
    806856            match head' … hd with
    807857            [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
    808             | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
     858             (* XXX: get_bit_addressable_sfr m cm s d l *)
     859            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero ?)
     860             (* XXX: read_from_internal_ram … s d *)
    809861            ]
    810       | INDIRECT i ⇒
     862      | INDIRECT i ⇒ (* JHM: simplify completely with read_from_internal_ram *)
    811863        λindirect: True.
    812864          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
    813865            match head' … hd with
    814             [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero )
    815             | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero )
     866            [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero ?)
     867            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero ?)
    816868            ]
     869          (* XXX: read_from_internal_ram … s (get_register … s [[false;false;i]]) *)
    817870      | _ ⇒ λother.
    818871        match other in False with [ ]
     
    828881                   PreStatus m cm
    829882            with
    830       [ DIRECT d ⇒
     883      [ DIRECT d ⇒ (* JHM: should simplify false branch with update_internal_ram *)
    831884        λdirect: True.
    832885          let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
    833886            match head' … bit_one with
    834887              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
    835               | false ⇒
    836                 let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
    837                   set_low_internal_ram ?? s memory
     888              | false ⇒ update_low_internal_ram … s seven_bits v
     889                (*let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
     890                  set_low_internal_ram ?? s memory*)
    838891              ]
    839       | INDIRECT i ⇒
     892      | INDIRECT i ⇒ (* JHM: should simplify completely with update_internal_ram *)
    840893        λindirect: True.
    841894          let register ≝ get_register ?? s [[ false; false; i ]] in
    842895          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
    843896            match head' … bit_one with
    844               [ false ⇒
    845                 let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
    846                   set_low_internal_ram ?? s memory
    847               | true ⇒
    848                 let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
    849                   set_high_internal_ram ?? s memory
     897              [ false ⇒ update_low_internal_ram … s seven_bits v
     898                (*let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
     899                  set_low_internal_ram ?? s memory*)
     900              | true ⇒ update_high_internal_ram … s seven_bits v
     901                (*let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
     902                  set_high_internal_ram ?? s memory*)
    850903              ]
    851904      | REGISTER r ⇒ λregister: True. set_register ?? s r v
     
    856909          let address ≝ get_register ?? s [[ false; false; e ]] in
    857910          let padded_address ≝ pad 8 8 address in
    858           let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
     911          (*
     912          let memory ≝ insert ?? padded_address v (external_ram ?? s) in
    859913            set_external_ram ?? s memory
     914          *)
     915          update_external_ram … s padded_address v
    860916      | EXT_INDIRECT_DPTR ⇒
    861917        λext_indirect_dptr: True.
    862918          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
    863           let memory ≝ insert ? 16 address v (external_ram ?? s) in
     919          (*
     920          let memory ≝ insert ?? address v (external_ram ?? s) in
    864921            set_external_ram ?? s memory
     922          *)
     923          update_external_ram … s address v
    865924      | _ ⇒
    866925        λother: False.
     
    868927      ] (subaddressing_modein … a).
    869928
    870 lemma clock_set_arg_8: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v).
    871   cases daemon
    872 qed.
    873 
     929lemma clock_set_arg_8: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v) ≝
     930  λm, cm, s, a, v.
     931    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
     932                                                acc_a ; acc_b ; ext_indirect ;
     933                                                ext_indirect_dptr ]] x) →
     934                   clock … cm s = clock … cm (set_arg_8 … s x v)
     935            with
     936      [ DIRECT d ⇒ (* JHM: should simplify false branch with update_internal_ram *)
     937        λdirect: True.
     938          let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
     939            match head' … bit_one with
     940              [ true ⇒ ?
     941              | false ⇒ ?
     942              ]
     943      | INDIRECT i ⇒ (* JHM: should simplify completely with update_internal_ram *)
     944        λindirect: True.
     945          let register ≝ get_register ?? s [[ false; false; i ]] in
     946          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
     947            match head' … bit_one with
     948              [ false ⇒ ?
     949              | true ⇒ ?
     950              ]
     951      | REGISTER r ⇒ λregister: True. ?
     952      | ACC_A ⇒ λacc_a: True. ?
     953      | ACC_B ⇒ λacc_b: True. ?
     954      | EXT_INDIRECT e ⇒
     955        λext_indirect: True.
     956          let address ≝ get_register ?? s [[ false; false; e ]] in
     957          let padded_address ≝ pad 8 8 address in
     958            ?
     959      | EXT_INDIRECT_DPTR ⇒
     960        λext_indirect_dptr: True.
     961          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
     962            ?
     963      | _ ⇒
     964        λother: False.
     965          match other in False with [ ]
     966      ] (subaddressing_modein … a).
     967  //
     968  whd in match set_arg_8; normalize nodelta
     969(* XXX: non-Russell way
     970  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
     971    cases x * normalize nodelta
     972  [1: #d #ok cases (vsplit ? 1 7 d) normalize nodelta
     973    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta
     974    [1: @clock_set_bit_addressable_sfr
     975    |2: @clock_update_low_internal_ram
     976    ]
     977  |2: #i #ok cases (vsplit ? 1 7 (get_register ?? s [[ false; false; i ]])) normalize nodelta
     978    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta
     979    [1: @clock_update_high_internal_ram
     980    |2: @clock_update_low_internal_ram
     981    ]
     982  |3: #b1 #ok @clock_update_external_ram
     983  |4: #b3 #ok @clock_update_low_internal_ram
     984  |5,6: #ok @clock_set_8051_sfr
     985  |12: #ok @clock_update_external_ram
     986  ]
     987  cases not_implemented (* JHM: there has to be a better way to deal with the absurd branches *)
     988*)
     989  [1: (* case DIRECT d *)
     990    cases (vsplit ? 1 7 d) normalize nodelta
     991    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta //
     992  |2: (* case DIRECT d; why the repetition? *)
     993    cases (vsplit ? 1 7 d) normalize nodelta
     994    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta //
     995  |3: (* case INDIRECT i *)
     996    cases (vsplit ? 1 7 (get_register ?? s [[ false; false; i ]])) normalize nodelta
     997    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta //
     998   |4: (* case INDIRECT i; why the repetition? *)
     999    cases (vsplit ? 1 7 (get_register ?? s [[ false; false; i ]])) normalize nodelta
     1000    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta //
     1001  ]
     1002qed.
     1003
     1004(* XXX: these --- like those above --- belong in StatusProofs*.ma ??? *)
    8741005lemma program_counter_set_arg_8: ∀M,cm,s,x,v. program_counter M cm s = program_counter … (set_arg_8 M cm s x v).
     1006  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
    8751007  cases daemon
    8761008qed.
     
    9541086        λbit_addr: True.
    9551087        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
     1088        let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
    9561089        match head' … bit_1 with
    9571090        [ true ⇒
    958           let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
    9591091          let trans ≝ true:::four_bits @@ [[false; false; false]] in
    9601092          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
    9611093            get_index_v … sfr (nat_of_bitvector … three_bits) ?
    9621094        | false ⇒
    963           let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
    9641095          let address' ≝ [[true; false; false]]@@four_bits in
    965           let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
     1096          let t ≝ lookup ?? address' (low_internal_ram ?? s) (zero ?) in
    9661097            get_index_v … t (nat_of_bitvector … three_bits) ?
    9671098        ]
     
    9691100        λn_bit_addr: True.
    9701101        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
     1102        let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
    9711103        match head' … bit_1 with
    9721104        [ true ⇒
    973           let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
    9741105          let trans ≝ true:::four_bits @@ [[false; false; false]] in
    9751106          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
    9761107            ¬(get_index_v ?? sfr (nat_of_bitvector … three_bits) ?)
    9771108        | false ⇒
    978           let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
    9791109          let address' ≝ [[true; false; false]]@@four_bits in
    9801110          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
     
    9971127      [ BIT_ADDR b ⇒ λbit_addr: True.
    9981128        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
     1129        let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
    9991130        match head' … bit_1 with
    10001131        [ true ⇒
    1001           let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
    10021132          let trans ≝ true:::four_bits @@ [[false; false; false]] in
    10031133          let sfr ≝ get_bit_addressable_sfr … s trans true in
     
    10051135            set_bit_addressable_sfr … s new_sfr trans
    10061136        | false ⇒
    1007           let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
    10081137          let address' ≝ [[true; false; false]]@@four_bits in
    1009           let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
     1138          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero ?) in
    10101139          let n_bit ≝ set_index … t (nat_of_bitvector … three_bits) v ? in
    1011           let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
     1140          (*
     1141          let memory ≝ insert ?? address' n_bit (low_internal_ram ?? s) in
    10121142            set_low_internal_ram … s memory
     1143          *)
     1144            update_low_internal_ram … s address' n_bit
    10131145        ]
    10141146      | CARRY ⇒
     
    10251157qed.
    10261158
    1027 lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v).
    1028   cases daemon
    1029 qed.
     1159(* JHM: Russell-style works, modulo some oddities...??? *)
     1160lemma clock_set_arg_1: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v)
     1161  ≝
     1162  λm: Type[0].
     1163  λcm.
     1164  λs: PreStatus m cm.
     1165  λa: [[bit_addr; carry]].
     1166  λv: Bit.     
     1167    match a
     1168    return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) →
     1169     clock m cm s = clock … (set_arg_1 m cm s x v)
     1170    with
     1171      [ BIT_ADDR b ⇒ λbit_addr: True.
     1172        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
     1173        let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     1174        match head' … bit_1 with
     1175        [ true ⇒
     1176          let trans ≝ true:::four_bits @@ [[false; false; false]] in
     1177          let sfr ≝ get_bit_addressable_sfr … s trans true in
     1178          let new_sfr ≝ set_index … sfr (nat_of_bitvector … three_bits) v ? in
     1179            ?
     1180        | false ⇒
     1181          let address' ≝ [[true; false; false]]@@four_bits in
     1182          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
     1183          let n_bit ≝ set_index … t (nat_of_bitvector … three_bits) v ? in
     1184            ?
     1185        ]
     1186      | CARRY ⇒
     1187        λcarry: True.
     1188        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
     1189        let new_psw ≝ v:::seven_bits in
     1190          ?
     1191      | _ ⇒
     1192        λother: False.
     1193          match other in False with
     1194            [ ]
     1195      ] (subaddressing_modein … a). //
     1196      whd in match set_arg_1; normalize nodelta     
     1197  [1: (* case: CARRY *)
     1198    cases (vsplit bool 1 7 (get_8051_sfr … s SFR_PSW))
     1199    #ignore #seven_bits normalize nodelta @clock_set_8051_sfr
     1200  |2: (* case: BIT_ADDR *)
     1201    cases (vsplit bool 1 7 b)
     1202    #bit_1 #seven_bits normalize nodelta cases (vsplit bool 4 3 seven_bits)
     1203    #four_bits #three_bits normalize nodelta cases (head' … bit_1)
     1204    [1: @clock_set_bit_addressable_sfr
     1205    |2: @clock_update_low_internal_ram
     1206    ]
     1207  |3: (* case: BIT_ADDR, again; why? *)
     1208    cases (vsplit bool 1 7 b)
     1209    #bit_1 #seven_bits normalize nodelta cases (vsplit bool 4 3 seven_bits)
     1210    #four_bits #three_bits normalize nodelta cases (head' … bit_1)
     1211    [1: @clock_set_bit_addressable_sfr
     1212    |2: @clock_update_low_internal_ram
     1213    ]
     1214  ]
     1215qed.
     1216
     1217lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v).
     1218(* JHM: boring, non-Russell way
     1219  #m #cm #s #x #v whd in match set_arg_1;
     1220  cases x * normalize nodelta
     1221  [14: #ok cases (vsplit bool 1 7 (get_8051_sfr … s SFR_PSW))
     1222    #ignore #seven_bits @clock_set_8051_sfr
     1223  |15: #b #ok cases (vsplit bool 1 7 b)
     1224    #bit_1 #seven_bits normalize nodelta cases (vsplit bool 4 3 seven_bits)
     1225    #four_bits #three_bits normalize nodelta cases (head' … bit_1)
     1226    [1: @clock_set_bit_addressable_sfr
     1227    |2: @clock_set_low_internal_ram
     1228    ]
     1229  ] cases not_implemented (* XXX: there has to be a better way to deal with the absurd branches *)
     1230*)
     1231  @clock_set_arg_1
     1232qed.
     1233
    10301234
    10311235definition construct_datalabels: list (Identifier × Word) →
    10321236  identifier_map ASMTag Word ≝
    10331237  λthe_preamble.
    1034   \fst (foldl ((identifier_map ASMTag Word) × Word) ? (λt,preamble.
     1238  \fst (foldl ?? (λt,preamble.
    10351239      let 〈datalabels, addr〉 ≝ t in
    10361240      let 〈name, size〉 ≝ preamble in
Note: See TracChangeset for help on using the changeset viewer.