Changeset 1946


Ignore:
Timestamp:
May 15, 2012, 12:01:30 AM (8 years ago)
Author:
sacerdot
Message:

\snd half_add => add everywhere

Location:
src/ASM
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r1929 r1946  
    33include alias "arithmetics/nat.ma".
    44include alias "basics/logic.ma".
    5    
     5
    66let rec traverse_code_internal
    77  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     
    1616  [ O ⇒ λprogram_size_refl. empty_map CostTag nat
    1717  | S program_size' ⇒ λprogram_size_refl.
    18     deplet 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in
     18    let new_program_counter' ≝ add 16 (bitvector_of_nat 16 1) program_counter in
    1919    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' program_size' ? in
    2020    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
     
    2222    | Some lbl ⇒ λlookup_refl.
    2323      let cost ≝ block_cost code_memory program_counter cost_labels in
    24         add … cost_mapping lbl cost
     24        cic:/matita/cerco/common/Identifiers/add.fix(0,2,2) ?? cost_mapping lbl cost
    2525    ] (refl … (lookup_opt … program_counter cost_labels))
    2626  ] (refl … program_size).
     
    6363          |2:
    6464            #n' #_ #program_size_refl_Sn' -traverse_code_internal destruct
    65             cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
     65            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
    6666            [1:
    6767              destruct
     
    9090                  #eqb_ref_assm
    9191                  -ind_hyp
    92                   <NEW_PC' in S_assm; #relevant <relevant -relevant
     92                  <S_assm
    9393                  change with (? < ?)
    9494                  @le_neq_to_lt assumption
     
    9797                generalize in match H2; whd in ⊢ (??% → ?);
    9898                >plus_n_Sm in ⊢ (% → ?);
    99                 cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter))
    100                 [1:
    101                   <NEW_PC' %
     99                cut(new_program_counter' = add 16 (bitvector_of_nat 16 1) program_counter)
     100                [1: %
    102101                |2:
    103102                  #new_program_counter_assm' >new_program_counter_assm'
     
    188187              @(transitive_le ? (S (nat_of_bitvector … program_counter)))
    189188              [1:
    190                 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
     189                cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
    191190                [1:
    192191                  destruct
     
    198197                  @le_S_S @le_S_S @le_O_n
    199198                |2:
    200                   #Sn_refl_assm >Sn_refl_assm <NEW_PC' @le_n
     199                  #Sn_refl_assm >Sn_refl_assm @le_n
    201200                ]
    202201              |2:
     
    209208            destruct
    210209            @(transitive_le … H2)
    211             cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
     210            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
    212211            [1:
    213212              destruct
     
    222221              change with (S (S n' + ?) ≤ ?)
    223222              >plus_n_Sm @monotonic_le_plus_r >S_assm
    224               <NEW_PC' @le_n
     223              @le_n
    225224            ]
    226225          ]
     
    243242        @eq_f >program_size_refl_Sn <plus_n_Sm
    244243        change with (? = (S ?) + ?) @eq_f2 try %
    245         cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
     244        cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
    246245        [1:
    247246          destruct
     
    254253        |2:
    255254          #S_assm
    256           cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter))
    257           [1:
    258             <NEW_PC' %
     255          cut(new_program_counter' = add … (bitvector_of_nat … 1) program_counter)
     256          [1: %
    259257          |2:
    260258           #new_program_counter_assm' >new_program_counter_assm'
    261259           cases program_size_invariant
    262260           [1:
    263              #destruct_assm destruct
     261             #destruct_assm @⊥ >destruct_assm in program_size_refl; #abs destruct(abs)
    264262           |2:
    265263             #program_size_invariant
  • src/ASM/Arithmetic.ma

    r1934 r1946  
    529529    full_add n b c false.
    530530
    531 example half_add_SO:
     531definition add ≝
     532  λn: nat.
     533  λl, r: BitVector n.
     534    \snd (half_add n l r).
     535
     536axiom add_zero:
     537  ∀n: nat.
     538  ∀l: BitVector n.
     539    l = add n l (zero …).
     540
     541axiom add_associative:
     542  ∀n: nat.
     543  ∀l, c, r: BitVector n.
     544    add … l (add … c r) = add … (add … l c) r.
     545
     546example add_SO:
    532547 ∀pc.
    533  \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
     548 add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1) = bitvector_of_nat … (S pc).
    534549 cases daemon.
    535550qed.
  • src/ASM/Assembly.ma

    r1943 r1946  
    818818  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    819819   let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) (sigma program pol ppc) lookup_datalabels  pi) in
    820     sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
     820    sigma program pol (add ? ppc (bitvector_of_nat ? 1)) =
    821821     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
    822822 #program #pol #ppc #pi #lookup_labels #lookup_datalabels #Hll #Hldl #Hppc
     
    824824 cases (sigma00 ???) #x #Hpmap #EQ
    825825 whd in match (sigma ???);
    826  whd in match (sigma program pol (\snd (half_add ???)));
     826 whd in match (sigma program pol (add ???));
    827827 whd in match sigma_safe; normalize nodelta
    828828 (*Problem1: backtracking cases (sigma0 program pol)*)
     
    834834 | #_ lapply (proj1 ?? ((proj2 ?? Hpmap) (proj1 ?? Hpmap))) #Hpmap1
    835835   lapply ((proj2 ?? ((proj2 ?? Hpmap) (proj1 ?? Hpmap))) (nat_of_bitvector 16 ppc) Hppc) #Hpmap2 -Hpmap
    836    <(bitvector_of_nat_nat_of_bitvector 16 ppc) >half_add_SO
     836   <(bitvector_of_nat_nat_of_bitvector 16 ppc) >add_SO
    837837   
    838838   >(Hpmap2 ? (refl …)) @eq_f @eq_f2 [%]
     
    946946   res = assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
    947947   let 〈len,code〉 ≝ res in
    948     sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
     948    sigma program pol (add ? ppc (bitvector_of_nat ? 1)) =
    949949     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
    950950≝ λprogram: pseudo_assembly_program.
     
    12701270        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels (\snd hd) in
    12711271        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
    1272         let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
     1272        let new_ppc ≝ add ? ppc (bitvector_of_nat ? 1) in
    12731273         〈new_pc, 〈new_ppc, (code @ program)〉〉)
    12741274      〈(zero ?), 〈(zero ?), [ ]〉〉
  • src/ASM/AssemblyProof.ma

    r1945 r1946  
    12511251qed.
    12521252
    1253 (* XXX: this looks almost certainly wrong *)
    1254 example half_add_SO:
    1255  ∀pc.
    1256  \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
    1257  cases daemon.
    1258 qed.
    1259 
    12601253(*
    12611254axiom not_eqvb_S:
     
    13181311  |2:
    13191312    #hd #tl #IH #pc #l2 * #H1 #H2
    1320 (*    >half_add_SO in H2; #H2 *)
     1313(*    >add_SO in H2; #H2 *)
    13211314    cases (IH … H2) #E1 #E2 %
    13221315    [1:
     
    16141607   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
    16151608   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
    1616    let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram … s) (zero 8) in
     1609   let pbu ≝ lookup ? 7 (add ? addr (bitvector_of_nat 7 1)) (low_internal_ram … s) (zero 8) in
    16171610   let bl ≝ lookup ? 7 addr ram (zero 8) in
    1618    let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
     1611   let bu ≝ lookup ? 7 (add ? addr (bitvector_of_nat 7 1)) ram (zero 8) in
    16191612    bu@@bl = \fst (sigma (pbu@@pbl)).
    16201613
     
    16721665    | Jmp _ ⇒ Some … M
    16731666    | Call _ ⇒
    1674        Some … (\snd (half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1))::M)
     1667       Some … (add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1)::M)
    16751668    | Mov _ _ ⇒ Some … M
    16761669    | Instruction instr ⇒
     
    21142107  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
    21152108  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
    2116   sp1 = \snd (half_add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1)) →
    2117   sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
     2109  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
     2110  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
    21182111  bu@@bl = \fst (sigma (pbu@@pbl)) →
    21192112   low_internal_ram T1 cm1
     
    21402133  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
    21412134  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
    2142   sp1 = \snd (half_add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1)) →
    2143   sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
     2135  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
     2136  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
    21442137  bu@@bl = \fst (sigma (pbu@@pbl)) →
    21452138   high_internal_ram T1 cm1
  • src/ASM/Fetch.ma

    r1941 r1946  
    99
    1010definition code_memory_size ≝ bitvector_max_nat 16.
    11 
    12 definition add ≝
    13   λn: nat.
    14   λl, r: BitVector n.
    15     \snd (half_add n l r).
    16 
    17 axiom add_zero:
    18   ∀n: nat.
    19   ∀l: BitVector n.
    20     l = add n l (zero …).
    21 
    22 axiom add_associative:
    23   ∀n: nat.
    24   ∀l, c, r: BitVector n.
    25     add … l (add … c r) = add … (add … l c) r.
    2611
    2712include alias "ASM/BitVectorTrie.ma".
  • src/ASM/Interpret.ma

    r1939 r1946  
    905905        (λx. λs.
    906906        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
    907         [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r))
     907        [ RELATIVE r ⇒ λ_. add ? (program_counter … s) (sign_extension r)
    908908        | _ ⇒ λabsd. ⊥
    909909        ] (subaddressing_modein … x)) instr' s
     
    987987        (λx. λs.
    988988        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
    989         [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r))
     989        [ RELATIVE r ⇒ λ_. add ? (program_counter … s) (sign_extension r)
    990990        | _ ⇒ λabsd. ⊥
    991991        ] (subaddressing_modein … x)) instr' s) try @absd
  • src/ASM/Status.ma

    r1882 r1946  
    11181118  λpc: Word.
    11191119    let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … code_mem ? in
    1120     let 〈flags, new_pc〉 ≝ half_add ? pc (bitvector_of_nat ? 1) in
     1120    let new_pc ≝ add ? pc (bitvector_of_nat ? 1) in
    11211121      〈instr, new_pc〉.
    11221122    cases not_implemented.
     
    11241124
    11251125lemma snd_fetch_pseudo_instruction:
    1126  ∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = \snd (half_add ? ppc (bitvector_of_nat ? 1)).
     1126 ∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = add ? ppc (bitvector_of_nat ? 1).
    11271127 #l #ppc whd in ⊢ (??(???%)?); @pair_elim
    1128  #lft #rgt @pair_elim #x #y #_ #_ %
     1128 #lft #rgt #_ %
    11291129qed.
    11301130
  • src/ASM/UtilBranch.ma

    r1928 r1946  
    7373  ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
    7474    S (nat_of_bitvector_aux n buffer bv) =
    75       nat_of_bitvector … (\snd (half_add n (bitvector_of_nat … 1) bv)).
     75      nat_of_bitvector … (add n (bitvector_of_nat … 1) bv).
    7676  #n #bv elim bv
    7777  [1:
     
    8989  ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
    9090    S (nat_of_bitvector … bv) = nat_of_bitvector …
    91       (\snd (half_add n (bitvector_of_nat … 1) bv)).
     91      (add n (bitvector_of_nat … 1) bv).
    9292  #n #bv elim bv
    9393  [1:
Note: See TracChangeset for help on using the changeset viewer.