Changeset 2160


Ignore:
Timestamp:
Jul 6, 2012, 5:26:21 PM (5 years ago)
Author:
mulligan
Message:

Added a new scratch file Test.ma for working on lemmas that are needed in the massive proof to avoid having to retypecheck everything. Lots of work from the last week on the AssemblyProofSplit?.ma file, as well as an attempt to use Russell-style types on set_arg_8.

Location:
src/ASM
Files:
1 added
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2157 r2160  
    384384qed.
    385385
     386inductive upper_lower: Type[0] ≝
     387  | upper: upper_lower
     388  | lower: upper_lower.
     389
     390definition eq_upper_lower:
     391    upper_lower → upper_lower → bool ≝
     392  λleft: upper_lower.
     393  λright: upper_lower.
     394  match left with
     395  [ upper ⇒
     396    match right with
     397    [ upper ⇒ true
     398    | _     ⇒ false
     399    ]
     400  | lower ⇒
     401    match right with
     402    [ lower ⇒ true
     403    | _     ⇒ false
     404    ]
     405  ].
     406
     407lemma eq_upper_lower_true_to_eq:
     408  ∀left: upper_lower.
     409  ∀right: upper_lower.
     410    eq_upper_lower left right = true → left = right.
     411  * * normalize try (#_ %)
     412  #absurd destruct(absurd)
     413qed.
     414
     415lemma eq_upper_lower_false_to_neq:
     416  ∀left: upper_lower.
     417  ∀right: upper_lower.
     418    eq_upper_lower left right = false → left ≠ right.
     419  * * normalize try (#absurd destruct(absurd))
     420  @nmk #absurd destruct(absurd)
     421qed.
     422
     423inductive accumulator_address_map_entry: Type[0] ≝
     424  | data: accumulator_address_map_entry
     425  | address: upper_lower → Word → accumulator_address_map_entry.
     426
     427definition eq_accumulator_address_map_entry:
     428    accumulator_address_map_entry → accumulator_address_map_entry → bool ≝
     429  λleft: accumulator_address_map_entry.
     430  λright: accumulator_address_map_entry.
     431    match left with
     432    [ data                     ⇒
     433      match right with
     434      [ data ⇒ true
     435      | _    ⇒ false
     436      ]
     437    | address upper_lower word ⇒
     438      match right with
     439      [ address upper_lower' word' ⇒
     440          eq_upper_lower upper_lower upper_lower' ∧ eq_bv … word word'
     441      | _                          ⇒ false
     442      ]
     443    ].
     444
     445lemma eq_accumulator_address_map_entry_true_to_eq:
     446  ∀left: accumulator_address_map_entry.
     447  ∀right: accumulator_address_map_entry.
     448    eq_accumulator_address_map_entry left right = true → left = right.
     449  #left #right cases left cases right
     450  [1:
     451    #_ %
     452  |2,3:
     453    #upper_lower #word normalize #absurd destruct(absurd)
     454  |4:
     455    #upper_lower #word #upper_lower' #word' normalize
     456    cases upper_lower' normalize nodelta
     457    cases upper_lower normalize
     458    [2,3:
     459      #absurd destruct(absurd)
     460    ]
     461    change with (eq_bv 16 ?? = true → ?)
     462    #relevant lapply (eq_bv_eq … relevant)
     463    #word_refl >word_refl %
     464  ]
     465qed.
     466
     467lemma eq_bv_false_to_neq:
     468  ∀n: nat.
     469  ∀left, right: BitVector n.
     470    eq_bv n left right = false → left ≠ right.
     471  #n #left elim left
     472  [1:
     473    #right >(BitVector_O … right) normalize #absurd destruct(absurd)
     474  |2:
     475    #n' #hd #tl #inductive_hypothesis #right
     476    cases (BitVector_Sn … right) #hd' * #tl' #right_refl
     477    >right_refl normalize
     478    cases hd normalize nodelta
     479    cases hd' normalize nodelta
     480    [2,3:
     481      #_ @nmk #absurd destruct(absurd)
     482    ]
     483    change with (eq_bv ??? = false → ?)
     484    #relevant lapply (inductive_hypothesis … relevant)
     485    #tl_neq_assm @nmk #tl_eq_assm cases tl_neq_assm
     486    #tl_eq_assm' @tl_eq_assm' destruct(tl_eq_assm) %
     487  ]
     488qed.
     489   
     490lemma eq_accumulator_address_map_entry_false_to_neq:
     491  ∀left: accumulator_address_map_entry.
     492  ∀right: accumulator_address_map_entry.
     493    eq_accumulator_address_map_entry left right = false → left ≠ right.
     494  #left #right cases left cases right
     495  [1:
     496    normalize #absurd destruct(absurd)
     497  |2,3:
     498    #upper_lower #word normalize #_
     499    @nmk #absurd destruct(absurd)
     500  |4:
     501    #upper_lower #word #upper_lower' #word' normalize
     502    cases upper_lower' normalize nodelta
     503    cases upper_lower normalize nodelta
     504    [2,3:
     505      #_ @nmk #absurd destruct(absurd)
     506    ]
     507    change with (eq_bv ??? = false → ?)
     508    #eq_bv_false_assm lapply(eq_bv_false_to_neq … eq_bv_false_assm)
     509    #word_neq_assm @nmk #address_eq_assm cases word_neq_assm
     510    #word_eq_assm @word_eq_assm destruct(address_eq_assm) %
     511  ]
     512qed.
     513
    386514(* XXX: changed this type.  Bool specifies whether byte is first or second
    387515        component of an address, and the Word is the pseudoaddress that it
     
    389517        A.
    390518*)
    391 definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)).
     519definition internal_pseudo_address_map ≝ list (Byte × (upper_lower × Word)) × accumulator_address_map_entry.
    392520
    393521include alias "ASM/BitVectorTrie.ma".
     
    402530
    403531axiom low_internal_ram_of_pseudo_internal_ram_hit:
    404  ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀high: bool. ∀points_to: Word. ∀addr:BitVector 7.
    405   assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … (〈high, points_to〉)  →
     532 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7.
     533  assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉  →
    406534   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
    407535   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
     
    409537   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
    410538   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in
    411      if high then
     539     if eq_upper_lower upper_lower upper then
    412540       (pbl = higher) ∧ (bl = phigher)
    413541     else
     
    426554   match addr with
    427555    [ DIRECT d ⇒
    428        ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
    429        ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
     556        if eq_bv … d (bitvector_of_nat … 224) then
     557          ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) ∧ eq_accumulator_address_map_entry (\snd M) data
     558        else
     559         ¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
    430560    | INDIRECT i ⇒
    431561       let d ≝ get_register … s [[false;false;i]] in
    432        ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
    433        ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
     562       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M))
    434563    | EXT_INDIRECT _ ⇒ true
    435     | REGISTER _ ⇒ true
    436     | ACC_A ⇒ match \snd M with [ None ⇒ true | _ ⇒ false ]
     564    | REGISTER r ⇒
     565        let address ≝ bit_address_of_register … s r in
     566          ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M)
     567    | ACC_A ⇒ match \snd M with [ data ⇒ true | _ ⇒ false ]
    437568    | ACC_B ⇒ true
    438569    | DPTR ⇒ true
     
    448579    | RELATIVE _ ⇒ true
    449580    | ADDR11 _ ⇒ true
    450     | ADDR16 _ ⇒ true ].
     581    | ADDR16 _ ⇒ true
     582    ].
    451583   
    452584definition next_internal_pseudo_address_map0 ≝
     
    464596      let a' ≝ addr_of a s in
    465597      let 〈callM, accM〉 ≝ M in
    466          Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈false, a'〉〉::
    467                  〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈true, a'〉〉::callM, accM〉
     598         Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, a'〉〉::
     599                 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈upper, a'〉〉::callM, accM〉
    468600    | Mov _ _ ⇒ Some … M
    469601    | Instruction instr ⇒
    470        match instr with
    471         [ ADD addr1 addr2 ⇒
    472            if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     602      match instr return λx. option internal_pseudo_address_map with
     603       [ ADD addr1 addr2 ⇒
     604         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     605           Some ? M
     606         else
     607           None ?
     608       | ADDC addr1 addr2 ⇒
     609         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     610           Some ? M
     611         else
     612           None ?
     613       | SUBB addr1 addr2 ⇒
     614         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     615           Some ? M
     616         else
     617           None ?
     618       | INC addr1 ⇒
     619         if addressing_mode_ok T M ? s addr1 then
     620           Some ? M
     621         else
     622           None ?
     623       | DEC addr1 ⇒
     624         if addressing_mode_ok T M … s addr1 then
     625           Some ? M
     626         else
     627           None ?
     628       | MUL addr1 addr2 ⇒
     629         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     630           Some ? M
     631         else
     632           None ?
     633       | DIV addr1 addr2 ⇒
     634         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     635           Some ? M
     636         else
     637           None ?
     638       | DA addr1 ⇒
     639         if addressing_mode_ok T M … s addr1 then
     640           Some ? M
     641         else
     642           None ?
     643       | JC addr1 ⇒ Some ? M
     644       | JNC addr1 ⇒ Some ? M
     645       | JB addr1 addr2 ⇒ Some ? M
     646       | JNB addr1 addr2 ⇒ Some ? M
     647       | JBC addr1 addr2 ⇒ Some ? M
     648       | JZ addr1 ⇒ Some ? M
     649       | JNZ addr1 ⇒ Some ? M
     650       | CJNE addr1 addr2 ⇒
     651         match addr1 with
     652         [ inl l ⇒
     653           let 〈left, right〉 ≝ l in
     654             if addressing_mode_ok T M … s left ∧ addressing_mode_ok T M … s right then
     655               Some ? M
     656             else if ¬(addressing_mode_ok T M … s left) ∧ ¬(addressing_mode_ok T M … s right) then
     657               Some ? M
     658             else
     659               None ?
     660         | inr r ⇒
     661           let 〈left, right〉 ≝ r in
     662             if addressing_mode_ok T M … s left ∧ addressing_mode_ok T M … s right then
     663               Some ? M
     664             else if ¬(addressing_mode_ok T M … s left) ∧ ¬(addressing_mode_ok T M … s right) then
     665               Some ? M
     666             else
     667               None ?
     668         ]
     669       | DJNZ addr1 addr2 ⇒
     670         if addressing_mode_ok T M … s addr1 then
     671           Some ? M
     672         else
     673           None ?
     674       | CLR addr1 ⇒
     675         if addressing_mode_ok T M … s addr1 then
     676           Some ? M
     677         else
     678           None ?
     679       | CPL addr1 ⇒
     680         if addressing_mode_ok T M … s addr1 then
     681           Some ? M
     682         else
     683           None ?
     684       | RL addr1 ⇒
     685         if addressing_mode_ok T M … s addr1 then
     686           Some ? M
     687         else
     688           None ?
     689       | RLC addr1 ⇒
     690         if addressing_mode_ok T M … s addr1 then
     691           Some ? M
     692         else
     693           None ?
     694       | RR addr1 ⇒
     695         if addressing_mode_ok T M … s addr1 then
     696           Some ? M
     697         else
     698           None ?
     699       | RRC addr1 ⇒
     700         if addressing_mode_ok T M … s addr1 then
     701           Some ? M
     702         else
     703           None ?
     704       | SWAP addr1 ⇒
     705         if addressing_mode_ok T M … s addr1 then
     706           Some ? M
     707         else
     708           None ?
     709       | SETB addr1 ⇒
     710         if addressing_mode_ok T M … s addr1 then
     711           Some ? M
     712         else
     713           None ?
     714       (* XXX: need to track addresses pushed and popped off the stack? *)
     715       | PUSH addr1 ⇒
     716         let 〈callM, accM〉 ≝ M in
     717         match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
     718         [ DIRECT d ⇒ λproof.
     719           let extended ≝ pad 8 8 d in
     720             Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, extended〉〉::callM, accM〉
     721         | _ ⇒ λother: False. ⊥
     722         ] (subaddressing_modein … addr1)
     723       | POP addr1 ⇒ Some … M
     724       | XCH addr1 addr2 ⇒
     725         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     726           Some ? M
     727         else
     728           None ?
     729       | XCHD addr1 addr2 ⇒
     730         if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     731           Some ? M
     732         else
     733           None ?
     734      | RET ⇒
     735        let 〈callM, accM〉 ≝ M in
     736        let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
     737        let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
     738          if sp_plus_1 ∧ sp_plus_2 then
     739            Some … M
     740          else
     741            None ?
     742      | RETI ⇒
     743        let 〈callM, accM〉 ≝ M in
     744        let sp_plus_1 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
     745        let sp_plus_2 ≝ assoc_list_exists ?? (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
     746          if sp_plus_1 ∧ sp_plus_2 then
     747            Some … M
     748          else
     749            None ?
     750      | NOP ⇒ Some … M
     751      | MOVX addr1 ⇒ Some … M
     752      | XRL addr1 ⇒
     753        match addr1 with
     754        [ inl l ⇒
     755          let 〈acc_a, others〉 ≝ l in
     756          let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
     757          let others_ok ≝ addressing_mode_ok T M … s others in
     758          if acc_a_ok ∧ others_ok then
    473759            Some ? M
    474            else
     760          else
    475761            None ?
    476         | ADDC addr1 addr2 ⇒
    477            if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     762        | inr r ⇒
     763          let 〈direct, others〉 ≝ r in
     764          let direct_ok ≝ addressing_mode_ok T M … s direct in
     765          let others_ok ≝ addressing_mode_ok T M … s others in
     766          if direct_ok ∧ others_ok then
    478767            Some ? M
    479            else
     768          else
    480769            None ?
    481         | SUBB addr1 addr2 ⇒
    482            if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     770        ]
     771      | ORL addr1 ⇒
     772        match addr1 with
     773        [ inl l ⇒
     774          match l with
     775          [ inl l ⇒
     776            let 〈acc_a, others〉 ≝ l in
     777            let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
     778            let others_ok ≝ addressing_mode_ok T M … s others in
     779            if acc_a_ok ∧ others_ok then
     780              Some ? M
     781            else
     782              None ?
     783          | inr r ⇒
     784            let 〈direct, others〉 ≝ r in
     785            let direct_ok ≝ addressing_mode_ok T M … s direct in
     786            let others_ok ≝ addressing_mode_ok T M … s others in
     787            if direct_ok ∧ others_ok then
     788              Some ? M
     789            else
     790              None ?
     791          ]
     792        | inr r ⇒
     793          let 〈carry, others〉 ≝ r in
     794          let carry_ok ≝ addressing_mode_ok T M … s carry in
     795          let others_ok ≝ addressing_mode_ok T M … s others in
     796          if carry_ok ∧ others_ok then
    483797            Some ? M
    484            else
    485             None ?       
    486         | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
     798          else
     799            None ?
     800        ]
     801      | ANL addr1 ⇒
     802        match addr1 with
     803        [ inl l ⇒
     804          match l with
     805          [ inl l ⇒
     806            let 〈acc_a, others〉 ≝ l in
     807            let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
     808            let others_ok ≝ addressing_mode_ok T M … s others in
     809            if acc_a_ok ∧ others_ok then
     810              Some ? M
     811            else
     812              None ?
     813          | inr r ⇒
     814            let 〈direct, others〉 ≝ r in
     815            let direct_ok ≝ addressing_mode_ok T M … s direct in
     816            let others_ok ≝ addressing_mode_ok T M … s others in
     817            if direct_ok ∧ others_ok then
     818              Some ? M
     819            else
     820              None ?
     821          ]
     822        | inr r ⇒
     823          let 〈carry, others〉 ≝ r in
     824          let carry_ok ≝ addressing_mode_ok T M … s carry in
     825          let others_ok ≝ addressing_mode_ok T M … s others in
     826          if carry_ok ∧ others_ok then
     827            Some ? M
     828          else
     829            None ?
     830        ]
     831      | MOV addr1 ⇒ Some … M
     832      ]
     833    ].
     834    cases other
     835qed.
    487836
    488837definition next_internal_pseudo_address_map ≝
     
    509858  λsigma: Word → Word.
    510859    match \snd M with
    511     [ None ⇒ sfrs
    512     | Some s ⇒
    513       let 〈high, address〉 ≝ s in
     860    [ data ⇒ sfrs
     861    | address upper_lower address ⇒
    514862      let index ≝ sfr_8051_index SFR_ACC_A in
    515       let 〈upper, lower〉 ≝ vsplit ? 8 8 (sigma address) in
    516         if high then
    517           set_index Byte 19 sfrs index upper ?
     863      let 〈high, low〉 ≝ vsplit ? 8 8 (sigma address) in
     864        if eq_upper_lower upper_lower upper then
     865          set_index Byte 19 sfrs index high ?
    518866        else
    519           set_index Byte 19 sfrs index lower ?
     867          set_index Byte 19 sfrs index low ?
    520868    ].
    521869  //
     
    640988*)
    641989
    642 (* XXX: check values returned for conditional jumps below! *)
     990(* XXX: check values returned for conditional jumps below! They are wrong,
     991        find correct values *)
    643992definition ticks_of0:
    644993    ∀p:pseudo_assembly_program.
    645       (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
     994      (Identifier → Word) → (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
    646995  λprogram: pseudo_assembly_program.
     996  λlookup_labels: Identifier → Word.
    647997  λsigma.
    648998  λpolicy.
     
    6531003      match instr with
    6541004      [ JC lbl ⇒
    655         if policy ppc then
    656           〈4, 4〉
    657         else
    658           〈2, 2〉
     1005        let lookup_address ≝ sigma (lookup_labels lbl) in
     1006        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1007        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1008          if sj_possible then
     1009            〈2, 2〉
     1010          else
     1011            〈4, 4〉
    6591012      | JNC lbl ⇒
    660         if policy ppc then
    661           〈4, 4〉
    662         else
    663           〈2, 2〉
     1013        let lookup_address ≝ sigma (lookup_labels lbl) in
     1014        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1015        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1016          if sj_possible then
     1017            〈2, 2〉
     1018          else
     1019            〈4, 4〉
    6641020      | JB bit lbl ⇒
    665         if policy ppc then
    666           〈4, 4〉
    667         else
    668           〈2, 2〉
     1021        let lookup_address ≝ sigma (lookup_labels lbl) in
     1022        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1023        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1024          if sj_possible then
     1025            〈2, 2〉
     1026          else
     1027            〈4, 4〉
    6691028      | JNB bit lbl ⇒
    670         if policy ppc then
    671           〈4, 4〉
    672         else
    673           〈2, 2〉
     1029        let lookup_address ≝ sigma (lookup_labels lbl) in
     1030        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1031        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1032          if sj_possible then
     1033            〈2, 2〉
     1034          else
     1035            〈4, 4〉
    6741036      | JBC bit lbl ⇒
    675         if policy ppc then
    676           〈4, 4〉
    677         else
    678           〈2, 2〉
     1037        let lookup_address ≝ sigma (lookup_labels lbl) in
     1038        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1039        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1040          if sj_possible then
     1041            〈2, 2〉
     1042          else
     1043            〈4, 4〉
    6791044      | JZ lbl ⇒
    680         if policy ppc then
    681           〈4, 4〉
    682         else
    683           〈2, 2〉
     1045        let lookup_address ≝ sigma (lookup_labels lbl) in
     1046        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1047        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1048          if sj_possible then
     1049            〈2, 2〉
     1050          else
     1051            〈4, 4〉
    6841052      | JNZ lbl ⇒
    685         if policy ppc then
    686           〈4, 4〉
    687         else
    688           〈2, 2〉
     1053        let lookup_address ≝ sigma (lookup_labels lbl) in
     1054        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1055        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1056          if sj_possible then
     1057            〈2, 2〉
     1058          else
     1059            〈4, 4〉
    6891060      | CJNE arg lbl ⇒
    690         if policy ppc then
    691           〈4, 4〉
    692         else
    693           〈2, 2〉
     1061        let lookup_address ≝ sigma (lookup_labels lbl) in
     1062        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1063        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1064          if sj_possible then
     1065            〈2, 2〉
     1066          else
     1067            〈4, 4〉
    6941068      | DJNZ arg lbl ⇒
    695         if policy ppc then
    696           〈4, 4〉
    697         else
    698           〈2, 2〉
     1069        let lookup_address ≝ sigma (lookup_labels lbl) in
     1070        let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1071        let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1072          if sj_possible then
     1073            〈2, 2〉
     1074          else
     1075            〈4, 4〉
    6991076      | ADD arg1 arg2 ⇒
    7001077        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
     
    7851162    | Cost cost ⇒ 〈0, 0〉
    7861163    | Jmp jmp ⇒
    787       if policy ppc then
    788         〈4, 4〉
     1164      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1165      let do_a_long ≝ policy ppc in
     1166      let lookup_address ≝ sigma (lookup_labels jmp) in
     1167      let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
     1168        if sj_possible ∧ ¬ do_a_long then
     1169          〈2, 2〉 (* XXX: SJMP *)
     1170        else
     1171        let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
     1172          if mj_possible ∧ ¬ do_a_long then
     1173            〈2, 2〉 (* XXX: AJMP *)
     1174          else
     1175            〈2, 2〉 (* XXX: LJMP *)
     1176    | Call call ⇒
     1177      (* XXX: collapse the branches as they are identical? *)
     1178      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     1179      let lookup_address ≝ sigma (lookup_labels call) in
     1180      let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
     1181      let do_a_long ≝ policy ppc in
     1182      if mj_possible ∧ ¬ do_a_long then
     1183        〈2, 2〉 (* ACALL *)
    7891184      else
    790         〈2, 2〉
    791     | Call call ⇒
    792       if policy ppc then
    793         〈4, 4〉
    794       else
    795         〈2, 2〉
     1185        〈2, 2〉 (* LCALL *)
    7961186    | Mov dptr tgt ⇒ 〈2, 2〉
    7971187    ].
     
    7991189definition ticks_of:
    8001190    ∀p:pseudo_assembly_program.
    801       (Word → Word) → (Word → bool) → ∀ppc:Word.
     1191      (Identifier → Word) → (Word → Word) → (Word → bool) → ∀ppc:Word.
    8021192       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
    8031193  λprogram: pseudo_assembly_program.
     1194  λlookup_labels.
    8041195  λsigma.
    8051196  λpolicy.
     
    8071198    let pseudo ≝ \snd program in
    8081199    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
    809      ticks_of0 program sigma policy ppc fetched.
     1200     ticks_of0 program lookup_labels sigma policy ppc fetched.
    8101201
    8111202(*
  • src/ASM/AssemblyProofSplit.ma

    r2143 r2160  
    360360  ∀sigma: Word → Word.
    361361  ∀policy: Word → bool.
    362     \snd M = (None …)
     362    \snd M = data
    363363      special_function_registers_8051 pseudo_assembly_program cm s =
    364364        special_function_registers_8051 (BitVectorTrie Byte 16)
     
    372372qed.
    373373
    374 lemma special_function_registers_8051_set_program_counter:
    375   ∀cm: pseudo_assembly_program.
    376   ∀ps: PreStatus pseudo_assembly_program cm.
    377   ∀v: Word.
    378   special_function_registers_8051 pseudo_assembly_program cm
    379    (set_program_counter pseudo_assembly_program cm ps v) =
    380      special_function_registers_8051 pseudo_assembly_program cm ps.
    381   #cm #ps #v %
    382 qed.
    383 
    384 (*
    385 lemma get_arg_8_status_of_pseudo_status:
     374lemma n_lt_19_elim_prop:
     375  ∀P: nat → Prop.
     376    P 0 → P 1 → P 2 → P 3 → P 4 → P 5 → P 6 → P 7 → P 8 → P 9 →
     377    P 10 → P 11 → P 12 → P 13 → P 14 → P 15 → P 16 → P 17 → P 18 →
     378      (∀n. n < 19 → P n).
     379  #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14
     380  #H15 #H16 #H17 #H18 #H19 #n
     381  cases n [1: // ]
     382  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
     383  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
     384  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
     385  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
     386  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
     387  #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ]
     388  #n' normalize in ⊢ (% → ?);
     389  #absurd repeat (lapply (le_S_S_to_le … absurd) #absurd)
     390  cases (lt_to_not_zero … absurd)
     391qed.
     392
     393lemma get_index_v_set_index_miss:
     394  ∀T: Type[0].
     395  ∀n, i, j: nat.
     396  ∀v: Vector T n.
     397  ∀b: T.
     398  ∀i_proof: i < n.
     399  ∀j_proof: j < n.
     400  i ≠ j →
     401    get_index_v T n (set_index T n v i b i_proof) j j_proof =
     402      get_index_v T n v j j_proof.
     403  #T #n #i #j #v lapply i lapply j elim v #i #j
     404  [1:
     405    #b #i_proof
     406    cases (lt_to_not_zero … i_proof)
     407  |2:
     408    #tl #inductive_hypothesis #j' #i' #b #i_proof #j_proof #i_neq_j
     409    lapply i_proof lapply i_neq_j cases i'
     410    [1:
     411      -i_neq_j #i_neq_j -i_proof #i_proof
     412      whd in match (set_index ??????);
     413      lapply j_proof lapply i_neq_j cases j'
     414      [1:
     415        #relevant @⊥ cases relevant -relevant #absurd @absurd %
     416      |2:
     417        #j' #_ -j_proof #j_proof %
     418      ]
     419    |2:
     420      #i' -i_neq_j #i_neq_j -i_proof #i_proof
     421      lapply j_proof lapply i_neq_j cases j'
     422      [1:
     423        #_ #j_proof %
     424      |2:
     425        #j' #i_neq_j #j_proof
     426        @inductive_hypothesis @nmk #relevant
     427        cases i_neq_j #absurd @absurd >relevant %
     428      ]
     429    ]
     430  ]
     431qed.
     432
     433lemma get_index_v_special_function_registers_8051_not_acc_a:
    386434  ∀M: internal_pseudo_address_map.
    387435  ∀cm: pseudo_assembly_program.
    388   ∀ps.
     436  ∀s: PreStatus pseudo_assembly_program cm.
    389437  ∀sigma: Word → Word.
    390438  ∀policy: Word → bool.
    391   ∀b: bool.
    392   ∀addr1: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; ext_indirect_dptr]].
    393     get_arg_8 (BitVectorTrie Byte 16)
    394      (code_memory_of_pseudo_assembly_program cm sigma policy)
    395      (status_of_pseudo_status M cm ps sigma policy) b addr1 =
    396     get_arg_8 pseudo_assembly_program cm ps b addr1.
    397   [2,3:
    398     @(subaddressing_mode_elim … addr1) try #w @I
     439  ∀n: nat.
     440  ∀proof: n < 19.
     441    n ≠ 17 →
     442   (get_index_v Byte 19
     443    (special_function_registers_8051 pseudo_assembly_program cm s) n
     444    proof =
     445   get_index_v Byte 19
     446     (special_function_registers_8051 (BitVectorTrie Byte 16)
     447       (code_memory_of_pseudo_assembly_program cm sigma policy)
     448       (status_of_pseudo_status M cm s sigma policy)) n
     449       proof).
     450  #M #cm #s #sigma #policy #n #proof lapply proof
     451  @(n_lt_19_elim_prop … proof) -proof #proof
     452  [18:
     453    #absurd @⊥ cases absurd -absurd #absurd @absurd %
    399454  ]
    400   #M #cm #ps #sigma #policy #b #addr1
    401   @(subaddressing_mode_elim … addr1)
    402   try #w
    403   [1:
    404     whd in ⊢ (??%%);
    405     @pair_elim #nu #nl #nu_nl_refl normalize nodelta
    406     @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
    407     cases (get_index_v bool ????) normalize nodelta try %
    408     cases daemon (* XXX: require axioms from Assembly.ma *)
    409   |2:
    410     whd in ⊢ (??%%);
    411     @pair_elim #nu #nl #nu_nl_refl normalize nodelta
    412     lapply (refl_to_jmrefl ??? nu_nl_refl) -nu_nl_refl #nu_nl_refl
    413     @(pair_replace ?????????? nu_nl_refl) [1: cases daemon (* XXX: !! *) ]
    414     @pair_elim #bit_one_v #three_bits #bit_one_v_three_bits_refl normalize nodelta
    415     cases (get_index_v bool ????) normalize nodelta
    416     cases daemon (* XXX: same as above *)
    417   |3:
    418     whd in ⊢ (??%%); @(bitvector_3_elim_prop … w)
    419     whd in match bit_address_of_register; normalize nodelta
    420     @pair_elim #un #ln #un_ln_refl
    421     cases (¬get_index_v bool ???? ∧ ¬get_index_v bool ????) normalize nodelta
    422     [1,3,5,7,9,11,13,15:
    423       cases daemon (* XXX: same as above *)
    424     |*:
    425       cases (¬get_index_v bool ???? ∧ get_index_v bool ????) normalize nodelta
    426       [1,3,5,7,9,11,13,15:
    427         cases daemon (* XXX: same as above *)
    428       |*:
    429         cases (get_index_v bool ???? ∧ get_index_v bool ????) normalize nodelta
    430         cases daemon (* XXX: same as above *)
    431       ]
    432     ]
    433   |4,5:
    434     whd in ⊢ (??%%); <status_of_pseudo_status_does_not_change_8051_sfrs %
    435   |6,7,8:
    436     %
    437   ]
    438 qed.
    439 *)
    440 
    441 (*
    442 lemma pi1_let_commute:
    443  ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c.
    444  pi1 … (let 〈x1,y1〉 ≝ c in t) = (let 〈x1,y1〉 ≝ c in pi1 … t).
    445  #A #B #C #P * #a #b * //
    446 qed.
    447 
    448 lemma pi1_let_as_commute:
    449  ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c.
    450  pi1 … (let 〈x1,y1〉 as H ≝ c in t) =
    451   (let 〈x1,y1〉 as H ≝ c in pi1 … t).
    452  #A #B #C #P * #a #b * //
    453 qed.
    454 
    455 lemma tech_pi1_let_as_commute:
    456  ∀A,B,C,P. ∀f. ∀c,c':A × B.
    457  ∀t: ∀a,b. 〈a,b〉=c → Σc:C.P c.
    458  ∀t': ∀a,b. 〈a,b〉=c' → Σc:C.P c.
    459   c=c' → (∀x,y,H,H'.t x y H = f (pi1 … (t' x y H'))) →
    460   pi1 … (let 〈x1,y1〉 as H ≝ c in t x1 y1 H) =
    461    f (pi1 … (let 〈x1,y1〉 as H ≝ c' in t' x1 y1 H)).
    462  #A #B #C #P #f * #a #b * #a' #b' #t #t' #EQ1 destruct normalize /2/
    463 qed.
    464 *)
     455  #_ cases s #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
     456  whd in match status_of_pseudo_status; normalize nodelta
     457  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     458  cases M #left #right cases right normalize nodelta try %
     459  -right * #address
     460  @pair_elim #high #low #high_low_refl normalize nodelta
     461  whd in match sfr_8051_index; normalize nodelta
     462  >get_index_v_set_index_miss try %
     463  #absurd destruct(absurd)
     464qed.
    465465
    466466include alias "arithmetics/nat.ma".
     
    477477  #fetch_many_assm whd in fetch_many_assm;
    478478  cases (eq_bv_eq … fetch_many_assm) assumption
     479qed.
     480
     481(* XXX: this needs an extra invariant relating address and word that we look
     482        up!
     483*)
     484definition map_lower_internal_ram_address_using_pseudo_address_map:
     485    ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝
     486  λM: internal_pseudo_address_map.
     487  λsigma: Word → Word.
     488  λaddress: Byte.
     489  λvalue: Byte.
     490  match assoc_list_lookup ?? address (eq_bv …) (\fst M) with
     491  [ None ⇒ value
     492  | Some upper_lower_word ⇒
     493    let 〈upper_lower, word〉 ≝ upper_lower_word in
     494    let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in
     495      if eq_upper_lower upper_lower upper then
     496        high
     497      else
     498        low
     499  ].
     500
     501lemma get_8051_sfr_status_of_pseudo_status:
     502  ∀M.
     503  ∀cm, ps, sigma, policy.
     504  ∀sfr.
     505    (sfr = SFR_ACC_A → \snd M = data) →
     506    get_8051_sfr (BitVectorTrie Byte 16)
     507      (code_memory_of_pseudo_assembly_program cm sigma policy)
     508      (status_of_pseudo_status M cm ps sigma policy) sfr =
     509    get_8051_sfr pseudo_assembly_program cm ps sfr.
     510  #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant
     511  [18:
     512     >relevant %
     513  ]
     514  cases sndM try % * #address
     515  whd in match get_8051_sfr;
     516  whd in match status_of_pseudo_status; normalize nodelta
     517  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     518  @pair_elim #upper #lower #upper_lower_refl
     519  @get_index_v_set_index_miss @nmk #relevant
     520  normalize in relevant; destruct(relevant)
     521qed.
     522
     523lemma bitvector_cases_hd_tl:
     524  ∀n: nat.
     525  ∀w: BitVector (S n).
     526   ∃hd: bool. ∃tl: BitVector n.
     527    w ≃ hd:::tl.
     528  #n #w cases (BitVector_Sn … w) #hd #relevant %{hd} @relevant
     529qed.
     530
     531lemma external_ram_set_bit_addressable_sfr:
     532  ∀M: Type[0].
     533  ∀cm: M.
     534  ∀ps.
     535  ∀w.
     536  ∀result: Byte.
     537    external_ram M cm
     538      (set_bit_addressable_sfr M cm ps w result) =
     539    external_ram M cm ps.
     540  #M #cm #ps #w #result cases daemon (* XXX: prove this with Russell in Status.ma!
     541  whd in match set_bit_addressable_sfr; normalize nodelta
     542  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
     543  cases (eqb ??) normalize nodelta [1: % ]
     544  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
     545  cases (eqb ??) normalize nodelta [1: % ]
     546  cases (eqb ??) normalize nodelta [1: % ]
     547  cases (eqb ??) normalize nodelta [1: % ]
     548  cases (eqb ??) normalize nodelta [1: % ]
     549  cases (eqb ??) normalize nodelta [1: % ]
     550  cases (eqb ??) normalize nodelta [1: % ]
     551  cases (eqb ??) normalize nodelta [1: % ]
     552  cases (eqb ??) normalize nodelta [1: % ]
     553  cases (eqb ??) normalize nodelta [1: % ]
     554  cases (eqb ??) normalize nodelta [1: % ]
     555  cases (eqb ??) normalize nodelta [1: % ]
     556  cases (eqb ??) normalize nodelta [1: % ]
     557  cases (eqb ??) normalize nodelta [1: % ]
     558  cases (eqb ??) normalize nodelta [1: % ]
     559  cases (eqb ??) normalize nodelta [1: % ]
     560  cases (eqb ??) normalize nodelta [1: % ]
     561  cases (eqb ??) normalize nodelta [1: % ]
     562  cases (eqb ??) normalize nodelta [1: % ]
     563  cases (eqb ??) normalize nodelta [1: % ]
     564  cases (eqb ??) normalize nodelta [1: % ]
     565  cases (eqb ??) normalize nodelta [1: % ]
     566  cases (eqb ??) normalize nodelta [1: % ]
     567  cases (eqb ??) normalize nodelta [1: % ]
     568  cases not_implemented *)
     569qed.
     570
     571lemma external_ram_set_arg_8:
     572  ∀M: Type[0].
     573  ∀cm: M.
     574  ∀ps.
     575  ∀addr1: [[direct; indirect; registr; acc_a; acc_b ]].
     576  ∀result.
     577    external_ram M cm (set_arg_8 M cm ps addr1 result) =
     578      external_ram M cm ps.
     579  [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     580  #M #cm #ps #addr1 #result
     581  @(subaddressing_mode_elim … addr1) try #w try %
     582  whd in ⊢ (??(???%)?); whd in ⊢ (??(???(???%))?); (* XXX: to be understood, slow match *)
     583  [1:
     584    cases (vsplit bool ???) #nu #nl normalize nodelta
     585    cases (vsplit bool ???) #ignore #three_bits normalize nodelta
     586    cases (get_index_v bool ????) normalize nodelta try %
     587    @external_ram_set_bit_addressable_sfr
     588  |2:
     589    cases (vsplit bool ???) #nu #nl normalize nodelta
     590    cases (vsplit bool ???) #ignore #three_bits normalize nodelta
     591    cases (get_index_v bool ????) normalize nodelta %
     592  ]
     593qed.
     594
     595lemma special_function_registers_8051_set_clock:
     596  ∀M: Type[0].
     597  ∀cm: M.
     598  ∀ps.
     599  ∀t.
     600    special_function_registers_8051 M cm (set_clock M cm ps t) =
     601      special_function_registers_8051 M cm ps.
     602  //
     603qed.
     604
     605lemma get_arg_8_pseudo_addressing_mode_ok:
     606  ∀M: internal_pseudo_address_map.
     607  ∀cm: pseudo_assembly_program.
     608  ∀ps: PreStatus pseudo_assembly_program cm.
     609  ∀sigma: Word → Word.
     610  ∀policy: Word → bool.
     611  ∀addr1: [[registr; direct]].
     612    addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →
     613      get_arg_8 (BitVectorTrie Byte 16)
     614        (code_memory_of_pseudo_assembly_program cm sigma policy)
     615        (status_of_pseudo_status M cm ps sigma policy) true addr1 =
     616      get_arg_8 pseudo_assembly_program cm ps true addr1.
     617  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     618  #M #cm #ps #sigma #policy #addr1
     619  @(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%);
     620  [1:
     621    whd in ⊢ (??%? → ??%?);
     622    whd in match bit_address_of_register; normalize nodelta
     623    @pair_elim #un #ln #un_ln_refl
     624    lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
     625    @(pair_replace ?????????? un_ln_refl)
     626    [1:
     627      whd in match get_8051_sfr; normalize nodelta
     628      whd in match sfr_8051_index; normalize nodelta
     629      @eq_f <get_index_v_special_function_registers_8051_not_acc_a
     630      try % #absurd destruct(absurd)
     631    |2:
     632      #assembly_mode_ok_refl
     633      >low_internal_ram_of_pseudo_internal_ram_miss
     634      [1:
     635        %
     636      |2:
     637        cases (assoc_list_exists ?????) in assembly_mode_ok_refl; normalize nodelta
     638        #absurd try % @sym_eq assumption
     639      ]
     640    ]
     641  |2:
     642    #addressing_mode_ok_refl whd in ⊢ (??%?);
     643    @pair_elim #nu #nl #nu_nl_refl normalize nodelta
     644    @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
     645    inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
     646    [1:
     647      whd in ⊢ (??%%); normalize nodelta
     648      cases (eqb ??) normalize nodelta [1: % ]
     649      cases (eqb ??) normalize nodelta [1: % ]
     650      cases (eqb ??) normalize nodelta [1: % ]
     651      cases (eqb ??) normalize nodelta [1: % ]
     652      cases (eqb ??) normalize nodelta [1:
     653        @get_8051_sfr_status_of_pseudo_status
     654        #absurd destruct(absurd)
     655      ]
     656      cases (eqb ??) normalize nodelta [1:
     657        @get_8051_sfr_status_of_pseudo_status
     658        #absurd destruct(absurd)
     659      ]
     660      cases (eqb ??) normalize nodelta [1:
     661        @get_8051_sfr_status_of_pseudo_status
     662        #absurd destruct(absurd)
     663      ]
     664      cases (eqb ??) normalize nodelta [1:
     665        @get_8051_sfr_status_of_pseudo_status
     666        #absurd destruct(absurd)
     667      ]
     668      cases (eqb ??) normalize nodelta [1:
     669        @get_8051_sfr_status_of_pseudo_status
     670        #absurd destruct(absurd)
     671      ]
     672      cases (eqb ??) normalize nodelta [1: % ]
     673      cases (eqb ??) normalize nodelta [1: % ]
     674      cases (eqb ??) normalize nodelta [1: % ]
     675      cases (eqb ??) normalize nodelta [1: % ]
     676      cases (eqb ??) normalize nodelta [1: % ]
     677      cases (eqb ??) normalize nodelta [1:
     678        @get_8051_sfr_status_of_pseudo_status
     679        #absurd destruct(absurd)
     680      ]
     681      cases (eqb ??) normalize nodelta [1:
     682        @get_8051_sfr_status_of_pseudo_status
     683        #absurd destruct(absurd)
     684      ]
     685      cases (eqb ??) normalize nodelta [1:
     686        @get_8051_sfr_status_of_pseudo_status
     687        #absurd destruct(absurd)
     688      ]
     689      cases (eqb ??) normalize nodelta [1:
     690        @get_8051_sfr_status_of_pseudo_status
     691        #absurd destruct(absurd)
     692      ]
     693      cases (eqb ??) normalize nodelta [1:
     694        @get_8051_sfr_status_of_pseudo_status
     695        #absurd destruct(absurd)
     696      ]
     697      cases (eqb ??) normalize nodelta [1:
     698        @get_8051_sfr_status_of_pseudo_status
     699        #absurd destruct(absurd)
     700      ]
     701      cases (eqb ??) normalize nodelta [1:
     702        @get_8051_sfr_status_of_pseudo_status
     703        #absurd destruct(absurd)
     704      ]
     705      cases (eqb ??) normalize nodelta [1:
     706        @get_8051_sfr_status_of_pseudo_status
     707        #absurd destruct(absurd)
     708      ]
     709      cases (eqb ??) normalize nodelta [1:
     710        @get_8051_sfr_status_of_pseudo_status
     711        #absurd destruct(absurd)
     712      ]
     713      cases (eqb ??) normalize nodelta [1:
     714        @get_8051_sfr_status_of_pseudo_status
     715        #absurd destruct(absurd)
     716      ]
     717      inversion (eqb ??) #eqb_refl normalize nodelta [1:
     718        @get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl
     719        whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl)
     720        >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
     721        #assoc_list_assm cases (conjunction_true … assoc_list_assm) #_
     722        #relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) %
     723      ]
     724      cases (eqb ??) normalize nodelta [1:
     725        @get_8051_sfr_status_of_pseudo_status
     726        #absurd destruct(absurd)
     727      ] %
     728    |2:
     729      lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant
     730      whd in match status_of_pseudo_status; normalize nodelta
     731      >low_internal_ram_of_pseudo_internal_ram_miss try %
     732      cut(arg = false:::(three_bits@@nl))
     733      [1:
     734        <get_index_v_refl
     735        cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits)
     736        [1:
     737          cut(ignore = [[get_index_v bool 4 nu 0 ?]])
     738          [1:
     739            @le_S_S @le_O_n
     740          |2:
     741            cut(ignore = \fst (vsplit bool 1 3 nu))
     742            [1:
     743              >ignore_three_bits_refl %
     744            |2:
     745              #ignore_refl >ignore_refl
     746              cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl
     747              >nu_refl %
     748            ]
     749          |3:
     750            #ignore_refl >ignore_refl in ignore_three_bits_refl;
     751            #relevant lapply (vsplit_ok ?????? (sym_eq … relevant))
     752            #nu_refl <nu_refl %
     753          ]
     754        |2:
     755          #nu_refl change with (? = (?:::three_bits)@@?) <nu_refl
     756          @sym_eq @vsplit_ok >nu_nl_refl %
     757        ]
     758      |2:
     759        #arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant;
     760        normalize nodelta
     761        [1:
     762          cases (eq_bv ???) normalize #absurd destruct(absurd)
     763        |2:
     764          #_ %
     765        ]
     766      ]
     767    ]
     768  ]
     769qed.
     770
     771lemma special_function_registers_8051_set_program_counter:
     772  ∀M: Type[0].
     773  ∀cm: M.
     774  ∀ps.
     775  ∀pc: Word.
     776    special_function_registers_8051 M cm (set_program_counter M cm ps pc) =
     777      special_function_registers_8051 M cm ps.
     778  //
     779qed.
     780
     781lemma special_function_registers_8052_set_program_counter:
     782  ∀M: Type[0].
     783  ∀cm: M.
     784  ∀ps.
     785  ∀pc: Word.
     786    special_function_registers_8052 M cm (set_program_counter M cm ps pc) =
     787      special_function_registers_8052 M cm ps.
     788  //
     789qed.
     790
     791lemma set_index_set_index_commutation:
     792  ∀A: Type[0].
     793  ∀n: nat.
     794  ∀v: Vector A n.
     795  ∀m, o: nat.
     796  ∀m_lt_proof: m < n.
     797  ∀o_lt_proof: o < n.
     798  ∀e, f: A.
     799    m ≠ o →
     800      set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof =
     801        set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof.
     802  #A #n #v elim v
     803  [1:
     804    #m #o #m_lt_proof
     805    normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof)
     806  |2:
     807    #n' #hd #tl #inductive_hypothesis
     808    #m #o
     809    cases m cases o
     810    [1:
     811      #m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant
     812      @relevant %
     813    |2,3:
     814      #o' normalize //
     815    |4:
     816      #m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm
     817      normalize @eq_f @inductive_hypothesis @nmk #relevant
     818      >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) %
     819    ]
     820  ]
     821qed.
     822
     823lemma special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051:
     824  ∀M: internal_pseudo_address_map.
     825  ∀cm: pseudo_assembly_program.
     826  ∀ps.
     827  ∀sigma: Word → Word.
     828  ∀policy: Word → bool.
     829  ∀sfr.
     830  ∀result: Byte.
     831    eqb (sfr_8051_index sfr) (sfr_8051_index SFR_ACC_A) = false →
     832      special_function_registers_8051 (BitVectorTrie Byte 16)
     833        (code_memory_of_pseudo_assembly_program cm sigma policy)
     834        (set_8051_sfr (BitVectorTrie Byte 16)
     835        (code_memory_of_pseudo_assembly_program cm sigma policy)
     836        (status_of_pseudo_status M cm ps sigma policy) sfr result) =
     837      sfr_8051_of_pseudo_sfr_8051 M
     838        (special_function_registers_8051 pseudo_assembly_program cm
     839        (set_8051_sfr pseudo_assembly_program cm ps sfr result)) sigma.
     840  #M #cm #ps #sigma #policy #sfr #result #sfr_neq_assm
     841  whd in match (set_8051_sfr ?????);
     842  cases M #callM * try % #upper_lower #address
     843  whd in match (special_function_registers_8051 ???);
     844  whd in match (sfr_8051_of_pseudo_sfr_8051 ???);
     845  @pair_elim #high #low #high_low_refl normalize nodelta
     846  cases (eq_upper_lower ??) normalize nodelta
     847  whd in match (set_8051_sfr ?????);
     848  @set_index_set_index_commutation @nmk #relevant
     849  @(absurd ? relevant (eqb_false_to_not_eq ?? sfr_neq_assm))
     850qed.
     851
     852lemma special_function_registers_8051_set_arg_8:
     853  ∀M: internal_pseudo_address_map.
     854  ∀cm: pseudo_assembly_program.
     855  ∀ps.
     856  ∀sigma: Word → Word.
     857  ∀policy: Word → bool.
     858  ∀addr1: [[ registr; direct ]].
     859  ∀result.
     860    addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →
     861    special_function_registers_8051 (BitVectorTrie Byte 16)
     862      (code_memory_of_pseudo_assembly_program cm sigma policy)
     863      (set_arg_8 (BitVectorTrie Byte 16)
     864        (code_memory_of_pseudo_assembly_program cm sigma policy)
     865        (status_of_pseudo_status M cm ps sigma policy) addr1 result) =
     866   sfr_8051_of_pseudo_sfr_8051 M
     867     (special_function_registers_8051 pseudo_assembly_program cm
     868     (set_arg_8 pseudo_assembly_program cm ps addr1 result)) sigma.
     869  cases daemon
     870(*
     871  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     872  #M #cm #ps #sigma #policy #addr1 #result
     873  @(subaddressing_mode_elim … addr1) #w #addressing_mode_ok_refl try %
     874  whd in match (set_arg_8 ?????); whd in ⊢ (??(???(???%))?);
     875  whd in match (set_arg_8 ?????) in ⊢ (???%); whd in ⊢ (???(??(???(???%))?));
     876  cases (vsplit bool ???) #nu #nl normalize nodelta
     877  cases (vsplit bool ???) #ignore #three_bits normalize nodelta
     878  cases (get_index_v bool ????) normalize nodelta try %
     879  whd in match (set_bit_addressable_sfr ?????); whd in match (set_bit_addressable_sfr ?????) in ⊢ (???%);
     880  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
     881  cases (eqb ??) normalize nodelta [1: % ]
     882  cases (eqb ??) normalize nodelta [1: cases not_implemented ]
     883  cases (eqb ??) normalize nodelta [1: % ]
     884  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     885  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     886  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     887  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     888  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     889  cases (eqb ??) normalize nodelta [1: % ]
     890  cases (eqb ??) normalize nodelta [1: % ]
     891  cases (eqb ??) normalize nodelta [1: % ]
     892  cases (eqb ??) normalize nodelta [1: % ]
     893  cases (eqb ??) normalize nodelta [1: % ]
     894  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     895  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     896  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     897  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     898  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     899  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     900  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     901  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     902  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     903  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     904  inversion (eqb ??) #eqb_refl normalize nodelta [1:
     905    whd in addressing_mode_ok_refl:(??%?); <(eqb_true_to_eq … eqb_refl) in addressing_mode_ok_refl;
     906    >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
     907    #relevant cases (conjunction_true … relevant) #_ #eq_acc_assm
     908    whd in match (status_of_pseudo_status ?????);
     909    whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     910    >(eq_accumulator_address_map_entry_true_to_eq … eq_acc_assm) normalize nodelta %
     911  ]
     912  cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 %  ]
     913  cases not_implemented *)
    479914qed.
    480915
     
    507942  ∀fetch_pseudo_refl: \fst  (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr.
    508943  ∀ticks: nat × nat.
    509   ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr).
     944  ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_datalabels sigma policy ppc (Instruction instr).
    510945  ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
    511946  ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x).
     
    9331368                  s
    9341369           ] (refl … instr))
    935   try (cases(other))
     1370  try cases other
    9361371  try assumption (*20s*)
    9371372  try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
     
    9551390  [1,3:
    9561391    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
    957     whd in ⊢ (??%?);
    9581392    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
    9591393    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
     1394    whd in ⊢ (??%?);
    9601395    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     1396    lapply maps_assm whd in ⊢ (??%? → ?);
     1397    inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta
     1398    [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl -M'
    9611399    (* XXX: work on the left hand side *)
    9621400    @(pair_replace ?????????? p) normalize nodelta
    9631401    [1,3:
    964       >(get_arg_8_set_program_counter … true addr1) in ⊢ (??%?);
    965       [2,4: (* /2 by _/ *) cases daemon ] @eq_f3 [2,3,5,6: % ]
    966       whd in ⊢ (??%?); @(subaddressing_mode_elim … addr1)
    967       #arg normalize nodelta whd in ⊢ (???%);
    968       [1,3:
    969         whd in match get_register; normalize nodelta
    970         @(bitvector_3_elim_prop … arg)
    971         whd in match bit_address_of_register; normalize nodelta
    972         @pair_elim #un #ln #un_ln_refl
    973         lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
    974         @(pair_replace ?????????? un_ln_refl)
    975         [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31:
    976           whd in match get_8051_sfr; normalize nodelta
    977           whd in match sfr_8051_index; normalize nodelta
    978           @eq_f <status_of_pseudo_status_does_not_change_8051_sfrs
    979           >EQs
    980           [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31:
    981             /demod nohyps/ %
    982           |*:
    983             cases daemon
    984           ]
    985         |*:
    986           >low_internal_ram_of_pseudo_internal_ram_miss
    987           cases daemon
    988           (* XXX: require axioms about low_internal_ram_of_pseudo_low_internal_ram *)         
     1402      >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1)
     1403      [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1404      >(get_arg_8_set_program_counter … true addr1)
     1405      [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1406      @get_arg_8_pseudo_addressing_mode_ok assumption
     1407    |2,4:
     1408      >p1 normalize nodelta >EQs
     1409      alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)".
     1410      >set_program_counter_status_of_pseudo_status
     1411       whd in ⊢ (??%%);
     1412      @split_eq_status
     1413      [1,10:
     1414        whd in ⊢ (??%%); >set_arg_8_set_program_counter
     1415        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1416        >low_internal_ram_set_program_counter
     1417        [1:
     1418          >low_internal_ram_set_program_counter
     1419          (* XXX: ??? *)
     1420        |2:
     1421          >low_internal_ram_set_clock
     1422          (* XXX: ??? *)
    9891423        ]
    990       |2,4:
    991         @pair_elim #nu #nl #nu_nl_refl
    992         lapply (refl_to_jmrefl ??? nu_nl_refl) -nu_nl_refl #nu_nl_refl
    993         @pair_elim #ignore #three_bits #ignore_three_bits_refl
    994         lapply (refl_to_jmrefl ??? ignore_three_bits_refl) -ignore_three_bits_refl #ignore_three_bits_refl
    995         inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
    996         [1,3:
    997           @(pair_replace ?????????? ignore_three_bits_refl) try %
    998           >get_index_v_refl normalize nodelta >EQs %
    999         |2,4:
    1000           @(pair_replace ?????????? ignore_three_bits_refl) try %
    1001           >get_index_v_refl normalize nodelta >EQs
    1002           cases daemon
    1003           (* XXX: require axioms about low_internal_ram as above *)
     1424      |2,11:
     1425        whd in ⊢ (??%%); >set_arg_8_set_program_counter
     1426        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1427        >high_internal_ram_set_program_counter
     1428        [1:
     1429          >high_internal_ram_set_program_counter
     1430          (* XXX: ??? *)
     1431        |2:
     1432          >high_internal_ram_set_clock
     1433          (* XXX: ??? *)
    10041434        ]
     1435      |3,12:
     1436        whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%);
     1437        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1438        >(external_ram_set_arg_8 ??? addr1)
     1439        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     1440      |4,13:
     1441        whd in ⊢ (??%%); >EQaddr_of normalize nodelta
     1442        [1:
     1443          >program_counter_set_program_counter
     1444          >set_arg_8_set_program_counter
     1445          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1446          >set_clock_set_program_counter >program_counter_set_program_counter
     1447          change with (add ??? = ?)
     1448          (* XXX: ??? *)
     1449        |2:
     1450          >set_arg_8_set_program_counter
     1451          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1452          >program_counter_set_program_counter
     1453          >set_arg_8_set_program_counter
     1454          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1455          >set_clock_set_program_counter >program_counter_set_program_counter
     1456          >sigma_increment_commutation <EQppc
     1457          whd in match (assembly_1_pseudoinstruction ??????);
     1458          whd in match (expand_pseudo_instruction ??????);
     1459          (* XXX: ??? *)
     1460        ]
     1461      |5,14:
     1462        whd in match (special_function_registers_8051 ???);
     1463        [1:
     1464          >special_function_registers_8051_set_program_counter
     1465          >special_function_registers_8051_set_clock
     1466          >set_arg_8_set_program_counter in ⊢ (???%);
     1467          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1468          >special_function_registers_8051_set_program_counter
     1469          >set_arg_8_set_program_counter
     1470          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1471          >special_function_registers_8051_set_program_counter
     1472          @special_function_registers_8051_set_arg_8 assumption
     1473        |2:
     1474          >special_function_registers_8051_set_clock
     1475          >set_arg_8_set_program_counter
     1476          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1477          >set_arg_8_set_program_counter
     1478          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1479          >special_function_registers_8051_set_program_counter
     1480          >special_function_registers_8051_set_program_counter
     1481          @special_function_registers_8051_set_arg_8 assumption
     1482        ]
     1483      |6,15:
     1484        whd in match (special_function_registers_8052 ???);
     1485        whd in match (special_function_registers_8052 ???) in ⊢ (???%);
     1486        [1:
     1487          >set_arg_8_set_program_counter
     1488          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1489          >set_arg_8_set_program_counter
     1490          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1491          >special_function_registers_8052_set_program_counter
     1492          >special_function_registers_8052_set_program_counter
     1493          @special_function_registers_8052_set_arg_8 assumption
     1494        |2:
     1495          whd in ⊢ (??%%);
     1496          >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption
     1497        ]
     1498        (* XXX: we need special_function_registers_8052_set_arg_8 *)
     1499      |7,16:
     1500        whd in match (p1_latch ???);
     1501        whd in match (p1_latch ???) in ⊢ (???%);
     1502        (* XXX: we need p1_latch_8052_set_arg_8 *)
     1503      |8,17:
     1504        whd in match (p3_latch ???);
     1505        whd in match (p3_latch ???) in ⊢ (???%);
     1506        (* XXX: we need p3_latch_8052_set_arg_8 *)
     1507      |9:
     1508        >clock_set_clock
     1509        >clock_set_program_counter in ⊢ (???%); >clock_set_clock
     1510        >EQticks <instr_refl @eq_f2
     1511        [1:
     1512          whd in ⊢ (??%%); whd in match (ticks_of0 ??????);
     1513        |2:
     1514          (* XXX: we need clock_set_arg_8 *)
     1515        ]
     1516      |18:
    10051517      ]
    10061518    ]
     
    10181530    |7,16,25,34:
    10191531    |8,17,26,35:
    1020       whd in ⊢ (??%%);
     1532      whd in ⊢ (??%%);maps_assm
    10211533     
    10221534    |9,18,27,36:
  • src/ASM/Interpret.ma

    r2130 r2160  
    944944    try (@or_intror //)
    945945    try #_
    946     try /demod nohyps by clock_set_clock,clock_set_8051_sfr,set_arg_8_ok,set_arg_1_ok,
     946    try /demod nohyps by clock_set_clock,clock_set_8051_sfr,clock_set_arg_8,set_arg_1_ok,
    947947                         program_counter_set_8051_sfr,program_counter_set_arg_1/
    948948    try (% @I) try (@or_introl % @I) try (@or_intror % @I) //
  • src/ASM/Status.ma

    r2139 r2160  
    617617qed.
    618618
    619 definition set_bit_addressable_sfr ≝
     619definition set_bit_addressable_sfr':
     620    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte →
     621      Σs':PreStatus M code_memory.
     622        clock … code_memory s = clock … code_memory s' ∧
     623        program_counter … code_memory s = program_counter … code_memory s' ≝
    620624  λM: Type[0].
    621625  λcode_memory:M.
     
    625629    let address ≝ nat_of_bitvector … b in
    626630      if (eqb address 128) then
    627         ?
     631        match not_implemented in False with [ ]
    628632      else if (eqb address 144) then
    629633        let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
     
    631635          status_2
    632636      else if (eqb address 160) then
    633         ?
     637        match not_implemented in False with [ ]
    634638      else if (eqb address 176) then
    635639        let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
     
    681685        set_8051_sfr ?? s SFR_ACC_B v
    682686      else
    683         ?.
    684       cases not_implemented
     687        match not_implemented in False with [ ].
     688  /2 by refl, pair_destruct/
     689qed.
     690
     691definition set_bit_addressable_sfr:
     692    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte →
     693      PreStatus M code_memory ≝ set_bit_addressable_sfr'.
     694
     695lemma clock_set_bit_addressable_sfr:
     696    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀b: Byte. ∀v: Byte.
     697        clock … code_memory s = clock … code_memory (set_bit_addressable_sfr M code_memory s b v).
     698  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
     699  cases (set_bit_addressable_sfr' ?????) #s' * //
     700qed.
     701
     702lemma program_counter_set_bit_addressable_sfr:
     703    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀b: Byte. ∀v: Byte.
     704        program_counter … code_memory s = program_counter … code_memory (set_bit_addressable_sfr M code_memory s b v).
     705  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
     706  cases (set_bit_addressable_sfr' ?????) #s' * //
    685707qed.
    686708
     
    880902qed.
    881903
    882 axiom clock_set_bit_addressable_sfr: ∀m,cm,s,d,v. clock m cm s = clock … (set_bit_addressable_sfr … s d v).
    883 
    884 definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ;
     904definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
    885905                                   acc_a ; acc_b ; ext_indirect ;
    886                                    ext_indirect_dptr ]] → Byte → Σs':PreStatus M code_memory.
    887                                    clock … code_memory s = clock … code_memory s' ≝
     906                                   ext_indirect_dptr ]]. Byte → Σs':PreStatus M code_memory.
     907                                   clock … code_memory s = clock … code_memory s' ∧
     908                                   (¬(is_a … direct addr) → p1_latch … code_memory s = p1_latch … code_memory s') ∧
     909                                   (¬(is_a … direct addr) → p3_latch … code_memory s = p3_latch … code_memory s') ∧
     910                                   program_counter … code_memory s = program_counter … code_memory s' ∧
     911                                   (¬(is_a … direct addr) → special_function_registers_8052 … code_memory s = special_function_registers_8052 … code_memory s') ≝
    888912  λm, cm, s, a, v.
    889913    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    890914                                                acc_a ; acc_b ; ext_indirect ;
    891915                                                ext_indirect_dptr ]] x) →
    892                    Σs':PreStatus m cm. clock m cm s = clock m cm s'
     916                   Σs':PreStatus m cm. ?
    893917                   (*CSC: bug here if one specified the two clock above*)
    894918            with
     
    936960          match other in False with [ ]
    937961      ] (subaddressing_modein … a).
    938 // qed.
     962  /6 by conj, False_ind/
     963qed.
    939964
    940965definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M code_memory ≝
    941966 set_arg_8'.
    942967
    943 lemma set_arg_8_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v).
    944  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta @pi2
     968lemma clock_set_arg_8: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v).
     969 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
     970 cases (set_arg_8' ?????) #s' * * * * //
     971qed.
     972
     973lemma 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).
     974 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
     975 cases (set_arg_8' ?????) #s' * * * * //
     976qed.
     977
     978lemma p1_latch_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. p1_latch M cm s = p1_latch … (set_arg_8 M cm s x v).
     979  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
     980  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
     981  cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ]
     982  * * * * #_ #relevant #_ #_ #_ @relevant @I
     983qed.
     984
     985lemma p3_latch_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. p3_latch M cm s = p3_latch … (set_arg_8 M cm s x v).
     986  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
     987  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
     988  cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ]
     989  * * * * #_ #_ #relevant #_ #_ @relevant @I
     990qed.
     991
     992lemma special_function_registers_8052_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. special_function_registers_8052 M cm s = special_function_registers_8052 … (set_arg_8 M cm s x v).
     993  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
     994  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
     995  cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ]
     996  * * * * #_ #_ #_ #_ #relevant @relevant @I
    945997qed.
    946998
Note: See TracChangeset for help on using the changeset viewer.