Changeset 1669 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Feb 1, 2012, 3:36:08 PM (9 years ago)
Author:
mulligan
Message:

Commit for claudio

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/ASMCosts.ma

    r1665 r1669  
    363363
    364364definition current_instruction ≝
    365   λs: Status.
    366     current_instruction0 (code_memory … s) (program_counter … s).
     365  λcode_memory.
     366  λs: Status code_memory.
     367    current_instruction0 code_memory (program_counter … s).
    367368
    368369definition ASM_classify0: instruction → status_class ≝
    … …  
    392393   ].
    393394
    394 definition ASM_classify: Status → status_class ≝
    395   λs: Status.
    396     ASM_classify0 (current_instruction s).
     395definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
     396  λcode_memory.
     397  λs: Status code_memory.
     398    ASM_classify0 (current_instruction … s).
    397399
    398400definition current_instruction_is_labelled ≝
     401  λcode_memory.
    399402  λcost_labels: BitVectorTrie costlabel 16.
    400   λs: Status.
    401   let pc ≝ program_counter … s in
     403  λs: Status code_memory.
     404  let pc ≝ program_counter … code_memory s in
    402405    match lookup_opt … pc cost_labels with
    403406    [ None ⇒ False
    … …  
    406409
    407410definition next_instruction_properly_relates_program_counters ≝
    408   λbefore: Status.
    409   λafter : Status.
    410   let size ≝ current_instruction_cost before in
    411   let pc_before ≝ program_counter … before in
    412   let pc_after ≝ program_counter … after in
     411  λcode_memory.
     412  λbefore: Status code_memory.
     413  λafter : Status code_memory.
     414  let size ≝ current_instruction_cost code_memory before in
     415  let pc_before ≝ program_counter … code_memory before in
     416  let pc_after ≝ program_counter … code_memory after in
    413417  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
    414418    sum = pc_after.
    415419
    416 definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
    417  λcost_labels.
    418   mk_abstract_status
    419    Status
    420    (λs,s'. (execute_1 s) = s')
    421    (λs,class. ASM_classify s = class)
    422    (current_instruction_is_labelled cost_labels)
    423    next_instruction_properly_relates_program_counters.
     420definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
     421  λcode_memory.
     422  λcost_labels.
     423    mk_abstract_status
     424      (Status code_memory)
     425      (λs,s'. (execute_1 … s) = s')
     426      (λs,class. ASM_classify … s = class)
     427      (current_instruction_is_labelled … cost_labels)
     428      (next_instruction_properly_relates_program_counters code_memory).
    424429
    425430let rec trace_any_label_length
    426   (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret)
    427     (start_status: Status) (final_status: Status)
    428       (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     431  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     432    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
     433      (final_status: Status code_memory)
     434      (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
    429435        on the_trace: nat ≝
    430436  match the_trace with
    … …  
    443449
    444450let rec compute_paid_trace_any_label
    445   (cost_labels: BitVectorTrie costlabel 16)
    446   (trace_ends_flag: trace_ends_with_ret)
    447    (start_status: Status) (final_status: Status)
    448      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     451  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     452    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
     453      (final_status: Status code_memory)
     454        (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
    449455       on the_trace: nat ≝
    450456  match the_trace with
    451   [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
    452   | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
    453   | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ current_instruction_cost pre_fun_call
     457  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status
     458  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status
     459  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ current_instruction_cost … pre_fun_call
    454460  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    455461     _ _ _ call_trace _ final_trace ⇒
    456       let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
    457       let final_trace_cost ≝ compute_paid_trace_any_label cost_labels end_flag … final_trace in
     462      let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in
     463      let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in
    458464        current_instruction_cost + final_trace_cost
    459465  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    460       let current_instruction_cost ≝ current_instruction_cost status_pre in
     466      let current_instruction_cost ≝ current_instruction_cost … status_pre in
    461467      let tail_trace_cost ≝
    462        compute_paid_trace_any_label cost_labels end_flag
     468       compute_paid_trace_any_label … cost_labels end_flag
    463469        status_init status_end tail_trace
    464470      in
    … …  
    467473
    468474definition compute_paid_trace_label_label ≝
    469  λcost_labels: BitVectorTrie costlabel 16.
     475  λcode_memory: BitVectorTrie Byte 16.
     476  λcost_labels: BitVectorTrie costlabel 16.
    470477  λtrace_ends_flag: trace_ends_with_ret.
    471    λstart_status: Status.
    472     λfinal_status: Status.
    473      λthe_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
    474       start_status final_status.
     478  λstart_status: Status code_memory.
     479  λfinal_status: Status code_memory.
     480  λthe_trace: trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    475481  match the_trace with
    476482  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
    … …  
    487493qed.
    488494
    489 axiom as_execute_preserves_code_memory:
    490   ∀cost_labels : BitVectorTrie costlabel 16.
    491   ∀start_status: ASM_abstract_status cost_labels.
    492   ∀final_status: ASM_abstract_status cost_labels.
    493     as_execute … start_status final_status →
    494       code_memory … start_status = code_memory … final_status.
    495 
    496 axiom trace_label_return_preserves_code_memory:
    497   ∀cost_labels : BitVectorTrie costlabel 16.
    498   ∀start_status: ASM_abstract_status cost_labels.
    499   ∀final_status: ASM_abstract_status cost_labels.
    500   ∀the_trace   : trace_label_return … start_status final_status.
    501     code_memory … start_status = code_memory … final_status.
    502 
    503495(* XXX: indexing bug re-emerges! *)
    504496example fetch_half_add:
     497  ∀code_memory: BitVectorTrie Byte 16.
    505498  ∀cost_labels: BitVectorTrie costlabel 16.
    506   ∀the_status : ASM_abstract_status cost_labels.
    507     \snd (\fst (fetch (code_memory … the_status) (program_counter … the_status))) =
    508       \snd (half_add 16 (program_counter (BitVectorTrie Byte 16) the_status)
    509         (bitvector_of_nat … (\snd (fetch (code_memory … the_status) (program_counter … the_status))))).
     499  ∀the_status : ASM_abstract_status code_memory cost_labels.
     500    \snd (\fst (fetch code_memory (program_counter … the_status))) =
     501      \snd (half_add 16 (program_counter … the_status)
     502        (bitvector_of_nat … (\snd (fetch code_memory (program_counter … the_status))))).
    510503  cases daemon
    511504qed.
    … …  
    523516    (m - n) + n = m.
    524517  #m #n #proof /2 by plus_minus/
     518qed.
     519
     520(* XXX: indexing bug *)
     521example fetch_twice_fetch_execute_1:
     522  ∀code_memory: BitVectorTrie Byte 16.
     523  ∀start_status: Status code_memory.
     524    \snd (\fst (fetch code_memory (program_counter … start_status))) =
     525      program_counter … (execute_1 … start_status).
     526  cases daemon
     527qed. (*
     528  #code_memory #start_status
     529  whd in match (execute_1 code_memory start_status);
     530  whd in match (execute_1' code_memory start_status); normalize nodelta
     531  cases (fetch code_memory (program_counter … start_status)) #instruction_pc #ticks
     532  cases instruction_pc #instruction #pc normalize nodelta *)
     533
     534lemma blah:
     535  ∀code_memory' : (BitVectorTrie Byte 16).
     536  ∀program_counter' : Word.
     537  ∀total_program_size : ℕ.
     538  ∀cost_labels : (BitVectorTrie costlabel 16).
     539  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
     540  ∀good_program_witness : (good_program code_memory' total_program_size).
     541  ∀program_size' : ℕ.
     542  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
     543  ∀ticks : ℕ.
     544  ∀instruction : instruction.
     545  ∀program_counter'' : Word.
     546  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
     547  ∀real_instruction : (preinstruction [[relative]]).
     548  ∀real_instruction_refl : (RealInstruction … real_instruction = instruction).
     549  ∀start_status : (Status code_memory').
     550  ∀final_status : (Status code_memory').
     551  ∀trace_ends_flag : trace_ends_with_ret.
     552  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
     553  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
     554  ∀classify_assm: ASM_classify0 instruction = cl_other.
     555  ∀pi1 : ℕ.
     556   (if match lookup_opt costlabel 16 program_counter'' cost_labels with 
     557         [None ⇒ true
     558         |Some _ ⇒ false
     559         ] 
     560    then
     561      ∀start_status0:Status code_memory'.
     562      ∀final_status0:Status code_memory'.
     563      ∀trace_ends_flag0:trace_ends_with_ret.
     564      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
     565        program_counter'' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
     566        (∃n:ℕ
     567                    .trace_any_label_length code_memory' cost_labels
     568                     trace_ends_flag0 start_status0 final_status0 the_trace0
     569                     +S n
     570                     =total_program_size)
     571                   ∧pi1
     572                    =compute_paid_trace_any_label code_memory' cost_labels
     573                     trace_ends_flag0 start_status0 final_status0 the_trace0
     574    else (pi1=O) )
     575   →(∃n:ℕ
     576     .trace_any_label_length code_memory' cost_labels trace_ends_flag
     577      start_status final_status the_trace
     578      +S n
     579      =total_program_size)
     580    ∧ticks+pi1
     581     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
     582      start_status final_status the_trace.
     583  #code_memory' #program_counter' #total_program_size #cost_labels
     584  #reachable_program_counter_witness #good_program_witness
     585  #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
     586  #real_instruction #real_instruction_refl #start_status #final_status
     587  #trace_ends_flag #the_trace #program_counter_refl #classify_assm #recursive_block_cost
     588  #recursive_assm @(trace_any_label_inv_ind … the_trace)
     589    [5:
     590      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
     591      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
     592      #the_trace_refl
     593      destruct
     594      whd in match (trace_any_label_length … (tal_step_default …));
     595      whd in match (compute_paid_trace_any_label … (tal_step_default …));
     596      whd in costed_assm:(?%);
     597      generalize in match costed_assm;
     598      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
     599      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
     600        in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
     601      #lookup_assm cases lookup_assm
     602      [1:
     603        #None_lookup_opt_assm normalize nodelta #ignore
     604        generalize in match recursive_assm;
     605        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 code_memory' status_pre)))
     606        [1:
     607          <fetch_twice_fetch_execute_1 <FETCH %
     608        |2:
     609          #program_counter_assm >program_counter_assm <None_lookup_opt_assm
     610          normalize nodelta #new_recursive_assm
     611          cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
     612            end_flag trace_any_label ?) [2: % ]
     613          #exists_assm #recursive_block_cost_assm %
     614          [1:
     615            cases exists_assm #exists_n #total_program_size_refl
     616            <total_program_size_refl
     617            %{(exists_n - current_instruction_cost … status_pre)}
     618          |2:
     619            >recursive_block_cost_assm
     620            whd in match (current_instruction_cost … status_pre);
     621            cut(ticks = \snd (fetch code_memory'
     622               (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
     623            [1:
     624              <FETCH %
     625            |2:
     626              #ticks_refl_assm >ticks_refl_assm %
     627            ]
     628          ]
     629        ]
     630      |2:
     631        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta
     632        #absurd cases absurd #absurd cases(absurd I)
     633      ]
     634    |1:
     635      #status_start #status_final #execute_assm #classifier_assm #costed_assm
     636      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     637      destruct
     638      whd in match (trace_any_label_length … (tal_base_not_return …));
     639      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
     640      whd in costed_assm;
     641      generalize in match costed_assm;
     642      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
     643      generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels)
     644        in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
     645      #lookup_assm cases lookup_assm
     646      [1:
     647        #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm
     648        #absurd cases absurd
     649      |2:
     650        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
     651        generalize in match recursive_assm;
     652        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_start)))
     653        [1:
     654          <fetch_twice_fetch_execute_1 <FETCH %
     655        |2:
     656          #program_counter_assm >program_counter_assm <Some_lookup_opt_assm
     657          normalize nodelta #new_recursive_assm >new_recursive_assm %
     658          [1:
     659            %{(pred total_program_size)} whd in ⊢ (??%?);
     660            @S_pred
     661            generalize in match good_program_witness;
     662            whd in match (good_program … total_program_size);
     663            #good_program_hyp
     664            lapply(good_program_hyp (program_counter … status_start) reachable_program_counter_witness)
     665            <FETCH normalize nodelta -good_program_hyp (* XXX: Claudio here *)
     666          |2:
     667            cut(ticks = \snd (fetch code_memory'
     668               (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
     669            [1:
     670              <FETCH %
     671            |2:
     672              #ticks_refl_assm >ticks_refl_assm
     673              <plus_n_O %
     674            ]
     675          ]
     676        ]
     677      |2:
     678        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta
     679        #absurd cases absurd #absurd cases(absurd I)
     680      ]
     681    |2:
     682      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
     683      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
     684    |3:
     685      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     686      #classifier_assm #after_return_assm #trace_label_return #costed_assm
     687      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     688      destruct @⊥
     689    ]
     690      change with (
     691        ASM_classify0 ? = ?) in classifier_assm;
     692      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
     693      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     694      <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
    525695qed.
    526696
    … …  
    533703          total_program_size ≤ program_size + nat_of_bitvector … program_counter' →
    534704          Σcost_of_block: nat.
    535             ∀start_status: Status.
    536             ∀final_status: Status.
     705          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
     706            ∀start_status: Status code_memory'.
     707            ∀final_status: Status code_memory'.
    537708            ∀trace_ends_flag.
    538             ∀the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
    539               code_memory' = code_memory … start_status →
    540                 program_counter' = program_counter … start_status →
    541                     (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
    542                       cost_of_block = compute_paid_trace_any_label cost_labels trace_ends_flag start_status final_status the_trace ≝
     709            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     710              program_counter' = program_counter … start_status →
     711                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
     712                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
     713          else
     714            (cost_of_block = 0) ≝
    543715  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter' → ? with
    544716  [ O ⇒ λbase_case. ⊥
    … …  
    546718    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
    547719    let to_continue ≝
    548       match lookup_opt … program_counter'' cost_labels with
     720      match lookup_opt … program_counter' cost_labels with
    549721      [ None ⇒ true
    550722      | Some _ ⇒ first_time_around
    551723      ]
    552724    in
    553       if to_continue then
    554         match instruction return λx. x = instruction → ? with
     725      ((if to_continue then
     726       pi1 … (match instruction return λx. x = instruction → ? with
    555727        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
    556728          match real_instruction return λx. x = real_instruction →
    557729          Σcost_of_block: nat.
    558             ∀start_status: Status.
    559             ∀final_status: Status.
     730            ∀start_status: Status code_memory'.
     731            ∀final_status: Status code_memory'.
    560732            ∀trace_ends_flag.
    561             ∀the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
    562               code_memory' = code_memory … start_status →
    563                 program_counter' = program_counter … start_status →
    564                     (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
    565                       cost_of_block = compute_paid_trace_any_label cost_labels trace_ends_flag start_status final_status the_trace with
     733            ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
     734              program_counter' = program_counter … start_status →
     735                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
     736                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
    566737          [ RET                    ⇒ λinstr. ticks
    567738          | JC   relative          ⇒ λinstr. ticks
    … …  
    575746          | DJNZ src_trgt relative ⇒ λinstr. ticks
    576747          | _                      ⇒ λinstr.
     748         
    577749              ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
    578750          ] (refl …)
    … …  
    588760        | MOVC  src trgt ⇒ λinstr.
    589761            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
    590         ] (refl …)
     762        ] (refl …))
    591763      else
    592         (0 : (Σn: nat. ?))
     764        0)
     765      : Σcost_of_block: nat.
     766          match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with
     767          [ true ⇒
     768            ∀start_status: Status code_memory'.
     769            ∀final_status: Status code_memory'.
     770            ∀trace_ends_flag.
     771            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     772              program_counter' = program_counter … start_status →
     773                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
     774                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
     775          | false ⇒
     776            (cost_of_block = 0)
     777          ])
    593778  ].
    594779  [1:
    … …  
    596781    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
    597782    @(le_to_lt_to_lt … base_case hyp)
     783  |2:
     784      change with (
     785        if to_continue then
     786          ?
     787        else
     788          (? = 0)) >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
     789       @pi2
     790  |3:
     791    change with (
     792      if to_continue then
     793        ?
     794      else
     795        (0 = 0)) >p normalize nodelta %
    598796  |4:
    599     #start_status #final_status #trace_ends_flag #the_trace #code_memory_refl #program_counter_refl
     797    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
     798    cases(block_cost' ?????????) -block_cost'
     799    @(blah … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … real_instruction_refl … the_trace program_counter_refl …)
     800    destruct %
     801  |4:
     802    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    600803    cases(block_cost' ?????????) -block_cost'
    601804    #recursive_block_cost #recursive_assm
    602805    @(trace_any_label_inv_ind … the_trace)
    603806    [1:
    604       #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
    605       #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl destruct
    606       cases classifier_assm
    607       whd in match (as_classifier ???);
    608       whd in ⊢ (??%? → ?);
    609       whd in match current_instruction; normalize nodelta
    610       whd in match current_instruction0; normalize nodelta
    611       #absurd @⊥ <FETCH in absurd; normalize nodelta
    612       #absurd destruct(absurd)
     807      #status_start #status_final #execute_assm #classifier_assm #costed_assm
     808      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     809      destruct
     810      whd in match (trace_any_label_length … (tal_base_not_return …));
     811      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
     812      whd in costed_assm;
    613813    |2:
    614814      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
    … …  
    623823      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    624824      #classifier_assm #after_return_assm #trace_label_return #costed_assm
     825      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     826      destruct
     827      whd in classifier_assm;
     828      whd in classifier_assm:(??%?);
     829      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
     830      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     831      @⊥ <FETCH in classifier_assm; normalize nodelta
     832      #absurd destruct(absurd)
     833    |4:
     834      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     835      #status_final #execute_assm #classifier_assm #after_return_assm
     836      #trace_label_return #costed_assm #trace_any_label #ends_flag_refl
     837      #start_status_refl #final_status_refl #the_trace_refl
     838      destruct
     839      whd in classifier_assm;
     840      whd in classifier_assm:(??%?);
     841      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
     842      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     843      @⊥ <FETCH in classifier_assm; normalize nodelta
     844      #absurd destruct(absurd)
     845    |5:
     846    ]
     847   
     848   
     849   
     850   
     851   
     852   
     853   
     854   
     855   
     856   
     857   
     858   
     859   
     860   
     861   
     862   
     863   
     864   
     865   
     866   
     867   
     868   
     869   
     870   
     871   
     872   
     873   
     874   
     875   
     876    |3:
     877      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     878      #classifier_assm #after_return_assm #trace_label_return #costed_assm
    625879      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    626880      destruct
    627881      whd in match (compute_paid_trace_any_label … (tal_base_call …));
    628882      whd in match (trace_any_label_length … (tal_base_call …));
    629       cases(recursive_assm status_pre_fun_call status_final doesnt_end_with_ret
    630         (tal_base_call (ASM_abstract_status cost_labels) status_pre_fun_call
    631           (execute_1 status_pre_fun_call) status_final
    632             (refl Status (execute_1 status_pre_fun_call)) classifier_assm
    633               after_return_assm trace_label_return costed_assm) ? ?)
     883      cases(recursive_assm …
     884        (tal_base_call (ASM_abstract_status code_memory' cost_labels)
     885         status_pre_fun_call (execute_1 … status_pre_fun_call) status_final (refl …)
     886         classifier_assm after_return_assm trace_label_return costed_assm) ?)
    634887      [1:
    635         * #recursive_n #recursive_trace_total #recursive_block_cost_assm % 
     888        * #recursive_n #recursive_trace_total #recursive_block_cost_assm %
    636889        [1:
    637890          %{(pred total_program_size)}
    … …  
    646899        ]
    647900      |2:
    648         %
    649       |3:
    650         cut(program_counter'' = \snd (\fst (fetch (code_memory … status_pre_fun_call) (program_counter … status_pre_fun_call))))
     901        cut(program_counter'' = \snd (\fst (fetch code_memory' (program_counter … status_pre_fun_call))))
    651902        [1:
    652903          cases FETCH %
    … …  
    658909        ]
    659910      ]
    660       [1:
    661911    |4:
    662912      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    … …  
    697947          <FETCH %
    698948        ]
     949     
    699950      |2:
    700951        lapply (trace_label_return_preserves_code_memory … (execute_1 status_pre_fun_call) status_after_fun_call)
Note: See TracChangeset for help on using the changeset viewer.