Ignore:
Timestamp:
Jun 8, 2012, 4:32:03 PM (8 years ago)
Author:
sacerdot
Message:

!! BEWARE: major commit !!

1) [affects everybody]

split for vectors renamed to vsplit to reduce ambiguity since split is
now also a function in the standard library.
Note: I have not been able to propagate the changes everywhere in
the front-end/back-end because some files do not compile

2) [affects everybody]

functions on Vectors copied both in the front and back-ends moved to
Vectors.ma

3) [affects only the back-end]

subaddressing_mode_elim redesigned from scratch and now also applied to
Policy.ma. Moreover, all daemons about that have been closed.
The new one is much simpler to apply since it behaves like a standard
elimination principle: @(subaddressing_mode_elim \ldots x) where x is
the thing to eliminate.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2026 r2032  
    2424  whd in match set_arg_16'; normalize nodelta
    2525  @(subaddressing_mode_elim … [[dptr]] … [[dptr]]) [1: // ]
    26   cases (split bool 8 8 w) #bu #bl normalize nodelta
     26  cases (vsplit bool 8 8 w) #bu #bl normalize nodelta
    2727  whd in match set_8051_sfr; normalize nodelta %
    2828qed.
     
    103103  @list_addressing_mode_tags_elim_prop try %
    104104  @list_addressing_mode_tags_elim_prop try %
    105   #EQ1 #EQ2 <EQ2 normalize cases (split bool 8 8 w) #b1 #b2 normalize <EQ1 %
     105  #EQ1 #EQ2 <EQ2 normalize cases (vsplit bool 8 8 w) #b1 #b2 normalize <EQ1 %
    106106qed.
    107107
     
    117117  @(subaddressing_mode_elim … [[bit_addr; carry]] … [[bit_addr; carry]]) [1: // ]
    118118  [1:
    119     #byte cases (split ????) #nu #nl normalize nodelta
    120     cases (split ????) #ignore #three_bits normalize nodelta
     119    #byte cases (vsplit ????) #nu #nl normalize nodelta
     120    cases (vsplit ????) #ignore #three_bits normalize nodelta
    121121    cases (get_index_v bool ????) normalize nodelta
    122122    [1:
     
    126126    ]
    127127  |2:
    128     cases (split ????) //
     128    cases (vsplit ????) //
    129129  ]
    130130qed.
     
    594594        | DA addr ⇒ λinstr_refl.
    595595            let s ≝ add_ticks1 s in
    596             let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
     596            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
    597597              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
    598598                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
    599599                let cy_flag ≝ get_index' ? O ? flags in
    600                 let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
     600                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
    601601                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
    602602                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
     
    672672            let s ≝ add_ticks1 s in
    673673            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
    674             let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
     674            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
    675675            let new_acc ≝ nl @@ nu in
    676676              set_8051_sfr … s SFR_ACC_A new_acc
     
    698698        | XCHD addr1 addr2 ⇒ λinstr_refl.
    699699            let s ≝ add_ticks1 s in
    700             let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
    701             let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in
     700            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
     701            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
    702702            let new_acc ≝ acc_nu @@ arg_nl in
    703703            let new_arg ≝ arg_nu @@ acc_nl in
     
    869869  <EQppc in fetch_many_assm;
    870870  @pair_elim #result #flags #sub16_refl
    871   @pair_elim #upper #lower #split_refl
     871  @pair_elim #upper #lower #vsplit_refl
    872872  cases (eq_bv ???) normalize nodelta
    873873  [1,3:
     
    974974  <EQppc in fetch_many_assm;
    975975  @pair_elim #result #flags #sub16_refl
    976   @pair_elim #upper #lower #split_refl
    977   inversion (eq_bv ???) #upper_split_refl normalize nodelta
     976  @pair_elim #upper #lower #vsplit_refl
     977  inversion (eq_bv ???) #upper_vsplit_refl normalize nodelta
    978978  [1,3:
    979979    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
     
    10761076  <EQppc in fetch_many_assm;
    10771077  @pair_elim #result #flags #sub16_refl
    1078   @pair_elim #upper #lower #split_refl
     1078  @pair_elim #upper #lower #vsplit_refl
    10791079  cases (eq_bv ???) normalize nodelta
    10801080  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
     
    15511551           >(eq_bv_eq … H2c)
    15521552           change with
    1553             ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
    1554                 (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
    1555            generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
    1556            generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 pol newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
     1553            ((?=let 〈ppc_bu,ppc_bl〉 ≝ vsplit bool 8 8 newppc in ?) →
     1554                (let 〈pc_bu,pc_bl〉 ≝ vsplit bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
     1555           generalize in match (refl … (vsplit … 8 8 newppc)) cases (vsplit bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
     1556           generalize in match (refl … (vsplit … 8 8 (sigma 〈preamble,instr_list〉 pol newppc))) cases (vsplit bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
    15571557           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
    15581558           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
     
    15701570               | >(pair_destruct_1 ????? EQpc)
    15711571                 >(pair_destruct_2 ????? EQpc)
    1572                  @split_elim #x #y #H <H -x y H;
     1572                 @vsplit_elim #x #y #H <H -x y H;
    15731573                 >(pair_destruct_1 ????? EQppc)
    15741574                 >(pair_destruct_2 ????? EQppc)
    1575                  @split_elim #x #y #H <H -x y H;
     1575                 @vsplit_elim #x #y #H <H -x y H;
    15761576                 >EQ0 % ]
    15771577            | >set_low_internal_ram_set_high_internal_ram
     
    15841584               | >(pair_destruct_1 ????? EQpc)
    15851585                 >(pair_destruct_2 ????? EQpc)
    1586                  @split_elim #x #y #H <H -x y H;
     1586                 @vsplit_elim #x #y #H <H -x y H;
    15871587                 >(pair_destruct_1 ????? EQppc)
    15881588                 >(pair_destruct_2 ????? EQppc)
    1589                  @split_elim #x #y #H <H -x y H;
     1589                 @vsplit_elim #x #y #H <H -x y H;
    15901590                 >EQ0 % ]           
    15911591            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
     
    16261626          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
    16271627          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
    1628           @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
     1628          @vsplit_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
    16291629          @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
    16301630          change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
    1631           @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
     1631          @vsplit_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
    16321632          >get_8051_sfr_set_8051_sfr
    16331633         
    16341634          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
    1635            change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
    1636            generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
    1637            cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
    1638            generalize in match (refl … (split bool 4 4 pc_bu))
    1639            cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
    1640            generalize in match (refl … (split bool 3 8 rest_addr))
    1641            cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
     1635           change with ((let 〈pc_bu,pc_bl〉 ≝ vsplit bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
     1636           generalize in match (refl … (vsplit bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
     1637           cases (vsplit ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
     1638           generalize in match (refl … (vsplit bool 4 4 pc_bu))
     1639           cases (vsplit ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
     1640           generalize in match (refl … (vsplit bool 3 8 rest_addr))
     1641           cases (vsplit ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
    16421642           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
    16431643           generalize in match
     
    16501650              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
    16511651            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
    1652               @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
     1652              @(bitvector_3_elim_prop … (\fst (vsplit bool 3 8 rest_addr))) %]] *)]
    16531653  |4: (* Jmp *) #label #MAP
    16541654      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
     
    16711671              false))
    16721672           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
    1673            generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
     1673           generalize in match (refl … (vsplit … 8 8 results)) cases (vsplit ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
    16741674           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
    16751675           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
     
    16901690         generalize in match
    16911691          (refl …
    1692             (split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
    1693          cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
     1692            (vsplit … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
     1693         cases (vsplit ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
    16941694         generalize in match
    16951695          (refl …
    1696             (split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
    1697          cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
     1696            (vsplit … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
     1697         cases (vsplit ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
    16981698         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
    16991699         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
     
    17061706           whd in ⊢ (???% → ?);
    17071707           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
    1708            change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
    1709            generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
    1710            cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
    1711            generalize in match (refl … (split bool 4 4 pc_bu))
    1712            cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
    1713            generalize in match (refl … (split bool 3 8 rest_addr))
    1714            cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
     1708           change with ((let 〈pc_bu,pc_bl〉 ≝ vsplit bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
     1709           generalize in match (refl … (vsplit bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
     1710           cases (vsplit ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
     1711           generalize in match (refl … (vsplit bool 4 4 pc_bu))
     1712           cases (vsplit ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
     1713           generalize in match (refl … (vsplit bool 3 8 rest_addr))
     1714           cases (vsplit ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
    17151715           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
    17161716           generalize in match
     
    17231723              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
    17241724            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
    1725               @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
     1725              @(bitvector_3_elim_prop … (\fst (vsplit bool 3 8 rest_addr))) %]]
    17261726  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
    17271727    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
     
    17881788            <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
    17891789            whd in ⊢ (??%%)
    1790             cases (split bool 4 4 ARG)
     1790            cases (vsplit bool 4 4 ARG)
    17911791            #nu' #nl'
    17921792            normalize nodelta
    1793             cases (split bool 1 3 nu')
     1793            cases (vsplit bool 1 3 nu')
    17941794            #bit_1' #ignore'
    17951795            normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.