Changeset 2135


Ignore:
Timestamp:
Jun 28, 2012, 2:34:55 PM (5 years ago)
Author:
sacerdot
Message:

One complex daemon changed to two simpler ones.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2132 r2135  
    197197inversion (assembly_1_pseudoinstruction ??????) #len' #assembled'
    198198whd in ⊢ (??%? → ?); #EQ1 #EQ2 destruct %
    199 qed.
    200 
    201 (* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *)     
    202 lemma assembly_ok:
    203   ∀program.
    204   ∀length_proof: |\snd program| ≤ 2^16.
    205   ∀sigma: Word → Word.
    206   ∀policy: Word → bool.
    207   ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
    208   ∀assembled.
    209   ∀costs': BitVectorTrie costlabel 16.
    210   let 〈preamble, instr_list〉 ≝ program in
    211   let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
    212   let datalabels ≝ construct_datalabels preamble in
    213   let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
    214     〈assembled,costs'〉 = assembly program sigma policy →
    215       (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
    216         let code_memory ≝ load_code_memory assembled in
    217         let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    218           ∀ppc.∀ppc_ok.
    219             let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in     
    220             let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
    221             let pc ≝ sigma ppc in
    222             let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
    223               encoding_check code_memory pc pc_plus_len assembled ∧
    224                   sigma newppc = add … pc (bitvector_of_nat … len).
    225   #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
    226   cases (assembly program sigma policy) * #assembled' #costs''
    227   @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
    228   cut (|instr_list| ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok
    229   #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
    230   @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
    231   * #assembly_ok1 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
    232   #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
    233   @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
    234   lapply (assembly_ok2 ppc ?) try // -assembly_ok2
    235   >eq_fetch_pseudo_instruction
    236   change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?)
    237   >eq_assembly_1_pseudoinstruction
    238   whd in ⊢ (% → ?); #assembly_ok
    239   %
    240   [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
    241       >snd_fetch_pseudo_instruction
    242       cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
    243       #spw1 #_ >spw1 -spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f
    244       >eq_fetch_pseudo_instruction whd in match instruction_size;
    245       normalize nodelta >create_label_cost_refl
    246       >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
    247       [>eq_assembly_1_pseudoinstruction % | skip]
    248   | lapply (load_code_memory_ok assembled' ?) [ assumption ]
    249     #load_code_memory_ok
    250     lapply (fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction) #EQlen
    251     (* Nice statement here *)
    252     cut (∀j. ∀H: j < |assembled|.
    253           nth_safe Byte j assembled H =
    254           \snd (next (load_code_memory assembled')
    255           (bitvector_of_nat 16
    256            (nat_of_bitvector …
    257             (add … (sigma ppc) (bitvector_of_nat … j))))))
    258     [1:
    259       cases daemon
    260     |2:
    261       -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
    262       elim assembled
    263       [1:
    264         #pc #_ whd <add_zero %
    265       | #hd #tl #IH #pc #H %
    266          [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
    267            >H -H whd in ⊢ (??%?); <add_zero //
    268          | >(?: add … pc (bitvector_of_nat … (S (|tl|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (|tl|)))
    269            [2: <add_bitvector_of_nat_Sm @add_associative ]
    270            @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
    271            <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm
    272            >add_associative % ]]
    273   ]]
    274 qed.
    275 
    276 (* XXX: should we add that costs = costs'? *)
    277 lemma fetch_assembly_pseudo2:
    278   ∀program.
    279   ∀length_proof: |\snd program| ≤ 2^16.
    280   ∀sigma.
    281   ∀policy.
    282   ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
    283   ∀ppc.∀ppc_ok.
    284   let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
    285   let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
    286   let code_memory ≝ load_code_memory assembled in
    287   let data_labels ≝ construct_datalabels (\fst program) in
    288   let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    289   let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
    290   let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
    291   let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
    292     fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
    293   * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
    294   @pair_elim #labels #costs #create_label_map_refl
    295   @pair_elim #assembled #costs' #assembled_refl
    296   letin code_memory ≝ (load_code_memory ?)
    297   letin data_labels ≝ (construct_datalabels ?)
    298   letin lookup_labels ≝ (λx. ?)
    299   letin lookup_datalabels ≝ (λx. ?)
    300   @pair_elim #pi #newppc #fetch_pseudo_refl
    301   lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')
    302   normalize nodelta try assumption
    303   >create_label_map_refl in ⊢ (match % with [_ ⇒ ?] → ?); #H
    304   lapply (H (sym_eq … assembled_refl)) -H
    305   lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
    306   cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
    307   #len #assembledi #EQ4 #H
    308   lapply (H ppc) >fetch_pseudo_refl #H
    309   lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy)
    310   >create_label_map_refl #X lapply (X ppc ppc_ok (load_code_memory assembled)) -X
    311   >EQ4 #H1 cases (H ppc_ok)
    312   #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
    313   >fetch_pseudo_refl in H1; #assm @assm assumption
    314 qed.
    315 
    316 (* XXX: changed this type.  Bool specifies whether byte is first or second
    317         component of an address, and the Word is the pseudoaddress that it
    318         corresponds to.  Second component is the same principle for the accumulator
    319         A.
    320 *)
    321 definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)).
    322 
    323 include alias "ASM/BitVectorTrie.ma".
    324  
    325 include "common/AssocList.ma".
    326 
    327 axiom low_internal_ram_of_pseudo_low_internal_ram:
    328  ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
    329 
    330 axiom high_internal_ram_of_pseudo_high_internal_ram:
    331  ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
    332 
    333 axiom low_internal_ram_of_pseudo_internal_ram_hit:
    334  ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀high: bool. ∀points_to: Word. ∀addr:BitVector 7.
    335   assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … (〈high, points_to〉)  →
    336    let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
    337    let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
    338    let bl ≝ lookup ? 7 addr ram (zero 8) in
    339    let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
    340    let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in
    341      if high then
    342        (pbl = higher) ∧ (bl = phigher)
    343      else
    344        (pbl = lower) ∧ (bl = plower).
    345 
    346 (* changed from add to sub *)
    347 axiom low_internal_ram_of_pseudo_internal_ram_miss:
    348  ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
    349   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
    350     assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false →
    351       lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
    352 
    353 definition addressing_mode_ok ≝
    354  λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
    355   λaddr:addressing_mode.
    356    match addr with
    357     [ DIRECT d ⇒
    358        ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
    359        ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
    360     | INDIRECT i ⇒
    361        let d ≝ get_register … s [[false;false;i]] in
    362        ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
    363        ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
    364     | EXT_INDIRECT _ ⇒ true
    365     | REGISTER _ ⇒ true
    366     | ACC_A ⇒ match \snd M with [ None ⇒ true | _ ⇒ false ]
    367     | ACC_B ⇒ true
    368     | DPTR ⇒ true
    369     | DATA _ ⇒ true
    370     | DATA16 _ ⇒ true
    371     | ACC_DPTR ⇒ true
    372     | ACC_PC ⇒ true
    373     | EXT_INDIRECT_DPTR ⇒ true
    374     | INDIRECT_DPTR ⇒ true
    375     | CARRY ⇒ true
    376     | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
    377     | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
    378     | RELATIVE _ ⇒ true
    379     | ADDR11 _ ⇒ true
    380     | ADDR16 _ ⇒ true ].
    381    
    382 definition next_internal_pseudo_address_map0 ≝
    383   λT.
    384   λcm:T.
    385   λaddr_of: Identifier → PreStatus T cm → Word.
    386   λfetched.
    387   λM: internal_pseudo_address_map.
    388   λs: PreStatus T cm.
    389    match fetched with
    390     [ Comment _ ⇒ Some ? M
    391     | Cost _ ⇒ Some … M
    392     | Jmp _ ⇒ Some … M
    393     | Call a ⇒
    394       let a' ≝ addr_of a s in
    395       let 〈callM, accM〉 ≝ M in
    396          Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈false, a'〉〉::
    397                  〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈true, a'〉〉::callM, accM〉
    398     | Mov _ _ ⇒ Some … M
    399     | Instruction instr ⇒
    400        match instr with
    401         [ ADD addr1 addr2 ⇒
    402            if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
    403             Some ? M
    404            else
    405             None ?
    406         | ADDC addr1 addr2 ⇒
    407            if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
    408             Some ? M
    409            else
    410             None ?
    411         | SUBB addr1 addr2 ⇒
    412            if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
    413             Some ? M
    414            else
    415             None ?       
    416         | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
    417 
    418 definition next_internal_pseudo_address_map ≝
    419  λM:internal_pseudo_address_map.
    420  λcm.
    421  λaddr_of.
    422  λs:PseudoStatus cm.
    423  λppc_ok.
    424     next_internal_pseudo_address_map0 ? cm addr_of
    425      (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
    426 
    427 definition code_memory_of_pseudo_assembly_program:
    428     ∀pap:pseudo_assembly_program.
    429       (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
    430   λpap.
    431   λsigma.
    432   λpolicy.
    433     let p ≝ pi1 … (assembly pap sigma policy) in
    434       load_code_memory (\fst p).
    435 
    436 definition sfr_8051_of_pseudo_sfr_8051 ≝
    437   λM: internal_pseudo_address_map.
    438   λsfrs: Vector Byte 19.
    439   λsigma: Word → Word.
    440     match \snd M with
    441     [ None ⇒ sfrs
    442     | Some s ⇒
    443       let 〈high, address〉 ≝ s in
    444       let index ≝ sfr_8051_index SFR_ACC_A in
    445       let 〈upper, lower〉 ≝ vsplit ? 8 8 (sigma address) in
    446         if high then
    447           set_index Byte 19 sfrs index upper ?
    448         else
    449           set_index Byte 19 sfrs index lower ?
    450     ].
    451   //
    452 qed.
    453 
    454 definition status_of_pseudo_status:
    455     internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
    456       ∀sigma: Word → Word. ∀policy: Word → bool.
    457         Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
    458   λM.
    459   λpap.
    460   λps.
    461   λsigma.
    462   λpolicy.
    463   let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
    464   let pc ≝ sigma (program_counter … ps) in
    465   let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
    466   let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
    467      mk_PreStatus (BitVectorTrie Byte 16)
    468       cm
    469       lir
    470       hir
    471       (external_ram … ps)
    472       pc
    473       (special_function_registers_8051 … ps)
    474       (special_function_registers_8052 … ps)
    475       (p1_latch … ps)
    476       (p3_latch … ps)
    477       (clock … ps).
    478 
    479 (*
    480 definition write_at_stack_pointer':
    481  ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
    482   λM: Type[0].
    483   λs: PreStatus M.
    484   λv: Byte.
    485     let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
    486     let bit_zero ≝ get_index_v… nu O ? in
    487     let bit_1 ≝ get_index_v… nu 1 ? in
    488     let bit_2 ≝ get_index_v… nu 2 ? in
    489     let bit_3 ≝ get_index_v… nu 3 ? in
    490       if bit_zero then
    491         let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
    492                               v (low_internal_ram ? s) in
    493           set_low_internal_ram ? s memory
    494       else
    495         let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
    496                               v (high_internal_ram ? s) in
    497           set_high_internal_ram ? s memory.
    498   [ cases l0 %
    499   |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
    500 qed.
    501 
    502 definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
    503  Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
    504 
    505   λticks_of.
    506   λs.
    507   let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
    508   let ticks ≝ ticks_of (program_counter ? s) in
    509   let s ≝ set_clock ? s (clock ? s + ticks) in
    510   let s ≝ set_program_counter ? s pc in
    511     match instr with
    512     [ Instruction instr ⇒
    513        execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
    514     | Comment cmt ⇒ s
    515     | Cost cst ⇒ s
    516     | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
    517     | Call call ⇒
    518       let a ≝ address_of_word_labels s call in
    519       let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    520       let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    521       let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
    522       let s ≝ write_at_stack_pointer' ? s pc_bl in
    523       let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    524       let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    525       let s ≝ write_at_stack_pointer' ? s pc_bu in
    526         set_program_counter ? s a
    527     | Mov dptr ident ⇒
    528        set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
    529     ].
    530  [
    531  |2,3,4: %
    532  | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
    533  |
    534  | %
    535  ]
    536  cases not_implemented
    537 qed.
    538 *)
    539 
    540 (*
    541 lemma execute_code_memory_unchanged:
    542  ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
    543  #ticks #ps whd in ⊢ (??? (??%))
    544  cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
    545   (program_counter pseudo_assembly_program ps)) #instr #pc
    546  whd in ⊢ (??? (??%)) cases instr
    547   [ #pre cases pre
    548      [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
    549        cases (vsplit ????) #z1 #z2 %
    550      | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
    551        cases (vsplit ????) #z1 #z2 %
    552      | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
    553        cases (vsplit ????) #z1 #z2 %
    554      | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
    555        [ #x1 whd in ⊢ (??? (??%))
    556      | *: cases not_implemented
    557      ]
    558   | #comment %
    559   | #cost %
    560   | #label %
    561   | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
    562     cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
    563     whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
    564     whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
    565     (* CSC: ??? *)
    566   | #dptr #label (* CSC: ??? *)
    567   ]
    568   cases not_implemented
    569 qed.
    570 *)
    571 
    572 (* DEAD CODE?
    573 lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
    574  ∀M:internal_pseudo_address_map.
    575  ∀ps,ps': PseudoStatus.
    576  ∀pol.
    577   ∀prf:code_memory … ps = code_memory … ps'.
    578    let pol' ≝ ? in
    579    match status_of_pseudo_status M ps pol with
    580     [ None ⇒ status_of_pseudo_status M ps' pol' = None …
    581     | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
    582     ].
    583  [2: <prf @pol]
    584  #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
    585  generalize in match (refl … (assembly (code_memory … ps) pol))
    586  cases (assembly ??) in ⊢ (???% → %)
    587   [ #K whd whd in ⊢ (??%?) <H >K %
    588   | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
    589 qed.
    590 *)
    591 
    592 definition ticks_of0:
    593     ∀p:pseudo_assembly_program.
    594       (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
    595   λprogram: pseudo_assembly_program.
    596   λsigma.
    597   λpolicy.
    598   λppc: Word.
    599   λfetched.
    600     match fetched with
    601     [ Instruction instr ⇒
    602       match instr with
    603       [ JC lbl ⇒ ? (*
    604         match pol lookup_labels ppc with
    605         [ short_jump ⇒ 〈2, 2〉
    606         | absolute_jump ⇒ ?
    607         | long_jump ⇒ 〈4, 4〉
    608         ] *)
    609       | JNC lbl ⇒ ? (*
    610         match pol lookup_labels ppc with
    611         [ short_jump ⇒ 〈2, 2〉
    612         | absolute_jump ⇒ ?
    613         | long_jump ⇒ 〈4, 4〉
    614         ] *)
    615       | JB bit lbl ⇒ ? (*
    616         match pol lookup_labels ppc with
    617         [ short_jump ⇒ 〈2, 2〉
    618         | absolute_jump ⇒ ?
    619         | long_jump ⇒ 〈4, 4〉
    620         ] *)
    621       | JNB bit lbl ⇒ ? (*
    622         match pol lookup_labels ppc with
    623         [ short_jump ⇒ 〈2, 2〉
    624         | absolute_jump ⇒ ?
    625         | long_jump ⇒ 〈4, 4〉
    626         ] *)
    627       | JBC bit lbl ⇒ ? (*
    628         match pol lookup_labels ppc with
    629         [ short_jump ⇒ 〈2, 2〉
    630         | absolute_jump ⇒ ?
    631         | long_jump ⇒ 〈4, 4〉
    632         ] *)
    633       | JZ lbl ⇒ ? (*
    634         match pol lookup_labels ppc with
    635         [ short_jump ⇒ 〈2, 2〉
    636         | absolute_jump ⇒ ?
    637         | long_jump ⇒ 〈4, 4〉
    638         ] *)
    639       | JNZ lbl ⇒ ? (*
    640         match pol lookup_labels  ppc with
    641         [ short_jump ⇒ 〈2, 2〉
    642         | absolute_jump ⇒ ?
    643         | long_jump ⇒ 〈4, 4〉
    644         ] *)
    645       | CJNE arg lbl ⇒ ? (*
    646         match pol lookup_labels ppc with
    647         [ short_jump ⇒ 〈2, 2〉
    648         | absolute_jump ⇒ ?
    649         | long_jump ⇒ 〈4, 4〉
    650         ] *)
    651       | DJNZ arg lbl ⇒ ? (*
    652         match pol lookup_labels ppc with
    653         [ short_jump ⇒ 〈2, 2〉
    654         | absolute_jump ⇒ ?
    655         | long_jump ⇒ 〈4, 4〉
    656         ] *)
    657       | ADD arg1 arg2 ⇒
    658         let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
    659          〈ticks, ticks〉
    660       | ADDC arg1 arg2 ⇒
    661         let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
    662          〈ticks, ticks〉
    663       | SUBB arg1 arg2 ⇒
    664         let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
    665          〈ticks, ticks〉
    666       | INC arg ⇒
    667         let ticks ≝ ticks_of_instruction (INC ? arg) in
    668          〈ticks, ticks〉
    669       | DEC arg ⇒
    670         let ticks ≝ ticks_of_instruction (DEC ? arg) in
    671          〈ticks, ticks〉
    672       | MUL arg1 arg2 ⇒
    673         let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
    674          〈ticks, ticks〉
    675       | DIV arg1 arg2 ⇒
    676         let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
    677          〈ticks, ticks〉
    678       | DA arg ⇒
    679         let ticks ≝ ticks_of_instruction (DA ? arg) in
    680          〈ticks, ticks〉
    681       | ANL arg ⇒
    682         let ticks ≝ ticks_of_instruction (ANL ? arg) in
    683          〈ticks, ticks〉
    684       | ORL arg ⇒
    685         let ticks ≝ ticks_of_instruction (ORL ? arg) in
    686          〈ticks, ticks〉
    687       | XRL arg ⇒
    688         let ticks ≝ ticks_of_instruction (XRL ? arg) in
    689          〈ticks, ticks〉
    690       | CLR arg ⇒
    691         let ticks ≝ ticks_of_instruction (CLR ? arg) in
    692          〈ticks, ticks〉
    693       | CPL arg ⇒
    694         let ticks ≝ ticks_of_instruction (CPL ? arg) in
    695          〈ticks, ticks〉
    696       | RL arg ⇒
    697         let ticks ≝ ticks_of_instruction (RL ? arg) in
    698          〈ticks, ticks〉
    699       | RLC arg ⇒
    700         let ticks ≝ ticks_of_instruction (RLC ? arg) in
    701          〈ticks, ticks〉
    702       | RR arg ⇒
    703         let ticks ≝ ticks_of_instruction (RR ? arg) in
    704          〈ticks, ticks〉
    705       | RRC arg ⇒
    706         let ticks ≝ ticks_of_instruction (RRC ? arg) in
    707          〈ticks, ticks〉
    708       | SWAP arg ⇒
    709         let ticks ≝ ticks_of_instruction (SWAP ? arg) in
    710          〈ticks, ticks〉
    711       | MOV arg ⇒
    712         let ticks ≝ ticks_of_instruction (MOV ? arg) in
    713          〈ticks, ticks〉
    714       | MOVX arg ⇒
    715         let ticks ≝ ticks_of_instruction (MOVX ? arg) in
    716          〈ticks, ticks〉
    717       | SETB arg ⇒
    718         let ticks ≝ ticks_of_instruction (SETB ? arg) in
    719          〈ticks, ticks〉
    720       | PUSH arg ⇒
    721         let ticks ≝ ticks_of_instruction (PUSH ? arg) in
    722          〈ticks, ticks〉
    723       | POP arg ⇒
    724         let ticks ≝ ticks_of_instruction (POP ? arg) in
    725          〈ticks, ticks〉
    726       | XCH arg1 arg2 ⇒
    727         let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
    728          〈ticks, ticks〉
    729       | XCHD arg1 arg2 ⇒
    730         let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
    731          〈ticks, ticks〉
    732       | RET ⇒
    733         let ticks ≝ ticks_of_instruction (RET ?) in
    734          〈ticks, ticks〉
    735       | RETI ⇒
    736         let ticks ≝ ticks_of_instruction (RETI ?) in
    737          〈ticks, ticks〉
    738       | NOP ⇒
    739         let ticks ≝ ticks_of_instruction (NOP ?) in
    740          〈ticks, ticks〉
    741       ]
    742     | Comment comment ⇒ 〈0, 0〉
    743     | Cost cost ⇒ 〈0, 0〉
    744     | Jmp jmp ⇒ 〈2, 2〉
    745     | Call call ⇒ 〈2, 2〉
    746     | Mov dptr tgt ⇒ 〈2, 2〉
    747     ].
    748     cases daemon
    749 qed.
    750 
    751 definition ticks_of:
    752     ∀p:pseudo_assembly_program.
    753       (Word → Word) → (Word → bool) → ∀ppc:Word.
    754        nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
    755   λprogram: pseudo_assembly_program.
    756   λsigma.
    757   λpolicy.
    758   λppc: Word. λppc_ok.
    759     let pseudo ≝ \snd program in
    760     let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
    761      ticks_of0 program sigma policy ppc fetched.
    762 
    763 (*
    764 lemma blah:
    765   ∀m: internal_pseudo_address_map.
    766   ∀s: PseudoStatus.
    767   ∀arg: Byte.
    768   ∀b: bool.
    769     addressing_mode_ok m s (DIRECT arg) = true →
    770       get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
    771       get_arg_8 ? s b (DIRECT arg).
    772   [2, 3: normalize % ]
    773   #m #s #arg #b #hyp
    774   whd in ⊢ (??%%)
    775   @vsplit_elim''
    776   #nu' #nl' #arg_nu_nl_eq
    777   normalize nodelta
    778   generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
    779   cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
    780   #get_index_v_eq
    781   normalize nodelta
    782   [2:
    783     normalize nodelta
    784     @vsplit_elim''
    785     #bit_one' #three_bits' #bit_one_three_bit_eq
    786     generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
    787     normalize nodelta
    788     generalize in match (refl ? (sub_7_with_carry ? ? ?))
    789     cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
    790     #Saddr #carr' #Saddr_carr_eq
    791     normalize nodelta
    792     #carr_hyp'
    793     @carr_hyp'
    794     [1:
    795     |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
    796         generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
    797         cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
    798         #member_eq
    799         normalize nodelta
    800         [2: #destr destruct(destr)
    801         |1: -carr_hyp';
    802             >arg_nu_nl_eq
    803             <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
    804             [1: >get_index_v_eq in ⊢ (??%? → ?)
    805             |2: @le_S @le_S @le_S @le_n
    806             ]
    807             cases (member (BitVector 8) ? (\fst ?) ?)
    808             [1: #destr normalize in destr; destruct(destr)
    809             |2:
    810             ]
    811         ]
    812     |3: >get_index_v_eq in ⊢ (??%?)
    813         change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
    814         >(vsplit_vector_singleton … bit_one_three_bit_eq)
    815         <arg_nu_nl_eq
    816         whd in hyp:(??%?)
    817         cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
    818         normalize nodelta [*: #ignore @sym_eq ]
    819     ]
    820   |
    821   ].
    822 *)
    823 (*
    824 map_address0 ... (DIRECT arg) = Some .. →
    825   get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
    826   get_arg_8 (internal_ram ...) (DIRECT arg)
    827 
    828 ((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
    829                      then Some internal_pseudo_address_map M 
    830                      else None internal_pseudo_address_map )
    831                     =Some internal_pseudo_address_map M')
    832 
    833 axiom low_internal_ram_write_at_stack_pointer:
    834  ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
    835  ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
    836   get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
    837   low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
    838   sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
    839   sp2 = add ? sp1 (bitvector_of_nat 8 1) →
    840   bu@@bl = sigma (pbu@@pbl) →
    841    low_internal_ram T1 cm1
    842      (write_at_stack_pointer …
    843        (set_8051_sfr …
    844          (write_at_stack_pointer …
    845            (set_8051_sfr …
    846              (set_low_internal_ram … s1
    847                (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
    848              SFR_SP sp1)
    849           bl)
    850         SFR_SP sp2)
    851       bu)
    852    = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
    853       (low_internal_ram …
    854        (write_at_stack_pointer …
    855          (set_8051_sfr …
    856            (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
    857           SFR_SP sp2)
    858         pbu)).
    859 
    860 lemma high_internal_ram_write_at_stack_pointer:
    861  ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
    862  ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
    863   get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
    864   high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
    865   sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
    866   sp2 = add ? sp1 (bitvector_of_nat 8 1) →
    867   bu@@bl = sigma (pbu@@pbl) →
    868    high_internal_ram T1 cm1
    869      (write_at_stack_pointer …
    870        (set_8051_sfr …
    871          (write_at_stack_pointer …
    872            (set_8051_sfr …
    873              (set_high_internal_ram … s1
    874                (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
    875              SFR_SP sp1)
    876           bl)
    877         SFR_SP sp2)
    878       bu)
    879    = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
    880       (high_internal_ram …
    881        (write_at_stack_pointer …
    882          (set_8051_sfr …
    883            (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
    884           SFR_SP sp2)
    885         pbu)).
    886   #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
    887   #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
    888   cases daemon (* XXX: !!! *)
    889 qed.
    890 *)
    891 
    892 (*CSC: ???*)
    893 (* XXX: we need a precondition here stating that the PPC is within the
    894         bounds of the instruction list in order for Jaap's specification to
    895         apply.
    896 *)
    897 lemma snd_assembly_1_pseudoinstruction_ok:
    898   ∀program: pseudo_assembly_program.
    899   ∀program_length_proof: |\snd program| ≤ 2^16.
    900   ∀sigma: Word → Word.
    901   ∀policy: Word → bool.
    902   ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
    903   ∀ppc: Word.
    904   ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
    905   ∀pi.
    906   ∀lookup_labels.
    907   ∀lookup_datalabels.
    908     let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
    909     lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)) →
    910     lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
    911     \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
    912     let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
    913       sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
    914   #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
    915   #lookup_labels #lookup_datalabels
    916   @pair_elim #labels #costs #create_label_cost_map_refl
    917   #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
    918   normalize nodelta
    919   generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
    920   #fetch_pseudo_refl
    921   letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
    922   letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
    923   lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
    924   @pair_elim #preamble #instr_list #program_refl
    925   lapply create_label_cost_map_refl; -create_label_cost_map_refl
    926   >program_refl in ⊢ (% → ?); #create_label_cost_map_refl
    927   >create_label_cost_map_refl
    928   <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
    929   lapply (H ppc ppc_in_bounds) -H
    930   @pair_elim #pi' #newppc #fetch_pseudo_refl'
    931   @pair_elim #len #assembled #assembly1_refl #H
    932   cases H
    933   #encoding_check_assm #sigma_newppc_refl
    934   >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
    935   >pi_refl' in assembly1_refl; #assembly1_refl
    936   >lookup_labels_refl >lookup_datalabels_refl
    937   >program_refl normalize nodelta
    938   >assembly1_refl
    939   <sigma_newppc_refl
    940   generalize in match fetch_pseudo_refl';
    941   whd in match (fetch_pseudo_instruction ???);
    942   @pair_elim #lbl #instr #nth_refl normalize nodelta
    943   #G cases (pair_destruct_right ?????? G) %
    944 qed.
    945 
    946 (* To be moved in ProofStatus *)
    947 lemma program_counter_set_program_counter:
    948   ∀T.
    949   ∀cm.
    950   ∀s.
    951   ∀x.
    952     program_counter T cm (set_program_counter T cm s x) = x.
    953   //
    954199qed.
    955200
     
    1030275  *)
    1031276qed.
     277
     278(*CSC: move elsewhere*)
     279lemma flatten_singleton:
     280 ∀A,a. flatten A [a] = a.
     281#A #a normalize //
     282qed.
     283
     284(*CSC: move elsewhere*)
     285lemma length_flatten_cons:
     286 ∀A,hd,tl.
     287  |flatten A (hd::tl)| = |hd| + |flatten A tl|.
     288 #A #hd #tl normalize //
     289qed.
     290
     291lemma tech_transitive_lt_3:
     292 ∀n1,n2,n3,b.
     293  n1 < b → n2 < b → n3 < b →
     294   n1 + n2 + n3 < 3 * b.
     295 #n1 #n2 #n3 #b #H1 #H2 #H3
     296 @(transitive_lt … (b + n2 + n3)) [ @monotonic_lt_plus_l @monotonic_lt_plus_l // ]
     297 @(transitive_lt … (b + b + n3)) [ @monotonic_lt_plus_l @monotonic_lt_plus_r // ]
     298 @(lt_to_le_to_lt … (b + b + b)) [ @monotonic_lt_plus_r // ] //
     299qed.
     300
     301lemma assembly1_pseudoinstruction_lt_2_to_16:
     302  ∀lookup_labels,sigma,policy,ppc,lookup_datalabels,pi.
     303  |\snd (assembly_1_pseudoinstruction
     304    lookup_labels sigma policy ppc lookup_datalabels pi)|
     305   < 2^16.
     306 #lookup_labels #sigma #policy #ppc #lookup_datalabels *
     307[ cut (128 < 2^16) [@leb_true_to_le %] #LT
     308  * whd in match (assembly_1_pseudoinstruction ??????);
     309  whd in match (expand_pseudo_instruction ??????);
     310  whd in match assembly_1_pseudoinstruction; normalize nodelta
     311  try (#arg1 #arg2 #arg3) try (#arg1 #arg2) try #arg1
     312  whd in match (expand_pseudo_instruction ??????);
     313  try
     314   (change with (|flatten ? [assembly1 ?]| < ?)
     315    >flatten_singleton
     316    @(transitive_lt … (assembly1_lt_128 ?))
     317    @LT)
     318  @pair_elim #x #y #_ cases x normalize nodelta
     319  try
     320   (change with (|flatten ? [assembly1 ?]| < ?)
     321    >flatten_singleton
     322    @(transitive_lt … (assembly1_lt_128 ?))
     323    @LT)
     324  change with (|flatten ? [assembly1 ?; assembly1 ?; assembly1 ?]| < ?)
     325  >length_flatten_cons >length_flatten_cons >length_flatten_cons <plus_n_O
     326  <associative_plus @(transitive_lt … (tech_transitive_lt_3 … (2^7) ???))
     327  try @assembly1_lt_128 @leb_true_to_le %
     328|2,3: #msg normalize in ⊢ (?%?); //
     329| #label whd in match (assembly_1_pseudoinstruction ??????);
     330  whd in match (expand_pseudo_instruction ??????);
     331  @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_
     332  [2: @pair_elim #x #y #_ cases (?∧?)]
     333  normalize in ⊢ (?%?); //
     334| #label whd in match (assembly_1_pseudoinstruction ??????);
     335  whd in match (expand_pseudo_instruction ??????);
     336  @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_
     337  normalize in ⊢ (?%?); //
     338| #dptr #id normalize in ⊢ (?%?); //
     339]
     340qed.
     341
     342(*CSC: move elsewhere*)         
     343axiom lt_to_lt_nat_of_bitvector_add:
     344 ∀n,v,m1,m2.
     345  m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 →
     346   nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <
     347   nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
     348
     349(* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *)     
     350lemma assembly_ok:
     351  ∀program.
     352  ∀length_proof: |\snd program| ≤ 2^16.
     353  ∀sigma: Word → Word.
     354  ∀policy: Word → bool.
     355  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
     356  ∀assembled.
     357  ∀costs': BitVectorTrie costlabel 16.
     358  let 〈preamble, instr_list〉 ≝ program in
     359  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
     360  let datalabels ≝ construct_datalabels preamble in
     361  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
     362    〈assembled,costs'〉 = assembly program sigma policy →
     363      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
     364        let code_memory ≝ load_code_memory assembled in
     365        let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
     366          ∀ppc.∀ppc_ok.
     367            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in     
     368            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
     369            let pc ≝ sigma ppc in
     370            let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
     371              encoding_check code_memory pc pc_plus_len assembled ∧
     372                  sigma newppc = add … pc (bitvector_of_nat … len).
     373  #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
     374  cases (assembly program sigma policy) * #assembled' #costs''
     375  @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
     376  cut (|instr_list| ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok
     377  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
     378  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
     379  * #assembly_ok1 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
     380  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
     381  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
     382  lapply (assembly_ok2 ppc ?) try // -assembly_ok2
     383  >eq_fetch_pseudo_instruction
     384  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?)
     385  >eq_assembly_1_pseudoinstruction
     386  whd in ⊢ (% → ?); #assembly_ok
     387  %
     388  [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
     389      >snd_fetch_pseudo_instruction
     390      cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
     391      #spw1 #_ >spw1 -spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f
     392      >eq_fetch_pseudo_instruction whd in match instruction_size;
     393      normalize nodelta >create_label_cost_refl
     394      >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
     395      [>eq_assembly_1_pseudoinstruction % | skip]
     396  | lapply (load_code_memory_ok assembled' ?) [ assumption ]
     397    #load_code_memory_ok
     398    lapply (fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction) #EQlen
     399    (* Nice statement here *)
     400    cut (∀j. ∀H: j < |assembled|.
     401          nth_safe Byte j assembled H =
     402          \snd (next (load_code_memory assembled')
     403          (bitvector_of_nat 16
     404           (nat_of_bitvector …
     405            (add … (sigma ppc) (bitvector_of_nat … j))))))
     406    [1: #j #H <load_code_memory_ok
     407        [ @assembly_ok cases daemon
     408        | cut (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (|assembled|))) ≤ |assembled'|)
     409          [
     410          | #LE @(lt_to_le_to_lt … LE)
     411            @lt_to_lt_nat_of_bitvector_add
     412            [ @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? eq_assembly_1_pseudoinstruction)
     413              / by /
     414            | @(transitive_le ???? assembly_ok1) cases daemon
     415            | assumption
     416            ]   
     417          ]
     418        ]
     419    |2:
     420      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
     421      elim assembled
     422      [1:
     423        #pc #_ whd <add_zero %
     424      | #hd #tl #IH #pc #H %
     425         [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
     426           >H -H whd in ⊢ (??%?); <add_zero //
     427         | >(?: add … pc (bitvector_of_nat … (S (|tl|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (|tl|)))
     428           [2: <add_bitvector_of_nat_Sm @add_associative ]
     429           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
     430           <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm
     431           >add_associative % ]]
     432  ]]
     433qed.
     434
     435(* XXX: should we add that costs = costs'? *)
     436lemma fetch_assembly_pseudo2:
     437  ∀program.
     438  ∀length_proof: |\snd program| ≤ 2^16.
     439  ∀sigma.
     440  ∀policy.
     441  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
     442  ∀ppc.∀ppc_ok.
     443  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
     444  let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
     445  let code_memory ≝ load_code_memory assembled in
     446  let data_labels ≝ construct_datalabels (\fst program) in
     447  let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
     448  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
     449  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
     450  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
     451    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
     452  * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
     453  @pair_elim #labels #costs #create_label_map_refl
     454  @pair_elim #assembled #costs' #assembled_refl
     455  letin code_memory ≝ (load_code_memory ?)
     456  letin data_labels ≝ (construct_datalabels ?)
     457  letin lookup_labels ≝ (λx. ?)
     458  letin lookup_datalabels ≝ (λx. ?)
     459  @pair_elim #pi #newppc #fetch_pseudo_refl
     460  lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')
     461  normalize nodelta try assumption
     462  >create_label_map_refl in ⊢ (match % with [_ ⇒ ?] → ?); #H
     463  lapply (H (sym_eq … assembled_refl)) -H
     464  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
     465  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
     466  #len #assembledi #EQ4 #H
     467  lapply (H ppc) >fetch_pseudo_refl #H
     468  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy)
     469  >create_label_map_refl #X lapply (X ppc ppc_ok (load_code_memory assembled)) -X
     470  >EQ4 #H1 cases (H ppc_ok)
     471  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
     472  >fetch_pseudo_refl in H1; #assm @assm assumption
     473qed.
     474
     475(* XXX: changed this type.  Bool specifies whether byte is first or second
     476        component of an address, and the Word is the pseudoaddress that it
     477        corresponds to.  Second component is the same principle for the accumulator
     478        A.
     479*)
     480definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)).
     481
     482include alias "ASM/BitVectorTrie.ma".
     483 
     484include "common/AssocList.ma".
     485
     486axiom low_internal_ram_of_pseudo_low_internal_ram:
     487 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
     488
     489axiom high_internal_ram_of_pseudo_high_internal_ram:
     490 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
     491
     492axiom low_internal_ram_of_pseudo_internal_ram_hit:
     493 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀high: bool. ∀points_to: Word. ∀addr:BitVector 7.
     494  assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … (〈high, points_to〉)  →
     495   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
     496   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
     497   let bl ≝ lookup ? 7 addr ram (zero 8) in
     498   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
     499   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in
     500     if high then
     501       (pbl = higher) ∧ (bl = phigher)
     502     else
     503       (pbl = lower) ∧ (bl = plower).
     504
     505(* changed from add to sub *)
     506axiom low_internal_ram_of_pseudo_internal_ram_miss:
     507 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
     508  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
     509    assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false →
     510      lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
     511
     512definition addressing_mode_ok ≝
     513 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
     514  λaddr:addressing_mode.
     515   match addr with
     516    [ DIRECT d ⇒
     517       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
     518       ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
     519    | INDIRECT i ⇒
     520       let d ≝ get_register … s [[false;false;i]] in
     521       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
     522       ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
     523    | EXT_INDIRECT _ ⇒ true
     524    | REGISTER _ ⇒ true
     525    | ACC_A ⇒ match \snd M with [ None ⇒ true | _ ⇒ false ]
     526    | ACC_B ⇒ true
     527    | DPTR ⇒ true
     528    | DATA _ ⇒ true
     529    | DATA16 _ ⇒ true
     530    | ACC_DPTR ⇒ true
     531    | ACC_PC ⇒ true
     532    | EXT_INDIRECT_DPTR ⇒ true
     533    | INDIRECT_DPTR ⇒ true
     534    | CARRY ⇒ true
     535    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
     536    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
     537    | RELATIVE _ ⇒ true
     538    | ADDR11 _ ⇒ true
     539    | ADDR16 _ ⇒ true ].
     540   
     541definition next_internal_pseudo_address_map0 ≝
     542  λT.
     543  λcm:T.
     544  λaddr_of: Identifier → PreStatus T cm → Word.
     545  λfetched.
     546  λM: internal_pseudo_address_map.
     547  λs: PreStatus T cm.
     548   match fetched with
     549    [ Comment _ ⇒ Some ? M
     550    | Cost _ ⇒ Some … M
     551    | Jmp _ ⇒ Some … M
     552    | Call a ⇒
     553      let a' ≝ addr_of a s in
     554      let 〈callM, accM〉 ≝ M in
     555         Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈false, a'〉〉::
     556                 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈true, a'〉〉::callM, accM〉
     557    | Mov _ _ ⇒ Some … M
     558    | Instruction instr ⇒
     559       match instr with
     560        [ ADD addr1 addr2 ⇒
     561           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     562            Some ? M
     563           else
     564            None ?
     565        | ADDC addr1 addr2 ⇒
     566           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     567            Some ? M
     568           else
     569            None ?
     570        | SUBB addr1 addr2 ⇒
     571           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     572            Some ? M
     573           else
     574            None ?       
     575        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
     576
     577definition next_internal_pseudo_address_map ≝
     578 λM:internal_pseudo_address_map.
     579 λcm.
     580 λaddr_of.
     581 λs:PseudoStatus cm.
     582 λppc_ok.
     583    next_internal_pseudo_address_map0 ? cm addr_of
     584     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
     585
     586definition code_memory_of_pseudo_assembly_program:
     587    ∀pap:pseudo_assembly_program.
     588      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
     589  λpap.
     590  λsigma.
     591  λpolicy.
     592    let p ≝ pi1 … (assembly pap sigma policy) in
     593      load_code_memory (\fst p).
     594
     595definition sfr_8051_of_pseudo_sfr_8051 ≝
     596  λM: internal_pseudo_address_map.
     597  λsfrs: Vector Byte 19.
     598  λsigma: Word → Word.
     599    match \snd M with
     600    [ None ⇒ sfrs
     601    | Some s ⇒
     602      let 〈high, address〉 ≝ s in
     603      let index ≝ sfr_8051_index SFR_ACC_A in
     604      let 〈upper, lower〉 ≝ vsplit ? 8 8 (sigma address) in
     605        if high then
     606          set_index Byte 19 sfrs index upper ?
     607        else
     608          set_index Byte 19 sfrs index lower ?
     609    ].
     610  //
     611qed.
     612
     613definition status_of_pseudo_status:
     614    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
     615      ∀sigma: Word → Word. ∀policy: Word → bool.
     616        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
     617  λM.
     618  λpap.
     619  λps.
     620  λsigma.
     621  λpolicy.
     622  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
     623  let pc ≝ sigma (program_counter … ps) in
     624  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
     625  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
     626     mk_PreStatus (BitVectorTrie Byte 16)
     627      cm
     628      lir
     629      hir
     630      (external_ram … ps)
     631      pc
     632      (special_function_registers_8051 … ps)
     633      (special_function_registers_8052 … ps)
     634      (p1_latch … ps)
     635      (p3_latch … ps)
     636      (clock … ps).
     637
     638(*
     639definition write_at_stack_pointer':
     640 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
     641  λM: Type[0].
     642  λs: PreStatus M.
     643  λv: Byte.
     644    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
     645    let bit_zero ≝ get_index_v… nu O ? in
     646    let bit_1 ≝ get_index_v… nu 1 ? in
     647    let bit_2 ≝ get_index_v… nu 2 ? in
     648    let bit_3 ≝ get_index_v… nu 3 ? in
     649      if bit_zero then
     650        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
     651                              v (low_internal_ram ? s) in
     652          set_low_internal_ram ? s memory
     653      else
     654        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
     655                              v (high_internal_ram ? s) in
     656          set_high_internal_ram ? s memory.
     657  [ cases l0 %
     658  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
     659qed.
     660
     661definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
     662 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
     663
     664  λticks_of.
     665  λs.
     666  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
     667  let ticks ≝ ticks_of (program_counter ? s) in
     668  let s ≝ set_clock ? s (clock ? s + ticks) in
     669  let s ≝ set_program_counter ? s pc in
     670    match instr with
     671    [ Instruction instr ⇒
     672       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
     673    | Comment cmt ⇒ s
     674    | Cost cst ⇒ s
     675    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
     676    | Call call ⇒
     677      let a ≝ address_of_word_labels s call in
     678      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     679      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     680      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
     681      let s ≝ write_at_stack_pointer' ? s pc_bl in
     682      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     683      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     684      let s ≝ write_at_stack_pointer' ? s pc_bu in
     685        set_program_counter ? s a
     686    | Mov dptr ident ⇒
     687       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
     688    ].
     689 [
     690 |2,3,4: %
     691 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
     692 |
     693 | %
     694 ]
     695 cases not_implemented
     696qed.
     697*)
     698
     699(*
     700lemma execute_code_memory_unchanged:
     701 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
     702 #ticks #ps whd in ⊢ (??? (??%))
     703 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
     704  (program_counter pseudo_assembly_program ps)) #instr #pc
     705 whd in ⊢ (??? (??%)) cases instr
     706  [ #pre cases pre
     707     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
     708       cases (vsplit ????) #z1 #z2 %
     709     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
     710       cases (vsplit ????) #z1 #z2 %
     711     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
     712       cases (vsplit ????) #z1 #z2 %
     713     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
     714       [ #x1 whd in ⊢ (??? (??%))
     715     | *: cases not_implemented
     716     ]
     717  | #comment %
     718  | #cost %
     719  | #label %
     720  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
     721    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
     722    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
     723    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
     724    (* CSC: ??? *)
     725  | #dptr #label (* CSC: ??? *)
     726  ]
     727  cases not_implemented
     728qed.
     729*)
     730
     731(* DEAD CODE?
     732lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
     733 ∀M:internal_pseudo_address_map.
     734 ∀ps,ps': PseudoStatus.
     735 ∀pol.
     736  ∀prf:code_memory … ps = code_memory … ps'.
     737   let pol' ≝ ? in
     738   match status_of_pseudo_status M ps pol with
     739    [ None ⇒ status_of_pseudo_status M ps' pol' = None …
     740    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
     741    ].
     742 [2: <prf @pol]
     743 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     744 generalize in match (refl … (assembly (code_memory … ps) pol))
     745 cases (assembly ??) in ⊢ (???% → %)
     746  [ #K whd whd in ⊢ (??%?) <H >K %
     747  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
     748qed.
     749*)
     750
     751definition ticks_of0:
     752    ∀p:pseudo_assembly_program.
     753      (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
     754  λprogram: pseudo_assembly_program.
     755  λsigma.
     756  λpolicy.
     757  λppc: Word.
     758  λfetched.
     759    match fetched with
     760    [ Instruction instr ⇒
     761      match instr with
     762      [ JC lbl ⇒ ? (*
     763        match pol lookup_labels ppc with
     764        [ short_jump ⇒ 〈2, 2〉
     765        | absolute_jump ⇒ ?
     766        | long_jump ⇒ 〈4, 4〉
     767        ] *)
     768      | JNC lbl ⇒ ? (*
     769        match pol lookup_labels ppc with
     770        [ short_jump ⇒ 〈2, 2〉
     771        | absolute_jump ⇒ ?
     772        | long_jump ⇒ 〈4, 4〉
     773        ] *)
     774      | JB bit lbl ⇒ ? (*
     775        match pol lookup_labels ppc with
     776        [ short_jump ⇒ 〈2, 2〉
     777        | absolute_jump ⇒ ?
     778        | long_jump ⇒ 〈4, 4〉
     779        ] *)
     780      | JNB bit lbl ⇒ ? (*
     781        match pol lookup_labels ppc with
     782        [ short_jump ⇒ 〈2, 2〉
     783        | absolute_jump ⇒ ?
     784        | long_jump ⇒ 〈4, 4〉
     785        ] *)
     786      | JBC bit lbl ⇒ ? (*
     787        match pol lookup_labels ppc with
     788        [ short_jump ⇒ 〈2, 2〉
     789        | absolute_jump ⇒ ?
     790        | long_jump ⇒ 〈4, 4〉
     791        ] *)
     792      | JZ lbl ⇒ ? (*
     793        match pol lookup_labels ppc with
     794        [ short_jump ⇒ 〈2, 2〉
     795        | absolute_jump ⇒ ?
     796        | long_jump ⇒ 〈4, 4〉
     797        ] *)
     798      | JNZ lbl ⇒ ? (*
     799        match pol lookup_labels  ppc with
     800        [ short_jump ⇒ 〈2, 2〉
     801        | absolute_jump ⇒ ?
     802        | long_jump ⇒ 〈4, 4〉
     803        ] *)
     804      | CJNE arg lbl ⇒ ? (*
     805        match pol lookup_labels ppc with
     806        [ short_jump ⇒ 〈2, 2〉
     807        | absolute_jump ⇒ ?
     808        | long_jump ⇒ 〈4, 4〉
     809        ] *)
     810      | DJNZ arg lbl ⇒ ? (*
     811        match pol lookup_labels ppc with
     812        [ short_jump ⇒ 〈2, 2〉
     813        | absolute_jump ⇒ ?
     814        | long_jump ⇒ 〈4, 4〉
     815        ] *)
     816      | ADD arg1 arg2 ⇒
     817        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
     818         〈ticks, ticks〉
     819      | ADDC arg1 arg2 ⇒
     820        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
     821         〈ticks, ticks〉
     822      | SUBB arg1 arg2 ⇒
     823        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
     824         〈ticks, ticks〉
     825      | INC arg ⇒
     826        let ticks ≝ ticks_of_instruction (INC ? arg) in
     827         〈ticks, ticks〉
     828      | DEC arg ⇒
     829        let ticks ≝ ticks_of_instruction (DEC ? arg) in
     830         〈ticks, ticks〉
     831      | MUL arg1 arg2 ⇒
     832        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
     833         〈ticks, ticks〉
     834      | DIV arg1 arg2 ⇒
     835        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
     836         〈ticks, ticks〉
     837      | DA arg ⇒
     838        let ticks ≝ ticks_of_instruction (DA ? arg) in
     839         〈ticks, ticks〉
     840      | ANL arg ⇒
     841        let ticks ≝ ticks_of_instruction (ANL ? arg) in
     842         〈ticks, ticks〉
     843      | ORL arg ⇒
     844        let ticks ≝ ticks_of_instruction (ORL ? arg) in
     845         〈ticks, ticks〉
     846      | XRL arg ⇒
     847        let ticks ≝ ticks_of_instruction (XRL ? arg) in
     848         〈ticks, ticks〉
     849      | CLR arg ⇒
     850        let ticks ≝ ticks_of_instruction (CLR ? arg) in
     851         〈ticks, ticks〉
     852      | CPL arg ⇒
     853        let ticks ≝ ticks_of_instruction (CPL ? arg) in
     854         〈ticks, ticks〉
     855      | RL arg ⇒
     856        let ticks ≝ ticks_of_instruction (RL ? arg) in
     857         〈ticks, ticks〉
     858      | RLC arg ⇒
     859        let ticks ≝ ticks_of_instruction (RLC ? arg) in
     860         〈ticks, ticks〉
     861      | RR arg ⇒
     862        let ticks ≝ ticks_of_instruction (RR ? arg) in
     863         〈ticks, ticks〉
     864      | RRC arg ⇒
     865        let ticks ≝ ticks_of_instruction (RRC ? arg) in
     866         〈ticks, ticks〉
     867      | SWAP arg ⇒
     868        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
     869         〈ticks, ticks〉
     870      | MOV arg ⇒
     871        let ticks ≝ ticks_of_instruction (MOV ? arg) in
     872         〈ticks, ticks〉
     873      | MOVX arg ⇒
     874        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
     875         〈ticks, ticks〉
     876      | SETB arg ⇒
     877        let ticks ≝ ticks_of_instruction (SETB ? arg) in
     878         〈ticks, ticks〉
     879      | PUSH arg ⇒
     880        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
     881         〈ticks, ticks〉
     882      | POP arg ⇒
     883        let ticks ≝ ticks_of_instruction (POP ? arg) in
     884         〈ticks, ticks〉
     885      | XCH arg1 arg2 ⇒
     886        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
     887         〈ticks, ticks〉
     888      | XCHD arg1 arg2 ⇒
     889        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
     890         〈ticks, ticks〉
     891      | RET ⇒
     892        let ticks ≝ ticks_of_instruction (RET ?) in
     893         〈ticks, ticks〉
     894      | RETI ⇒
     895        let ticks ≝ ticks_of_instruction (RETI ?) in
     896         〈ticks, ticks〉
     897      | NOP ⇒
     898        let ticks ≝ ticks_of_instruction (NOP ?) in
     899         〈ticks, ticks〉
     900      ]
     901    | Comment comment ⇒ 〈0, 0〉
     902    | Cost cost ⇒ 〈0, 0〉
     903    | Jmp jmp ⇒ 〈2, 2〉
     904    | Call call ⇒ 〈2, 2〉
     905    | Mov dptr tgt ⇒ 〈2, 2〉
     906    ].
     907    cases daemon
     908qed.
     909
     910definition ticks_of:
     911    ∀p:pseudo_assembly_program.
     912      (Word → Word) → (Word → bool) → ∀ppc:Word.
     913       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
     914  λprogram: pseudo_assembly_program.
     915  λsigma.
     916  λpolicy.
     917  λppc: Word. λppc_ok.
     918    let pseudo ≝ \snd program in
     919    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
     920     ticks_of0 program sigma policy ppc fetched.
     921
     922(*
     923lemma blah:
     924  ∀m: internal_pseudo_address_map.
     925  ∀s: PseudoStatus.
     926  ∀arg: Byte.
     927  ∀b: bool.
     928    addressing_mode_ok m s (DIRECT arg) = true →
     929      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
     930      get_arg_8 ? s b (DIRECT arg).
     931  [2, 3: normalize % ]
     932  #m #s #arg #b #hyp
     933  whd in ⊢ (??%%)
     934  @vsplit_elim''
     935  #nu' #nl' #arg_nu_nl_eq
     936  normalize nodelta
     937  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
     938  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
     939  #get_index_v_eq
     940  normalize nodelta
     941  [2:
     942    normalize nodelta
     943    @vsplit_elim''
     944    #bit_one' #three_bits' #bit_one_three_bit_eq
     945    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
     946    normalize nodelta
     947    generalize in match (refl ? (sub_7_with_carry ? ? ?))
     948    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
     949    #Saddr #carr' #Saddr_carr_eq
     950    normalize nodelta
     951    #carr_hyp'
     952    @carr_hyp'
     953    [1:
     954    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
     955        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
     956        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
     957        #member_eq
     958        normalize nodelta
     959        [2: #destr destruct(destr)
     960        |1: -carr_hyp';
     961            >arg_nu_nl_eq
     962            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
     963            [1: >get_index_v_eq in ⊢ (??%? → ?)
     964            |2: @le_S @le_S @le_S @le_n
     965            ]
     966            cases (member (BitVector 8) ? (\fst ?) ?)
     967            [1: #destr normalize in destr; destruct(destr)
     968            |2:
     969            ]
     970        ]
     971    |3: >get_index_v_eq in ⊢ (??%?)
     972        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
     973        >(vsplit_vector_singleton … bit_one_three_bit_eq)
     974        <arg_nu_nl_eq
     975        whd in hyp:(??%?)
     976        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
     977        normalize nodelta [*: #ignore @sym_eq ]
     978    ]
     979  |
     980  ].
     981*)
     982(*
     983map_address0 ... (DIRECT arg) = Some .. →
     984  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
     985  get_arg_8 (internal_ram ...) (DIRECT arg)
     986
     987((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
     988                     then Some internal_pseudo_address_map M 
     989                     else None internal_pseudo_address_map )
     990                    =Some internal_pseudo_address_map M')
     991
     992axiom low_internal_ram_write_at_stack_pointer:
     993 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
     994 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
     995  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
     996  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
     997  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
     998  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
     999  bu@@bl = sigma (pbu@@pbl) →
     1000   low_internal_ram T1 cm1
     1001     (write_at_stack_pointer …
     1002       (set_8051_sfr …
     1003         (write_at_stack_pointer …
     1004           (set_8051_sfr …
     1005             (set_low_internal_ram … s1
     1006               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
     1007             SFR_SP sp1)
     1008          bl)
     1009        SFR_SP sp2)
     1010      bu)
     1011   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
     1012      (low_internal_ram …
     1013       (write_at_stack_pointer …
     1014         (set_8051_sfr …
     1015           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
     1016          SFR_SP sp2)
     1017        pbu)).
     1018
     1019lemma high_internal_ram_write_at_stack_pointer:
     1020 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
     1021 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
     1022  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
     1023  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
     1024  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
     1025  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
     1026  bu@@bl = sigma (pbu@@pbl) →
     1027   high_internal_ram T1 cm1
     1028     (write_at_stack_pointer …
     1029       (set_8051_sfr …
     1030         (write_at_stack_pointer …
     1031           (set_8051_sfr …
     1032             (set_high_internal_ram … s1
     1033               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
     1034             SFR_SP sp1)
     1035          bl)
     1036        SFR_SP sp2)
     1037      bu)
     1038   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
     1039      (high_internal_ram …
     1040       (write_at_stack_pointer …
     1041         (set_8051_sfr …
     1042           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
     1043          SFR_SP sp2)
     1044        pbu)).
     1045  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
     1046  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
     1047  cases daemon (* XXX: !!! *)
     1048qed.
     1049*)
     1050
     1051(*CSC: ???*)
     1052(* XXX: we need a precondition here stating that the PPC is within the
     1053        bounds of the instruction list in order for Jaap's specification to
     1054        apply.
     1055*)
     1056lemma snd_assembly_1_pseudoinstruction_ok:
     1057  ∀program: pseudo_assembly_program.
     1058  ∀program_length_proof: |\snd program| ≤ 2^16.
     1059  ∀sigma: Word → Word.
     1060  ∀policy: Word → bool.
     1061  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
     1062  ∀ppc: Word.
     1063  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
     1064  ∀pi.
     1065  ∀lookup_labels.
     1066  ∀lookup_datalabels.
     1067    let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
     1068    lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)) →
     1069    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
     1070    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
     1071    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
     1072      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
     1073  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
     1074  #lookup_labels #lookup_datalabels
     1075  @pair_elim #labels #costs #create_label_cost_map_refl
     1076  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
     1077  normalize nodelta
     1078  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
     1079  #fetch_pseudo_refl
     1080  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
     1081  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
     1082  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
     1083  @pair_elim #preamble #instr_list #program_refl
     1084  lapply create_label_cost_map_refl; -create_label_cost_map_refl
     1085  >program_refl in ⊢ (% → ?); #create_label_cost_map_refl
     1086  >create_label_cost_map_refl
     1087  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
     1088  lapply (H ppc ppc_in_bounds) -H
     1089  @pair_elim #pi' #newppc #fetch_pseudo_refl'
     1090  @pair_elim #len #assembled #assembly1_refl #H
     1091  cases H
     1092  #encoding_check_assm #sigma_newppc_refl
     1093  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
     1094  >pi_refl' in assembly1_refl; #assembly1_refl
     1095  >lookup_labels_refl >lookup_datalabels_refl
     1096  >program_refl normalize nodelta
     1097  >assembly1_refl
     1098  <sigma_newppc_refl
     1099  generalize in match fetch_pseudo_refl';
     1100  whd in match (fetch_pseudo_instruction ???);
     1101  @pair_elim #lbl #instr #nth_refl normalize nodelta
     1102  #G cases (pair_destruct_right ?????? G) %
     1103qed.
     1104
     1105(* To be moved in ProofStatus *)
     1106lemma program_counter_set_program_counter:
     1107  ∀T.
     1108  ∀cm.
     1109  ∀s.
     1110  ∀x.
     1111    program_counter T cm (set_program_counter T cm s x) = x.
     1112  //
     1113qed.
Note: See TracChangeset for help on using the changeset viewer.