Changeset 2172 for src/ASM


Ignore:
Timestamp:
Jul 10, 2012, 2:39:38 PM (7 years ago)
Author:
mulligan
Message:

Moved new versions of get_ / set_arg_* into Status.ma. Commented out proofs that are no longer working.

Location:
src/ASM
Files:
5 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProofSplit.ma

    r2160 r2172  
    1 include "ASM/AssemblyProof.ma".
    2 include alias "arithmetics/nat.ma".
    3 include alias "basics/logic.ma".
    4 
    5 lemma set_arg_16_mk_Status_commutation:
    6   ∀M: Type[0].
    7   ∀cm: M.
    8   ∀s: PreStatus M cm.
    9   ∀w: Word.
    10   ∀d: [[dptr]].
    11     set_arg_16 M cm s w d =
    12       mk_PreStatus M cm
    13         (low_internal_ram … s)
    14         (high_internal_ram … s)
    15         (external_ram … s)
    16         (program_counter … s)
    17         (special_function_registers_8051 … (set_arg_16 M cm s w d))
    18         (special_function_registers_8052 … s)
    19         (p1_latch … s)
    20         (p3_latch … s)
    21         (clock … s).
    22   #M #cm #s #w #d
    23   whd in match set_arg_16; normalize nodelta
    24   whd in match set_arg_16'; normalize nodelta
    25   @(subaddressing_mode_elim … d)
    26   cases (vsplit bool 8 8 w) #bu #bl normalize nodelta
    27   whd in match set_8051_sfr; normalize nodelta %
    28 qed.
    29 
    30 lemma set_program_counter_mk_Status_commutation:
    31   ∀M: Type[0].
    32   ∀cm: M.
    33   ∀s: PreStatus M cm.
    34   ∀w: Word.
    35     set_program_counter M cm s w =
    36       mk_PreStatus M cm
    37         (low_internal_ram … s)
    38         (high_internal_ram … s)
    39         (external_ram … s)
    40         w
    41         (special_function_registers_8051 … s)
    42         (special_function_registers_8052 … s)
    43         (p1_latch … s)
    44         (p3_latch … s)
    45         (clock … s).
    46   //
    47 qed.
    48 
    49 lemma set_clock_mk_Status_commutation:
    50   ∀M: Type[0].
    51   ∀cm: M.
    52   ∀s: PreStatus M cm.
    53   ∀c: nat.
    54     set_clock M cm s c =
    55       mk_PreStatus M cm
    56         (low_internal_ram … s)
    57         (high_internal_ram … s)
    58         (external_ram … s)
    59         (program_counter … s)
    60         (special_function_registers_8051 … s)
    61         (special_function_registers_8052 … s)
    62         (p1_latch … s)
    63         (p3_latch … s)
    64         c.
    65   //
    66 qed.
    67 
    68 lemma get_8051_sfr_set_clock:
    69   ∀M: Type[0].
    70   ∀cm: M.
    71   ∀s: PreStatus M cm.
    72   ∀sfr: SFR8051.
    73   ∀t: Time.
    74     get_8051_sfr M cm (set_clock M cm s t) sfr =
    75       get_8051_sfr M cm s sfr.
    76   #M #cm #s #sfr #t %
    77 qed.
    78 
    79 lemma get_8051_sfr_set_program_counter:
    80   ∀M: Type[0].
    81   ∀cm: M.
    82   ∀s: PreStatus M cm.
    83   ∀sfr: SFR8051.
    84   ∀pc: Word.
    85     get_8051_sfr M cm (set_program_counter M cm s pc) =
    86       get_8051_sfr M cm s.
    87   #M #cm #s #sfr #pc %
    88 qed.
    89 
    90 lemma special_function_registers_8051_set_arg_16:
    91   ∀M, M': Type[0].
    92   ∀cm: M.
    93   ∀cm': M'.
    94   ∀s: PreStatus M cm.
    95   ∀s': PreStatus M' cm'.
    96   ∀w, w': Word.
    97   ∀d, d': [[dptr]].
    98    special_function_registers_8051 ?? s = special_function_registers_8051 … s' →
    99     w = w' →
    100       special_function_registers_8051 ?? (set_arg_16 … s w d) =
    101         special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d').
    102   #M #M' #cm #cm' #s #s' #w #w'
    103   #d @(subaddressing_mode_elim … d)
    104   #d' @(subaddressing_mode_elim … d')
    105   #EQ1 #EQ2 <EQ2 normalize cases (vsplit bool 8 8 w) #b1 #b2 normalize <EQ1 %
    106 qed.
    107 
    108 lemma program_counter_set_arg_1:
    109   ∀M: Type[0].
    110   ∀cm: M.
    111   ∀s: PreStatus M cm.
    112   ∀addr: [[bit_addr; carry]].
    113   ∀b: Bit.
    114     program_counter M cm (set_arg_1 M cm s addr b) = program_counter M cm s.
    115   #M #cm #s whd in match set_arg_1; whd in match set_arg_1'; normalize nodelta
    116   #addr #b
    117   @(subaddressing_mode_elim … addr)
    118   [1:
    119     #byte cases (vsplit ????) #nu #nl normalize nodelta
    120     cases (vsplit ????) #ignore #three_bits normalize nodelta
    121     cases (get_index_v bool ????) normalize nodelta
    122     [1:
    123       @program_counter_set_bit_addressable_sfr
    124     |2:
    125       @program_counter_set_low_internal_ram
    126     ]
    127   |2:
    128     cases (vsplit ????) //
    129   ]
    130 qed.
    131 
    132 lemma get_ov_flag_set_program_counter:
    133   ∀M: Type[0].
    134   ∀cm: M.
    135   ∀s: PreStatus M cm.
    136   ∀pc: Word.
    137     get_ov_flag M cm (set_program_counter M cm s pc) =
    138       get_ov_flag M cm s.
    139   #M #cm #s #pc %
    140 qed.
    141 
    142 lemma external_ram_set_program_counter:
    143   ∀M: Type[0].
    144   ∀cm: M.
    145   ∀s: PreStatus M cm.
    146   ∀pc: Word.
    147     external_ram M cm (set_program_counter M cm s pc) =
    148       external_ram M cm s.
    149   #M #cm #s #pc %
    150 qed.
    151 
    152 lemma low_internal_ram_set_program_counter:
    153   ∀M: Type[0].
    154   ∀cm: M.
    155   ∀s: PreStatus M cm.
    156   ∀pc: Word.
    157     low_internal_ram M cm (set_program_counter M cm s pc) =
    158       low_internal_ram M cm s.
    159   #M #cm #s #pc %
    160 qed.
    161 
    162 lemma high_internal_ram_set_program_counter:
    163   ∀M: Type[0].
    164   ∀cm: M.
    165   ∀s: PreStatus M cm.
    166   ∀pc: Word.
    167     high_internal_ram M cm (set_program_counter M cm s pc) =
    168       high_internal_ram M cm s.
    169   #M #cm #s #pc %
    170 qed.
    171 
    172 lemma get_arg_8_set_program_counter:
    173   ∀M: Type[0].
    174   ∀cm: M.
    175   ∀s: PreStatus M cm.
    176   ∀flag: bool.
    177   ∀addr: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; ext_indirect; ext_indirect_dptr]].
    178   ∀pc: Word.
    179     get_arg_8 M cm (set_program_counter M cm s pc) flag addr =
    180       get_arg_8 M cm s flag addr.
    181   [2,3:
    182     cases addr #subaddressing_mode
    183     cases subaddressing_mode
    184     try (#addr1 whd in ⊢ (% → %);)
    185     whd in ⊢ (% → %); //
    186   ]
    187   #M #cm #s #flag #addr #pc
    188   whd in match get_arg_8; normalize nodelta
    189   cases addr *
    190   try (#addr1 #absurd normalize in absurd; cases absurd @I)
    191   try (#absurd normalize in absurd; cases absurd @I)
    192   try (#addr1 #addr2) try #addr1
    193   normalize nodelta %
    194 qed.
    195 
    196 lemma external_ram_set_flags:
    197   ∀M: Type[0].
    198   ∀cm: M.
    199   ∀s: PreStatus M cm.
    200   ∀opt: option Bit.
    201   ∀bit1, bit2: Bit.
    202     external_ram M cm (set_flags M cm s bit1 opt bit2) =
    203       external_ram M cm s.
    204   #M #cm #s #opt #bit1 #bit2 %
    205 qed.
    206 
    207 lemma low_internal_ram_set_flags:
    208   ∀M: Type[0].
    209   ∀cm: M.
    210   ∀s: PreStatus M cm.
    211   ∀opt: option Bit.
    212   ∀bit1, bit2: Bit.
    213     low_internal_ram M cm (set_flags M cm s bit1 opt bit2) =
    214       low_internal_ram M cm s.
    215   #M #cm #s #opt #bit1 #bit2 %
    216 qed.
    217 
    218 lemma high_internal_ram_set_flags:
    219   ∀M: Type[0].
    220   ∀cm: M.
    221   ∀s: PreStatus M cm.
    222   ∀opt: option Bit.
    223   ∀bit1, bit2: Bit.
    224     high_internal_ram M cm (set_flags M cm s bit1 opt bit2) =
    225       high_internal_ram M cm s.
    226   #M #cm #s #opt #bit1 #bit2 %
    227 qed.
    228 
    229 lemma low_internal_ram_set_clock:
    230   ∀M: Type[0].
    231   ∀cm: M.
    232   ∀s: PreStatus M cm.
    233   ∀t: Time.
    234     low_internal_ram M cm (set_clock M cm s t) =
    235       low_internal_ram M cm s.
    236   #M #cm #s #t %
    237 qed.
    238 
    239 lemma high_internal_ram_set_clock:
    240   ∀M: Type[0].
    241   ∀cm: M.
    242   ∀s: PreStatus M cm.
    243   ∀t: Time.
    244     high_internal_ram M cm (set_clock M cm s t) =
    245       high_internal_ram M cm s.
    246   #M #cm #s #t %
    247 qed.
    248 
    249 lemma external_ram_set_clock:
    250   ∀M: Type[0].
    251   ∀cm: M.
    252   ∀s: PreStatus M cm.
    253   ∀t: Time.
    254     external_ram M cm (set_clock M cm s t) =
    255       external_ram M cm s.
    256   #M #cm #s #t %
    257 qed.
    258 
    259 lemma set_8051_sfr_set_program_counter:
    260   ∀M: Type[0].
    261   ∀cm: M.
    262   ∀s: PreStatus M cm.
    263   ∀pc: Word.
    264   ∀sfr: SFR8051.
    265   ∀v: Byte.
    266     set_8051_sfr M cm (set_program_counter M cm s pc) sfr v =
    267       set_program_counter M cm (set_8051_sfr M cm s sfr v) pc.
    268   #M #cm #s #pc #sfr #v %
    269 qed.
    270 
    271 lemma low_internal_ram_set_8051_sfr:
    272   ∀M: Type[0].
    273   ∀cm: M.
    274   ∀s: PreStatus M cm.
    275   ∀sfr: SFR8051.
    276   ∀v: Byte.
    277     low_internal_ram M cm (set_8051_sfr M cm s sfr v) =
    278       low_internal_ram M cm s.
    279   #M #cm #s #sfr #v %
    280 qed.
    281 
    282 lemma high_internal_ram_set_8051_sfr:
    283   ∀M: Type[0].
    284   ∀cm: M.
    285   ∀s: PreStatus M cm.
    286   ∀sfr: SFR8051.
    287   ∀v: Byte.
    288     high_internal_ram M cm (set_8051_sfr M cm s sfr v) =
    289       high_internal_ram M cm s.
    290   #M #cm #s #sfr #v %
    291 qed.
    292 
    293 lemma external_ram_set_8051_sfr:
    294   ∀M: Type[0].
    295   ∀cm: M.
    296   ∀s: PreStatus M cm.
    297   ∀sfr: SFR8051.
    298   ∀v: Byte.
    299     external_ram M cm (set_8051_sfr M cm s sfr v) =
    300       external_ram M cm s.
    301   #M #cm #s #sfr #v %
    302 qed.
    303 
    304 lemma get_arg_8_set_clock:
    305   ∀M: Type[0].
    306   ∀cm: M.
    307   ∀s: PreStatus M cm.
    308   ∀addr.
    309   ∀t: Time.
    310     get_arg_8 M cm (set_clock M cm s t) addr =
    311       get_arg_8 M cm s addr.
    312   #M #cm #s #addr #t %
    313 qed.
    314 
    315 lemma set_program_counter_set_program_counter:
    316   ∀M: Type[0].
    317   ∀cm: M.
    318   ∀s: PreStatus M cm.
    319   ∀pc: Word.
    320   ∀pc': Word.
    321     set_program_counter M cm (set_program_counter M cm s pc) pc' =
    322       set_program_counter M cm s pc'.
    323   #M #cm #s #pc #pc' %
    324 qed.
    325 
    326 (* XXX: move elsewhere *)
    327 lemma bitvector_8_cases:
    328   ∀w: BitVector 8.
    329     ∃b0,b1,b2,b3,b4,b5,b6,b7: bool.
    330       w ≃ [[b0;b1;b2;b3;b4;b5;b6;b7]].
    331  #w repeat (cases (BitVector_Sn … w)  #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w)
    332  >(BitVector_O … w) %
    333 qed.
    334 
    335 (* XXX: not true
    336 lemma p3_latch_set_arg_8:
    337   ∀M: Type[0].
    338   ∀cm: M.
    339   ∀s: PreStatus M cm.
    340   ∀args.
    341   ∀v: Byte.
    342     p3_latch M cm (set_arg_8 M cm s args v) =
    343       p3_latch M cm s.
    344   #M #cm #s #args #v
    345   @(subaddressing_mode_elim … args)
    346   try #w try %
    347   whd in match set_arg_8; normalize nodelta
    348   whd in match set_arg_8'; normalize nodelta
    349   inversion (vsplit bool ???) #nu #nl #nu_nl_refl normalize nodelta
    350   inversion (vsplit bool ???) #ignore #three_bits #ignore_three_bits_refl normalize nodelta
    351   inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta try %
    352   whd in match set_bit_addressable_sfr; normalize nodelta
    353   @(bitvector_8_elim_prop … w)
    354 *)
    355 
    356 lemma status_of_pseudo_status_does_not_change_8051_sfrs:
    357   ∀M: internal_pseudo_address_map.
    358   ∀cm: pseudo_assembly_program.
    359   ∀s: PreStatus pseudo_assembly_program cm.
    360   ∀sigma: Word → Word.
    361   ∀policy: Word → bool.
    362     \snd M = data →
    363       special_function_registers_8051 pseudo_assembly_program cm s =
    364         special_function_registers_8051 (BitVectorTrie Byte 16)
    365           (code_memory_of_pseudo_assembly_program cm sigma policy)
    366           (status_of_pseudo_status M cm s sigma policy).
    367   #M #cm #s #sigma #policy #None_proof cases s
    368   #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
    369   whd in match status_of_pseudo_status; normalize nodelta
    370   whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    371   >None_proof %
    372 qed.
    373 
    374 lemma 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)
    391 qed.
    392 
    393 lemma 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   ]
    431 qed.
    432 
    433 lemma get_index_v_special_function_registers_8051_not_acc_a:
    434   ∀M: internal_pseudo_address_map.
    435   ∀cm: pseudo_assembly_program.
    436   ∀s: PreStatus pseudo_assembly_program cm.
    437   ∀sigma: Word → Word.
    438   ∀policy: Word → bool.
    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 %
    454   ]
    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)
    464 qed.
     1include "ASM/StatusProofsSplit.ma".
    4652
    4663include alias "arithmetics/nat.ma".
    … …  
    47310  ∀i: instruction.
    47411    fetch_many code_memory final_pc start_pc [i] →
    475       〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory start_pc.
     12      〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory
     13start_pc.
    47614  #code_memory #final_pc #start_pc #i * #new_pc
    47715  #fetch_many_assm whd in fetch_many_assm;
    … …  
    47917qed.
    48018
    481 (* XXX: this needs an extra invariant relating address and word that we look
    482         up!
    483 *)
    484 definition 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 
    501 lemma 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)
    521 qed.
    522 
    523 lemma 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
    529 qed.
    530 
    531 lemma 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 *)
    569 qed.
    570 
    571 lemma 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   ]
    593 qed.
    594 
    595 lemma 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   //
    603 qed.
    604 
    605 lemma 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   ]
    769 qed.
    770 
    771 lemma 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   //
    779 qed.
    780 
    781 lemma 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   //
    789 qed.
    790 
    791 lemma 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   ]
    821 qed.
    822 
    823 lemma 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))
    850 qed.
    851 
    852 lemma 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 *)
    914 qed.
    915 
    91619include alias "ASM/Vector.ma".
     20include "ASM/Test.ma".
    91721
    91822lemma main_lemma_preinstruction:

  • src/ASM/Status.ma

    r2160 r2172  
    546546    set_8051_sfr ?? status SFR_SP (bitvector_of_nat 8 7).
    547547 
    548 definition get_bit_addressable_sfr ≝
    549   λM: Type[0].
    550   λcode_memory:M.
    551   λs: PreStatus M code_memory.
    552   λn: nat.
    553   λb: BitVector n.
     548
     549definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝
     550  λb: Byte.
     551    let address ≝ nat_of_bitvector … b in
     552      if (eqb address 128) then None ?
     553      else if (eqb address 144) then Some … (inl … SFR_P1)
     554      else if (eqb address 160) then None ?
     555      else if (eqb address 176) then Some … (inl … SFR_P3)
     556      else if (eqb address 153) then Some … (inl … SFR_SBUF)
     557      else if (eqb address 138) then Some … (inl … SFR_TL0)
     558      else if (eqb address 139) then Some … (inl … SFR_TL1)
     559      else if (eqb address 140) then Some … (inl … SFR_TH0)
     560      else if (eqb address 141) then Some … (inl … SFR_TH1)
     561      else if (eqb address 200) then Some … (inr … SFR_T2CON)
     562      else if (eqb address 202) then Some … (inr … SFR_RCAP2L)
     563      else if (eqb address 203) then Some … (inr … SFR_RCAP2H)
     564      else if (eqb address 204) then Some … (inr … SFR_TL2)
     565      else if (eqb address 205) then Some … (inr … SFR_TH2)
     566      else if (eqb address 135) then Some … (inl … SFR_PCON)
     567      else if (eqb address 136) then Some … (inl … SFR_TCON)
     568      else if (eqb address 137) then Some … (inl … SFR_TMOD)
     569      else if (eqb address 152) then Some … (inl … SFR_SCON)
     570      else if (eqb address 168) then Some … (inl … SFR_IE)
     571      else if (eqb address 184) then Some … (inl … SFR_IP)
     572      else if (eqb address 129) then Some … (inl … SFR_SP)
     573      else if (eqb address 130) then Some … (inl … SFR_DPL)
     574      else if (eqb address 131) then Some … (inl … SFR_DPH)
     575      else if (eqb address 208) then Some … (inl … SFR_PSW)
     576      else if (eqb address 224) then Some … (inl … SFR_ACC_A)
     577      else if (eqb address 240) then Some … (inl … SFR_ACC_B)
     578      else None ?.
     579
     580definition get_bit_addressable_sfr:
     581    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → bool → Byte ≝
     582  λM: Type[0].
     583  λcode_memory:M.
     584  λs: PreStatus M code_memory.
     585  λb: Byte.
    554586  λl: bool.
    555     let address ≝ nat_of_bitvector … b in
    556       if (eqb address 128) then
    557         ?
    558       else if (eqb address 144) then
     587  match sfr_of_Byte b with
     588  [ None ⇒ match not_implemented in False with [ ]
     589  | Some sfr8051_8052 ⇒
     590    match sfr8051_8052 with
     591    [ inl sfr ⇒
     592      match sfr with
     593      [ SFR_P1 ⇒
    559594        if l then
    560           (p1_latch ?? s)
     595          p1_latch … s
    561596        else
    562           (get_8051_sfr ?? s SFR_P1)
    563       else if (eqb address 160) then
    564         ?
    565       else if (eqb address 176) then
     597          get_8051_sfr … s SFR_P1
     598      | SFR_P3 ⇒
    566599        if l then
    567           (p3_latch ?? s)
     600          p3_latch … s
    568601        else
    569           (get_8051_sfr ?? s SFR_P3)
    570       else if (eqb address 153) then
    571         get_8051_sfr ?? s SFR_SBUF
    572       else if (eqb address 138) then
    573         get_8051_sfr ?? s SFR_TL0
    574       else if (eqb address 139) then
    575         get_8051_sfr ?? s SFR_TL1
    576       else if (eqb address 140) then
    577         get_8051_sfr ?? s SFR_TH0
    578       else if (eqb address 141) then
    579         get_8051_sfr ?? s SFR_TH1
    580       else if (eqb address 200) then
    581         get_8052_sfr ?? s SFR_T2CON
    582       else if (eqb address 202) then
    583         get_8052_sfr ?? s SFR_RCAP2L
    584       else if (eqb address 203) then
    585         get_8052_sfr ?? s SFR_RCAP2H
    586       else if (eqb address 204) then
    587         get_8052_sfr ?? s SFR_TL2
    588       else if (eqb address 205) then
    589         get_8052_sfr ?? s SFR_TH2
    590       else if (eqb address 135) then
    591         get_8051_sfr ?? s SFR_PCON
    592       else if (eqb address 136) then
    593         get_8051_sfr ?? s SFR_TCON
    594       else if (eqb address 137) then
    595         get_8051_sfr ?? s SFR_TMOD
    596       else if (eqb address 152) then
    597         get_8051_sfr ?? s SFR_SCON
    598       else if (eqb address 168) then
    599         get_8051_sfr ?? s SFR_IE
    600       else if (eqb address 184) then
    601         get_8051_sfr ?? s SFR_IP
    602       else if (eqb address 129) then
    603         get_8051_sfr ?? s SFR_SP
    604       else if (eqb address 130) then
    605         get_8051_sfr ?? s SFR_DPL
    606       else if (eqb address 131) then
    607         get_8051_sfr ?? s SFR_DPH
    608       else if (eqb address 208) then
    609         get_8051_sfr ?? s SFR_PSW
    610       else if (eqb address 224) then
    611         get_8051_sfr ?? s SFR_ACC_A
    612       else if (eqb address 240) then
    613         get_8051_sfr ?? s SFR_ACC_B
    614       else
    615         ?.
    616       cases not_implemented
    617 qed.
    618 
    619 definition 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' ≝
     602          get_8051_sfr … s SFR_P3
     603      | _ ⇒ get_8051_sfr … s sfr
     604      ]
     605    | inr sfr ⇒ get_8052_sfr M code_memory s sfr
     606    ]
     607  ].
     608
     609definition set_bit_addressable_sfr:
     610    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → PreStatus M code_memory ≝
    624611  λM: Type[0].
    625612  λcode_memory:M.
    … …  
    627614  λb: Byte.
    628615  λv: Byte.
    629     let address ≝ nat_of_bitvector … b in
    630       if (eqb address 128) then
    631         match not_implemented in False with [ ]
    632       else if (eqb address 144) then
    633         let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
    634         let status_2 ≝ set_p1_latch ?? s v in
    635           status_2
    636       else if (eqb address 160) then
    637         match not_implemented in False with [ ]
    638       else if (eqb address 176) then
    639         let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
    640         let status_2 ≝ set_p3_latch ?? s v in
    641           status_2
    642       else if (eqb address 153) then
    643         set_8051_sfr ?? s SFR_SBUF v
    644       else if (eqb address 138) then
    645         set_8051_sfr ?? s SFR_TL0 v
    646       else if (eqb address 139) then
    647         set_8051_sfr ?? s SFR_TL1 v
    648       else if (eqb address 140) then
    649         set_8051_sfr ?? s SFR_TH0 v
    650       else if (eqb address 141) then
    651         set_8051_sfr ?? s SFR_TH1 v
    652       else if (eqb address 200) then
    653         set_8052_sfr ?? s SFR_T2CON v
    654       else if (eqb address 202) then
    655         set_8052_sfr ?? s SFR_RCAP2L v
    656       else if (eqb address 203) then
    657         set_8052_sfr ?? s SFR_RCAP2H v
    658       else if (eqb address 204) then
    659         set_8052_sfr ?? s SFR_TL2 v
    660       else if (eqb address 205) then
    661         set_8052_sfr ?? s SFR_TH2 v
    662       else if (eqb address 135) then
    663         set_8051_sfr ?? s SFR_PCON v
    664       else if (eqb address 136) then
    665         set_8051_sfr ?? s SFR_TCON v
    666       else if (eqb address 137) then
    667         set_8051_sfr ?? s SFR_TMOD v
    668       else if (eqb address 152) then
    669         set_8051_sfr ?? s SFR_SCON v
    670       else if (eqb address 168) then
    671         set_8051_sfr ?? s SFR_IE v
    672       else if (eqb address 184) then
    673         set_8051_sfr ?? s SFR_IP v
    674       else if (eqb address 129) then
    675         set_8051_sfr ?? s SFR_SP v
    676       else if (eqb address 130) then
    677         set_8051_sfr ?? s SFR_DPL v
    678       else if (eqb address 131) then
    679         set_8051_sfr ?? s SFR_DPH v
    680       else if (eqb address 208) then
    681         set_8051_sfr ?? s SFR_PSW v
    682       else if (eqb address 224) then
    683         set_8051_sfr ?? s SFR_ACC_A v
    684       else if (eqb address 240) then
    685         set_8051_sfr ?? s SFR_ACC_B v
    686       else
    687         match not_implemented in False with [ ].
    688   /2 by refl, pair_destruct/
    689 qed.
    690 
    691 definition 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'.
     616   match sfr_of_Byte b with
     617   [ None ⇒ match not_implemented in False with [ ]
     618   | Some sfr8051_8052 ⇒
     619      match sfr8051_8052 with
     620      [ inl sfr ⇒
     621         match sfr with
     622         [ SFR_P1 ⇒
     623           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
     624           set_p1_latch ?? s v
     625         | SFR_P3 ⇒
     626           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
     627           set_p3_latch ?? s v
     628         | _ ⇒ set_8051_sfr ?? s sfr v ]
     629      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]].
    694630
    695631lemma clock_set_bit_addressable_sfr:
    … …  
    697633        clock … code_memory s = clock … code_memory (set_bit_addressable_sfr M code_memory s b v).
    698634  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
    699   cases (set_bit_addressable_sfr' ?????) #s' * //
     635  cases (sfr_of_Byte ?)
     636  [1:
     637    normalize nodelta cases not_implemented
     638  |2:
     639    * * normalize nodelta %
     640  ]
    700641qed.
    701642
    … …  
    704645        program_counter … code_memory s = program_counter … code_memory (set_bit_addressable_sfr M code_memory s b v).
    705646  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
    706   cases (set_bit_addressable_sfr' ?????) #s' * //
     647  cases (sfr_of_Byte ?)
     648  [1:
     649    normalize nodelta cases not_implemented
     650  |2:
     651    * * %
     652  ]
    707653qed.
    708654
    … …  
    863809          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
    864810          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
    865           let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in
     811          let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
    866812            lookup ? 16 address (external_ram ?? s) (zero 8)
    867813      | ACC_PC ⇒
    … …  
    872818      | DIRECT d ⇒
    873819        λdirect: True.
    874           let 〈 nu, nl 〉 ≝ vsplit ? 4 4 d in
    875           let bit_one ≝ get_index_v ? ? nu 0 ? in
    876           let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
    877             match bit_one with
    878               [ false ⇒
    879                   let address ≝ three_bits @@ nl in
    880                     lookup ? 7 address (low_internal_ram ?? s) (zero 8)
    881               | true ⇒ get_bit_addressable_sfr ?? s 8 d l
    882               ]
     820          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
     821            match head' … hd with
     822            [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
     823            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
     824            ]
    883825      | INDIRECT i ⇒
    884826        λindirect: True.
    885           let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_register ?? s [[ false; false; i]]) in
    886           let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in
    887           let bit_1 ≝ get_index_v ?? bit_one_v O ? in
    888           match  bit_1 with
    889             [ false ⇒
    890                 lookup ? 7 (three_bits @@ nl) (low_internal_ram ?? s) (zero 8)
    891             | true ⇒
    892                 lookup ? 7 (three_bits @@ nl) (high_internal_ram ?? s) (zero 8)
     827          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
     828            match head' … hd with
     829            [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)
     830            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
    893831            ]
    894832      | _ ⇒ λother.
    895833        match other in False with [ ]
    896834      ] (subaddressing_modein … a).
    897   [1,2:
    898      normalize
    899      repeat (@ le_S_S)
    900      @ le_O_n
    901   ]
    902 qed.
    903 
    904 definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
     835
     836definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
    905837                                   acc_a ; acc_b ; ext_indirect ;
    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') ≝
     838                                   ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝
    912839  λm, cm, s, a, v.
    913840    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    914841                                                acc_a ; acc_b ; ext_indirect ;
    915842                                                ext_indirect_dptr ]] x) →
    916                    Σs':PreStatus m cm. ?
    917                    (*CSC: bug here if one specified the two clock above*)
     843                   PreStatus m cm
    918844            with
    919845      [ DIRECT d ⇒
    920846        λdirect: True.
    921           let 〈 nu, nl 〉 ≝ vsplit … 4 4 d in
    922           let bit_one ≝ get_index_v ? ? nu 0 ? in
    923           let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
    924             match bit_one with
    925               [ true ⇒ set_bit_addressable_sfr ?? s d v
     847          let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
     848            match head' … bit_one with
     849              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
    926850              | false ⇒
    927                 let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ?? s) in
     851                let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
    928852                  set_low_internal_ram ?? s memory
    929853              ]
    … …  
    931855        λindirect: True.
    932856          let register ≝ get_register ?? s [[ false; false; i ]] in
    933           let 〈nu, nl〉 ≝ vsplit ? 4 4 register in
    934           let bit_1 ≝ get_index_v … nu 0 ? in
    935           let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in
    936             match bit_1 with
     857          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
     858            match head' … bit_one with
    937859              [ false ⇒
    938                 let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ?? s) in
     860                let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
    939861                  set_low_internal_ram ?? s memory
    940862              | true ⇒
    941                 let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ?? s) in
     863                let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
    942864                  set_high_internal_ram ?? s memory
    943865              ]
    … …  
    960882          match other in False with [ ]
    961883      ] (subaddressing_modein … a).
    962   /6 by conj, False_ind/
    963 qed.
    964 
    965 definition 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 ≝
    966  set_arg_8'.
    967884
    968885lemma 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' * * * * //
     886  cases daemon
    971887qed.
    972888
    973889lemma 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' * * * * //
     890  cases daemon
    976891qed.
    977892
    … …  
    979894  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
    980895  #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
     896  cases daemon
    983897qed.
    984898
    … …  
    986900  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
    987901  #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
     902  cases daemon
    990903qed.
    991904
    … …  
    993906  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
    994907  #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
     908  cases daemon
    997909qed.
    998910
    … …  
    1056968      [ BIT_ADDR b ⇒
    1057969        λbit_addr: True.
    1058           let 〈 nu, nl 〉 ≝ vsplit … 4 4 b in
    1059           let bit_1 ≝ get_index_v ? ? nu 0 ? in
    1060           let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in
    1061             match bit_1 with
    1062               [ true ⇒
    1063                 let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    1064                 let d ≝ address ÷ 8 in
    1065                 let m ≝ address mod 8 in
    1066                 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    1067                 let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in
    1068                   get_index_v … sfr m ?
    1069               | false ⇒
    1070                 let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    1071                 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1072                 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
    1073                   get_index_v … t (modulus address 8) ?
    1074               ]
     970        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
     971        match head' … bit_1 with
     972        [ true ⇒
     973          let address ≝ nat_of_bitvector … seven_bits in
     974          let d ≝ address ÷ 8 in
     975          let m ≝ address mod 8 in
     976          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
     977          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
     978            get_index_v … sfr m ?
     979        | false ⇒
     980          let address ≝ nat_of_bitvector … seven_bits in
     981          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     982          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
     983            get_index_v … t (modulus address 8) ?
     984        ]
    1075985      | N_BIT_ADDR n ⇒
    1076986        λn_bit_addr: True.
    1077           let 〈 nu, nl 〉 ≝ vsplit … 4 4 n in
    1078           let bit_1 ≝ get_index_v ? ? nu 0 ? in
    1079           let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in
    1080             match bit_1 with
    1081               [ true ⇒
    1082                 let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    1083                 let d ≝ address ÷ 8 in
    1084                 let m ≝ address mod 8 in
    1085                 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    1086                 let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in
    1087                   ¬(get_index_v … sfr m ?)
    1088               | false ⇒
    1089                 let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    1090                 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1091                 let trans ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
    1092                   ¬(get_index_v … trans (modulus address 8) ?)
    1093               ]
     987        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
     988        match head' … bit_1 with
     989        [ true ⇒
     990          let address ≝ nat_of_bitvector … seven_bits in
     991          let d ≝ address ÷ 8 in
     992          let m ≝ address mod 8 in
     993          let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
     994          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
     995            ¬(get_index_v … sfr m ?)
     996        | false ⇒
     997          let address ≝ nat_of_bitvector … seven_bits in
     998          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     999          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
     1000            ¬(get_index_v … t (modulus address 8) ?)
     1001        ]
    10941002      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
    10951003      | _ ⇒ λother.
    10961004        match other in False with [ ]
    10971005      ] (subaddressing_modein … a).
    1098       [3,6:
    1099          normalize
    1100          repeat (@ le_S_S)
    1101          @ le_O_n
    1102       |1,2,4,5:
    1103          @modulus_less_than
    1104       ]
     1006      @modulus_less_than
    11051007qed.
    11061008     
    1107 definition set_arg_1': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → Σs':PreStatus M code_memory. clock ? code_memory s = clock ? code_memory s' ≝
     1009definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝
    11081010  λm: Type[0].
    11091011  λcm.
    … …  
    11111013  λa: [[bit_addr; carry]].
    11121014  λv: Bit.
    1113     match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with
     1015    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → ? with
    11141016      [ BIT_ADDR b ⇒ λbit_addr: True.
    1115         let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
    1116         let bit_1 ≝ get_index_v ?? nu 0 ? in
    1117         let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in
    1118         match bit_1 return λ_. ? with
    1119           [ true ⇒
    1120             let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    1121             let d ≝ address ÷ 8 in
    1122             let m ≝ address mod 8 in
    1123             let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    1124             let sfr ≝ get_bit_addressable_sfr ?? s ? t true in
    1125             let new_sfr ≝ set_index … sfr m v ? in
    1126               set_bit_addressable_sfr ?? s new_sfr t
    1127           | false ⇒
    1128             let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    1129             let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1130             let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
    1131             let n_bit ≝ set_index … t (modulus address 8) v ? in
    1132             let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
    1133               set_low_internal_ram ?? s memory
    1134           ]
     1017        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
     1018        match head' … bit_1 with
     1019        [ true ⇒
     1020          let address ≝ nat_of_bitvector … seven_bits in
     1021          let d ≝ address ÷ 8 in
     1022          let m ≝ address mod 8 in
     1023          let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
     1024          let sfr ≝ get_bit_addressable_sfr … s t true in
     1025          let new_sfr ≝ set_index … sfr m v ? in
     1026            set_bit_addressable_sfr … s new_sfr t
     1027        | false ⇒
     1028          let address ≝ nat_of_bitvector … seven_bits in
     1029          let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     1030          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
     1031          let n_bit ≝ set_index … t (modulus address 8) v ? in
     1032          let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
     1033            set_low_internal_ram … s memory
     1034        ]
    11351035      | CARRY ⇒
    11361036        λcarry: True.
    1137         let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
    1138         let bit_1 ≝ get_index_v… nu 1 ? in
    1139         let bit_2 ≝ get_index_v… nu 2 ? in
    1140         let bit_3 ≝ get_index_v… nu 3 ? in
    1141         let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in
     1037        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
     1038        let new_psw ≝ v:::seven_bits in
    11421039          set_8051_sfr ?? s SFR_PSW new_psw
    11431040      | _ ⇒
    … …  
    11461043            [ ]
    11471044      ] (subaddressing_modein … a).
    1148 try (repeat @le_S_S @le_O_n)
    1149 /by/
    1150 qed.
    1151 
    1152 definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝ set_arg_1'.
     1045  @modulus_less_than
     1046qed.
    11531047
    11541048lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v).
    1155  #M #cm #s #x #v whd in match set_arg_1; normalize nodelta @pi2
     1049  cases daemon
    11561050qed.
    11571051

  • src/ASM/StatusProofs.ma

    r2124 r2172  
    200200  #x try (#y #H) try #H whd in H; try cases H try %
    201201  whd in match set_arg_8; normalize nodelta
    202   whd in match set_arg_8'; normalize nodelta
    203   cases (vsplit bool 4 4 ?) #nu' #nl' normalize nodelta
    204   cases (vsplit bool 1 3 nu') #bit1' #ignore' normalize nodelta
    205   cases (get_index_v bool 4 nu' 0 ?) normalize nodelta
    206   try % cases daemon (*@(set_bit_addressable_sfr_set_program_counter)*)
     202  cases (vsplit bool ???) #bit_one #seven_bits normalize nodelta
     203  cases (head' bool ??) normalize nodelta
     204  try % cases daemon (* XXX: need @(set_bit_addressable_sfr_set_program_counter) *)
    207205qed.
    208206 
    … …  
    349347  #m #cm #s #addr #byte
    350348  whd in match set_arg_8; normalize nodelta
     349  cases daemon (*
    351350  whd in match set_arg_8'; normalize nodelta
    352351  cases addr #subaddressing_modein_proof
    … …  
    357356  cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta
    358357  cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta
    359   cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try %
     358  cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try % *)
    360359qed.
    361360
    … …  
    366365  #m #cm #s #addr #v
    367366  whd in match set_arg_1; normalize nodelta
     367  cases daemon (*
    368368  whd in match set_arg_1'; normalize nodelta
    369369  cases addr #subaddressing_modein_proof
    … …  
    376376  cases (get_index_v bool 4 nu ??) normalize nodelta
    377377  (* XXX: try /demod/ try % *)
    378   cases daemon
     378  cases daemon *)
    379379qed.
    380380

  • src/ASM/StatusProofsSplit.ma

    r2170 r2172  
    113113  ∀b: Bit.
    114114    program_counter M cm (set_arg_1 M cm s addr b) = program_counter M cm s.
    115   #M #cm #s whd in match set_arg_1; whd in match set_arg_1'; normalize nodelta
     115  #M #cm #s whd in match set_arg_1; cases daemon (* whd in match set_arg_1'; normalize nodelta
    116116  #addr #b
    117117  @(subaddressing_mode_elim … addr)
    … …  
    127127  |2:
    128128    cases (vsplit ????) //
    129   ]
     129  ] *)
    130130qed.
    131131
    … …  
    551551  #M #cm #ps #addr1 #result
    552552  @(subaddressing_mode_elim … addr1) try #w try %
    553   whd in ⊢ (??(???%)?); whd in ⊢ (??(???(???%))?); (* XXX: to be understood, slow match *)
     553  whd in ⊢ (??(???%)?); cases daemon (*whd in ⊢ (??(???(???%))?); (* XXX: to be understood, slow match *)
    554554  [1:
    555555    cases (vsplit bool ???) #nu #nl normalize nodelta
    … …  
    561561    cases (vsplit bool ???) #ignore #three_bits normalize nodelta
    562562    cases (get_index_v bool ????) normalize nodelta %
    563   ]
     563  ] *)
    564564qed.
    565565
    … …  
    612612  |2:
    613613    #addressing_mode_ok_refl whd in ⊢ (??%?);
    614     @pair_elim #nu #nl #nu_nl_refl normalize nodelta
     614    @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (*
    615615    @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
    616616    inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
    … …  
    737737      ]
    738738    ]
    739   ]
     739  ] *)
    740740qed.
    741741

  • src/ASM/Test.ma

    r2171 r2172  
    1 (**************************************************************************)
    2 (*       ___                                                              *)
    3 (*      ||M||                                                             *)
    4 (*      ||A||       A project by Andrea Asperti                           *)
    5 (*      ||T||                                                             *)
    6 (*      ||I||       Developers:                                           *)
    7 (*      ||T||         The HELM team.                                      *)
    8 (*      ||A||         http://helm.cs.unibo.it                             *)
    9 (*      \   /                                                             *)
    10 (*       \ /        This file is distributed under the terms of the       *)
    11 (*        v         GNU General Public License Version 2                  *)
    12 (*                                                                        *)
    13 (**************************************************************************)
    14 
    151include "ASM/Assembly.ma".
    162include "ASM/Interpret.ma".
    … …  
    316302 //
    317303qed.
    318 
    319 definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝
    320   λb: Byte.
    321     let address ≝ nat_of_bitvector … b in
    322       if (eqb address 128) then None ?
    323       else if (eqb address 144) then Some … (inl … SFR_P1)
    324       else if (eqb address 160) then None ?
    325       else if (eqb address 176) then Some … (inl … SFR_P3)
    326       else if (eqb address 153) then Some … (inl … SFR_SBUF)
    327       else if (eqb address 138) then Some … (inl … SFR_TL0)
    328       else if (eqb address 139) then Some … (inl … SFR_TL1)
    329       else if (eqb address 140) then Some … (inl … SFR_TH0)
    330       else if (eqb address 141) then Some … (inl … SFR_TH1)
    331       else if (eqb address 200) then Some … (inr … SFR_T2CON)
    332       else if (eqb address 202) then Some … (inr … SFR_RCAP2L)
    333       else if (eqb address 203) then Some … (inr … SFR_RCAP2H)
    334       else if (eqb address 204) then Some … (inr … SFR_TL2)
    335       else if (eqb address 205) then Some … (inr … SFR_TH2)
    336       else if (eqb address 135) then Some … (inl … SFR_PCON)
    337       else if (eqb address 136) then Some … (inl … SFR_TCON)
    338       else if (eqb address 137) then Some … (inl … SFR_TMOD)
    339       else if (eqb address 152) then Some … (inl … SFR_SCON)
    340       else if (eqb address 168) then Some … (inl … SFR_IE)
    341       else if (eqb address 184) then Some … (inl … SFR_IP)
    342       else if (eqb address 129) then Some … (inl … SFR_SP)
    343       else if (eqb address 130) then Some … (inl … SFR_DPL)
    344       else if (eqb address 131) then Some … (inl … SFR_DPH)
    345       else if (eqb address 208) then Some … (inl … SFR_PSW)
    346       else if (eqb address 224) then Some … (inl … SFR_ACC_A)
    347       else if (eqb address 240) then Some … (inl … SFR_ACC_B)
    348       else None ?.
    349 
    350 definition set_bit_addressable_sfr:
    351     ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte →
    352       PreStatus M code_memory ≝
    353   λM: Type[0].
    354   λcode_memory:M.
    355   λs: PreStatus M code_memory.
    356   λb: Byte.
    357   λv: Byte.
    358    match sfr_of_Byte b with
    359    [ None ⇒ match not_implemented in False with [ ]
    360    | Some sfr8051_8052 ⇒
    361       match sfr8051_8052 with
    362       [ inl sfr ⇒
    363          match sfr with
    364          [ SFR_P1 ⇒
    365            let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
    366            set_p1_latch ?? s v
    367          | SFR_P3 ⇒
    368            let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
    369            set_p3_latch ?? s v
    370          | _ ⇒ set_8051_sfr ?? s sfr v ]
    371       | inr sfr ⇒ set_8052_sfr ?? s sfr v ]].
    372 
     304 
    373305definition map_address_Byte_using_internal_pseudo_address_map ≝
    374306 λM,sigma,d,v.
    … …  
    376308  [ None ⇒ v
    377309  | Some sfr8051_8052 ⇒
    378      match sfr8051_8052 with
    379      [ inl sfr ⇒
    380         map_address_using_internal_pseudo_address_map M sigma sfr v
    381      | inr _ ⇒ v ]].
     310    match sfr8051_8052 with
     311    [ inl sfr ⇒
     312      map_address_using_internal_pseudo_address_map M sigma sfr v
     313    | inr _ ⇒ v
     314    ]
     315  ].
    382316
    383317lemma set_bit_addressable_sfr_status_of_pseudo_status':
    … …  
    390324  =status_of_pseudo_status M code_memory
    391325   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
     326  whd in match map_address_Byte_using_internal_pseudo_address_map;
    392327  whd in match set_bit_addressable_sfr;
    393   whd in match map_address_Byte_using_internal_pseudo_address_map;
    394328  normalize nodelta
    395329  @(let M ≝ pseudo_assembly_program in
    … …  
    412346         | _ ⇒ set_8051_sfr ?? s sfr v ]
    413347      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]])
    414  normalize nodelta
    415  /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/
    416  whd in match map_address_using_internal_pseudo_address_map; normalize nodelta //
     348  normalize nodelta
     349  /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/
     350  whd in match map_address_using_internal_pseudo_address_map; normalize nodelta //
    417351qed.
    418352
    … …  
    610544     map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v
    611545  | _ ⇒ v ].
    612 
    613 definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
    614                                    acc_a ; acc_b ; ext_indirect ;
    615                                    ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝
    616   λm, cm, s, a, v.
    617     match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    618                                                 acc_a ; acc_b ; ext_indirect ;
    619                                                 ext_indirect_dptr ]] x) →
    620                    PreStatus m cm
    621             with
    622       [ DIRECT d ⇒
    623         λdirect: True.
    624           let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
    625             match head' … bit_one with
    626               [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
    627               | false ⇒
    628                 let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
    629                   set_low_internal_ram ?? s memory
    630               ]
    631       | INDIRECT i ⇒
    632         λindirect: True.
    633           let register ≝ get_register ?? s [[ false; false; i ]] in
    634           let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
    635             match head' … bit_one with
    636               [ false ⇒
    637                 let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
    638                   set_low_internal_ram ?? s memory
    639               | true ⇒
    640                 let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
    641                   set_high_internal_ram ?? s memory
    642               ]
    643       | REGISTER r ⇒ λregister: True. set_register ?? s r v
    644       | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
    645       | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
    646       | EXT_INDIRECT e ⇒
    647         λext_indirect: True.
    648           let address ≝ get_register ?? s [[ false; false; e ]] in
    649           let padded_address ≝ pad 8 8 address in
    650           let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in
    651             set_external_ram ?? s memory
    652       | EXT_INDIRECT_DPTR ⇒
    653         λext_indirect_dptr: True.
    654           let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
    655           let memory ≝ insert ? 16 address v (external_ram ?? s) in
    656             set_external_ram ?? s memory
    657       | _ ⇒
    658         λother: False.
    659           match other in False with [ ]
    660       ] (subaddressing_modein … a).
    661546
    662547(*CSC: move elsewhere*)
    … …  
    767652      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ]
    768653qed.
    769 
    770 definition get_bit_addressable_sfr:
    771     ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → bool → Byte ≝
    772   λM: Type[0].
    773   λcode_memory:M.
    774   λs: PreStatus M code_memory.
    775   λb: Byte.
    776   λl: bool.
    777   match sfr_of_Byte b with
    778   [ None ⇒ match not_implemented in False with [ ]
    779   | Some sfr8051_8052 ⇒
    780     match sfr8051_8052 with
    781     [ inl sfr ⇒
    782       match sfr with
    783       [ SFR_P1 ⇒
    784         if l then
    785           p1_latch … s
    786         else
    787           get_8051_sfr … s SFR_P1
    788       | SFR_P3 ⇒
    789         if l then
    790           p3_latch … s
    791         else
    792           get_8051_sfr … s SFR_P3
    793       | _ ⇒ get_8051_sfr … s sfr
    794       ]
    795     | inr sfr ⇒ get_8052_sfr M code_memory s sfr
    796     ]
    797   ].
    798 
    799 definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ;
    800                                           acc_a ; acc_b ; data ; acc_dptr ;
    801                                           acc_pc ; ext_indirect ;
    802                                           ext_indirect_dptr ]] → Byte ≝
    803   λm, cm, s, l, a.
    804     match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    805                                                 acc_a ; acc_b ; data ; acc_dptr ;
    806                                                 acc_pc ; ext_indirect ;
    807                                                 ext_indirect_dptr ]] x) → ? with
    808       [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
    809       | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
    810       | DATA d ⇒ λdata: True. d
    811       | REGISTER r ⇒ λregister: True. get_register ?? s r
    812       | EXT_INDIRECT_DPTR ⇒
    813         λext_indirect_dptr: True.
    814           let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
    815             lookup ? 16 address (external_ram ?? s) (zero 8)
    816       | EXT_INDIRECT e ⇒
    817         λext_indirect: True.
    818           let address ≝ get_register ?? s [[ false; false; e ]]  in
    819           let padded_address ≝ pad 8 8 address in
    820             lookup ? 16 padded_address (external_ram ?? s) (zero 8)
    821       | ACC_DPTR ⇒
    822         λacc_dptr: True.
    823           let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
    824           let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
    825           let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
    826             lookup ? 16 address (external_ram ?? s) (zero 8)
    827       | ACC_PC ⇒
    828         λacc_pc: True.
    829           let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
    830           let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
    831             lookup ? 16 address (external_ram ?? s) (zero 8)
    832       | DIRECT d ⇒
    833         λdirect: True.
    834           let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
    835             match head' … hd with
    836             [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
    837             | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
    838             ]
    839       | INDIRECT i ⇒
    840         λindirect: True.
    841           let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
    842             match head' … hd with
    843             [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)
    844             | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)
    845             ]
    846       | _ ⇒ λother.
    847         match other in False with [ ]
    848       ] (subaddressing_modein … a).
    849654
    850655lemma p1_latch_status_of_pseudo_status:
    … …  
    1081886qed.
    1082887
    1083 definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] →
    1084                        bool → bool ≝
    1085   λm, cm, s, a, l.
    1086     match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
    1087                                                  n_bit_addr ;
    1088                                                  carry ]] x) → ? with
    1089       [ BIT_ADDR b ⇒
    1090         λbit_addr: True.
    1091         let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
    1092         match head' … bit_1 with
    1093         [ true ⇒
    1094           let address ≝ nat_of_bitvector … seven_bits in
    1095           let d ≝ address ÷ 8 in
    1096           let m ≝ address mod 8 in
    1097           let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    1098           let sfr ≝ get_bit_addressable_sfr ?? s trans l in
    1099             get_index_v … sfr m ?
    1100         | false ⇒
    1101           let address ≝ nat_of_bitvector … seven_bits in
    1102           let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1103           let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
    1104             get_index_v … t (modulus address 8) ?
    1105         ]
    1106       | N_BIT_ADDR n ⇒
    1107         λn_bit_addr: True.
    1108         let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
    1109         match head' … bit_1 with
    1110         [ true ⇒
    1111           let address ≝ nat_of_bitvector … seven_bits in
    1112           let d ≝ address ÷ 8 in
    1113           let m ≝ address mod 8 in
    1114           let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    1115           let sfr ≝ get_bit_addressable_sfr ?? s trans l in
    1116             ¬(get_index_v … sfr m ?)
    1117         | false ⇒
    1118           let address ≝ nat_of_bitvector … seven_bits in
    1119           let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1120           let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
    1121             ¬(get_index_v … t (modulus address 8) ?)
    1122         ]
    1123       | CARRY ⇒ λcarry: True. get_cy_flag ?? s
    1124       | _ ⇒ λother.
    1125         match other in False with [ ]
    1126       ] (subaddressing_modein … a).
    1127       @modulus_less_than
    1128 qed.
    1129 
    1130888definition map_bit_address_mode_using_internal_pseudo_address_map_get ≝
    1131889 λM:internal_pseudo_address_map.λcm: pseudo_assembly_program.λs:PreStatus ? cm.λsigma: Word → Word. λaddr. λl.
    … …  
    12501008qed.
    12511009
    1252 definition set_arg_1': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → Σs':PreStatus M code_memory. clock ? code_memory s = clock ? code_memory s' ≝
    1253   λm: Type[0].
    1254   λcm.
    1255   λs: PreStatus m cm.
    1256   λa: [[bit_addr; carry]].
    1257   λv: Bit.
    1258     match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with
    1259       [ BIT_ADDR b ⇒ λbit_addr: True.
    1260         let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
    1261         match head' … bit_1 with
    1262         [ true ⇒
    1263           let address ≝ nat_of_bitvector … seven_bits in
    1264           let d ≝ address ÷ 8 in
    1265           let m ≝ address mod 8 in
    1266           let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    1267           let sfr ≝ get_bit_addressable_sfr … s t true in
    1268           let new_sfr ≝ set_index … sfr m v ? in
    1269             set_bit_addressable_sfr … s new_sfr t
    1270         | false ⇒
    1271           let address ≝ nat_of_bitvector … seven_bits in
    1272           let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
    1273           let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
    1274           let n_bit ≝ set_index … t (modulus address 8) v ? in
    1275           let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
    1276             set_low_internal_ram … s memory
    1277         ]
    1278       | CARRY ⇒
    1279         λcarry: True.
    1280         let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
    1281         let new_psw ≝ v:::seven_bits in
    1282           set_8051_sfr ?? s SFR_PSW new_psw
    1283       | _ ⇒
    1284         λother: False.
    1285           match other in False with
    1286             [ ]
    1287       ] (subaddressing_modein … a).
    1288   try (repeat @le_S_S @le_O_n)
    1289   try @modulus_less_than
    1290   /by/
    1291   cases daemon (* XXX: russell type for preservation of clock on set_bit_addressable_sfr *)
    1292 qed.
    1293 
    1294 definition set_arg_1:
    1295     ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] →
    1296       Bit → PreStatus M code_memory ≝ set_arg_1'.
    1297 
    12981010definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝
    12991011  λM: internal_pseudo_address_map.
    … …  
    13721084        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b) sigma policy.
    13731085  whd in match set_arg_1; normalize nodelta
    1374   whd in match set_arg_1'; normalize nodelta
    13751086  whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_1; normalize nodelta
    13761087  whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_2; normalize nodelta
    … …  
    14331144  ]
    14341145qed.
     1146
     1147lemma clock_status_of_pseudo_status:
     1148 ∀M,cm,sigma,policy,s.
     1149  clock …
     1150   (code_memory_of_pseudo_assembly_program cm sigma policy)
     1151   (status_of_pseudo_status M cm s sigma policy)
     1152  = clock … cm s.
     1153//
     1154qed.
     1155
     1156lemma set_clock_status_of_pseudo_status:
     1157 ∀M,cm,sigma,policy,s,v.
     1158  set_clock …
     1159   (code_memory_of_pseudo_assembly_program cm sigma policy)
     1160   (status_of_pseudo_status M cm s sigma policy) v
     1161  = status_of_pseudo_status M cm (set_clock … cm s v) sigma policy.
     1162//
     1163qed.
Note: See TracChangeset for help on using the changeset viewer.