Ignore:
Timestamp:
Jun 28, 2012, 12:55:05 AM (8 years ago)
Author:
sacerdot
Message:

No more need for functional extensionality.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2129 r2131  
    146146  ∀sigma: Word → Word.
    147147  ∀policy: Word → bool.
    148   let lookup_labels ≝ λx:Identifier. address_of_word_labels_code_mem (\snd  program) x in
     148  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
     149  let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    149150  ∀ppc.∀ppc_ok.
    150151  ∀code_memory.
     
    157158    encoding_check code_memory pc pc_plus_len assembled →
    158159      fetch_many code_memory pc_plus_len pc instructions.
    159   #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #ppc_ok #code_memory
     160  #program #sigma #policy
     161  @pair_elim #labels #costs #create_label_cost_map_refl
     162  letin lookup_labels ≝ (λx.?) #ppc #ppc_ok #code_memory
    160163  letin lookup_datalabels ≝ (λx.?)
    161164  letin pi ≝ (fst ???)
     
    193196      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
    194197        let code_memory ≝ load_code_memory assembled in
    195         let lookup_labels ≝ λx. address_of_word_labels_code_mem instr_list x in 
     198        let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    196199          ∀ppc.∀ppc_ok.
    197200            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in     
     
    213216  >eq_fetch_pseudo_instruction
    214217  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?)
    215   > (?:((λx.bitvector_of_nat ? (lookup_def … labels x 0)) =
    216        (λx.address_of_word_labels_code_mem instr_list x)))
    217   [2: lapply (create_label_cost_map_ok 〈preamble,instr_list〉) >create_label_cost_refl
    218       #H (*CSC: REQUIRES FUNCTIONAL EXTENSIONALITY; REPHRASE THE LEMMA *) cases daemon ]
    219218  >eq_assembly_1_pseudoinstruction
    220219  whd in ⊢ (% → ?); #assembly_ok
     
    225224      #spw1 #_ >spw1 -spw1 [2: @(transitive_le … ppc_ok) // ] @eq_f @eq_f
    226225      >eq_fetch_pseudo_instruction whd in match instruction_size;
    227       normalize nodelta (*CSC: TRUE, NEEDS LEMMA AND FUNCTIONAL EXTENSIONALITY *)
     226      normalize nodelta (*CSC: TRUE, NEEDS LEMMA *)
    228227      cases daemon
    229228  | lapply (load_code_memory_ok assembled' ?) [ assumption ]
     
    271270  let code_memory ≝ load_code_memory assembled in
    272271  let data_labels ≝ construct_datalabels (\fst program) in
    273   let lookup_labels ≝ λx. address_of_word_labels_code_mem (\snd program) x in 
     272  let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    274273  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
    275274  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
     
    286285  lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')
    287286  normalize nodelta try assumption
    288   @pair_elim #labels' #costs' #create_label_map_refl' #H
     287  >create_label_map_refl in ⊢ (match % with [_ ⇒ ?] → ?); #H
    289288  lapply (H (sym_eq … assembled_refl)) -H
    290289  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
     
    292291  #len #assembledi #EQ4 #H
    293292  lapply (H ppc) >fetch_pseudo_refl #H
    294   lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc ppc_ok (load_code_memory assembled))
     293  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy)
     294  >create_label_map_refl #X lapply (X ppc ppc_ok (load_code_memory assembled)) -X
    295295  >EQ4 #H1 cases (H ppc_ok)
    296296  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
     
    890890  ∀lookup_labels.
    891891  ∀lookup_datalabels.
    892     lookup_labels = (λx. (address_of_word_labels_code_mem (\snd program) x)) →
     892    let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
     893    lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)) →
    893894    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
    894895    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
     
    897898  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
    898899  #lookup_labels #lookup_datalabels
     900  @pair_elim #labels #costs #create_label_cost_map_refl
    899901  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
    900902  normalize nodelta
     
    905907  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
    906908  @pair_elim #preamble #instr_list #program_refl
    907   @pair_elim #labels #costs' #create_label_cost_map_refl
     909  lapply create_label_cost_map_refl; -create_label_cost_map_refl
     910  >program_refl in ⊢ (% → ?); #create_label_cost_map_refl
     911  >create_label_cost_map_refl
    908912  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
    909913  lapply (H ppc ppc_in_bounds) -H
Note: See TracChangeset for help on using the changeset viewer.