Changeset 2032


Ignore:
Timestamp:
Jun 8, 2012, 4:32:03 PM (5 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.

Location:
src
Files:
23 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r1882 r2032  
    7575      ].
    7676
     77lemma eq_a_to_eq:
     78  ∀a,b.
     79    eq_a a b = true → a = b.
     80 #a #b
     81 cases a cases b
     82 #K
     83 try cases (eq_true_false K)
     84 %
     85qed.
     86
     87lemma eq_a_reflexive:
     88  ∀a. eq_a a a = true.
     89  #a cases a %
     90qed.
     91
     92let rec member_addressing_mode_tag
     93  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
     94    on v: Prop ≝
     95  match v with
     96  [ VEmpty ⇒ False
     97  | VCons n' hd tl ⇒
     98      bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
     99  ].
     100
     101lemma mem_decidable:
     102  ∀n: nat.
     103  ∀v: Vector addressing_mode_tag n.
     104  ∀element: addressing_mode_tag.
     105    mem … eq_a n v element = true ∨
     106      mem … eq_a … v element = false.
     107  #n #v #element //
     108qed.
     109
     110lemma eq_a_elim:
     111  ∀tag.
     112  ∀hd.
     113  ∀P: bool → Prop.
     114    (tag = hd → P (true)) →
     115      (tag ≠ hd → P (false)) →
     116        P (eq_a tag hd).
     117  #tag #hd #P
     118  cases tag
     119  cases hd
     120  #true_hyp #false_hyp
     121  try @false_hyp
     122  try @true_hyp
     123  try %
     124  #absurd destruct(absurd)
     125qed.
     126
    77127(* to avoid expansion... *)
    78128let rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
     
    99149   ].
    100150
     151lemma is_a_decidable:
     152  ∀hd.
     153  ∀element.
     154    is_a hd element = true ∨ is_a hd element = false.
     155  #hd #element //
     156qed.
    101157
    102158let rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : bool ≝
     
    106162     is_a he A ∨ is_in ? tl A ].
    107163
     164lemma is_a_to_mem_to_is_in:
     165 ∀he,a,m,q.
     166   is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
     167 #he #a #m #q
     168 elim q
     169 [1:
     170   #_ #K assumption
     171 |2:
     172   #m' #t #q' #II #H1 #H2
     173   normalize
     174   change with (orb ??) in H2:(??%?);
     175   cases (inclusive_disjunction_true … H2)
     176   [1:
     177     #K
     178     <(eq_a_to_eq … K) >H1 %
     179   |2:
     180     #K
     181     >II
     182     try assumption
     183     cases (is_a t a)
     184     normalize
     185     %
     186   ]
     187 ]
     188qed.
     189
     190lemma is_a_true_to_is_in:
     191  ∀n: nat.
     192  ∀x: addressing_mode.
     193  ∀tag: addressing_mode_tag.
     194  ∀supervector: Vector addressing_mode_tag n.
     195  mem addressing_mode_tag eq_a n supervector tag →
     196    is_a tag x = true →
     197      is_in … supervector x.
     198  #n #x #tag #supervector
     199  elim supervector
     200  [1:
     201    #absurd cases absurd
     202  |2:
     203    #n' #hd #tl #inductive_hypothesis
     204    whd in match (mem … eq_a (S n') (hd:::tl) tag);
     205    @eq_a_elim normalize nodelta
     206    [1:
     207      #tag_hd_eq #irrelevant
     208      whd in match (is_in (S n') (hd:::tl) x);
     209      <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
     210      @I
     211    |2:
     212      #tag_hd_neq
     213      whd in match (is_in (S n') (hd:::tl) x);
     214      change with (
     215        mem … eq_a n' tl tag)
     216          in match (fold_right … n' ? false tl);
     217      #mem_hyp #is_a_hyp
     218      cases(is_a hd x)
     219      [1:
     220        normalize nodelta //
     221      |2:
     222        normalize nodelta
     223        @inductive_hypothesis assumption
     224      ]
     225    ]
     226  ]
     227qed.
     228
    108229record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
    109230{
     
    119240  ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l
    120241 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
     242
     243lemma is_in_subvector_is_in_supervector:
     244  ∀m, n: nat.
     245  ∀subvector: Vector addressing_mode_tag m.
     246  ∀supervector: Vector addressing_mode_tag n.
     247  ∀element: addressing_mode.
     248    subvector_with … eq_a subvector supervector →
     249      is_in m subvector element → is_in n supervector element.
     250  #m #n #subvector #supervector #element
     251  elim subvector
     252  [1:
     253    #subvector_with_proof #is_in_proof
     254    cases is_in_proof
     255  |2:
     256    #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
     257    whd in match (is_in … (hd':::tl') element);
     258    cases (is_a_decidable hd' element)
     259    [1:
     260      #is_a_true >is_a_true
     261      #irrelevant
     262      whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
     263      @(is_a_true_to_is_in … is_a_true)
     264      lapply(subvector_with_proof)
     265      cases(mem … eq_a n supervector hd') //
     266    |2:
     267      #is_a_false >is_a_false normalize nodelta
     268      #assm
     269      @inductive_hypothesis
     270      [1:
     271        generalize in match subvector_with_proof;
     272        whd in match (subvector_with … eq_a (hd':::tl') supervector);
     273        cases(mem_decidable n supervector hd')
     274        [1:
     275          #mem_true >mem_true normalize nodelta
     276          #assm assumption
     277        |2:
     278          #mem_false >mem_false #absurd
     279          cases absurd
     280        ]
     281      |2:
     282        assumption
     283      ]
     284    ]
     285  ]
     286qed.
     287
     288
     289let rec subaddressing_mode_elim_type
     290  (m: nat) (fixed_v: Vector addressing_mode_tag (S m)) (origaddr: fixed_v)
     291    (Q: fixed_v → Prop)
     292     (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
     293       on v: Prop ≝
     294  match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
     295  [ VEmpty         ⇒ λm_refl. λv_refl. Q origaddr
     296  | VCons n' hd tl ⇒ λm_refl. λv_refl.
     297    let tail_call ≝ subaddressing_mode_elim_type m fixed_v origaddr Q n' tl ?
     298    in
     299    match hd return λa: addressing_mode_tag. a = hd → ? with
     300    [ addr11            ⇒ λhd_refl. (∀w: Word11.      Q (ADDR11 w)) → tail_call
     301    | addr16            ⇒ λhd_refl. (∀w: Word.        Q (ADDR16 w)) → tail_call
     302    | direct            ⇒ λhd_refl. (∀w: Byte.        Q (DIRECT w)) → tail_call
     303    | indirect          ⇒ λhd_refl. (∀w: Bit.         Q (INDIRECT w)) → tail_call
     304    | ext_indirect      ⇒ λhd_refl. (∀w: Bit.         Q (EXT_INDIRECT w)) → tail_call
     305    | acc_a             ⇒ λhd_refl.                  Q ACC_A → tail_call
     306    | registr           ⇒ λhd_refl. (∀w: BitVector 3. Q (REGISTER w)) → tail_call
     307    | acc_b             ⇒ λhd_refl.                  Q ACC_B → tail_call
     308    | dptr              ⇒ λhd_refl.                  Q DPTR → tail_call
     309    | data              ⇒ λhd_refl. (∀w: Byte.        Q (DATA w))  → tail_call
     310    | data16            ⇒ λhd_refl. (∀w: Word.        Q (DATA16 w)) → tail_call
     311    | acc_dptr          ⇒ λhd_refl.                  Q ACC_DPTR → tail_call
     312    | acc_pc            ⇒ λhd_refl.                  Q ACC_PC → tail_call
     313    | ext_indirect_dptr ⇒ λhd_refl.                  Q EXT_INDIRECT_DPTR → tail_call
     314    | indirect_dptr     ⇒ λhd_refl.                  Q INDIRECT_DPTR → tail_call
     315    | carry             ⇒ λhd_refl.                  Q CARRY → tail_call
     316    | bit_addr          ⇒ λhd_refl. (∀w: Byte.        Q (BIT_ADDR w)) → tail_call
     317    | n_bit_addr        ⇒ λhd_refl. (∀w: Byte.        Q (N_BIT_ADDR w)) → tail_call
     318    | relative          ⇒ λhd_refl. (∀w: Byte.        Q (RELATIVE w)) → tail_call
     319    ] (refl … hd)
     320  ] (refl … n) (refl_jmeq … v).
     321  [20:
     322    generalize in match proof; destruct
     323    whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
     324    cases (mem … eq_a ? fixed_v hd) normalize nodelta
     325    [1:
     326      whd in match (subvector_with … eq_a tl fixed_v);
     327      #assm assumption
     328    |2:
     329      normalize in ⊢ (% → ?);
     330      #absurd cases absurd
     331    ]
     332  ]
     333  @(is_in_subvector_is_in_supervector … proof)
     334  destruct @I
     335qed.
     336
     337lemma subaddressing_mode_elim0:
     338  ∀n: nat.
     339  ∀v: Vector addressing_mode_tag (S n).
     340  ∀addr: v.
     341  ∀Q: v → Prop.
     342  ∀m,w,H.
     343  (∀xaddr: v. ¬ is_in … w xaddr → Q xaddr) →
     344   subaddressing_mode_elim_type n v addr Q m w H.
     345 #n #v #addr #Q #m #w elim w
     346 [ /2/
     347 | #n' #hd #tl #IH cases hd #H
     348   #INV whd #PO @IH #xaddr cases xaddr *
     349   try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV
     350   @ALREADYSEEN ]
     351qed.
     352
     353lemma subaddressing_mode_elim:
     354  ∀n: nat.
     355  ∀v: Vector addressing_mode_tag (S n).
     356  ∀addr: v.
     357  ∀Q: v → Prop.
     358   subaddressing_mode_elim_type n v addr Q (S n) v ?.
     359[ #n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; //
     360| @subvector_with_refl @eq_a_reflexive
     361]
     362qed.
    121363 
    122364inductive preinstruction (A: Type[0]) : Type[0] ≝
  • src/ASM/Arithmetic.ma

    r2028 r2032  
    55  λpc: Word.
    66  λa: Word11.
    7   let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in
    8   let 〈n1, n2〉 ≝ split … 4 4 pc_upper in
    9   let 〈b123, b〉 ≝ split … 3 8 a in
     7  let 〈pc_upper, ignore〉 ≝ vsplit … 8 8 pc in
     8  let 〈n1, n2〉 ≝ vsplit … 4 4 pc_upper in
     9  let 〈b123, b〉 ≝ vsplit … 3 8 a in
    1010  let b1 ≝ get_index_v … b123 0 ? in
    1111  let b2 ≝ get_index_v … b123 1 ? in
     
    454454      [ None ⇒ None ?
    455455      | Some result ⇒
    456           let 〈high_bits, low_bits〉 ≝ split bool ? n (multiplication n result c) in
     456          let 〈high_bits, low_bits〉 ≝ vsplit bool ? n (multiplication n result c) in
    457457            Some ? (subtraction n b low_bits)
    458458      ].
     
    571571  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
    572572  | nat_eq n' ⇒ λv. v
    573   | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
     573  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
    574574  ].
    575575
     
    579579  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v)
    580580  | nat_eq n' ⇒ λv. v
    581   | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
     581  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
    582582  ].
    583583
  • src/ASM/Assembly.ma

    r2028 r2032  
    212212                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
    213213                  [ DATA16 w ⇒ λ_.
    214                      let b1_b2 ≝ split ? 8 8 w in
     214                     let b1_b2 ≝ vsplit ? 8 8 w in
    215215                     let b1 ≝ \fst b1_b2 in
    216216                     let b2 ≝ \snd b1_b2 in
     
    364364     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    365365      [ ADDR11 w ⇒ λ_.
    366          let v1_v2 ≝ split ? 3 8 w in
     366         let v1_v2 ≝ vsplit ? 3 8 w in
    367367         let v1 ≝ \fst v1_v2 in
    368368         let v2 ≝ \snd v1_v2 in
     
    372372     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    373373      [ ADDR11 w ⇒ λ_.
    374          let v1_v2 ≝ split ? 3 8 w in
     374         let v1_v2 ≝ vsplit ? 3 8 w in
    375375         let v1 ≝ \fst v1_v2 in
    376376         let v2 ≝ \snd v1_v2 in
     
    382382     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
    383383      [ ADDR16 w ⇒ λ_.
    384          let b1_b2 ≝ split ? 8 8 w in
     384         let b1_b2 ≝ vsplit ? 8 8 w in
    385385         let b1 ≝ \fst b1_b2 in
    386386         let b2 ≝ \snd b1_b2 in
     
    390390     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
    391391      [ ADDR16 w ⇒ λ_.
    392          let b1_b2 ≝ split ? 8 8 w in
     392         let b1_b2 ≝ vsplit ? 8 8 w in
    393393         let b1 ≝ \fst b1_b2 in
    394394         let b2 ≝ \snd b1_b2 in
     
    431431   let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    432432   let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length lookup_address false in
    433    let 〈upper, lower〉 ≝ split ? 8 8 result in
     433   let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
    434434   if eq_bv ? upper (zero 8) then
    435435     let address ≝ RELATIVE lower in
     
    535535  | Comment comment ⇒ [ ]
    536536  | Call call ⇒
    537     let 〈addr_5, resta〉 ≝ split ? 5 11 (sigma (lookup_labels call)) in
     537    let 〈addr_5, resta〉 ≝ vsplit ? 5 11 (sigma (lookup_labels call)) in
    538538    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    539539    let do_a_long ≝ policy ppc in
    540     let 〈pc_5, restp〉 ≝ split ? 5 11 pc_plus_jmp_length in
     540    let 〈pc_5, restp〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in
    541541    if eq_bv ? addr_5 pc_5 ∧ ¬ do_a_long then
    542542      let address ≝ ADDR11 resta in
     
    554554    let lookup_address ≝ sigma (lookup_labels jmp) in
    555555    let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length lookup_address false in
    556     let 〈upper, lower〉 ≝ split ? 8 8 result in
     556    let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
    557557    if eq_bv ? upper (zero 8) ∧ ¬ do_a_long then
    558558      let address ≝ RELATIVE lower in
    559559        [ SJMP address ]
    560560    else
    561       let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (sigma (lookup_labels jmp)) in
    562       let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc_plus_jmp_length in
     561      let 〈fst_5_addr, rest_addr〉 ≝ vsplit ? 5 11 (sigma (lookup_labels jmp)) in
     562      let 〈fst_5_pc, rest_pc〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in
    563563      if eq_bv ? fst_5_addr fst_5_pc ∧ ¬ do_a_long then
    564564        let address ≝ ADDR11 rest_addr in
     
    866866
    867867(*CSC: FALSE!!!*)
    868 axiom fetch_pseudo_instruction_split:
     868axiom fetch_pseudo_instruction_vsplit:
    869869 ∀instr_list,ppc.
    870870  ∃pre,suff,lbl.
     
    936936   cases (sigma00 ????) in ⊢ (??%? → %); normalize nodelta [#_ * #abs @abs %]
    937937   #res #K
    938    cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1
     938   cases (fetch_pseudo_instruction_vsplit (\snd program) ppc) #pre * #suff * #lbl #EQ1
    939939   generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?;
    940940   cases daemon (* CSC: XXXXXXXX Ero qui
  • src/ASM/AssemblyProof.ma

    r2024 r2032  
    6262  try @le_n
    6363  <minus_n_n @[[]]
    64 qed.
    65 
    66 lemma super_rewrite2:
    67   ∀A:Type[0].
    68   ∀n, m: nat.
    69   ∀v1: Vector A n.
    70   ∀v2: Vector A m.
    71   ∀P: ∀m. Vector A m → Prop.
    72     n = m → v1 ≃ v2 → P n v1 → P m v2.
    73   #A #n #m #v1 #v2 #P #eq #jmeq
    74   destruct #assm assumption
    75 qed.
    76 
    77 lemma vector_cons_append:
    78   ∀A: Type[0].
    79   ∀n: nat.
    80   ∀e: A.
    81   ∀v: Vector A n.
    82     e ::: v = [[ e ]] @@ v.
    83   #A #n #e #v
    84   cases v try %
    85   #n' #hd #tl %
    86 qed.
    87 
    88 lemma vector_cons_append2:
    89   ∀A: Type[0].
    90   ∀n, m: nat.
    91   ∀v: Vector A n.
    92   ∀q: Vector A m.
    93   ∀hd: A.
    94     hd:::(v@@q) = (hd:::v)@@q.
    95   #A #n #m #v #q
    96   elim v try (#hd %)
    97   #n' #hd' #tl' #ih #hd'
    98   <ih %
    99 qed.
    100 
    101 lemma jmeq_cons_vector_monotone:
    102   ∀A: Type[0].
    103   ∀m, n: nat.
    104   ∀v: Vector A m.
    105   ∀q: Vector A n.
    106   ∀prf: m = n.
    107   ∀hd: A.
    108     v ≃ q → hd:::v ≃ hd:::q.
    109   #A #m #n #v #q #prf #hd #E
    110   @(super_rewrite2 A … E)
    111   try assumption %
    112 qed.
    113 
    114 lemma vector_associative_append:
    115   ∀A: Type[0].
    116   ∀n, m, o:  nat.
    117   ∀v: Vector A n.
    118   ∀q: Vector A m.
    119   ∀r: Vector A o.
    120     (v @@ q) @@ r ≃ v @@ (q @@ r).
    121   #A #n #m #o #v #q #r
    122   elim v try %
    123   #n' #hd #tl #ih
    124   <(vector_cons_append2 A … hd)
    125   @jmeq_cons_vector_monotone
    126   try assumption
    127   @associative_plus
    12864qed.
    12965
     
    186122    >vector_cons_append
    187123    change with (bool_to_Prop (subvector_with ??????))
    188     @(super_rewrite2 … (vector_associative_append … q [[hd]] tl))
     124    @(dependent_rewrite_vectors … (vector_associative_append … q [[hd]] tl))
    189125    try @associative_plus
    190126    @inductive_hypothesis
     
    214150  <(vector_cons_empty … ([[h]] @@ v))
    215151  @(subvector_multiple_append … eq reflex [[ ]] v ? [[h]])
    216 qed.
    217 
    218 lemma eq_a_reflexive:
    219   ∀a. eq_a a a = true.
    220   #a cases a %
    221152qed.
    222153
     
    1056987     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
    1057988
    1058 lemma split_zero:
     989lemma vsplit_zero:
    1059990  ∀A,m.
    1060991  ∀v: Vector A m.
    1061     〈[[]], v〉 = split A 0 m v.
     992    〈[[]], v〉 = vsplit A 0 m v.
    1062993  #A #m #v
    1063994  cases v try %
     
    11511082qed.
    11521083
    1153 lemma split_succ:
     1084lemma vsplit_succ:
    11541085  ∀A: Type[0].
    11551086  ∀m, n: nat.
     
    11581089  ∀v: Vector A (m + n).
    11591090  ∀hd: A.
    1160     v = l@@r → (〈l, r〉 = split A m n v → 〈hd:::l, r〉 = split A (S m) n (hd:::v)).
     1091    v = l@@r → (〈l, r〉 = vsplit A m n v → 〈hd:::l, r〉 = vsplit A (S m) n (hd:::v)).
    11611092  #A #m
    11621093  elim m
     
    11701101    whd in ⊢ (???%);
    11711102    >tail_head
    1172     <(? : split A (S m') n (l@@r) = split' A (S m') n (l@@r))
     1103    <(? : vsplit A (S m') n (l@@r) = vsplit' A (S m') n (l@@r))
    11731104    try (<hyp <head_head' %)
    11741105    elim l normalize //
     
    11761107qed.
    11771108
    1178 lemma split_prod:
     1109lemma vsplit_prod:
    11791110  ∀A: Type[0].
    11801111  ∀m, n: nat.
     
    11821113  ∀v: Vector A m.
    11831114  ∀q: Vector A n.
    1184     p = v@@q → 〈v, q〉 = split A m n p.
     1115    p = v@@q → 〈v, q〉 = vsplit A m n p.
    11851116  #A #m elim m
    11861117  [1:
     
    11881119    >hyp <(vector_append_zero A n q v)
    11891120    >(prod_vector_zero_eq_left A …)
    1190     @split_zero
     1121    @vsplit_zero
    11911122  |2:
    11921123    #r #ih #n #p #v #q #hyp
     
    11941125    cases (Vector_Sn A r v) #hd #exists
    11951126    cases exists #tl #jmeq
    1196     >jmeq @split_succ try %
     1127    >jmeq @vsplit_succ try %
    11971128    @ih %
    11981129  ]
     
    12001131
    12011132(*
    1202 lemma split_prod_exists:
     1133lemma vsplit_prod_exists:
    12031134  ∀A, m, n.
    12041135  ∀p: Vector A (m + n).
    12051136  ∃v: Vector A m.
    12061137  ∃q: Vector A n.
    1207     〈v, q〉 = split A m n p.
     1138    〈v, q〉 = vsplit A m n p.
    12081139  #A #m #n #p
    12091140  elim m
     
    12171148*)
    12181149
    1219 definition split_elim:
     1150definition vsplit_elim:
    12201151  ∀A: Type[0].
    12211152  ∀l, m: nat.
     
    12241155    (∀vl: Vector A l.
    12251156     ∀vm: Vector A m.
    1226       v = vl@@vm → P 〈vl,vm〉) → P (split A l m v) ≝
     1157      v = vl@@vm → P 〈vl,vm〉) → P (vsplit A l m v) ≝
    12271158  λa: Type[0].
    12281159  λl, m: nat.
     
    14131344 [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
    14141345 normalize in ⊢ (???% → ?);
    1415  [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
     1346 [92,94,42,93,95: @vsplit_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
    14161347  normalize in ⊢ (???% → ?);]
    14171348 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
     
    18861817  λs: PreStatus M.
    18871818  λv: Byte.
    1888     let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
     1819    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
    18891820    let bit_zero ≝ get_index_v… nu O ? in
    18901821    let bit_1 ≝ get_index_v… nu 1 ? in
     
    19221853      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    19231854      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    1924       let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     1855      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
    19251856      let s ≝ write_at_stack_pointer' ? s pc_bl in
    19261857      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     
    19501881  [ #pre cases pre
    19511882     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
    1952        cases (split ????) #z1 #z2 %
     1883       cases (vsplit ????) #z1 #z2 %
    19531884     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
    1954        cases (split ????) #z1 #z2 %
     1885       cases (vsplit ????) #z1 #z2 %
    19551886     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
    1956        cases (split ????) #z1 #z2 %
     1887       cases (vsplit ????) #z1 #z2 %
    19571888     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
    19581889       [ #x1 whd in ⊢ (??? (??%))
     
    19631894  | #label %
    19641895  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
    1965     cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
    1966     whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
     1896    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
     1897    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
    19671898    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
    19681899    (* CSC: ??? *)
     
    21732104qed.
    21742105
    2175 axiom split_append:
     2106axiom vsplit_append:
    21762107  ∀A: Type[0].
    21772108  ∀m, n: nat.
    21782109  ∀v, v': Vector A m.
    21792110  ∀q, q': Vector A n.
    2180     let 〈v', q'〉 ≝ split A m n (v@@q) in
     2111    let 〈v', q'〉 ≝ vsplit A m n (v@@q) in
    21812112      v = v' ∧ q = q'.
    21822113
    2183 lemma split_vector_singleton:
     2114lemma vsplit_vector_singleton:
    21842115  ∀A: Type[0].
    21852116  ∀n: nat.
     
    22152146  #m #s #arg #b #hyp
    22162147  whd in ⊢ (??%%)
    2217   @split_elim''
     2148  @vsplit_elim''
    22182149  #nu' #nl' #arg_nu_nl_eq
    22192150  normalize nodelta
     
    22242155  [2:
    22252156    normalize nodelta
    2226     @split_elim''
     2157    @vsplit_elim''
    22272158    #bit_one' #three_bits' #bit_one_three_bit_eq
    22282159    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
     
    22432174        |1: -carr_hyp';
    22442175            >arg_nu_nl_eq
    2245             <(split_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
     2176            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
    22462177            [1: >get_index_v_eq in ⊢ (??%? → ?)
    22472178            |2: @le_S @le_S @le_S @le_n
     
    22542185    |3: >get_index_v_eq in ⊢ (??%?)
    22552186        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
    2256         >(split_vector_singleton … bit_one_three_bit_eq)
     2187        >(vsplit_vector_singleton … bit_one_three_bit_eq)
    22572188        <arg_nu_nl_eq
    22582189        whd in hyp:(??%?)
  • 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
  • src/ASM/Interpret.ma

    r2014 r2032  
    1313qed.
    1414   
    15 lemma eq_a_to_eq:
    16   ∀a,b.
    17     eq_a a b = true → a = b.
    18  #a #b
    19  cases a cases b
    20  #K
    21  try cases (eq_true_false K)
    22  %
    23 qed.
    24 
    25 lemma is_a_to_mem_to_is_in:
    26  ∀he,a,m,q.
    27    is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
    28  #he #a #m #q
    29  elim q
    30  [1:
    31    #_ #K assumption
    32  |2:
    33    #m' #t #q' #II #H1 #H2
    34    normalize
    35    change with (orb ??) in H2:(??%?);
    36    cases (inclusive_disjunction_true … H2)
    37    [1:
    38      #K
    39      <(eq_a_to_eq … K) >H1 %
    40    |2:
    41      #K
    42      >II
    43      try assumption
    44      cases (is_a t a)
    45      normalize
    46      %
    47    ]
    48  ]
    49 qed.
    50 
    5115lemma execute_1_technical:
    5216  ∀n, m: nat.
     
    261225        | DA addr ⇒ λinstr_refl.
    262226            let s ≝ add_ticks1 s in
    263             let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
     227            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
    264228              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
    265229                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
    266230                let cy_flag ≝ get_index' ? O ? flags in
    267                 let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
     231                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
    268232                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
    269233                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
     
    339303            let s ≝ add_ticks1 s in
    340304            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
    341             let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
     305            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
    342306            let new_acc ≝ nl @@ nu in
    343307              set_8051_sfr … s SFR_ACC_A new_acc
     
    365329        | XCHD addr1 addr2 ⇒ λinstr_refl.
    366330            let s ≝ add_ticks1 s in
    367             let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
    368             let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in
     331            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
     332            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
    369333            let new_acc ≝ acc_nu @@ arg_nl in
    370334            let new_arg ≝ arg_nu @@ acc_nl in
     
    685649        | DA addr ⇒ λinstr_refl.
    686650            let s ≝ add_ticks1 s in
    687             let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
     651            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
    688652              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
    689653                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
    690654                let cy_flag ≝ get_index' ? O ? flags in
    691                 let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
     655                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
    692656                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
    693657                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
     
    763727            let s ≝ add_ticks1 s in
    764728            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
    765             let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
     729            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
    766730            let new_acc ≝ nl @@ nu in
    767731              set_8051_sfr … s SFR_ACC_A new_acc
     
    789753        | XCHD addr1 addr2 ⇒ λinstr_refl.
    790754            let s ≝ add_ticks1 s in
    791             let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
    792             let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in
     755            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
     756            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
    793757            let new_acc ≝ acc_nu @@ arg_nl in
    794758            let new_arg ≝ arg_nu @@ acc_nl in
     
    1026990        match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
    1027991        [ ADDR11 a ⇒ λaddr11: True.
    1028           let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 program_counter in
    1029           let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
     992          let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 program_counter in
     993          let 〈nu, nl〉 ≝ vsplit ? 4 4 pc_bu in
    1030994          let bit ≝ get_index' ? O ? nl in
    1031           let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
     995          let 〈relevant1, relevant2〉 ≝ vsplit ? 3 8 a in
    1032996          let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    1033997          let 〈carry, new_pc〉 ≝ half_add ? program_counter new_addr in
     
    10491013    | _ ⇒ false
    10501014    ].
    1051 
    1052 let rec member_addressing_mode_tag
    1053   (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
    1054     on v: Prop ≝
    1055   match v with
    1056   [ VEmpty ⇒ False
    1057   | VCons n' hd tl ⇒
    1058       bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
    1059   ].
    1060 
    1061 lemma is_a_decidable:
    1062   ∀hd.
    1063   ∀element.
    1064     is_a hd element = true ∨ is_a hd element = false.
    1065   #hd #element //
    1066 qed.
    1067 
    1068 lemma mem_decidable:
    1069   ∀n: nat.
    1070   ∀v: Vector addressing_mode_tag n.
    1071   ∀element: addressing_mode_tag.
    1072     mem … eq_a n v element = true ∨
    1073       mem … eq_a … v element = false.
    1074   #n #v #element //
    1075 qed.
    1076 
    1077 lemma eq_a_elim:
    1078   ∀tag.
    1079   ∀hd.
    1080   ∀P: bool → Prop.
    1081     (tag = hd → P (true)) →
    1082       (tag ≠ hd → P (false)) →
    1083         P (eq_a tag hd).
    1084   #tag #hd #P
    1085   cases tag
    1086   cases hd
    1087   #true_hyp #false_hyp
    1088   try @false_hyp
    1089   try @true_hyp
    1090   try %
    1091   #absurd destruct(absurd)
    1092 qed.
    1093  
    1094 lemma is_a_true_to_is_in:
    1095   ∀n: nat.
    1096   ∀x: addressing_mode.
    1097   ∀tag: addressing_mode_tag.
    1098   ∀supervector: Vector addressing_mode_tag n.
    1099   mem addressing_mode_tag eq_a n supervector tag →
    1100     is_a tag x = true →
    1101       is_in … supervector x.
    1102   #n #x #tag #supervector
    1103   elim supervector
    1104   [1:
    1105     #absurd cases absurd
    1106   |2:
    1107     #n' #hd #tl #inductive_hypothesis
    1108     whd in match (mem … eq_a (S n') (hd:::tl) tag);
    1109     @eq_a_elim normalize nodelta
    1110     [1:
    1111       #tag_hd_eq #irrelevant
    1112       whd in match (is_in (S n') (hd:::tl) x);
    1113       <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
    1114       @I
    1115     |2:
    1116       #tag_hd_neq
    1117       whd in match (is_in (S n') (hd:::tl) x);
    1118       change with (
    1119         mem … eq_a n' tl tag)
    1120           in match (fold_right … n' ? false tl);
    1121       #mem_hyp #is_a_hyp
    1122       cases(is_a hd x)
    1123       [1:
    1124         normalize nodelta //
    1125       |2:
    1126         normalize nodelta
    1127         @inductive_hypothesis assumption
    1128       ]
    1129     ]
    1130   ]
    1131 qed.
    1132 
    1133 lemma is_in_subvector_is_in_supervector:
    1134   ∀m, n: nat.
    1135   ∀subvector: Vector addressing_mode_tag m.
    1136   ∀supervector: Vector addressing_mode_tag n.
    1137   ∀element: addressing_mode.
    1138     subvector_with … eq_a subvector supervector →
    1139       is_in m subvector element → is_in n supervector element.
    1140   #m #n #subvector #supervector #element
    1141   elim subvector
    1142   [1:
    1143     #subvector_with_proof #is_in_proof
    1144     cases is_in_proof
    1145   |2:
    1146     #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
    1147     whd in match (is_in … (hd':::tl') element);
    1148     cases (is_a_decidable hd' element)
    1149     [1:
    1150       #is_a_true >is_a_true
    1151       #irrelevant
    1152       whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
    1153       @(is_a_true_to_is_in … is_a_true)
    1154       lapply(subvector_with_proof)
    1155       cases(mem … eq_a n supervector hd') //
    1156     |2:
    1157       #is_a_false >is_a_false normalize nodelta
    1158       #assm
    1159       @inductive_hypothesis
    1160       [1:
    1161         generalize in match subvector_with_proof;
    1162         whd in match (subvector_with … eq_a (hd':::tl') supervector);
    1163         cases(mem_decidable n supervector hd')
    1164         [1:
    1165           #mem_true >mem_true normalize nodelta
    1166           #assm assumption
    1167         |2:
    1168           #mem_false >mem_false #absurd
    1169           cases absurd
    1170         ]
    1171       |2:
    1172         assumption
    1173       ]
    1174     ]
    1175   ]
    1176 qed.
    1177  
    1178 let rec subaddressing_mode_elim_type
    1179   (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
    1180     (Q: addressing_mode → T → Prop)
    1181       (p_addr11:            ∀w: Word11.      is_in m fixed_v (ADDR11 w)        → T)
    1182       (p_addr16:            ∀w: Word.        is_in m fixed_v (ADDR16 w)        → T)
    1183       (p_direct:            ∀w: Byte.        is_in m fixed_v (DIRECT w)        → T)
    1184       (p_indirect:          ∀w: Bit.         is_in m fixed_v (INDIRECT w)      → T)
    1185       (p_ext_indirect:      ∀w: Bit.         is_in m fixed_v (EXT_INDIRECT w)  → T)
    1186       (p_acc_a:                              is_in m fixed_v ACC_A             → T)
    1187       (p_register:          ∀w: BitVector 3. is_in m fixed_v (REGISTER w)      → T)
    1188       (p_acc_b:                              is_in m fixed_v ACC_B             → T)
    1189       (p_dptr:                               is_in m fixed_v DPTR              → T)
    1190       (p_data:              ∀w: Byte.        is_in m fixed_v (DATA w)          → T)
    1191       (p_data16:            ∀w: Word.        is_in m fixed_v (DATA16 w)        → T)
    1192       (p_acc_dptr:                           is_in m fixed_v ACC_DPTR          → T)
    1193       (p_acc_pc:                             is_in m fixed_v ACC_PC            → T)
    1194       (p_ext_indirect_dptr:                  is_in m fixed_v EXT_INDIRECT_DPTR → T)
    1195       (p_indirect_dptr:                      is_in m fixed_v INDIRECT_DPTR     → T)
    1196       (p_carry:                              is_in m fixed_v CARRY             → T)
    1197       (p_bit_addr:          ∀w: Byte.        is_in m fixed_v (BIT_ADDR w)      → T)
    1198       (p_n_bit_addr:        ∀w: Byte.        is_in m fixed_v (N_BIT_ADDR w)    → T)
    1199       (p_relative:          ∀w: Byte.        is_in m fixed_v (RELATIVE w)      → T)
    1200         (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
    1201       on v: Prop ≝
    1202   match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
    1203   [ VEmpty         ⇒ λm_refl. λv_refl.
    1204       ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
    1205         Q addr (
    1206         match addr return λx: addressing_mode. is_in … fixed_v x → T with 
    1207         [ ADDR11 x          ⇒ p_addr11 x
    1208         | ADDR16 x          ⇒ p_addr16 x
    1209         | DIRECT x          ⇒ p_direct x
    1210         | INDIRECT x        ⇒ p_indirect x
    1211         | EXT_INDIRECT x    ⇒ p_ext_indirect x
    1212         | ACC_A             ⇒ p_acc_a
    1213         | REGISTER x        ⇒ p_register x
    1214         | ACC_B             ⇒ p_acc_b
    1215         | DPTR              ⇒ p_dptr
    1216         | DATA x            ⇒ p_data x
    1217         | DATA16 x          ⇒ p_data16 x
    1218         | ACC_DPTR          ⇒ p_acc_dptr
    1219         | ACC_PC            ⇒ p_acc_pc
    1220         | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
    1221         | INDIRECT_DPTR     ⇒ p_indirect_dptr
    1222         | CARRY             ⇒ p_carry
    1223         | BIT_ADDR x        ⇒ p_bit_addr x
    1224         | N_BIT_ADDR x      ⇒ p_n_bit_addr x
    1225         | RELATIVE x        ⇒ p_relative x
    1226         ] p)
    1227   | VCons n' hd tl ⇒ λm_refl. λv_refl.
    1228     let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
    1229       p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
    1230         p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
    1231           p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
    1232             p_bit_addr p_n_bit_addr p_relative n' tl ?
    1233     in
    1234     match hd return λa: addressing_mode_tag. a = hd → ? with
    1235     [ addr11            ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
    1236     | addr16            ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
    1237     | direct            ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
    1238     | indirect          ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
    1239     | ext_indirect      ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
    1240     | acc_a             ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
    1241     | registr           ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
    1242     | acc_b             ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
    1243     | dptr              ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
    1244     | data              ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
    1245     | data16            ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
    1246     | acc_dptr          ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
    1247     | acc_pc            ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
    1248     | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
    1249     | indirect_dptr     ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
    1250     | carry             ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
    1251     | bit_addr          ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
    1252     | n_bit_addr        ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
    1253     | relative          ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
    1254     ] (refl … hd)
    1255   ] (refl … n) (refl_jmeq … v).
    1256   [20:
    1257     generalize in match proof; destruct
    1258     whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
    1259     cases (mem … eq_a m fixed_v hd) normalize nodelta
    1260     [1:
    1261       whd in match (subvector_with … eq_a tl fixed_v);
    1262       #assm assumption
    1263     |2:
    1264       normalize in ⊢ (% → ?);
    1265       #absurd cases absurd
    1266     ]
    1267   ]
    1268   @(is_in_subvector_is_in_supervector … proof)
    1269   destruct @I
    1270 qed.
    1271 
    1272 (* XXX: todo *)
    1273 lemma subaddressing_mode_elim':
    1274   ∀T: Type[2].
    1275   ∀n: nat.
    1276   ∀o: nat.
    1277   ∀v1: Vector addressing_mode_tag n.
    1278   ∀v2: Vector addressing_mode_tag o.
    1279   ∀Q: addressing_mode → T → Prop.
    1280   ∀fixed_v: Vector addressing_mode_tag (n + o).
    1281   ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
    1282   ∀fixed_v_proof: fixed_v = v1 @@ v2.
    1283   ∀subaddressing_mode_proof.
    1284     subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
    1285       P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.
    1286   #T #n #o #v1 #v2
    1287   elim v1 cases v2
    1288   [1:
    1289     #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
    1290     #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
    1291     #subaddressing_mode_proof destruct normalize
    1292     #addr #absurd cases absurd
    1293   |2:
    1294     #n' #hd #tl #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
    1295     #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
    1296     destruct normalize in match ([[]]@@hd:::tl);
    1297   ]
    1298   cases daemon
    1299 qed.
    1300 
    1301 (* XXX: todo *)
    1302 lemma subaddressing_mode_elim:
    1303   ∀T: Type[2].
    1304   ∀m: nat.
    1305   ∀n: nat.
    1306   ∀Q: addressing_mode → T → Prop.
    1307   ∀fixed_v: Vector addressing_mode_tag m.
    1308   ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
    1309   ∀v: Vector addressing_mode_tag n.
    1310   ∀proof.
    1311     subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
    1312       P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
    1313   #T #m #n #Q #fixed_v
    1314   elim fixed_v
    1315   [1:
    1316     #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
    1317     #P14 #P15 #P16 #P17 #P18 #P19 #v #proof
    1318     normalize
    1319   |2:
    1320   ]
    1321   cases daemon
    1322 qed.
    13231015
    13241016definition program_counter_after_other ≝
     
    13971089              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    13981090              let s ≝ set_8051_sfr … s SFR_SP new_sp in
    1399               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
     1091              let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
    14001092              let s ≝ write_at_stack_pointer … s pc_bl in
    14011093              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    14021094              let s ≝ set_8051_sfr … s SFR_SP new_sp in
    14031095              let s ≝ write_at_stack_pointer … s pc_bu in
    1404               let 〈thr, eig〉 ≝ split ? 3 8 a in
    1405               let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
     1096              let 〈thr, eig〉 ≝ vsplit ? 3 8 a in
     1097              let 〈fiv, thr'〉 ≝ vsplit ? 5 3 pc_bu in
    14061098              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
    14071099                set_program_counter … s new_addr
     
    14151107              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    14161108              let s ≝ set_8051_sfr … s SFR_SP new_sp in
    1417               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
     1109              let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
    14181110              let s ≝ write_at_stack_pointer … s pc_bl in
    14191111              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     
    15151207      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    15161208      let s ≝ set_8051_sfr … s SFR_SP new_sp in
    1517       let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in
     1209      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
    15181210      let s ≝ write_at_stack_pointer … s pc_bl in
    15191211      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
  • src/ASM/Policy.ma

    r2018 r2032  
    141141        let a ≝ bitvector_of_nat 16 addr in
    142142        let p ≝ bitvector_of_nat 16 pc in
    143         let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 a in
    144         let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 p in
     143        let 〈fst_5_addr, rest_addr〉 ≝ vsplit bool 5 11 a in
     144        let 〈fst_5_pc, rest_pc〉 ≝ vsplit bool 5 11 p in
    145145        eq_bv 5 fst_5_addr fst_5_pc = true
    146146     | long_jump   ⇒ True
     
    359359            + added
    360360    else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in
    361   let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (bitvector_of_nat ? addr) in
    362   let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 (bitvector_of_nat ? (\fst inc_sigma)) in
     361  let 〈fst_5_addr, rest_addr〉 ≝ vsplit ? 5 11 (bitvector_of_nat ? addr) in
     362  let 〈fst_5_pc, rest_pc〉 ≝ vsplit ? 5 11 (bitvector_of_nat ? (\fst inc_sigma)) in
    363363  if eq_bv ? fst_5_addr fst_5_pc
    364364  then medium_jump
     
    655655 [1: #pi cases pi
    656656   [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    657      [1,2,3,6,7,24,25: #x #y
    658      |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    659      #H cases H
    660    |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    661      #_ cases a cases b
    662      [1,5,7,8,9: #_ / by refl/
    663      |10,14,16,17,18: #_ / by refl/
    664      |19,23,25,26,27: #_ / by refl/
    665      |28,32,34,35,36: #_ / by refl/
    666      |37,41,43,44,45: #_ / by refl/
    667      |46,50,52,53,54: #_ / by refl/
    668      |55,59,61,62,63: #_ / by refl/
    669      |64,68,70,71,72: #_ / by refl/
    670      |73,77,79,80,81: #_ / by refl/
    671      |2,3,4,6: cases x #a cases a
    672        [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb
    673        |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb
    674        |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb
    675        |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb
    676        |5,6,7,10,11,12,13,14: #Hb cases Hb
    677        |24,25,26,29,30,31,32,33: #Hb cases Hb
    678        |43,44,45,48,49,50,51,52: #Hb cases Hb
    679        |62,63,64,67,68,69,70,71: #Hb cases Hb
    680        |15,34,53,72: #b #Hb #H normalize in H; destruct (H)
    681        ]
    682      |11,12,13,15: cases x #a cases a
    683        [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb
    684        |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb
    685        |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb
    686        |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb
    687        |5,6,7,10,11,12,13,14: #Hb cases Hb
    688        |24,25,26,29,30,31,32,33: #Hb cases Hb
    689        |43,44,45,48,49,50,51,52: #Hb cases Hb
    690        |62,63,64,67,68,69,70,71: #Hb cases Hb
    691        |15,34,53,72: #b #Hb #H normalize in H; destruct (H)
    692        ]
    693      |20,21,22,24: cases x #a cases a
    694        [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb
    695        |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb
    696        |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb
    697        |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb
    698        |5,6,7,10,11,12,13,14: #Hb cases Hb
    699        |24,25,26,29,30,31,32,33: #Hb cases Hb
    700        |43,44,45,48,49,50,51,52: #Hb cases Hb
    701        |62,63,64,67,68,69,70,71: #Hb cases Hb
    702        |15,34,53,72: #b #Hb #H normalize in H; destruct (H)
    703        ]
    704      |29,30,31,33: cases x #a cases a #a1 #a2
    705        [1,3,5,7: cases a2 #b cases b
    706          [2,3,4,9,15,16,17,18,19: #b #Hb cases Hb
    707          |21,22,23,28,34,35,36,37,38: #b #Hb cases Hb
    708          |40,41,42,47,53,54,55,56,57: #b #Hb cases Hb
    709          |59,60,61,66,72,73,74,75,76: #b #Hb cases Hb
    710          |5,6,7,10,11,12,13,14: #Hb cases Hb
    711          |24,25,26,29,30,31,32,33: #Hb cases Hb
    712          |43,44,45,48,49,50,51,52: #Hb cases Hb
    713          |62,63,64,67,68,69,70,71: #Hb cases Hb
    714          |1,8: #b #Hb #H normalize in H; destruct (H)
    715          |20,27: #b #Hb #H normalize in H; destruct (H)
    716          |39,46: #b #Hb #H normalize in H; destruct (H)
    717          |58,65: #b #Hb #H normalize in H; destruct (H)
    718          ]
    719        |2,4,6,8: cases a1 #b cases b
    720          [1,3,8,9,15,16,17,18,19: #b #Hb cases Hb
    721          |20,22,27,28,34,35,36,37,38: #b #Hb cases Hb
    722          |39,41,46,47,53,54,55,56,57: #b #Hb cases Hb
    723          |58,60,65,66,72,73,74,75,76: #b #Hb cases Hb
    724          |5,6,7,10,11,12,13,14: #Hb cases Hb
    725          |24,25,26,29,30,31,32,33: #Hb cases Hb
    726          |43,44,45,48,49,50,51,52: #Hb cases Hb
    727          |62,63,64,67,68,69,70,71: #Hb cases Hb
    728          |2,4: #b #Hb #H normalize in H; destruct (H)
    729          |21,23: #b #Hb #H normalize in H; destruct (H)
    730          |40,42: #b #Hb #H normalize in H; destruct (H)
    731          |59,61: #b #Hb #H normalize in H; destruct (H)
    732          ]
    733        ]
    734      |38,39,40,42: cases x #a cases a
    735        [2,3,8,9,15,16,17,18,19: #b #Hb cases Hb
    736        |21,22,27,28,34,35,36,37,38: #b #Hb cases Hb
    737        |40,41,46,47,53,54,55,56,57: #b #Hb cases Hb
    738        |59,60,65,66,72,73,74,75,76: #b #Hb cases Hb
    739        |5,6,7,10,11,12,13,14: #Hb cases Hb
    740        |24,25,26,29,30,31,32,33: #Hb cases Hb
    741        |43,44,45,48,49,50,51,52: #Hb cases Hb
    742        |62,63,64,67,68,69,70,71: #Hb cases Hb
    743        |1,4: #b #Hb #H normalize in H; destruct (H)
    744        |20,23: #b #Hb #H normalize in H; destruct (H)
    745        |39,42: #b #Hb #H normalize in H; destruct (H)
    746        |58,61: #b #Hb #H normalize in H; destruct (H)
    747        ]
    748      |47,48,49,51: cases x #a #H normalize in H; destruct (H)
    749      |56,57,58,60: cases x #a #H normalize in H; destruct (H)
    750      |65,66,67,69: cases x #a #H normalize in H; destruct (H)
    751      |74,75,76,78: cases x #a #H normalize in H; destruct (H)
    752      ]
     657     try (#x #y #H #_) try (#x #H #_) try (#H #_) cases H
     658   |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #_ try (#_ %)
     659     try (#abs normalize in abs; destruct (abs) @I)
     660     cases a; cases b; try (#_ %) try (#abs normalize in abs; destruct(abs) @I)
     661     try (@(subaddressing_mode_elim … x) #w #abs normalize in abs; destruct (abs) @I)
     662     cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w
     663     try ( #abs normalize in abs; destruct (abs) @I)
     664     @(subaddressing_mode_elim … a1) #w2 #abs normalize in abs; destruct (abs)
    753665   ]
    754666  |2,3,6: #x [3: #y] #H cases H
  • src/ASM/Status.ma

    r1946 r2032  
    693693    let c ≝ get_index_v … r 1 ? in
    694694    let d ≝ get_index_v … r 2 ? in
    695     let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
     695    let 〈 un, ln 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
    696696    let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in
    697697    let offset ≝
     
    736736  λcode_memory:M.
    737737  λs: PreStatus M code_memory.
    738     let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_SP) in
     738    let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_SP) in
    739739    let m ≝ get_index_v ?? nu O ? in
    740740    let r1 ≝ get_index_v ?? nu 1 ? in
     
    761761  λs: PreStatus M code_memory.
    762762  λv: Byte.
    763     let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ?? s SFR_SP) in
     763    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ?? s SFR_SP) in
    764764    let bit_zero ≝ get_index_v ?? nu O ? in
    765765    let bit_1 ≝ get_index_v ?? nu 1 ? in
     
    785785   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M ? s = clock M ? s' with
    786786     [ DPTR ⇒ λ_:True.
    787        let 〈 bu, bl 〉 ≝ split … 8 8 v in
     787       let 〈 bu, bl 〉 ≝ vsplit … 8 8 v in
    788788       let status ≝ set_8051_sfr … s SFR_DPH bu in
    789789       let status ≝ set_8051_sfr … status SFR_DPL bl in
     
    850850      | DIRECT d ⇒
    851851        λdirect: True.
    852           let 〈 nu, nl 〉 ≝ split ? 4 4 d in
     852          let 〈 nu, nl 〉 ≝ vsplit ? 4 4 d in
    853853          let bit_one ≝ get_index_v ? ? nu 0 ? in
    854           let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
     854          let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
    855855            match bit_one with
    856856              [ false ⇒
     
    861861      | INDIRECT i ⇒
    862862        λindirect: True.
    863           let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ?? s [[ false; false; i]]) in
    864           let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
     863          let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_register ?? s [[ false; false; i]]) in
     864          let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in
    865865          let bit_1 ≝ get_index_v ?? bit_one_v O ? in
    866866          match  bit_1 with
     
    895895      [ DIRECT d ⇒
    896896        λdirect: True.
    897           let 〈 nu, nl 〉 ≝ split … 4 4 d in
     897          let 〈 nu, nl 〉 ≝ vsplit … 4 4 d in
    898898          let bit_one ≝ get_index_v ? ? nu 0 ? in
    899           let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
     899          let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
    900900            match bit_one with
    901901              [ true ⇒ set_bit_addressable_sfr ?? s d v
     
    907907        λindirect: True.
    908908          let register ≝ get_register ?? s [[ false; false; i ]] in
    909           let 〈nu, nl〉 ≝ split ? 4 4 register in
     909          let 〈nu, nl〉 ≝ vsplit ? 4 4 register in
    910910          let bit_1 ≝ get_index_v … nu 0 ? in
    911           let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
     911          let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in
    912912            match bit_1 with
    913913              [ false ⇒
     
    10041004      [ BIT_ADDR b ⇒
    10051005        λbit_addr: True.
    1006           let 〈 nu, nl 〉 ≝ split … 4 4 b in
     1006          let 〈 nu, nl 〉 ≝ vsplit … 4 4 b in
    10071007          let bit_1 ≝ get_index_v ? ? nu 0 ? in
    1008           let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
     1008          let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in
    10091009            match bit_1 with
    10101010              [ true ⇒
     
    10231023      | N_BIT_ADDR n ⇒
    10241024        λn_bit_addr: True.
    1025           let 〈 nu, nl 〉 ≝ split … 4 4 n in
     1025          let 〈 nu, nl 〉 ≝ vsplit … 4 4 n in
    10261026          let bit_1 ≝ get_index_v ? ? nu 0 ? in
    1027           let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
     1027          let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in
    10281028            match bit_1 with
    10291029              [ true ⇒
     
    10611061    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with
    10621062      [ BIT_ADDR b ⇒ λbit_addr: True.
    1063         let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
     1063        let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
    10641064        let bit_1 ≝ get_index_v ?? nu 0 ? in
    1065         let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
     1065        let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in
    10661066        match bit_1 return λ_. ? with
    10671067          [ true ⇒
     
    10831083      | CARRY ⇒
    10841084        λcarry: True.
    1085         let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
     1085        let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
    10861086        let bit_1 ≝ get_index_v… nu 1 ? in
    10871087        let bit_2 ≝ get_index_v… nu 2 ? in
  • src/ASM/StatusProofs.ma

    r1962 r2032  
    2727  #m #s #v
    2828  whd in match write_at_stack_pointer; normalize nodelta
    29   cases(split … 4 4 ?) #nu #nl normalize nodelta
     29  cases(vsplit … 4 4 ?) #nu #nl normalize nodelta
    3030  cases(get_index_v … 4 nu 0 ?) //
    3131qed.
     
    178178  whd in match set_arg_8; normalize nodelta
    179179  whd in match set_arg_8'; normalize nodelta
    180   cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
    181   cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
     180  cases (vsplit bool 4 4 ?) #nu' #nl' normalize nodelta
     181  cases (vsplit bool 1 3 nu') #bit1' #ignore' normalize nodelta
    182182  cases (get_index_v bool 4 nu' 0 ?) normalize nodelta
    183183  try % @set_bit_addressable_sfr_set_code_memory
     
    201201  whd in match set_arg_8; normalize nodelta
    202202  whd in match set_arg_8'; normalize nodelta
    203   cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
    204   cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
     203  cases (vsplit bool 4 4 ?) #nu' #nl' normalize nodelta
     204  cases (vsplit bool 1 3 nu') #bit1' #ignore' normalize nodelta
    205205  cases (get_index_v bool 4 nu' 0 ?) normalize nodelta
    206206  try % cases daemon (*@(set_bit_addressable_sfr_set_program_counter)*)
     
    238238  = special_function_registers_8051 T cm s.
    239239 #T #cm #s #x whd in ⊢ (??(???%)?);
    240  cases (split ????) #nu #nl normalize nodelta;
     240 cases (vsplit ????) #nu #nl normalize nodelta;
    241241 cases (get_index_v bool ????) %
    242242qed.
     
    250250 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
    251251 #T #s #x whd in ⊢ (??(??%)?);
    252  cases (split ????) #nu #nl normalize nodelta;
     252 cases (vsplit ????) #nu #nl normalize nodelta;
    253253 cases (get_index_v bool ????) %
    254254qed.*)
     
    299299 ∀T,cm,s,x. external_ram T cm (write_at_stack_pointer T cm s x) = external_ram T cm s.
    300300 #T #cm #s #x whd in ⊢ (??(???%)?);
    301  cases (split ????) #nu #nl normalize nodelta;
     301 cases (vsplit ????) #nu #nl normalize nodelta;
    302302 cases (get_index_v bool ????) %
    303303qed.
     
    308308  = special_function_registers_8052 T cm s.
    309309 #T #cm #s #x whd in ⊢ (??(???%)?);
    310  cases (split ????) #nu #nl normalize nodelta;
     310 cases (vsplit ????) #nu #nl normalize nodelta;
    311311 cases (get_index_v bool ????) %
    312312qed.
     
    315315 ∀T,cm,s,x. p1_latch T cm (write_at_stack_pointer T cm s x) = p1_latch T cm s.
    316316 #T #cm #s #x whd in ⊢ (??(???%)?);
    317  cases (split ????) #nu #nl normalize nodelta;
     317 cases (vsplit ????) #nu #nl normalize nodelta;
    318318 cases (get_index_v bool ????) %
    319319qed.
     
    322322 ∀T,cm,s,x. p3_latch T cm (write_at_stack_pointer T cm s x) = p3_latch T cm s.
    323323 #T #cm #s #x whd in ⊢ (??(???%)?);
    324  cases (split ????) #nu #nl normalize nodelta;
     324 cases (vsplit ????) #nu #nl normalize nodelta;
    325325 cases (get_index_v bool ????) %
    326326qed.
     
    356356  try (#ignore #addr normalize in addr; cases addr)
    357357  normalize nodelta try #_ try /demod/ try %
    358   cases (split bool 4 4 ?) #nu #nl normalize nodelta
    359   cases (split bool 1 3 ?) #ignore #three_bits normalize nodelta
     358  cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta
     359  cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta
    360360  cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try %
    361361qed.
     
    373373  try (#addr normalize in addr; cases addr)
    374374  normalize nodelta
    375   cases (split bool 4 4 ?) #nu #nl normalize nodelta try /demod/ try %
    376   cases (split bool 1 3 ?) #ignore #three_bits normalize nodelta
     375  cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta try /demod/ try %
     376  cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta
    377377  cases (get_index_v bool 4 nu ??) normalize nodelta
    378378  (* XXX: try /demod/ try % *)
     
    391391  try (#addr normalize in addr; cases addr)
    392392  normalize nodelta
    393   cases (split bool 8 8 v) #bu #bl normalize nodelta /demod/ %
     393  cases (vsplit bool 8 8 v) #bu #bl normalize nodelta /demod/ %
    394394qed.
    395395
     
    413413  #m #cm #s #v
    414414  whd in match write_at_stack_pointer; normalize nodelta
    415   cases (split bool 4 4 ?) #nu #nl normalize nodelta
     415  cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta
    416416  cases (get_index_v bool 4 nu ??) normalize nodelta /demod/ %
    417417qed.
  • src/ASM/Util.ma

    r2005 r2032  
    172172qed.
    173173
    174 let rec split
     174let rec safe_split
    175175  (A: Type[0]) (l: list A) (index: nat) (proof: index ≤ |l|)
    176176    on index ≝
     
    181181    [ nil ⇒ λnil_absrd. ?
    182182    | cons hd tl ⇒ λcons_prf.
    183       let 〈l1, l2〉 ≝ split A tl index' ? in
     183      let 〈l1, l2〉 ≝ safe_split A tl index' ? in
    184184        〈hd :: l1, l2〉
    185185    ] succ_prf
  • src/ASM/Vector.ma

    r1908 r2032  
    4040  non associative with precedence 90
    4141  for @{ 'get_index_v $l $n }.
     42
     43lemma dependent_rewrite_vectors:
     44  ∀A:Type[0].
     45  ∀n, m: nat.
     46  ∀v1: Vector A n.
     47  ∀v2: Vector A m.
     48  ∀P: ∀m. Vector A m → Prop.
     49    n = m → v1 ≃ v2 → P n v1 → P m v2.
     50  #A #n #m #v1 #v2 #P #eq #jmeq
     51  destruct #assm assumption
     52qed.
     53
     54lemma jmeq_cons_vector_monotone:
     55  ∀A: Type[0].
     56  ∀m, n: nat.
     57  ∀v: Vector A m.
     58  ∀q: Vector A n.
     59  ∀prf: m = n.
     60  ∀hd: A.
     61    v ≃ q → hd:::v ≃ hd:::q.
     62  #A #m #n #v #q #prf #hd #E
     63  @(dependent_rewrite_vectors A … E)
     64  try assumption %
     65qed.
    4266
    4367(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    161185[ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].
    162186
    163 let rec split' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
     187let rec vsplit' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
    164188 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
    165189  [ O ⇒ λv. 〈[[ ]], v〉
    166   | S m' ⇒ λv. let 〈l,r〉 ≝ split' A m' n (tail ?? v) in 〈head' ?? v:::l, r〉
     190  | S m' ⇒ λv. let 〈l,r〉 ≝ vsplit' A m' n (tail ?? v) in 〈head' ?? v:::l, r〉
    167191  ].
    168192(* Prevent undesirable unfolding. *)
    169 let rec split (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝
    170  split' A m n v.
     193let rec vsplit (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝
     194 vsplit' A m n v.
    171195
    172196definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
     
    303327interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
    304328
    305 axiom split_elim':
     329lemma vector_cons_append:
     330  ∀A: Type[0].
     331  ∀n: nat.
     332  ∀e: A.
     333  ∀v: Vector A n.
     334    e ::: v = [[ e ]] @@ v.
     335  #A #n #e #v
     336  cases v try %
     337  #n' #hd #tl %
     338qed.
     339
     340lemma vector_cons_append2:
     341  ∀A: Type[0].
     342  ∀n, m: nat.
     343  ∀v: Vector A n.
     344  ∀q: Vector A m.
     345  ∀hd: A.
     346    hd:::(v@@q) = (hd:::v)@@q.
     347  #A #n #m #v #q
     348  elim v try (#hd %)
     349  #n' #hd' #tl' #ih #hd'
     350  <ih %
     351qed.
     352
     353lemma vector_associative_append:
     354  ∀A: Type[0].
     355  ∀n, m, o:  nat.
     356  ∀v: Vector A n.
     357  ∀q: Vector A m.
     358  ∀r: Vector A o.
     359    (v @@ q) @@ r ≃ v @@ (q @@ r).
     360  #A #n #m #o #v #q #r
     361  elim v try %
     362  #n' #hd #tl #ih
     363  <(vector_cons_append2 A … hd)
     364  @jmeq_cons_vector_monotone
     365  try assumption
     366  @associative_plus
     367qed.
     368
     369axiom vsplit_elim':
    306370  ∀A: Type[0].
    307371  ∀B: Type[1].
     
    310374  ∀P: B → Prop.
    311375    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
    312       P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt).
    313 
    314 axiom split_elim'':
     376      P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt).
     377
     378axiom vsplit_elim'':
    315379  ∀A: Type[0].
    316380  ∀B,B': Type[1].
     
    320384  ∀P: B → B' → Prop.
    321385    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
    322       P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt)
    323         (let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt).
     386      P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt)
     387        (let 〈lft, rgt〉 ≝ vsplit A l m v in T' lft rgt).
    324388   
    325389let rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
     
    432496  λv: Vector A (S n).
    433497  λa: A.
    434     let 〈v',dropped〉 ≝ split ? n 1 (switch_bv_plus ? 1 n v) in a:::v'.
     498    let 〈v',dropped〉 ≝ vsplit ? n 1 (switch_bv_plus ? 1 n v) in a:::v'.
    435499(*    reverse … (shift_left_1 … (reverse … v) a).*)
    436500
     
    441505    [ nat_lt _ _ ⇒ λv,a. replicate … a
    442506    | nat_eq _   ⇒ λv,a. replicate … a
    443     | nat_gt d m ⇒ λv,a. let 〈v0,v'〉 ≝ split … v in switch_bv_plus … (v' @@ (replicate … a))
     507    | nat_gt d m ⇒ λv,a. let 〈v0,v'〉 ≝ vsplit … v in switch_bv_plus … (v' @@ (replicate … a))
    444508    ].
    445509
     
    522586  fold_right … (λy,v. (eq_a x y) ∨ v) false l.
    523587
     588lemma mem_append: ∀A,eq_a. (∀x. eq_a x x = true) → ∀n,m.∀v: Vector A n. ∀w: Vector A m. ∀x. mem A eq_a … (v@@x:::w) x.
     589 #A #eq_a #refl #n #m #v elim v
     590 [ #w #x whd whd in match (mem ?????); >refl //
     591 | /2/
     592 ]
     593qed.
     594
    524595let rec subvector_with
    525596  (a: Type[0]) (n: nat) (m: nat) (eq: a → a → bool) (sub: Vector a n) (sup: Vector a m)
     
    533604      false
    534605  ].
    535    
     606
     607lemma subvector_with_refl0:
     608 ∀A:Type[0]. ∀n. ∀eq: A → A → bool. (∀a. eq a a = true) → ∀v: Vector A n.
     609  ∀m. ∀w: Vector A m. subvector_with A … eq v (w@@v).
     610 #A #n #eq #refl #v elim v
     611 [ //
     612 | #m #hd #tl #IH #m #w whd in match (subvector_with ??????); >mem_append //
     613   change with (bool_to_Prop (subvector_with ??????)) lapply (IH … (w@@[[hd]]))
     614  lapply (vector_associative_append ???? w [[hd]] tl) #EQ
     615  @(dependent_rewrite_vectors … EQ) //
     616 ]
     617qed.
     618
     619lemma subvector_with_refl:
     620 ∀A:Type[0]. ∀n. ∀eq: A → A → bool. (∀a. eq a a = true) → ∀v: Vector A n.
     621  subvector_with A … eq v v.
     622 #A #n #eq #refl #v @(subvector_with_refl0 … v … [[]]) //
     623qed.
     624
    536625(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    537626(* Lemmas.                                                                    *)
  • src/ASM/WellLabeled.ma

    r1494 r2032  
    3131        match acall return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    3232        [ ADDR11 addr11 ⇒ λ_.
    33           let 〈pc_bu, pc_bl〉 ≝ split … 8 8 pc in
    34           let 〈thr, eig〉 ≝ split … 3 8 addr11 in
    35           let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
     33          let 〈pc_bu, pc_bl〉 ≝ vsplit … 8 8 pc in
     34          let 〈thr, eig〉 ≝ vsplit … 3 8 addr11 in
     35          let 〈fiv, thr'〉 ≝ vsplit … 5 3 pc_bu in
    3636          let new_pc ≝ (fiv @@ thr) @@ pc_bl in
    3737            match lookup_opt … new_pc cost_labels with
     
    4444        match ajmp return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    4545        [ ADDR11 addr11 ⇒ λ_.
    46           let 〈pc_bu, pc_bl〉 ≝ split … 8 8 pc in
    47           let 〈nu, nl〉 ≝ split … 4 4 pc_bu in
     46          let 〈pc_bu, pc_bl〉 ≝ vsplit … 8 8 pc in
     47          let 〈nu, nl〉 ≝ vsplit … 4 4 pc_bu in
    4848          let bit ≝ get_index' … O ? nl in
    49           let 〈relevant1, relevant2〉 ≝ split … 3 8 addr11 in
     49          let 〈relevant1, relevant2〉 ≝ vsplit … 3 8 addr11 in
    5050          let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    5151          let 〈carry, new_pc〉 ≝ half_add … pc new_addr in
  • src/Clight/Csem.ma

    r1988 r2032  
    197197      [ Vint sz1 n1 ⇒ match v2 with
    198198          [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    199                           (λn1. Some ? (Vint sz2 (\snd (split ??? (multiplication ? n1 n2))))) (None ?)
     199                          (λn1. Some ? (Vint sz2 (\snd (vsplit ??? (multiplication ? n1 n2))))) (None ?)
    200200        | _ ⇒ None ? ]
    201201      | _ ⇒ None ? ]
  • src/Clight/SimplifyCasts.ma

    r2030 r2032  
    4646  reduce_bits n m exp v = Some ? v' → v' = truncate n (S m) v.
    4747#n #m elim n
    48 [ 1: #exp #v #v' #H normalize in v v' H; destruct normalize >split_O_n //
     48[ 1: #exp #v #v' #H normalize in v v' H; destruct normalize >vsplit_O_n //
    4949| 2: #n' #Hind #exp #v #v' #H >truncate_tail
    5050 > (Hind ??? (reduce_bits_ok ?? exp v v' H)) // ] qed.
     
    328328qed.
    329329 
    330 lemma split_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n).  ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2.
     330lemma vsplit_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n).  ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2.
    331331# A #m #n elim m
    332332[ 1: normalize #v
     
    343343] qed.
    344344
    345 lemma split_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n).  ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2.
     345lemma vsplit_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n).  ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2.
    346346# A #m #n elim m
    347347[ 1: normalize #v @(ex_intro … (VEmpty ?)) @(ex_intro … v) normalize //
     
    355355] qed.
    356356
    357 lemma split_zero:
     357lemma vsplit_zero:
    358358  ∀A,m.
    359359  ∀v: Vector A m.
    360     〈[[]], v〉 = split A 0 m v.
     360    〈[[]], v〉 = vsplit A 0 m v.
    361361  #A #m #v
    362362  elim v
     
    368368
    369369
    370 lemma split_zero2:
     370lemma vsplit_zero2:
    371371  ∀A,m.
    372372  ∀v: Vector A m.
    373     〈[[]], v〉 = split' A 0 m v.
     373    〈[[]], v〉 = vsplit' A 0 m v.
    374374  #A #m #v
    375375  elim v
     
    382382(* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma.
    383383 * TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *)
    384 axiom split_succ:
     384axiom vsplit_succ:
    385385  ∀A, m, n.
    386386  ∀l: Vector A m.
     
    388388  ∀v: Vector A (m + n).
    389389  ∀hd.
    390     v = l@@r → (〈l, r〉 = split ? m n v → 〈hd:::l, r〉 = split ? (S m) n (hd:::v)).
    391 
    392 axiom split_succ2:
     390    v = l@@r → (〈l, r〉 = vsplit ? m n v → 〈hd:::l, r〉 = vsplit ? (S m) n (hd:::v)).
     391
     392axiom vsplit_succ2:
    393393  ∀A, m, n.
    394394  ∀l: Vector A m.
     
    396396  ∀v: Vector A (m + n).
    397397  ∀hd.
    398     v = l@@r → (〈l, r〉 = split' ? m n v → 〈hd:::l, r〉 = split' ? (S m) n (hd:::v)).
     398    v = l@@r → (〈l, r〉 = vsplit' ? m n v → 〈hd:::l, r〉 = vsplit' ? (S m) n (hd:::v)).
    399399     
    400 lemma split_prod2:
     400lemma vsplit_prod2:
    401401  ∀A,m,n.
    402402  ∀p: Vector A (m + n).
    403403  ∀v: Vector A m.
    404404  ∀q: Vector A n.
    405     p = v@@q → 〈v, q〉 = split' A m n p.
     405    p = v@@q → 〈v, q〉 = vsplit' A m n p.
    406406  #A #m
    407407  elim m
     
    409409    >hyp <(vector_append_zero A n q v)
    410410    >(prod_vector_zero_eq_left A …)
    411     @split_zero2
     411    @vsplit_zero2
    412412  | #r #ih #n #p #v #q #hyp
    413413    >hyp
     
    416416    cases exists
    417417    #tl #jmeq >jmeq
    418     @split_succ2 [1: % |2: @ih % ]
     418    @vsplit_succ2 [1: % |2: @ih % ]
    419419  ]
    420420qed.
    421421
    422 lemma split_prod:
     422lemma vsplit_prod:
    423423  ∀A,m,n.
    424424  ∀p: Vector A (m + n).
    425425  ∀v: Vector A m.
    426426  ∀q: Vector A n.
    427     p = v@@q → 〈v, q〉 = split A m n p.
     427    p = v@@q → 〈v, q〉 = vsplit A m n p.
    428428  #A #m
    429429  elim m
     
    431431    >hyp <(vector_append_zero A n q v)
    432432    >(prod_vector_zero_eq_left A …)
    433     @split_zero
     433    @vsplit_zero
    434434  | #r #ih #n #p #v #q #hyp
    435435    >hyp
     
    438438    cases exists
    439439    #tl #jmeq >jmeq
    440     @split_succ [1: % |2: @ih % ]
    441   ]
    442 qed.
    443 
    444 
    445 (* Stolen from AssemblyProof.ma *)
    446 lemma super_rewrite2:
    447  ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
    448   ∀P: ∀m. Vector A m → Prop.
    449    n=m → v1 ≃ v2 → P n v1 → P m v2.
    450  #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
    451 qed.
    452 
    453 lemma vector_cons_append:
    454   ∀A: Type[0].
    455   ∀n: nat.
    456   ∀e: A.
    457   ∀v: Vector A n.
    458     e ::: v = [[ e ]] @@ v.
    459   # A # N # E # V
    460   elim V
    461   [ normalize %
    462   | # NN # AA # VV # IH
    463     normalize
    464     %
    465 qed.
    466 
    467 lemma vector_cons_append2:
    468   ∀A: Type[0].
    469   ∀n, m: nat.
    470   ∀v: Vector A n.
    471   ∀q: Vector A m.
    472   ∀hd: A.
    473     hd:::(v@@q) = (hd:::v)@@q.
    474   #A #n #m #v #q
    475   elim v
    476   [ #hd %
    477   | #n' #hd' #tl' #ih #hd' <ih %
    478   ]
    479 qed.
    480 
    481 lemma jmeq_cons_vector_monotone:
    482   ∀A: Type[0].
    483   ∀m, n: nat.
    484   ∀v: Vector A m.
    485   ∀q: Vector A n.
    486   ∀prf: m = n.
    487   ∀hd: A.
    488     v ≃ q → hd:::v ≃ hd:::q.
    489   #A #m #n #v #q #prf #hd #E
    490   @(super_rewrite2 A … E)
    491   [ assumption | % ]
    492 qed.
    493 
    494 lemma vector_associative_append:
    495   ∀A: Type[0].
    496   ∀n, m, o:  nat.
    497   ∀v: Vector A n.
    498   ∀q: Vector A m.
    499   ∀r: Vector A o.
    500     ((v @@ q) @@ r)
    501     ≃
    502     (v @@ (q @@ r)).
    503   #A #n #m #o #v #q #r
    504   elim v
    505   [ %
    506   | #n' #hd #tl #ih
    507     <(vector_cons_append2 A … hd)
    508     @jmeq_cons_vector_monotone
    509     //
     440    @vsplit_succ [1: % |2: @ih % ]
    510441  ]
    511442qed.
     
    514445#s1 #v normalize elim s1 normalize nodelta
    515446normalize in v;
    516 elim (split_eq ??? (v⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
     447elim (vsplit_eq ??? (v⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
    517448[ 2,4: //
    518449| 1,3: #l * #r normalize nodelta #Eq1
    519        <(split_prod bool 16 16 … Eq1)
    520        elim (split_eq ??? (r⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
     450       <(vsplit_prod bool 16 16 … Eq1)
     451       elim (vsplit_eq ??? (r⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
    521452       [ 2,4: //
    522453       | 1,3: #lr * #rr normalize nodelta #Eq2
    523               <(split_prod bool 8 8 … Eq2)
     454              <(vsplit_prod bool 8 8 … Eq2)
    524455              cut (v = (l @@ lr) @@ rr)
    525456              [ 1,3 : destruct >(vector_associative_append ? 16 8) //
    526457              | 2,4: #Hrewrite destruct
    527                      <(split_prod bool 24 8 … Hrewrite) @refl
     458                     <(vsplit_prod bool 24 8 … Hrewrite) @refl
    528459              ]
    529460       ]
     
    555486| 22: normalize elim b_sg elim a_sg normalize
    556487      normalize in val;
    557       elim (split_eq ??? (val⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
     488      elim (vsplit_eq ??? (val⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
    558489      [ 2,4,6,8: normalize //
    559490      | 1,3,5,7: #left * #right normalize #Eq1
    560                  <(split_prod bool 16 16 … Eq1)
    561                  elim (split_eq ??? (right⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
     491                 <(vsplit_prod bool 16 16 … Eq1)
     492                 elim (vsplit_eq ??? (right⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
    562493                 [ 2,4,6,8: //
    563494                 | 1,3,5,7: #rightleft * #rightright normalize #Eq2
    564                             <(split_prod bool 8 8 … Eq2)
     495                            <(vsplit_prod bool 8 8 … Eq2)
    565496                            cut (val = (left @@ rightleft) @@ rightright)
    566497                            [ 1,3,5,7: destruct >(vector_associative_append ? 16 8) //
    567498                            | 2,4,6,8: #Hrewrite destruct
    568                                        <(split_prod bool 24 8 … Hrewrite) @refl
     499                                       <(vsplit_prod bool 24 8 … Hrewrite) @refl
    569500                            ]
    570501                 ]
     
    616547>Heq in i; #i @i qed.
    617548
    618 (* cast_int_int behaves as truncate (≃ split) when downsizing *)
     549(* cast_int_int behaves as truncate (≃ vsplit) when downsizing *)
    619550(* ∀src_sz,target_sz,sg. ∀i. size_le target_sz src_sz → cast_int_int src_sz sg target_sz i = truncate *)
    620551
    621 lemma split_to_truncate : ∀m,n,i. (\snd  (split bool m n i)) = truncate  m n i.
     552lemma vsplit_to_truncate : ∀m,n,i. (\snd  (vsplit bool m n i)) = truncate  m n i.
    622553#m #n #i normalize // qed.
    623554
     
    640571  whd in match (addition_n ???);
    641572  whd in match (addition_n ???) in ⊢ (???%);
    642   >split_to_truncate >split_to_truncate
     573  >vsplit_to_truncate >vsplit_to_truncate
    643574  <truncate_add_with_carries
    644575  [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint rint false);
     
    677608@(ex_intro … tl)
    678609>Heq >Heq
    679 elim (split_eq2 … tl) #l * #r #Eq
     610elim (vsplit_eq2 … tl) #l * #r #Eq
    680611normalize
    681  <(split_prod bool n m tl l r Eq)
    682  <(split_prod2 bool n m tl l r Eq)
     612 <(vsplit_prod bool n m tl l r Eq)
     613 <(vsplit_prod2 bool n m tl l r Eq)
    683614 normalize //
    684615qed.
     
    690621     whd in match (truncate ???);
    691622     whd in match (truncate ???) in ⊢ (???%);
    692      <split_zero <split_zero //
     623     <vsplit_zero <vsplit_zero //
    693624| 2: #m' #Hind #n #i normalize in i;
    694625     elim (Vector_Sn … i) #hd * #tl #Heq     
     
    713644          * #Left #Right normalize nodelta
    714645          #H generalize in ⊢ (???(???(????(???(match % with [ _ ⇒ ? | _ ⇒  ?])))));
    715           #b >(split_to_truncate (S m')) >truncate_tail
     646          #b >(vsplit_to_truncate (S m')) >truncate_tail
    716647          cases b
    717648          normalize nodelta
     
    736667  whd in match (subtraction ???);
    737668  whd in match (subtraction ???) in ⊢ (???%);
    738   >split_to_truncate >split_to_truncate
     669  >vsplit_to_truncate >vsplit_to_truncate
    739670  >integer_neg_trunc <truncate_add_with_carries
    740671  [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint ? false);
  • src/Clight/casts.ma

    r1599 r2032  
    22
    33definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝
    4 λm,n,x. \snd (split … x).
    5 
    6 lemma split_O_n : ∀A,n,x. split A O n x = 〈[[ ]], x〉.
     4λm,n,x. \snd (vsplit … x).
     5
     6lemma vsplit_O_n : ∀A,n,x. vsplit A O n x = 〈[[ ]], x〉.
    77#A #n cases n [ #x @(vector_inv_n … x) @refl | #m #x @(vector_inv_n … x) // ]
    88qed.
    99
    1010lemma truncate_eq : ∀n,x. truncate 0 n x = x.
    11 #n #x normalize >split_O_n @refl
     11#n #x normalize >vsplit_O_n @refl
    1212qed.
    1313
     
    6666qed.
    6767
    68 lemma split_eq' : ∀A,m,n,v. split A m n v = split' A m n v.
     68lemma vsplit_eq' : ∀A,m,n,v. vsplit A m n v = vsplit' A m n v.
    6969#A #m cases m
    7070[ #n cases n
     
    7575] qed. 
    7676
    77 lemma split_left : ∀A,m,n,h,t.
    78   split A (S m) n (h:::t) = (let 〈l,r〉 ≝ split A m n t in 〈h:::l,r〉).
    79 #A #m #n #h #t normalize >split_eq' @refl
     77lemma vsplit_left : ∀A,m,n,h,t.
     78  vsplit A (S m) n (h:::t) = (let 〈l,r〉 ≝ vsplit A m n t in 〈h:::l,r〉).
     79#A #m #n #h #t normalize >vsplit_eq' @refl
    8080qed.
    8181
    8282lemma truncate_head : ∀m,n,h,t.
    8383  truncate (S m) n (h:::t) = truncate m n t.
    84 #m #n #h #t normalize >split_eq' cases (split' bool m n t) //
     84#m #n #h #t normalize >vsplit_eq' cases (vsplit' bool m n t) //
    8585qed.
    8686
  • src/Cminor/toRTLabs.ma

    r1884 r2032  
    828828| #l % [ % [ @(fn_con_env … (pi2 ?? r)) | @(fn_con_env … (pi2 ?? cr)) ] | @(fn_con_env … (pi2 ?? br)) ] repeat @fn_contains_step @I
    829829| #l @(fn_con_env … (pi2 ?? cr)) repeat @fn_contains_step @I
    830 | #_ (* see above *) <E @(pi2 ?? r)
     830| (*#_ (* see above *) <E @(pi2 ?? r)*) (*CSC: FIXME!!!*) cases daemon
    831831| @(pi2 … (pf_entry …))
    832832| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
  • src/RTL/RTLToERTL.ma

    r1995 r2032  
    246246  λglobals,params.
    247247  let n ≝ min (|params|) (|RegisterParams|) in
    248   let hdw_stack_params ≝ split ? params n ? in
     248  let hdw_stack_params ≝ vsplit ? params n ? in
    249249  let hdw_params ≝ \fst hdw_stack_params in
    250250  let stack_params ≝ \snd hdw_stack_params in
  • src/RTLabs/RTLabsToRTL.ma

    r1995 r2032  
    134134  [ I8 ⇒ λint. ? | I16 ⇒ λint. ? | I32 ⇒ λint. ? ].
    135135[ %[@[int]] //
    136 | %[@(let 〈h,l〉 ≝ split ? 8 … int in [l;h])] cases (split ????) //
    137 | %[@(let 〈h1,l〉 ≝ split ? 8 … int in
    138       let 〈h2,l〉 ≝ split ? 8 … l in
    139       let 〈h3,l〉 ≝ split ? 8 … l in
     136| %[@(let 〈h,l〉 ≝ vsplit ? 8 … int in [l;h])] cases (vsplit ????) //
     137| %[@(let 〈h1,l〉 ≝ vsplit ? 8 … int in
     138      let 〈h2,l〉 ≝ vsplit ? 8 … l in
     139      let 〈h3,l〉 ≝ vsplit ? 8 … l in
    140140       [l;h3;h2;h1])]
    141   cases (split ????) #h1 #l normalize
    142   cases (split ????) #h2 #l normalize
    143   cases (split ????) // ]
     141  cases (vsplit ????) #h1 #l normalize
     142  cases (vsplit ????) #h2 #l normalize
     143  cases (vsplit ????) // ]
    144144qed.
    145145
     
    533533  λtranslates: list ?.
    534534  λsrcr2i: register.
    535   let 〈tmp_destrs1, tmp_destrs2〉 ≝ split … tmp_destrs i i_prf in
     535  let 〈tmp_destrs1, tmp_destrs2〉 ≝ vsplit … tmp_destrs i i_prf in
    536536  let tmp_destrs2' ≝
    537537    match tmp_destrs2 with
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r1882 r2032  
    119119  [ I8 ⇒ λint. ? | I16 ⇒ λint. ? | I32 ⇒ λint. ? ].
    120120[ %[@[int]] //
    121 | %[@(let 〈h,l〉 ≝ split ? 8 … int in [l;h])] cases (split ????) normalize //
    122 | %[@(let 〈h1,l〉 ≝ split ? 8 … int in
    123       let 〈h2,l〉 ≝ split ? 8 … l in
    124       let 〈h3,l〉 ≝ split ? 8 … l in
     121| %[@(let 〈h,l〉 ≝ vsplit ? 8 … int in [l;h])] cases (vsplit ????) normalize //
     122| %[@(let 〈h1,l〉 ≝ vsplit ? 8 … int in
     123      let 〈h2,l〉 ≝ vsplit ? 8 … l in
     124      let 〈h3,l〉 ≝ vsplit ? 8 … l in
    125125       [l;h3;h2;h1])]
    126   cases (split ????) #h1 #l normalize
    127   cases (split ????) #h2 #l normalize
    128   cases (split ????) // ]
     126  cases (vsplit ????) #h1 #l normalize
     127  cases (vsplit ????) #h2 #l normalize
     128  cases (vsplit ????) // ]
    129129qed.
    130130
  • src/common/FrontEndOps.ma

    r1878 r2032  
    244244  [ Vint sz1 n1 ⇒ match v2 with
    245245    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    246                     (λn1. Some ? (Vint ? (\snd (split … (multiplication ? n1 n2)))))
     246                    (λn1. Some ? (Vint ? (\snd (vsplit … (multiplication ? n1 n2)))))
    247247                    (None ?)
    248248    | _ ⇒ None ? ]
  • src/common/FrontEndVal.ma

    r1987 r2032  
    2525match n return λn. BitVector (n*8) → ? with
    2626[ O ⇒ λ_. [ ]
    27 | S m ⇒ λv. let 〈h,t〉 ≝ split ??? v in h::(bytes_of_bitvector m t)
     27| S m ⇒ λv. let 〈h,t〉 ≝ vsplit ??? v in h::(bytes_of_bitvector m t)
    2828] v.
    2929
  • src/common/Integers.ma

    r1516 r2032  
    136136
    137137definition neg : int → int ≝ two_complement_negation wordsize.
    138 definition mul ≝ λx,y. \snd (split ? wordsize wordsize (multiplication wordsize x y)).
     138definition mul ≝ λx,y. \snd (vsplit ? wordsize wordsize (multiplication wordsize x y)).
    139139
    140140definition zero_ext_n : ∀w,n:nat. BitVector w → BitVector w ≝
     
    142142  match nat_compare n w return λx,y.λ_. BitVector y → BitVector y with
    143143  [ nat_lt n' w' ⇒ λi.
    144       let 〈h,l〉 ≝ split ? (S w') n' (switch_bv_plus ??? i) in
     144      let 〈h,l〉 ≝ vsplit ? (S w') n' (switch_bv_plus ??? i) in
    145145      switch_bv_plus ??? (pad ?? l)
    146146  | _ ⇒ λi.i
     
    153153  match nat_compare n w return λx,y.λ_. BitVector y → BitVector y with
    154154  [ nat_lt n' w' ⇒ λi.
    155       let 〈h,l〉 ≝ split ? (S w') n' (switch_bv_plus ??? i) in
     155      let 〈h,l〉 ≝ vsplit ? (S w') n' (switch_bv_plus ??? i) in
    156156      switch_bv_plus ??? (pad_vector ? (match l with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ]) ?? l)
    157157  | _ ⇒ λi.i
  • src/common/Values.ma

    r1872 r2032  
    214214  [ Vint sz1 n1 ⇒ match v2 with
    215215    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    216                     (λn1. Vint sz2 (\snd (split … (multiplication ? n1 n2))))
     216                    (λn1. Vint sz2 (\snd (vsplit … (multiplication ? n1 n2))))
    217217                    Vundef
    218218    | _ ⇒ Vundef ]
Note: See TracChangeset for help on using the changeset viewer.