Changeset 2157


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

Anticipating a proof needed before.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2156 r2157  
    731731whd in ⊢ (??%? → ?); #EQ1 #EQ2 destruct %
    732732qed.
     733
     734(* XXX: easy but tedious *)
     735lemma assembly1_lt_128:
     736  ∀i: instruction.
     737    |(assembly1 i)| < 128.
     738  cases daemon
     739(* XXX: commented out as takes ages to type check
     740  #i cases i
     741  try (#assm1 #assm2) try #assm1
     742  [8:
     743    cases assm1
     744    try (#assm1 #assm2) try #assm1
     745    whd in match assembly1; normalize nodelta
     746    whd in match assembly_preinstruction; normalize nodelta
     747    try @(subaddressing_mode_elim … assm2)
     748    try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta
     749    [32:
     750      cases assm1 -assm1 #assm1 normalize nodelta
     751      cases assm1 #addr1 #addr2 normalize nodelta
     752      [1:
     753        @(subaddressing_mode_elim … addr2)
     754      |2:
     755        @(subaddressing_mode_elim … addr1)
     756      ]
     757      #w
     758    |35,36,37:
     759      cases assm1 -assm1 #assm1 normalize nodelta
     760      [1,3:
     761        cases assm1 -assm1 #assm1 normalize nodelta
     762      ]
     763      cases assm1 #addr1 #addr2 normalize nodelta
     764      @(subaddressing_mode_elim … addr2) try #w
     765    |49:
     766      cases assm1 -assm1 #assm1 normalize nodelta
     767      [1:
     768        cases assm1 -assm1 #assm1 normalize nodelta
     769        [1:
     770          cases assm1 -assm1 #assm1 normalize nodelta
     771          [1:
     772            cases assm1 -assm1 #assm1 normalize nodelta
     773            [1:
     774              cases assm1 -assm1 #assm1 normalize nodelta
     775            ]
     776          ]
     777        ]
     778      ]
     779      cases assm1 #addr1 #addr2 normalize nodelta
     780      [1,3,4,5:
     781        @(subaddressing_mode_elim … addr2) try #w
     782      |*:
     783        @(subaddressing_mode_elim … addr1) try #w
     784        normalize nodelta
     785        [1,2:
     786          @(subaddressing_mode_elim … addr2) try #w
     787        ]
     788      ]
     789    |50:
     790      cases assm1 -assm1 #assm1 normalize nodelta
     791      cases assm1 #addr1 #addr2 normalize nodelta
     792      [1:
     793        @(subaddressing_mode_elim … addr2) try #w
     794      |2:
     795        @(subaddressing_mode_elim … addr1) try #w
     796      ]
     797    ]
     798    normalize repeat @le_S_S @le_O_n
     799  ]
     800  whd in match assembly1; normalize nodelta
     801  [6:
     802    normalize repeat @le_S_S @le_O_n
     803  |7:
     804    @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n
     805  |*:
     806    @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n
     807  ]
     808  *)
     809qed.
     810
     811lemma assembly1_pseudoinstruction_lt_2_to_16:
     812  ∀lookup_labels,sigma,policy,ppc,lookup_datalabels,pi.
     813  |\snd (assembly_1_pseudoinstruction
     814    lookup_labels sigma policy ppc lookup_datalabels pi)|
     815   < 2^16.
     816 #lookup_labels #sigma #policy #ppc #lookup_datalabels *
     817[ cut (128 < 2^16) [@leb_true_to_le %] #LT
     818  * whd in match (assembly_1_pseudoinstruction ??????);
     819  whd in match (expand_pseudo_instruction ??????);
     820  whd in match assembly_1_pseudoinstruction; normalize nodelta
     821  try (#arg1 #arg2 #arg3) try (#arg1 #arg2) try #arg1
     822  whd in match (expand_pseudo_instruction ??????);
     823  try
     824   (change with (|flatten ? [assembly1 ?]| < ?)
     825    >flatten_singleton
     826    @(transitive_lt … (assembly1_lt_128 ?))
     827    @LT)
     828  @pair_elim #x #y #_ cases x normalize nodelta
     829  try
     830   (change with (|flatten ? [assembly1 ?]| < ?)
     831    >flatten_singleton
     832    @(transitive_lt … (assembly1_lt_128 ?))
     833    @LT)
     834  change with (|flatten ? [assembly1 ?; assembly1 ?; assembly1 ?]| < ?)
     835  >length_flatten_cons >length_flatten_cons >length_flatten_cons <plus_n_O
     836  <associative_plus @(transitive_lt … (tech_transitive_lt_3 … (2^7) ???))
     837  try @assembly1_lt_128 @leb_true_to_le %
     838|2,3: #msg normalize in ⊢ (?%?); //
     839| #label whd in match (assembly_1_pseudoinstruction ??????);
     840  whd in match (expand_pseudo_instruction ??????);
     841  @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_
     842  [2: @pair_elim #x #y #_ cases (?∧?)]
     843  normalize in ⊢ (?%?); //
     844| #label whd in match (assembly_1_pseudoinstruction ??????);
     845  whd in match (expand_pseudo_instruction ??????);
     846  @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_
     847  normalize in ⊢ (?%?); //
     848| #dptr #id normalize in ⊢ (?%?); //
     849]
     850qed.
     851
     852
    733853
    734854definition assembly:
  • 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.