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

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

File:
1 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:
Note: See TracChangeset for help on using the changeset viewer.