Ignore:
Timestamp:
Jun 27, 2012, 7:14:32 PM (8 years ago)
Author:
mulligan
Message:

Large changes from today trying to complete the main theorem. Again :(

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2128 r2129  
    6464          let 〈instr, pc', ticks〉 ≝ fetch code_memory pc in
    6565           (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' pc_plus_len) = true.
     66  cases daemon
     67(* XXX: commented out as takes ages to typecheck
    6668  #pc #i #code_memory #assembled cases i [8: *]
    6769 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
     
    8385 whd in match fetch; normalize nodelta <H1 whd in ⊢ (match % with [ _ ⇒ ? ]);
    8486 [17,18,19,20,21,22,23,24,25,26,32,34,35,36,37,39: <H3]
    85  try <H2 whd >eq_instruction_refl >H4 @eq_bv_refl
     87 try <H2 whd >eq_instruction_refl >H4 @eq_bv_refl *)
    8688qed.
    8789
     
    936938  ∀i: instruction.
    937939    |(assembly1 i)| < 128.
     940  cases daemon
     941(* XXX: commented out as takes ages to type check
    938942  #i cases i
    939943  try (#assm1 #assm2) try #assm1
     
    10041008    @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n
    10051009  ]
    1006 qed.
     1010  *)
     1011qed.
Note: See TracChangeset for help on using the changeset viewer.