Changeset 892


Ignore:
Timestamp:
Jun 7, 2011, 5:28:57 PM (8 years ago)
Author:
sacerdot
Message:

First fundamental lemma almost finished.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r890 r892  
    356356  λelimU: A ⊎ B → bool.
    357357    elimA (λa. elimB (λb. elimU (inl ? ? a) ∧ elimU (inr ? ? b))).
    358                            
     358
     359(*                           
    359360definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
    360361  λP.
     
    438439axiom instruction_elim_complete:
    439440 ∀P. instruction_elim P = true → ∀i. P i = true.
    440 
     441*)
    441442(*definition eq_instruction ≝
    442443  λi, j: instruction.
     
    453454    eq hd a ∨ (vect_member A ? eq tl a)
    454455  ].
    455    
     456
    456457let rec list_addressing_mode_tags_elim_prop
    457458  (n: nat)
     
    671672 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
    672673  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
    673 
     674(*
    674675axiom half_add_SO:
    675676 ∀pc.
     
    683684 ∀pc.
    684685 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
    685 
     686*)
    686687axiom bitvector_elim_complete:
    687688 ∀n,P. bitvector_elim n P = true → ∀bv. P bv.
     
    718719        eq_instruction (\fst instr_pc)) i = true.
    719720*)
     721
    720722lemma test:
    721   ∀pc,i,code_memory.
    722       let assembled ≝ assembly1 i in
     723  ∀pc,i,code_memory,assembled.
     724    assembled = assembly1 i →
    723725      let len ≝ length … assembled in
    724726      encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
     
    727729      let 〈instr,pc'〉 ≝ instr_pc in
    728730       (eq_instruction instr i ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
    729  #pc #i #code_memory cases i [8: *]
     731 #pc #i #code_memory #assembled cases i [8: *]
    730732 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
    731  [47,48,49: |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg
     733 [47,48,49:
     734 |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg
    732735  [2,3,5,7,10,12,16,17,18,21,25,26,27,30,31,32,37,38,39,40,41,42,43,44,45,48,51,58,
    733    59,60,63,64,65,66,67: #ARG]
    734  [1: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2
    735  
    736  [7: #arg2]
     736   59,60,63,64,65,66,67: #ARG]]
     737 [4,5,6,7,8,9,10,11,12,13,22,23,24,27,28,39,40,41,42,43,44,45,46,47,48,49,50,51,52,
     738  56,57,69,70,72,73,75: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2
     739  [1,2,4,7,9,10,12,13,15,16,17,18,20,22,23,24,25,26,27,28,29,30,31,32,33,36,37,38,
     740   39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,
     741   68,69,70,71: #ARG2]]
     742 [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
     743 normalize in ⊢ (???% → ?)
     744 [42,93,95: @split_elim #vl #vm #E >E -E; normalize in ⊢ (???% → ?)
     745 |92,94: cases daemon ]
     746 #H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2)
     747 try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4
     748 change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
     749 whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
     750 [1,2,3,4,5,6,7,8,9,10,15,18,19,20,21,22: <H3]
     751 [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,27,29,32,33,36,
     752  37,38,39,40,41,44,45, 46,49,50,53,54,57,58,62,64,65,68,69,79,82,85,86,87,88,
     753  89,90,91,92,93,94: <H2]
     754 whd >eq_instruction_refl >H4 try @eq_bv_refl
     755qed.
     756     
     757
     758 |*:
     759 >eq_instruction_refl >H4 @eq_bv_refl
     760qed.
     761
    737762 
    738763  whd
Note: See TracChangeset for help on using the changeset viewer.