Changeset 2131


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

No more need for functional extensionality.

Location:
src/ASM
Files:
3 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
  • src/ASM/AssemblyProofSplit.ma

    r2129 r2131  
    379379  ∀newppc: Word.
    380380  ∀lookup_labels: Identifier → Word.
    381   ∀EQlookup_labels: lookup_labels = (λx:Identifier. address_of_word_labels_code_mem instr_list x).
     381  ∀EQlookup_labels: lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)).
    382382  ∀lookup_datalabels: Identifier → Word.
    383383  ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
     
    400400                      status_of_pseudo_status M' cm s sigma policy).
    401401    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
    402   cases daemon (* XXX: commented out as it takes 45 minutes to typecheck *)
    403   (*
    404402  #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels
    405403  #costs #create_label_cost_refl #newppc
     
    13731371  (* XXX: finally, prove the equality using sigma commutation *)
    13741372  cases daemon
    1375   ] *)
    1376 qed.
     1373  ]
     1374qed.
  • src/ASM/AssemblyProofSplitSplit.ma

    r2129 r2131  
    6363    lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
    6464    @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
    65     @(pose … (λx. address_of_word_labels_code_mem instr_list x)) #lookup_labels #EQlookup_labels
     65    @(pose … (λx. bitvector_of_nat ? (lookup_def … labels x 0))) #lookup_labels #EQlookup_labels
    6666    @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
    6767    whd in match execute_1_pseudo_instruction; normalize nodelta
    6868    whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta
    6969    lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc
    70     lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc ? pi … EQlookup_labels EQlookup_datalabels ?)
    71     [1: >fetch_pseudo_refl % |2: skip |3: assumption ]
     70    lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc … pi … lookup_labels lookup_datalabels)
     71    [1: assumption |2: assumption] >create_label_cost_refl
     72    #X lapply (X EQlookup_labels EQlookup_datalabels ?) -X
     73    [1: >fetch_pseudo_refl %]
    7274    #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
    7375    generalize in match assm1; -assm1 -assm2 -assm3
    7476    normalize nodelta
    7577    inversion pi
    76     [(*2,3:
     78    [2,3:
    7779      #arg #_
    7880      (* XXX: we first work on sigma_increment_commutation *)
     
    138140        (λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
    139141        (refl …) ? (refl …))
    140       try assumption try % >assembly_refl assumption
     142      [1,2,3: try assumption try %] >assembly_refl assumption
    141143    |4: (* Jmp *)
    142144      #arg1 #pi_refl
     
    182184          >EQnewpc
    183185          inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
    184           @sym_eq >address_of_word_labels_assm
    185           [1:
    186             >EQlookup_labels in mjc_refl; #mjc_refl
    187             @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
    188             >(andb_true_l … mj_possible_refl) @I
    189           ]
     186          @sym_eq
     187          >EQlookup_labels in mjc_refl; #mjc_refl
     188          @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
     189          >(andb_true_l … mj_possible_refl) @I
    190190        |3:
    191           >EQlookup_labels normalize nodelta
    192           >address_of_word_labels_assm try %
     191          >EQlookup_labels normalize nodelta %
    193192        |5:
    194193          >EQnewpc
    195194          inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
    196           @sym_eq >address_of_word_labels_assm
    197           [1:
    198             >EQlookup_labels in sjc_refl; #sjc_refl
    199             >(pair_destruct_2 ????? (sym_eq … half_add_refl))
    200             @(short_jump_cond_ok ???? (sym_eq … sjc_refl))
    201             >(andb_true_l … sj_possible_refl) @I
    202           ]
     195          @sym_eq
     196          >EQlookup_labels in sjc_refl; #sjc_refl
     197          >(pair_destruct_2 ????? (sym_eq … half_add_refl))
     198          @(short_jump_cond_ok ???? (sym_eq … sjc_refl))
     199          >(andb_true_l … sj_possible_refl) @I
    203200        ]
    204201        @(is_well_labelled_witness … fetch_pseudo_refl)
     
    212209        @commutative_plus
    213210      ]
    214     |*)5: (* Call *)
     211    |5: (* Call *)
    215212      #arg1 #pi_refl
    216213      (* XXX: we first work on sigma_increment_commutation *)
     
    249246        @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
    250247        try /demod nohyps/ [1: %]
    251         @pair_elim #thr #eig #thr_eig_refl
    252248        @pair_elim #fiv #thr' #fiv_thr_refl' whd in ⊢ (??%%);
    253249        @split_eq_status try /demod nohyps/ try %
     
    256252          cases daemon
    257253        |3:
    258           >program_counter_set_program_counter
    259254          whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl
    260255          >EQlookup_labels normalize nodelta
     
    262257          <EQnewpc @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
    263258          #relevant >fst_5_rest_refl
    264           check absolute_jump_cond
    265           <(vsplit_ok ?????? (sym_eq … thr_eig_refl))
    266259          lapply pc_bu_bl_refl' -pc_bu_bl_refl'
    267260          >program_counter_set_8051_sfr >set_clock_set_program_counter
Note: See TracChangeset for help on using the changeset viewer.