Changeset 2148


Ignore:
Timestamp:
Jul 3, 2012, 4:14:45 AM (5 years ago)
Author:
sacerdot
Message:
  1. specification made more user-friendly for AssemblyProof?
  2. no more daemons in AssemblyProof?
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2147 r2148  
    707707     next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction))
    708708     ∧
    709      (nat_of_bitvector … pc < nat_of_bitvector … next_pc ∨
     709     (nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction < 2^16
     710      (*nat_of_bitvector … pc < nat_of_bitvector … next_pc*) ∨
    710711      S (nat_of_bitvector … ppc) = |instr_list| ∧ next_pc = zero …).
    711712
  • src/ASM/AssemblyProof.ma

    r2147 r2148  
    397397   cases (SIGMAOK2 (bitvector_of_nat … m) ?) -SIGMAOK2
    398398   [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption ]
    399    #_ *
     399   #H *
    400400   [ #LTsigma_m %1 @(transitive_le … IH) -IH
    401      <add_bitvector_of_nat_Sm >add_commutative
    402      @(transitive_le … LTsigma_m) %2 %
     401     <add_bitvector_of_nat_Sm >add_commutative >H -H
     402     >nat_of_bitvector_add
     403     [ //
     404     | >nat_of_bitvector_bitvector_of_nat_inverse try assumption lapply LTsigma_m
     405       whd in match instruction_size; normalize nodelta
     406       inversion (assembly_1_pseudoinstruction ??????) #len #assembled #EQ #X
     407       @(transitive_le … X) @le_S_S //
     408     ]
    403409   | * #EQ1 #EQ2 %2 %
    404410     [ <add_bitvector_of_nat_Sm >add_commutative assumption
     
    495501            [ @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? eq_assembly_1_pseudoinstruction)
    496502              / by /
    497             | <EQlen cases daemon (*CSC: TRUE BECAUSE OF NO_OVERFLOW*)
     503            | <EQlen assumption
    498504            | assumption
    499505            ]
Note: See TracChangeset for help on using the changeset viewer.