Ignore:
Timestamp:
Nov 15, 2012, 7:06:45 PM (8 years ago)
Author:
tranquil
Message:

completely separated program counters from code pointers in joint languages: the advantage is program counters with an unbounded offset in Pos

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semanticsUtils.ma

    r2457 r2470  
    6767(******************************** GRAPHS **************************************)
    6868
    69 definition bitvector_from_pos :
    70   ∀n.Pos → BitVector n ≝
    71   λn,p.bitvector_of_Z n (Zpred (pos p)).
    72 
    73 definition pos_from_bitvector :
    74   ∀n.BitVector n → Pos ≝
    75   λn,v.
    76   match Zsucc (Z_of_unsigned_bitvector n v)
    77   return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ?
    78   with
    79   [ OZ ⇒ λprf.⊥
    80   | pos x ⇒ λ_. x
    81   | neg x ⇒ λprf.⊥
    82   ] (refl …).
    83 @hide_prf
    84 elim v in prf;
    85 [2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.
    86 
    87 lemma pos_pos_from_bitvector :
    88   ∀n,bv.pos (pos_from_bitvector n bv) = Zsucc (Z_of_unsigned_bitvector n bv).
    89 #n #bv elim bv -n
    90 [ %
    91 | #n * #bv #IH [ % | @IH ]
    92 ]
    93 qed.
    94 
    95 lemma bitvector_from_pos_from_bitvector :
    96   ∀n,bv.bitvector_from_pos n (pos_from_bitvector n bv) = bv.
    97 #n #bv whd in ⊢ (??%?); >pos_pos_from_bitvector
    98 >Zpred_Zsucc //
    99 qed.
    100 
    101 lemma divide_elim : ∀P : (natp × natp) → Prop.∀m,n : Pos.
    102   (∀q,r.
    103     ppos m = natp_plus (natp_times q (ppos n)) r →
    104     natp_lt r n →
    105     P (〈q,r〉)) →
    106   P (divide m n).
    107 #P #m #n #H
    108 lapply (refl … (divide m n))
    109 cases (divide ??) in ⊢ (???%→%);
    110 #q #r #EQ elim (divide_ok … EQ) -EQ @H
    111 qed.
    112 
    113 lemma lt_divisor_to_eq_mod : ∀p,q : Pos.
    114   p < q → \snd (divide p q) = ppos p.
    115 #p #q #H @divide_elim * [2: #quot ]
    116 * [2,4: #rest] normalize #EQ destruct(EQ) #_ [2: %]
    117 @⊥ elim (lt_to_not_le ?? H) #H @H -H -H
    118 [ @(transitive_le … (quot*q)) ] /2 by /
    119 qed.
    120 
    121 lemma pos_from_bitvector_from_pos :
    122   ∀n,p.
    123   p ≤ two_power_nat n →
    124   pos_from_bitvector n (bitvector_from_pos n p) = p.
    125 #n #p #H
    126 cut (pos (pos_from_bitvector n (bitvector_from_pos n p)) = pos p)
    127 [2: #EQ destruct(EQ) <e0 in ⊢ (???%); % ]
    128 >pos_pos_from_bitvector
    129 whd in match (bitvector_from_pos ??);
    130 >Z_of_unsigned_bitvector_of_Z
    131 cases p in H ⊢ %;
    132 [ #_ %
    133 |*: #p' #H
    134   whd in match (Zpred ?);
    135   whd in match (Z_two_power_nat ?);
    136   whd in ⊢ (??(?%)?);
    137   >lt_divisor_to_eq_mod [1,3: normalize nodelta whd in match (Zsucc ?); ]
    138   whd
    139   <succ_pred_n try assumption % #ABS destruct(ABS)
    140 ]
    141 qed.
    142 
    143 lemma pos_from_bitvector_max : ∀n,bv.
    144   pos_from_bitvector n bv ≤ two_power_nat n.
    145 #n #bv
    146 change with (pos (pos_from_bitvector n bv) ≤ Z_two_power_nat n)
    147 >pos_pos_from_bitvector
    148 @Zlt_to_Zle
    149 @bv_Z_unsigned_max
    150 qed.
    151 
    152 definition graph_offset_of_label : label → option offset ≝
    153   λl.let p ≝ word_of_identifier … l in
    154   if leb p (two_power_nat offset_size) then
    155     return mk_offset (bitvector_from_pos … p)
    156   else
    157     None ?.
    158 
    159 definition graph_label_of_offset: offset → label ≝
    160  λo.an_identifier ? (pos_from_bitvector ? (offv o)).
    161 
    16269definition make_sem_graph_params :
    16370  ∀pars : unserialized_params.
     
    17178      g_pars
    17279      (spars ?)
    173       graph_offset_of_label
    174       graph_label_of_offset
    175       ??
     80      (word_of_identifier ?)
     81      (an_identifier ?)
     82      ? (refl …)
    17683    ).
    177 whd in match graph_label_of_offset;
    178 whd in match graph_offset_of_label;
    179 whd in match word_of_identifier;
    180 normalize nodelta * #x
    181 @(leb_elim ? (two_power_nat ?)) normalize nodelta
    182 [ #_ >bitvector_from_pos_from_bitvector %
    183 | #ABS @⊥ @(absurd ?? ABS) @pos_from_bitvector_max
    184 | #H whd >(pos_from_bitvector_from_pos … H) %
    185 | #_ %
    186 ]
    187 qed.
     84* #p % qed.
    18885
    18986(******************************** LINEAR **************************************)
    19087
    191 definition lin_offset_of_nat : ℕ → option offset ≝
    192   λn.
    193   if leb (S n) (2^offset_size) then
    194     return mk_offset (bitvector_of_nat ? n)
    195   else
    196     None ?.
     88lemma succ_pos_of_nat_of_pos : ∀p.succ_pos_of_nat (nat_of_pos p) = succ p.
     89@pos_elim [%]
     90#p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.
    19791
    198 definition lin_nat_of_offset : offset → ℕ ≝
    199   λo.nat_of_bitvector ? (offv o).
    20092
    20193definition make_sem_lin_params :
     
    210102      lin_pars
    211103      (spars ?)
    212       lin_offset_of_nat
    213       lin_nat_of_offset
     104      succ_pos_of_nat
     105      (λp.pred (nat_of_pos p))
    214106      ??
    215107    ).
    216 [ * ] #x
    217 whd in match lin_offset_of_nat;
    218 whd in match lin_nat_of_offset;
    219 normalize nodelta
    220 @leb_elim normalize nodelta #H
    221 [ >bitvector_of_nat_inverse_nat_of_bitvector %
    222 | @⊥ cases H #H @H -H -H //
    223 | whd >(nat_of_bitvector_bitvector_of_nat_inverse … H) %
    224 | %
    225 ]
    226 qed.
     108[ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
     109| #n >nat_succ_pos %
     110] qed.
Note: See TracChangeset for help on using the changeset viewer.