Ignore:
Timestamp:
May 18, 2012, 6:14:01 PM (7 years ago)
Author:
sacerdot
Message:

Some more progress, but now we must prove something on a Russell function
without using Russell: too painful.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r1967 r1969  
    8585qed.
    8686
     87lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P.
     88 #P #A #a #abs destruct
     89qed.
    8790
    8891theorem main_thm:
     
    157160    >(eq_instruction_to_eq … eq_instr) -instr whd in ⊢ (??%?);
    158161    (* XXX: now we start to work on the mk_PreStatus equality *)
     162    (* XXX: lhs *)
    159163    change with (set_arg_16 ????? = ?)
    160164    >set_program_counter_mk_Status_commutation
    161165    >set_clock_mk_Status_commutation
    162166    >set_arg_16_mk_Status_commutation
    163    
     167    (* XXX: rhs *)
    164168    change with (? = status_of_pseudo_status ?? (set_arg_16 ?????) ??)
    165169    >set_program_counter_mk_Status_commutation
    166170    >set_clock_mk_Status_commutation
    167171    >set_arg_16_mk_Status_commutation in ⊢ (???%);
    168    
    169    
     172    (* here we are *)
    170173    @split_eq_status //
    171174    [1:
     
    177180      ]
    178181    ]
     182  |1: (* Instruction *) -pi;  *
     183    [1,2,3: (* ADD, ADDC, SUBB *)
     184    @list_addressing_mode_tags_elim_prop try % whd
     185    @list_addressing_mode_tags_elim_prop try % whd #arg
     186    (* XXX: we first work on sigma_increment_commutation *)
     187    #sigma_increment_commutation
     188    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
     189    (* XXX: we work on the maps *)
     190    whd in ⊢ (??%? → ?);
     191    try (change with (if ? then ? else ? = ? → ?)
     192         cases (addressing_mode_ok ????? ∧ addressing_mode_ok ?????) normalize nodelta)
     193    #H try @(None_Some_elim ??? H) @(Some_Some_elim ????? H) #map_refl_assm <map_refl_assm
     194    (* XXX: we assume the fetch_many hypothesis *)
     195    #fetch_many_assm
     196    (* XXX: we give the existential *)
     197    %{1}
     198    whd in match (execute_1_pseudo_instruction0 ?????);
     199    (* XXX: work on the left hand side of the equality *)
     200    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
     201    (* XXX: execute fetches some more *)
     202    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     203    whd in fetch_many_assm;
     204    >EQassembled in fetch_many_assm;
     205    cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
     206    #eq_instr #EQticks whd in EQticks:(???%); >EQticks
     207    #fetch_many_assm whd in fetch_many_assm;
     208    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
     209    >(eq_instruction_to_eq … eq_instr) -instr whd in ⊢ (??%?);
     210    [ @(pose … (execute_1_preinstruction' ???????))
     211      #lhs whd in ⊢ (???% → ?); #EQlhs
     212      @(pose … (execute_1_preinstruction' ???????))
     213      #rhs whd in ⊢ (???% → ?); #EQrhs
     214     
     215      CSC: delirium
     216     
     217      >EQlhs -EQlhs >EQrhs -EQrhs
     218      cases (add_8_with_carry ???) #bits1 #bits2 whd in ⊢ (??%%);
     219     
     220     lapply (refl ? (execute_1_preinstruction' ???????));
     221    [ whd in match (execute_1_preinstruction' ???????);
     222
     223    whd in ⊢ (??%?);
     224    [ whd in ⊢ (??(???%)%);
     225      whd in match (execute_1_preinstruction' ???????);
     226      cases (add_8_with_carry ???) #bits1 #bits2 whd in ⊢ (??%?);
     227      @pair_elim #result #flags #Heq1
     228    whd in match execute_1_preinstruction'; normalize nodelta
     229    (* XXX: now we start to work on the mk_PreStatus equality *)
     230    whd in ⊢ (??%?);
     231 
     232 
     233 
     234    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2
     235    (* XXX: we take up the hypotheses *)
     236    #sigma_increment_commutation #next_map_assm #fetch_many_assm
     237    (* XXX: we give the existential *)
     238    %{1}
     239    whd in match (execute_1_pseudo_instruction0 ?????);
     240    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
     241    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     242    (* XXX: fetching of the instruction *)
     243    whd in fetch_many_assm;
     244    >EQassembled in fetch_many_assm;
     245    cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
     246    #eq_instr #EQticks whd in EQticks:(???%); >EQticks
     247    #fetch_many_assm whd in fetch_many_assm;
     248    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
     249    >(eq_instruction_to_eq … eq_instr) -instr
     250    (* XXX: now we start to work on the mk_PreStatus equality *)
     251    whd in ⊢ (??%?);
     252    check execute_1_preinstruction
     253   
     254   
     255     #MAP #H1 #H2 #EQ %[1,3,5:@1]
     256       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
     257       change in ⊢ (? → ??%?) with (execute_1_0 ??)
     258       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
     259       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
     260       >H2b >(eq_instruction_to_eq … H2a)
     261       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
     262       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
     263       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
     264       normalize nodelta; #MAP;
     265       [1: change in ⊢ (? → %) with
     266        ((let 〈result,flags〉 ≝
     267          add_8_with_carry
     268           (get_arg_8 ? ps false ACC_A)
     269           (get_arg_8 ?
     270             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
     271             false (DIRECT ARG2))
     272           ? in ?) = ?)
     273        [2,3: %]
     274        change in ⊢ (???% → ?) with
     275         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
     276        >get_arg_8_set_clock
     277       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
     278         [2,4: #abs @⊥ normalize in abs; destruct (abs)
     279         |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
     280       [ change in ⊢ (? → %) with
     281        ((let 〈result,flags〉 ≝
     282          add_8_with_carry
     283           (get_arg_8 ? ps false ACC_A)
     284           (get_arg_8 ?
     285             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
     286             false (DIRECT ARG2))
     287           ? in ?) = ?)
     288          >get_arg_8_set_low_internal_ram
     289       
     290        cases (add_8_with_carry ???)
     291         
     292        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
     293       #result #flags
     294       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
     295
    179296
    180297  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?);
     
    192309         whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)
    193310         cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
    194   |6: (* Mov *) #arg1 #arg2
    195        #H1 #H2 #EQ %[@1]
    196        normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    197        change in ⊢ (? → ??%?) with (execute_1_0 ??)
    198        cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
    199        * * #H2a #H2b whd in ⊢ (% → ?) #H2c
    200        >H2b >(eq_instruction_to_eq … H2a)
    201        generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
    202        @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
    203        @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
    204        normalize nodelta;
    205        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
    206        #result #flags
    207        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
    208311  |5: (* Call *) #label #MAP
    209312      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
Note: See TracChangeset for help on using the changeset viewer.