Changeset 1648


Ignore:
Timestamp:
Jan 18, 2012, 11:01:14 AM (6 years ago)
Author:
mulligan
Message:

new version of utilities/monad.ma with typecheck command comented out

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1646 r1648  
    118118qed.
    119119
    120 axiom is_in_subvector_is_in_supervector:
     120lemma is_in_singleton_to_is_a:
     121  ∀tag.
     122  ∀element.
     123    is_in … [[tag]] element → is_a tag element.
     124  #tag #element
     125  normalize in ⊢ (% → ?);
     126  cases (is_a tag element)
     127  [1:
     128    normalize nodelta #irrelevant
     129    @I
     130  |2:
     131    normalize nodelta #absurd
     132    cases absurd
     133  ]
     134qed.
     135       
     136lemma is_a_decidable:
     137  ∀hd.
     138  ∀element.
     139    is_a hd element = true ∨ is_a hd element = false.
     140  #hd #element //
     141qed.
     142
     143lemma mem_decidable:
     144  ∀n: nat.
     145  ∀v: Vector addressing_mode_tag n.
     146  ∀element: addressing_mode_tag.
     147    mem … eq_a n v element = true ∨
     148      mem … eq_a … v element = false.
     149  #n #v #element //
     150qed.
     151
     152(*
     153lemma is_in_cons_hd_tl_to_is_in_tl:
     154  ∀n: nat.
     155  ∀the_vect: Vector addressing_mode_tag n.
     156  ∀h: addressing_mode_tag.
     157  ∀element: addressing_mode.
     158    is_in (S n) (h:::the_vect) element →
     159      is_in n the_vect element. *)
     160
     161lemma is_in_subvector_is_in_supervector:
    121162  ∀m, n: nat.
    122163  ∀subvector: Vector addressing_mode_tag m.
     164  ∀supervector: Vector addressing_mode_tag n.
    123165  ∀element: addressing_mode.
    124   ∀supervector: Vector addressing_mode_tag n.
    125166    subvector_with … eq_a subvector supervector →
    126167      is_in m subvector element → is_in n supervector element.
     168  (*
     169  #m #n #subvector #supervector #element
     170  elim subvector
     171  [1:
     172    #subvector_with_proof #is_in_proof
     173    cases is_in_proof
     174  |2:
     175    #n #hd #tl #inductive_hypothesis
     176    cases supervector
     177    [1:
     178      #subvector_with_proof #is_in_proof
     179      cases subvector_with_proof
     180    |2:
     181      #n' #hd' #tl' #subvector_with_proof #is_in_proof
     182      whd in match (is_in … (hd':::tl') element);
     183      cases (is_a_decidable hd' element)
     184      [1:
     185        #is_a_true >is_a_true normalize nodelta
     186        @I
     187      |2:
     188        #is_a_false >is_a_false normalize nodelta
     189        @inductive_hypothesis'
     190        [2:
     191          assumption
     192        |1:
     193        ]
     194      ]     
     195    ]
     196  ]
     197qed.
     198  |3:
     199    #n #hd #tl #inductive_hypothesis
     200    #subvector_with_proof #is_in_proof
     201    @inductive_hypothesis
     202    [1:
     203      assumption
     204  |4:
     205  ]
     206qed.
     207 
     208 
     209 
     210  [1:
     211    #n #supervector #subvector_proof #is_in_proof
     212    cases is_in_proof
     213  |2:
     214    #m' #hd #tl #inductive_hypothesis #n' #supervector
     215    #subvector_proof #is_in_proof
     216    generalize in match is_in_proof;
     217    cases(is_a_decidable hd element)
     218    whd in match (is_in … (hd:::tl) element);
     219    [1:
     220      #is_a_true >is_a_true normalize nodelta
     221      #irrelevant
     222    |2:
     223      #is_a_false >is_a_false normalize nodelta
     224      #assm
     225      @inductive_hypothesis
     226      [1:
     227        generalize in match subvector_proof;
     228        whd in match (subvector_with … eq_a (hd:::tl) supervector);
     229        cases(mem_decidable n' supervector hd)
     230        [1:
     231          #mem_true >mem_true normalize nodelta
     232          #assm assumption
     233        |2:
     234          #mem_false >mem_false #absurd
     235          cases absurd
     236        ]
     237      |2:
     238        assumption
     239      ]
     240    ]
     241   
     242   
     243   
     244   
     245    generalize in match subvector_proof;
     246    whd in match (subvector_with … eq_a (hd:::tl) supervector);
     247    cases(mem_decidable n' supervector hd)
     248    [1:
     249      #mem_true >mem_true normalize nodelta
     250      #subvector_with_proof
     251      @inductive_hypothesis
     252      [1:
     253        assumption
     254      |2:
     255        generalize in match is_in_proof;
     256        whd in match (is_in (S m') (hd:::tl) element);
     257        cases(is_a_decidable hd element)
     258        [1:
     259          #is_a_true >is_a_true normalize nodelta
     260          #irrelevant
     261          whd whd in match (is_in … tl element);
     262        |2:
     263          #is_a_false >is_a_false normalize nodelta
     264          #assm assumption
     265        ]
     266      ]
     267    |2:
     268      #mem_false >mem_false normalize nodelta
     269      #absurd cases absurd
     270    ]
     271    |1:
     272      normalize nodelta #subvector_with_assm
     273      cases(is_a_decidable hd element)
     274      [1:
     275        #is_a_hd
     276        generalize in match subvector_proof;
     277        whd in match (subvector_with … eq_a (hd:::tl) supervector);
     278      |2:
     279        #not_is_a_hd
     280      ]
     281    ]
     282  ] *)
     283  cases daemon
     284qed.
    127285
    128286let rec member_addressing_mode_tag
     
    538696  λgood_program_witness: good_program code_memory program_size.
    539697    traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness.
    540 
     698 
    541699definition compute_costs ≝
    542700  λprogram: list Byte.
    543701  λcost_labels: BitVectorTrie costlabel 16.
    544   λhas_main: bool.
    545   λreachable_program_counter_witness:
    546    ∀lbl: costlabel.
    547    ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
    548      reachable_program_counter (load_code_memory program) (|program| + 1) program_counter. 
     702  λreachable_program_witness.
    549703  λgood_program_witness: good_program (load_code_memory program) (|program| + 1).
    550704    let program_size ≝ |program| + 1 in
    551705    let code_memory ≝ load_code_memory program in
    552       traverse_code code_memory cost_labels program_size reachable_program_counter_witness ?.
     706      traverse_code code_memory cost_labels program_size reachable_program_witness ?.
    553707  @good_program_witness
    554708qed.
  • src/ASM/CostsProof.ma

    r1620 r1648  
    66include alias "arithmetics/nat.ma".
    77include alias "basics/logic.ma".
     8
     9definition current_instruction0 ≝
     10  λcode_memory: BitVectorTrie Byte 16.
     11  λprogram_counter: Word.
     12    \fst (\fst (fetch … code_memory program_counter)).
     13
     14definition current_instruction ≝
     15  λs: Status.
     16    current_instruction0 (code_memory … s) (program_counter … s).
     17
     18definition ASM_classify0: instruction → status_class ≝
     19  λi: instruction.
     20    match i with
     21     [ RealInstruction pre ⇒
     22       match pre with
     23        [ RET ⇒ cl_return
     24        | JZ _ ⇒ cl_jump
     25        | JNZ _ ⇒ cl_jump
     26        | JC _ ⇒ cl_jump
     27        | JNC _ ⇒ cl_jump
     28        | JB _ _ ⇒ cl_jump
     29        | JNB _ _ ⇒ cl_jump
     30        | JBC _ _ ⇒ cl_jump
     31        | CJNE _ _ ⇒ cl_jump
     32        | DJNZ _ _ ⇒ cl_jump
     33        | _ ⇒ cl_other
     34        ]
     35     | ACALL _ ⇒ cl_call
     36     | LCALL _ ⇒ cl_call
     37     | JMP _ ⇒ cl_call
     38     | AJMP _ ⇒ cl_jump
     39     | LJMP _ ⇒ cl_jump
     40     | SJMP _ ⇒ cl_jump
     41     | _ ⇒ cl_other
     42     ].
     43
     44definition ASM_classify: Status → status_class ≝
     45 λs: Status.
     46   ASM_classify0 (current_instruction s).
    847
    948let rec compute_max_trace_label_label_cost
  • src/utilities/monad.ma

    r1647 r1648  
    126126interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f).
    127127
     128(*
    128129check (λM : Monad.λA,B,C,P.λp.λf : ∀a,b.P 〈a,b〉 → monad M C.! «a,b,H» ← p; f a b H)
     130*)
    129131
    130132record MonadProps : Type[1] ≝
Note: See TracChangeset for help on using the changeset viewer.