Changeset 1939


Ignore:
Timestamp:
May 14, 2012, 10:37:08 AM (8 years ago)
Author:
mulligan
Message:

Changes to get things to compile and to avoid the dependency circularity between ASM/Interpret.ma and common/StructuredTraces.ma. New file ASM/AbstractStatus.ma factors out the definition (not the implementation!) of an abstract status, which both of the previously mentioned files require.

Location:
src
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1936 r1939  
    107107  ∀P: ∀m. Vector A m → Prop.
    108108    n = m → v1 ≃ v2 → P n v1 → P m v2.
    109   #A #n #m #v1 #v2 #P #EQ
    110   <EQ in v2; #V #JMEQ
    111   >JMEQ //
     109  #A #n #m #v1 #v2 #P #eq #jmeq
     110  destruct #assm assumption
    112111qed.
    113112
     
    119118    e ::: v = [[ e ]] @@ v.
    120119  #A #n #e #v
    121   elim v
    122   [1:
    123     normalize %
    124   |2:
    125     #NN #AA #VV #IH
    126     normalize
    127     %
    128   ]
     120  cases v try %
     121  #n' #hd #tl %
    129122qed.
    130123
     
    137130    hd:::(v@@q) = (hd:::v)@@q.
    138131  #A #n #m #v #q
    139   elim v
    140   [1:
    141     #hd %
    142   |2:
    143     #n' #hd' #tl' #ih #hd'
    144     <ih %
    145   ]
     132  elim v try (#hd %)
     133  #n' #hd' #tl' #ih #hd'
     134  <ih %
    146135qed.
    147136
     
    185174    mem A eq ? (p@@(a:::r)) a = true.
    186175  #A #m #o #eq #reflex #p #a
    187   elim p
    188   [1:
    189     normalize
    190     >reflex
    191     #H %
    192   |2:
    193     #m' #hd #tl #inductive_hypothesis
    194     normalize
    195     cases (eq ??) normalize nodelta
    196     [1:
    197       #_ %
    198     |2:
    199       @inductive_hypothesis
    200     ]
    201   ]
     176  elim p try (normalize >reflex #H %)
     177  #m' #hd #tl #inductive_hypothesis
     178  normalize
     179  cases (eq ??) normalize nodelta
     180  try (#irrelevant %)
     181  @inductive_hypothesis
    202182qed.
    203183
     
    212192    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
    213193  #A #m #o #eq #reflex #p #a
    214   elim p
    215   [1:
    216     #r #assm assumption
    217   |2:
    218     #m' #hd #tl #inductive_hypothesis #r #assm
    219     normalize
    220     cases (eq ??) try %
    221     @inductive_hypothesis assumption
    222   ]
     194  elim p try (#r #assm assumption)
     195  #m' #hd #tl #inductive_hypothesis #r #assm
     196  normalize
     197  cases (eq ??) try %
     198  @inductive_hypothesis assumption
    223199qed.
    224200
     
    234210    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
    235211  #A #o #n #eq #reflex #h #v
    236   elim v
     212  elim v try (normalize #m #irrelevant @I)
     213  #m' #hd #tl #inductive_hypothesis #m #q
     214  change with (bool_to_Prop (andb ??))
     215  cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true)
    237216  [1:
    238     normalize #m #_ @I
     217    @mem_monotonic_wrt_append try assumption
     218    @mem_monotonic_wrt_append try assumption
     219    normalize >reflex %
    239220  |2:
    240     #m' #hd #tl #inductive_hypothesis #m #q
    241     change with (bool_to_Prop (andb ??))
    242     cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true)
    243     [1:
    244       @mem_monotonic_wrt_append try assumption
    245       @mem_monotonic_wrt_append try assumption
    246       normalize >reflex %
    247     |2:
    248       #assm >assm
    249       >vector_cons_append
    250       change with (bool_to_Prop (subvector_with ??????))
    251       @(super_rewrite2 … (vector_associative_append … q [[hd]] tl))
    252       try @associative_plus
    253       @inductive_hypothesis
    254     ]
     221    #assm >assm
     222    >vector_cons_append
     223    change with (bool_to_Prop (subvector_with ??????))
     224    @(super_rewrite2 … (vector_associative_append … q [[hd]] tl))
     225    try @associative_plus
     226    @inductive_hypothesis
    255227  ]
    256228qed.
     
    803775    eq_sum A B leq req s s = true.
    804776  #A #B #leq #req #s #leq_refl #req_refl
    805   cases s
    806   whd in ⊢ (? → ??%?);
    807   assumption
     777  cases s assumption
    808778qed.
    809779
     
    828798  try @eq_addressing_mode_refl
    829799  [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
    830     whd in ⊢ (??%?);
    831     try %
     800    whd in ⊢ (??%?); try %
    832801    >eq_addressing_mode_refl
    833802    >eq_addressing_mode_refl %
     
    852821    |3:
    853822      #arg1_left normalize nodelta
    854       >(eq_sum_refl …) [1: %
    855       |2,3: #arg @eq_prod_refl #arg @eq_addressing_mode_refl ]
     823      >(eq_sum_refl …)
     824      [1:
     825        %
     826      |2,3:
     827        #arg @eq_prod_refl #arg @eq_addressing_mode_refl
     828      ]
    856829    |4:
    857830      #arg1_left normalize nodelta
     
    12911264*)
    12921265
    1293 lemma split_elim:
     1266definition split_elim:
    12941267  ∀A: Type[0].
    12951268  ∀l, m: nat.
     
    12981271    (∀vl: Vector A l.
    12991272     ∀vm: Vector A m.
    1300       v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
    1301   cases daemon (* XXX: problem with dependent types *)
    1302 qed.
     1273      v = vl@@vm → P 〈vl,vm〉) → P (split A l m v) ≝
     1274  λa: Type[0].
     1275  λl, m: nat.
     1276  λv: Vector a (l + m).
     1277  λP.
     1278  match v return λn: nat. λv: Vector a (n + m).
     1279    (∀vl: Vector a ?.
     1280     ∀vm: Vector a m.
     1281      v = vl@@vm → P 〈vl,vm〉) → P (split a ? m v) with
     1282  [ VEmpty ⇒ ?
     1283  | VCons v' hd tl ⇒ ?
     1284  ] ?.
    13031285
    13041286(* XXX: this looks almost certainly wrong *)
  • src/ASM/Interpret.ma

    r1938 r1939  
    22include "ASM/StatusProofs.ma".
    33include "ASM/Fetch.ma".
    4 include "common/StructuredTraces.ma".
     4include "ASM/AbstractStatus.ma".
    55
    66definition sign_extension: Byte → Word ≝
     
    120120include alias "arithmetics/nat.ma".
    121121include alias "ASM/BitVectorTrie.ma".
    122 
    123 definition ASM_classify00: ∀a. preinstruction a → status_class ≝
    124   λa, pre.
    125   match pre with
    126   [ RET ⇒ cl_return
    127   | RETI ⇒ cl_return
    128   | JZ _ ⇒ cl_jump
    129   | JNZ _ ⇒ cl_jump
    130   | JC _ ⇒ cl_jump
    131   | JNC _ ⇒ cl_jump
    132   | JB _ _ ⇒ cl_jump
    133   | JNB _ _ ⇒ cl_jump
    134   | JBC _ _ ⇒ cl_jump
    135   | CJNE _ _ ⇒ cl_jump
    136   | DJNZ _ _ ⇒ cl_jump
    137   | _ ⇒ cl_other
    138   ].
    139 
    140 definition ASM_classify0: instruction → status_class ≝
    141   λi.
    142   match i with
    143    [ RealInstruction pre ⇒ ASM_classify00 [[relative]] pre
    144    | ACALL _ ⇒ cl_call
    145    | LCALL _ ⇒ cl_call
    146    | JMP _ ⇒ cl_call
    147    | AJMP _ ⇒ cl_other
    148    | LJMP _ ⇒ cl_other
    149    | SJMP _ ⇒ cl_other
    150    | _ ⇒ cl_other
    151    ].
    152 
    153 definition current_instruction0 ≝
    154   λcode_memory: BitVectorTrie Byte 16.
    155   λprogram_counter: Word.
    156     \fst (\fst (fetch … code_memory program_counter)).
    157 
    158 definition current_instruction ≝
    159   λcode_memory.
    160   λs: Status code_memory.
    161     current_instruction0 code_memory (program_counter … s).
    162    
    163 definition current_instruction_label ≝
    164   λcode_memory.
    165   λcost_labels: BitVectorTrie costlabel 16.
    166   λs: Status code_memory.
    167   let pc ≝ program_counter … code_memory s in
    168     lookup_opt … pc cost_labels.
    169 
    170 definition next_instruction_properly_relates_program_counters ≝
    171   λcode_memory.
    172   λbefore: Status code_memory.
    173   λafter : Status code_memory.
    174     let program_counter_before ≝ program_counter ? code_memory before in
    175     let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
    176       program_counter ? code_memory after = program_counter_after.
    177 
    178 definition word_deqset: DeqSet ≝
    179   mk_DeqSet Word (eq_bv 16) ?.
    180   @refl_iff_eq_bv_true
    181 qed.
    182    
    183 definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
    184   λcode_memory.
    185   λs: Status code_memory.
    186     ASM_classify0 (current_instruction … s).
    187122
    188123definition execute_1_preinstruction':
  • src/common/StructuredTraces.ma

    r1938 r1939  
    66include "basics/lists/listb.ma".
    77include "ASM/Util.ma".
    8 
    9 inductive status_class : Type[0] ≝
    10 | cl_return : status_class
    11 | cl_jump   : status_class
    12 | cl_call   : status_class
    13 | cl_other : status_class.
    14 
    15 record abstract_status : Type[1] ≝
    16 {
    17     as_status :> Type[0]
    18   ; as_execute : as_status → as_status → Prop
    19   ; as_pc : DeqSet
    20   ; as_pc_of : as_status → as_pc
    21   ; as_classifier : as_status → status_class → Prop
    22   ; as_label : as_status → option costlabel
    23   ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
    24   ; as_final: as_status → Prop
    25 }.
     8include "ASM/AbstractStatus.ma".
    269
    2710(* temporary alias for backward compatibility *)
     
    436419  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
    437420    (start_status: S) (final_status: S)
     421     
    438422      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
    439423        on the_trace: list (Σl: costlabel. ∃s. as_label S s = Some … l) ≝
     
    492476  ]
    493477qed.
     478
     479(* XXX: dependent type madness *)
     480
     481let rec tll_rel_to_traces_same_cost
     482  (S: abstract_status) (S': abstract_status)
     483    (trace_ends_flag_l: trace_ends_with_ret) (trace_ends_flag_r: trace_ends_with_ret)
     484    (start_status_l: S) (final_status_l: S) (start_status_r: S') (final_status_r: S')
     485      (the_trace_l: trace_label_label S trace_ends_flag_l start_status_l final_status_l)
     486        (the_trace_r: trace_label_label S' trace_ends_flag_r start_status_r final_status_r)
     487          on the_trace_l:
     488            tll_rel … the_trace_l the_trace_r →
     489              as_compute_cost_trace_label_label … the_trace_l =
     490                as_compute_cost_trace_label_label S' trace_ends_flag_r ? ? the_trace_r ≝ ?.
     491and tal_rel_to_traces_same_cost
     492  (S: abstract_status) (S': abstract_status) (trace_ends_flag_l: trace_ends_with_ret)
     493    (trace_ends_flag_r: trace_ends_with_ret)
     494      (start_status_l: S) (final_status_l: S) (start_status_r: S') (final_status_r: S')
     495        (the_trace_l: trace_any_label S trace_ends_flag_l start_status_l final_status_l)
     496          (the_trace_r: trace_any_label S' trace_ends_flag_r start_status_r final_status_r)
     497          on the_trace_l:
     498            tal_rel … the_trace_l the_trace_r →
     499              as_compute_cost_trace_any_label … the_trace_l =
     500                as_compute_cost_trace_any_label … the_trace_r ≝ ?
     501and tlr_rel_to_traces_same_cost
     502  (S: abstract_status) (S': abstract_status) (start_status_l: S) (final_status_l: S)
     503    (start_status_r: S') (final_status_r: S')
     504      (the_trace_l: trace_label_return S start_status_l final_status_l)
     505        (the_trace_r: trace_label_return S' start_status_r final_status_r)
     506        on the_trace_l:
     507          tlr_rel … the_trace_l the_trace_r →
     508            as_compute_cost_trace_label_return … the_trace_l =
     509              as_compute_cost_trace_label_return … the_trace_r ≝ ?.
     510  cases daemon
     511qed.
Note: See TracChangeset for help on using the changeset viewer.