Changeset 2132


Ignore:
Timestamp:
Jun 28, 2012, 10:41:59 AM (5 years ago)
Author:
sacerdot
Message:

Two more daemons closed, one left.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2131 r2132  
    180180    ].
    181181
     182lemma fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels:
     183 ∀lookup_labels,sigma,policy,ppc,pi.
     184  ∀lookup_datalabels1,lookup_datalabels2.
     185   \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels1 pi) =
     186   \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels2 pi).
     187#lookup_labels #sigma #policy #ppc #pi #lookup_datalabels1 #lookup_datalabels2
     188cases pi //
     189qed.
     190
     191lemma fst_snd_assembly_1_pseudoinstruction:
     192 ∀lookup_labels,sigma,policy,ppc,pi,lookup_datalabels,len,assembled.
     193   assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi
     194   = 〈len,assembled〉 →
     195    len = |assembled|.
     196#lookup #sigma #policy #ppc #pi #lookup_datalabels #len #assembled
     197inversion (assembly_1_pseudoinstruction ??????) #len' #assembled'
     198whd in ⊢ (??%? → ?); #EQ1 #EQ2 destruct %
     199qed.
     200
    182201(* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *)     
    183202lemma assembly_ok:
     
    224243      #spw1 #_ >spw1 -spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f
    225244      >eq_fetch_pseudo_instruction whd in match instruction_size;
    226       normalize nodelta (*CSC: TRUE, NEEDS LEMMA *)
    227       cases daemon
     245      normalize nodelta >create_label_cost_refl
     246      >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
     247      [>eq_assembly_1_pseudoinstruction % | skip]
    228248  | lapply (load_code_memory_ok assembled' ?) [ assumption ]
    229249    #load_code_memory_ok
    230     cut (len=|assembled|)
    231     [1: (*CSC: provable before cleaning *)
    232         cases daemon
    233     ]
    234     #EQlen
     250    lapply (fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction) #EQlen
    235251    (* Nice statement here *)
    236252    cut (∀j. ∀H: j < |assembled|.
Note: See TracChangeset for help on using the changeset viewer.