Ignore:
Timestamp:
Jul 27, 2012, 5:53:25 PM (8 years ago)
Author:
mulligan
Message:

Changed proof strategy for main lemma after noticed that the current approach would not work with POP, RET, etc. Ported throughout the assembly proof and all the way up to Test.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2265 r2272  
    390390qed.
    391391
    392 lemma get_index_v_set_index_hit:
    393   ∀A: Type[0].
    394   ∀n: nat.
    395   ∀v: Vector A n.
    396   ∀i: nat.
    397   ∀e: A.
    398   ∀i_lt_n_proof: i < n.
    399   ∀i_lt_n_proof': i < n.
    400     get_index_v A n (set_index A n v i e i_lt_n_proof) i i_lt_n_proof' = e.
    401   #A #n #v elim v
    402   [1:
    403     #i #e #i_lt_n_proof
    404     cases (lt_to_not_zero … i_lt_n_proof)
    405   |2:
    406     #n' #hd #tl #inductive_hypothesis #i #e
    407     cases i
    408     [1:
    409       #i_lt_n_proof #i_lt_n_proof' %
    410     |2:
    411       #i' #i_lt_n_proof' #i_lt_n_proof''
    412       whd in ⊢ (??%?); @inductive_hypothesis
    413     ]
    414   ]
    415 qed.
     392axiom insert_low_internal_ram_of_pseudo_low_internal_ram':
     393  ∀M, M', sigma,cm,s,addr,v,v'.
     394    (∀addr'.
     395      ((false:::addr) = addr' →
     396        map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v =
     397        map_internal_ram_address_using_pseudo_address_map M' sigma (false:::addr) v') ∧
     398      ((false:::addr) ≠ addr' →
     399        let 〈callM, accM〉 ≝ M in
     400        let 〈callM', accM'〉 ≝ M' in
     401          accM = accM' ∧
     402            assoc_list_lookup … addr' (eq_bv 8) … callM =
     403              assoc_list_lookup … addr' (eq_bv 8) … callM')) →
     404    insert Byte 7 addr v'
     405      (low_internal_ram_of_pseudo_low_internal_ram M'
     406      (low_internal_ram pseudo_assembly_program cm s)) =
     407    low_internal_ram_of_pseudo_low_internal_ram M
     408      (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
    416409
    417 (*
    418410lemma write_at_stack_pointer_status_of_pseudo_status:
    419411  ∀M, M'.
     
    423415  ∀s, s'.
    424416  ∀new_b, new_b'.
    425     M = M' →
    426     map_internal_ram_address_using_pseudo_address_map M sigma new_b = new_b' →
     417    map_internal_ram_address_using_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_SP) new_b = new_b' →
    427418    status_of_pseudo_status M cm s sigma policy = s' →
    428419    write_at_stack_pointer ?? s' new_b' =
    429     status_of_pseudo_status M cm (write_at_stack_pointer ? cm s new_b) sigma policy.
     420    status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s new_b) sigma policy.
    430421  #M #M' #cm #sigma #policy #s #s' #new_b #new_b'
    431   #Mrefl #new_b_refl #s_refl <Mrefl <new_b_refl <s_refl
     422  #new_b_refl #s_refl <new_b_refl <s_refl
    432423  whd in match write_at_stack_pointer; normalize nodelta
    433424  @pair_elim #nu #nl #nu_nl_refl normalize nodelta
     
    449440    ]
    450441  |2:
    451     cases (get_index_v bool ????) normalize nodelta
    452     whd in match status_of_pseudo_status; normalize nodelta
    453     whd in match set_low_internal_ram; normalize nodelta
    454     @split_eq_status try %
    455     [1:
    456       @(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma)
    457     |2:
    458       @(insert_high_internal_ram_of_pseudo_high_internal_ram … sigma)
     442    @if_then_else_status_of_pseudo_status try %
     443    [2:
     444      @sym_eq <set_low_internal_ram_status_of_pseudo_status
     445      [1:
     446        @eq_f2
     447        [2:
     448          @insert_low_internal_ram_of_pseudo_low_internal_ram'
     449    @sym_eq
     450    [2:
     451      <set_low_internal_ram_status_of_pseudo_status
     452      [1:
     453        @eq_f2
     454        [2:
     455          @sym_eq
     456          >(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma … new_b')
     457          [2:
     458            >new_b_refl
     459    ]
    459460  ]
    460 *)
     461qed.
    461462
    462463lemma main_lemma_preinstruction:
     
    519520            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
    520521                                                   (get_arg_8 … s false addr2) false in
    521             let cy_flag ≝ get_index' ? O  ? flags in
     522            let cy_flag ≝ get_index' ? O ? flags in
    522523            let ac_flag ≝ get_index' ? 1 ? flags in
    523524            let ov_flag ≝ get_index' ? 2 ? flags in
     
    917918  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
    918919  whd in match execute_1_preinstruction; normalize nodelta
    919   [1,2: (* ADD and ADDC *)
     920  [(*1,2: (* ADD and ADDC *)
    920921    (* XXX: work on the right hand side *)
    921922    (* XXX: switch to the left hand side *)
     
    15351536      ]
    15361537    ]
    1537   |12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *)
     1538  |*)12: (* JC *)
     1539    >EQP -P normalize nodelta
     1540    whd in match expand_pseudo_instruction; normalize nodelta
     1541    whd in match expand_relative_jump; normalize nodelta
     1542    whd in match expand_relative_jump_internal; normalize nodelta
     1543    @pair_elim #sj_possible #disp #sj_possible_disp_refl
     1544    inversion sj_possible #sj_possible_refl normalize nodelta
     1545    [1:
     1546      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1547      whd in maps_assm:(??%%);
     1548      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
     1549      whd in ⊢ (??%?); normalize nodelta
     1550      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1551      whd in ⊢ (??%?);
     1552      @if_then_else_status_of_pseudo_status
     1553      >EQs >EQticks <instr_refl normalize nodelta
     1554      [1:
     1555        @(get_cy_flag_status_of_pseudo_status M') %
     1556      |2:
     1557        @sym_eq @set_program_counter_status_of_pseudo_status
     1558        [1:
     1559        |2:
     1560          @sym_eq @set_clock_status_of_pseudo_status try %
     1561          whd in match ticks_of0; normalize nodelta
     1562          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
     1563          [1:
     1564            @eq_f2 try %
     1565            >sigma_increment_commutation
     1566            lapply sigma_policy_witness whd in match sigma_policy_specification; normalize nodelta
     1567            * #sigma_zero_assm #relevant cases (relevant ppc ?)
     1568            [1:
     1569              -relevant
     1570              [2:
     1571                >EQcm assumption
     1572              |1:
     1573                #relevant #_ <EQppc >relevant @eq_f @eq_f @eq_f
     1574                >EQlookup_labels >EQcm >create_label_cost_refl @eq_f2
     1575              ]
     1576            |2:
     1577            ]
     1578          |2:
     1579            >sj_possible_refl %
     1580          ]
     1581        ]
     1582      |3:
     1583      ]
     1584    ]
    15381585    cases daemon
    1539   |29,30: (* ANL and ORL *)
     1586  |13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *)
     1587    cases daemon
     1588  |(*29,30: (* ANL and ORL *)
    15401589    inversion addr
    15411590    [1,3:
     
    22282277      @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … b … false (refl …) addressing_mode_ok_assm_1)
    22292278    ]
    2230   |42: (* PUSH *)
     2279  |*)42: (* PUSH *)
    22312280    >EQP -P normalize nodelta lapply instr_refl
    22322281    @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.