Changeset 2157 for src/ASM/Assembly.ma


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

Anticipating a proof needed before.

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