Changeset 420


Ignore:
Timestamp:
Dec 14, 2010, 4:12:43 PM (9 years ago)
Author:
mulligan
Message:

All proof obligations closed.

Location:
Deliverables/D4.1/Matita
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Assembly.ma

    r419 r420  
    405405include "Status.ma".
    406406
    407 ndefinition assembly_jump: ? → (jump ?) → (? → [[relative]]) → instruction ≝
    408   λA: Type[0].
    409   λj: jump A.
    410   λaddr_of: A → [[relative]].
     407ndefinition assembly_jump: (jump String) → (String → [[relative]]) → instruction ≝
     408  λj: jump String.
     409  λaddr_of: String → [[relative]].
    411410    match j with
    412       [ JC jmp ⇒ Jump [[relative]] (JC ? (addr_of jmp))
     411      [ JC jmp ⇒ Jump ? (JC ? (addr_of jmp))
    413412      | JNC jmp ⇒ Jump ? (JNC ? (addr_of jmp))
    414413      | JZ jmp ⇒ Jump ? (JZ ? (addr_of jmp))
     
    419418      | CJNE jmp jmp' ⇒ Jump ? (CJNE ? jmp (addr_of jmp'))
    420419      | DJNZ jmp jmp' ⇒ Jump ? (DJNZ ? jmp (addr_of jmp'))
     420      ]. (*
     421        match jmp return λx. bool_to_Prop (is_in … [[ register; direct ]] x) → ? with
     422          [ DIRECT d ⇒ λdptr: True. Jump ? (DJNZ ? jmp (addr_of jmp'))
     423          | REGISTER r ⇒ λregister:True. Jump ? (DJNZ ? jmp (addr_of jmp'))
     424          | _ ⇒ λother: False. ⊥
     425          ] (subaddressing_modein … jmp)
    421426      ].
     427  nassumption;
     428nqed. *)
    422429
    423430ndefinition address_of: BitVectorTrie (BitVector eight) eight → String → addressing_mode ≝
     
    433440nqed.
    434441
    435 ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie ? sixteen)) ≝
     442ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
    436443  λp.
    437444    let 〈preamble, instr_list〉 ≝ p in
    438445    let 〈datalabels, ignore〉 ≝
    439       fold_left ? ? (
     446      fold_left ((BitVectorTrie (BitVector sixteen) sixteen) × Nat) ? (
    440447        λt. λpreamble.
    441448          let 〈datalabels, addr〉 ≝ t in
     
    445452              〈(Stub ? ?), Z〉 preamble in
    446453    let 〈pc_labels, costs〉 ≝
    447       fold_left ? ? (
     454      fold_left ((Nat × (BitVectorTrie ? ?)) × (BitVectorTrie ? ?)) ? (
    448455        λt. λi.
    449456          let 〈pc_labels, costs〉 ≝ t in
     
    469476              | WithLabel jmp ⇒
    470477                let fake_addr ≝ RELATIVE (zero eight) in
    471                 let fake_jump ≝ assembly_jump ? jmp (λx. fake_addr) in
     478                let fake_jump ≝ assembly_jump jmp (λx: String. fake_addr) in
    472479                let code_memory ≝ load_code_memory (assembly1 fake_jump) in
    473480                let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in
    474481                let 〈instr', program_counter'〉 ≝ instr_pc' in
    475                 let program_counter_n' ≝ nat_of_bitvector ? program_counter' in
     482                let program_counter_n' ≝ nat_of_bitvector sixteen program_counter' in
    476483                  〈〈program_counter + program_counter_n', labels〉, costs〉
    477484              ]
     
    497504                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? trgt) datalabels (zero ?) in
    498505                    let address ≝ DATA16 pc_offset in
    499                       assembly1 (MOV ? (? ? ? ? 〈DPTR, address〉))
     506                      assembly1 (MOV ? (Left ? ? (Left ? ? (Right ? ? 〈DPTR, address〉))))
    500507                  | Instruction instr ⇒ assembly1 instr
    501508                  | Jmp jmp ⇒
     
    505512                      assembly1 (LJMP ? address)
    506513                  | WithLabel jmp ⇒
    507                     assembly1 (assembly_jump ? jmp (address_of labels))
     514                    assembly1 (assembly_jump jmp (address_of labels))
    508515                  ]
    509516            ) instr_list
    510517          ) in
    511         Just ? 〈flat_list, costs〉.
     518        Just (List ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉.
     519  ##[##2,3,4,5,6: nnormalize; //;
     520  ##| nwhd in ⊢ (? (? ? ? %));
     521      ncases (less_than_b (nat_of_bitvector eight ?) two_hundred_and_fifty_six)
     522        [ nnormalize; //;
     523      ##| nnormalize;
     524          nelim not_implemented;
     525      ##]
     526  ##]
     527nqed.
    512528
    513529(*
  • Deliverables/D4.1/Matita/depends

    r414 r420  
    1616Connectives.ma Plogic/equality.ma
    1717Bool.ma Universes.ma
    18 Assembly.ma ASM.ma Arithmetic.ma BitVectorTrie.ma Fetch.ma Map.ma Status.ma
     18Assembly.ma ASM.ma Arithmetic.ma BitVectorTrie.ma Fetch.ma Status.ma
    1919List.ma Maybe.ma Util.ma
    2020Interpret.ma Fetch.ma Status.ma
     
    2222Compare.ma Universes.ma
    2323BitVector.ma String.ma Vector.ma
    24 String.ma Char.ma List.ma
     24String.ma Char.ma Compare.ma List.ma
    2525Plogic/equality.ma Universes.ma
    2626Nat.ma Bool.ma Cartesian.ma Connectives.ma
Note: See TracChangeset for help on using the changeset viewer.