Ignore:
Timestamp:
Jul 6, 2012, 11:34:09 AM (8 years ago)
Author:
sacerdot
Message:

Anticipating a proof needed before.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2151 r2157  
    179179    | _ ⇒ True
    180180    ].
    181 
    182 (* XXX: easy but tedious *)
    183 lemma assembly1_lt_128:
    184   ∀i: instruction.
    185     |(assembly1 i)| < 128.
    186   cases daemon
    187 (* XXX: commented out as takes ages to type check
    188   #i cases i
    189   try (#assm1 #assm2) try #assm1
    190   [8:
    191     cases assm1
    192     try (#assm1 #assm2) try #assm1
    193     whd in match assembly1; normalize nodelta
    194     whd in match assembly_preinstruction; normalize nodelta
    195     try @(subaddressing_mode_elim … assm2)
    196     try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta
    197     [32:
    198       cases assm1 -assm1 #assm1 normalize nodelta
    199       cases assm1 #addr1 #addr2 normalize nodelta
    200       [1:
    201         @(subaddressing_mode_elim … addr2)
    202       |2:
    203         @(subaddressing_mode_elim … addr1)
    204       ]
    205       #w
    206     |35,36,37:
    207       cases assm1 -assm1 #assm1 normalize nodelta
    208       [1,3:
    209         cases assm1 -assm1 #assm1 normalize nodelta
    210       ]
    211       cases assm1 #addr1 #addr2 normalize nodelta
    212       @(subaddressing_mode_elim … addr2) try #w
    213     |49:
    214       cases assm1 -assm1 #assm1 normalize nodelta
    215       [1:
    216         cases assm1 -assm1 #assm1 normalize nodelta
    217         [1:
    218           cases assm1 -assm1 #assm1 normalize nodelta
    219           [1:
    220             cases assm1 -assm1 #assm1 normalize nodelta
    221             [1:
    222               cases assm1 -assm1 #assm1 normalize nodelta
    223             ]
    224           ]
    225         ]
    226       ]
    227       cases assm1 #addr1 #addr2 normalize nodelta
    228       [1,3,4,5:
    229         @(subaddressing_mode_elim … addr2) try #w
    230       |*:
    231         @(subaddressing_mode_elim … addr1) try #w
    232         normalize nodelta
    233         [1,2:
    234           @(subaddressing_mode_elim … addr2) try #w
    235         ]
    236       ]
    237     |50:
    238       cases assm1 -assm1 #assm1 normalize nodelta
    239       cases assm1 #addr1 #addr2 normalize nodelta
    240       [1:
    241         @(subaddressing_mode_elim … addr2) try #w
    242       |2:
    243         @(subaddressing_mode_elim … addr1) try #w
    244       ]
    245     ]
    246     normalize repeat @le_S_S @le_O_n
    247   ]
    248   whd in match assembly1; normalize nodelta
    249   [6:
    250     normalize repeat @le_S_S @le_O_n
    251   |7:
    252     @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n
    253   |*:
    254     @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n
    255   ]
    256   *)
    257 qed.
    258 
    259 lemma assembly1_pseudoinstruction_lt_2_to_16:
    260   ∀lookup_labels,sigma,policy,ppc,lookup_datalabels,pi.
    261   |\snd (assembly_1_pseudoinstruction
    262     lookup_labels sigma policy ppc lookup_datalabels pi)|
    263    < 2^16.
    264  #lookup_labels #sigma #policy #ppc #lookup_datalabels *
    265 [ cut (128 < 2^16) [@leb_true_to_le %] #LT
    266   * whd in match (assembly_1_pseudoinstruction ??????);
    267   whd in match (expand_pseudo_instruction ??????);
    268   whd in match assembly_1_pseudoinstruction; normalize nodelta
    269   try (#arg1 #arg2 #arg3) try (#arg1 #arg2) try #arg1
    270   whd in match (expand_pseudo_instruction ??????);
    271   try
    272    (change with (|flatten ? [assembly1 ?]| < ?)
    273     >flatten_singleton
    274     @(transitive_lt … (assembly1_lt_128 ?))
    275     @LT)
    276   @pair_elim #x #y #_ cases x normalize nodelta
    277   try
    278    (change with (|flatten ? [assembly1 ?]| < ?)
    279     >flatten_singleton
    280     @(transitive_lt … (assembly1_lt_128 ?))
    281     @LT)
    282   change with (|flatten ? [assembly1 ?; assembly1 ?; assembly1 ?]| < ?)
    283   >length_flatten_cons >length_flatten_cons >length_flatten_cons <plus_n_O
    284   <associative_plus @(transitive_lt … (tech_transitive_lt_3 … (2^7) ???))
    285   try @assembly1_lt_128 @leb_true_to_le %
    286 |2,3: #msg normalize in ⊢ (?%?); //
    287 | #label whd in match (assembly_1_pseudoinstruction ??????);
    288   whd in match (expand_pseudo_instruction ??????);
    289   @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_
    290   [2: @pair_elim #x #y #_ cases (?∧?)]
    291   normalize in ⊢ (?%?); //
    292 | #label whd in match (assembly_1_pseudoinstruction ??????);
    293   whd in match (expand_pseudo_instruction ??????);
    294   @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_
    295   normalize in ⊢ (?%?); //
    296 | #dptr #id normalize in ⊢ (?%?); //
    297 ]
    298 qed.
    299181
    300182lemma monotone_sigma:
Note: See TracChangeset for help on using the changeset viewer.