Changeset 1963


Ignore:
Timestamp:
May 17, 2012, 2:23:37 AM (8 years ago)
Author:
sacerdot
Message:

More progress in restoring the original proof.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1955 r1963  
    544544    add … l (add … c r) = add … (add … l c) r.
    545545
     546axiom add_commutative:
     547  ∀n: nat.
     548  ∀l, r: BitVector n.
     549    add … l r = add … r l.
     550
    546551example add_SO:
    547552  ∀n: nat.
  • src/ASM/AssemblyProofSplit.ma

    r1958 r1963  
    22include alias "arithmetics/nat.ma".
    33include alias "basics/logic.ma".
     4
     5axiom add_commutative:
     6  ∀n: nat.
     7  ∀l, r: BitVector n.
     8    add … l r = add … r l.
    49
    510theorem main_thm:
     
    2429  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
    2530  whd in match execute_1_pseudo_instruction; normalize nodelta
    26   whd in match ticks_of; normalize nodelta <EQppc #H2 >EQ2 normalize nodelta
     31  whd in match ticks_of; normalize nodelta <EQppc >EQ2 normalize nodelta
    2732  lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc
    28   inversion pi
     33  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … policy … ppc pi … EQlookup_labels EQlookup_datalabels ?)
     34  [1: >EQ2 %
     35  |2:
     36  |3: normalize nodelta
     37  cases pi
    2938  [2,3:
    30     #comment_or_cost #instr_refl #next_internal_pseudo_refl
    31     %{0} @split_eq_status whd in match execute_1_pseudo_instruction;
    32     whd in match execute_1_pseudo_instruction0; normalize nodelta
    33     whd in match ticks_of0; normalize nodelta //
    34     [1:
    35       destruct /demod/
    36     |2:
    37     |3:
    38     |4:
    39     |5:
    40     |6:
    41     ]
    42  
    43   lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … policy … ppc pi … EQlookup_labels EQlookup_datalabels ?)
    44   [>EQ2 %]
    45   inversion pi
    46   [2,3: (* Comment, Cost *)
    47     #ARG #EQ
     39    #ARG
    4840    #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3;
     41    #H2
    4942    whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
    5043    whd in match (execute_1_pseudo_instruction0 ?????);
    51     %{0} @split_eq_statusCSC: this works :-) (lapply H3 -H3 letin sixteen ≝ 16 #H3 // /demod/)
    52    CSC: STOP HERE, was // but requires -H3 because of 16!
    53    ⇒ CHANGE TO AVOID \fst and \pi1! (*
    54    try (<H3 -H0 -H3 //)
    55    [ <add_zero in H3; #H3 >H3 -H0 -H3 //
    56    | -H0 -H3 /demod/*)
    57   |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?)
     44    %{0} @split_eq_status //
     45    [1,2: /demod/ >EQnewppc >H3 <add_zero % (*CSC: auto not working, why? *) ]
     46  |6: (* Mov *) #arg1 #arg2
     47      #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3;
     48      #H2
     49      whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
     50      %{1}
     51      lapply H2 -H2 whd in ⊢ (% → ??%?);
     52      cases (fetch ??) * #instr #newppc' #ticks normalize nodelta
     53      * * #H2a #H2b whd in ⊢ (% → ?); #H2c
     54
     55CSC: XXX (I am porting the code below)
     56
     57      whd in match (execute_1_pseudo_instruction0 ?????);
     58       %{1}
     59       whd in ⊢ (??%?);
     60      cases (fetch ??) * #instr #newppc' #ticks normalize nodelta
     61      whd in ⊢ (??%?);
     62     
     63       >H2b >(eq_instruction_to_eq … H2a)
     64       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
     65       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
     66       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
     67       normalize nodelta;
     68       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
     69       #result #flags
     70       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
     71
     72
     73
     74  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?);
    5875   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
    5976       [3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
Note: See TracChangeset for help on using the changeset viewer.