Changeset 2275 for src/common


Ignore:
Timestamp:
Jul 30, 2012, 1:05:55 PM (7 years ago)
Author:
tranquil
Message:
  • moved around some code (I8051.ma does not depend on ByteValues?.ma anymore, rather the other way around)
  • proposed reimplementation of beval with pointer arithmetics and stuff
Location:
src/common
Files:
1 edited
1 copied

Legend:

Unmodified
Added
Removed
  • src/common/ByteValues.ma

    r2176 r2275  
    44
    55include "common/Pointers.ma".
     6include "ASM/I8051.ma".
     7include "ASM/BitVectorTrie.ma".
    68
    79record part (*r: region*): Type[0] ≝
     
    7476  [ O ⇒ λ_.[]
    7577  | S m ⇒ λpr':n=S m.(BVptr p (mk_part … part …))::bevals_of_pointer_aux p (S part) m ?] (refl ? n).
    76 /3/ (*Andrea: by _ cannot be re-parsed*) qed.
     78<pr >pr' <plus_n_Sm_fast
     79// qed.
    7780
    7881definition bevals_of_pointer: pointer → list beval ≝
     
    164167definition BVfalse: beval ≝ BVByte (zero …).
    165168definition beval_of_bool : bool → beval ≝ λb. if b then BVtrue else BVfalse.
     169
     170definition hw_register_env ≝ BitVectorTrie beval 6.
     171definition empty_hw_register_env: hw_register_env ≝ Stub ….
     172definition hwreg_retrieve: hw_register_env → Register → beval ≝
     173 λenv,r. lookup … (bitvector_of_register r) env BVundef.
     174definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
     175 λr,v,env. insert … (bitvector_of_register r) v env.
  • src/common/ByteValues_paolo.ma

    r2233 r2275  
    44
    55include "common/Pointers.ma".
     6include "ASM/I8051.ma".
     7include "ASM/BitVectorTrie.ma".
    68
    79record part (*r: region*): Type[0] ≝
     
    2426inductive beval: Type[0] ≝
    2527  | BVundef: beval
     28  | BVnonzero: beval
    2629  | BVByte: Byte → beval
    2730  | BVnull: (*∀r:region.*) part  → beval
    28   | BVptr: ∀p:pointer. part (*ptype p*) → beval.
     31  | BVptr: block → ∀p:part.Vector Byte (S p) → beval.
     32
     33include "utilities/hide.ma".
    2934
    3035definition eq_beval: beval → beval → bool ≝
     
    3237  match v1 with
    3338   [ BVundef      ⇒ match v2 with [ BVundef      ⇒ true                           | _ ⇒ false ]
     39   | BVnonzero    ⇒ match v2 with [ BVnonzero    ⇒ true                           | _ ⇒ false ]
    3440   | BVByte b1    ⇒ match v2 with [ BVByte b2    ⇒ eq_bv … b1 b2                  | _ ⇒ false ]
    3541   | BVnull p1    ⇒ match v2 with [ BVnull p2    ⇒ eqb p1 p2                      | _ ⇒ false ]
    36    | BVptr P1 p1  ⇒ match v2 with [ BVptr P2 p2  ⇒ eq_pointer … P1 P2 ∧ eqb p1 p2 | _ ⇒ false ]].
    37 
    38 axiom CorruptedValue: String.
    39 
    40 let rec pointer_of_bevals_aux (p:pointer) (part: nat) (l: list beval) on l : res pointer ≝
     42   | BVptr b1 p1 o1  ⇒
     43      match v2 with
     44      [ BVptr b2 p2 o2  ⇒
     45        eq_block … b1 b2 ∧ eqb p1 p2 ∧
     46          (* equivalent to equality if p1 = p2 *)
     47          subvector_with … (eq_bv 8) o1 o2
     48      | _ ⇒ false
     49      ]
     50   ].
     51
     52include alias "arithmetics/nat.ma".
     53
     54lemma commutative_plus_fast : commutative ? plus.
     55#n elim n [ @plus_n_O ]
     56#n' #IH #m <plus_n_Sm_fast <IH %
     57qed.
     58
     59lemma distributive_times_plus_fast : distributive ? times plus.
     60#n elim n [ #m #p % ]
     61#n' #IH #m #p normalize
     62>IH
     63>associative_plus in ⊢ (???%);
     64<(associative_plus ? p) in ⊢ (???%);
     65>(commutative_plus_fast ? p) in ⊢ (???%);
     66>(associative_plus p)
     67@associative_plus
     68qed.
     69
     70axiom CorruptedPointer: String.
     71
     72let rec vflatten A n m (v : Vector (Vector A m) n) on v : Vector A (n * m) ≝
     73match v return λn.λ_ : Vector ? n.Vector ? (n * m) with
     74[ VEmpty ⇒ VEmpty ?
     75| VCons n' hd tl ⇒ hd @@ vflatten ? n' m tl
     76].
     77
     78lemma times_n_Sm_fast : ∀n,m.n + n * m = n * S m.
     79#n elim n -n
     80[ #m % ]
     81#n #IH #m normalize <IH
     82<associative_plus >(commutative_plus_fast n)
     83>associative_plus >IH %
     84qed.
     85
     86lemma commutative_times_fast : commutative ? times.
     87#n elim n -n
     88[ #m <times_n_O % ]
     89#n #IH #m normalize <times_n_Sm_fast >IH %
     90qed.
     91
     92let rec pointer_of_bevals_aux (b:block) (part: nat) (acc : BitVector (part*8))
     93  (l: list beval) on l : res pointer ≝
    4194 match l with
    4295  [ nil ⇒
    43      if eqb part (size_pointer (*ptype p*)) then
    44       OK … p
     96     If eqb part (size_pointer (*ptype p*)) then with prf do
     97      return mk_pointer b (mk_offset (acc⌈BitVector (part*8)↦?⌉))
    4598     else
    46       Error … [MSG CorruptedValue]
     99      Error … [MSG CorruptedPointer]
    47100  | cons v tl ⇒
    48101     match v with
    49       [ BVptr p' part' ⇒
    50          if eq_pointer p p' ∧ eqb part part' then
    51           pointer_of_bevals_aux p (S part) tl
     102      [ BVptr b' part' o' ⇒
     103        let acc' ≝ vflatten … o' in
     104        if eq_block b b' ∧
     105           eqb part part' ∧
     106           subvector_with ??? eq_b acc acc' then
     107           pointer_of_bevals_aux b (S part') acc' tl
    52108         else
    53           Error … [MSG CorruptedValue]
    54       | _ ⇒ Error … [MSG CorruptedValue]]].
    55 
    56 axiom NotAPointer: String.
     109          Error … [MSG CorruptedPointer]
     110      | _ ⇒ Error … [MSG CorruptedPointer]
     111      ]
     112  ].
     113  @hide_prf
     114  >commutative_times_fast
     115  lapply prf @(eqb_elim part) #H * >H % qed.
    57116
    58117(* CSC: use vectors in place of lists? Or even better products of tuples
     
    61120 λl.
    62121 match l with
    63   [ nil ⇒ Error … [MSG NotAPointer]
     122  [ nil ⇒ Error … [MSG CorruptedPointer]
    64123  | cons he tl ⇒
    65124     match he with
    66       [ BVptr p part ⇒
    67          if eqb part 0 then pointer_of_bevals_aux p 1 tl else Error … [MSG NotAPointer]
    68       | _ ⇒ Error … [MSG NotAPointer]]].
    69 
     125      [ BVptr b part o ⇒
     126         if eqb part 0 then
     127           pointer_of_bevals_aux b (S part) (vflatten … o) tl
     128         else Error … [MSG CorruptedPointer]
     129      | _ ⇒ Error … [MSG CorruptedPointer]
     130      ]
     131  ].
     132
     133let rec rvsplit A n m on n : Vector A (n * m) → Vector (Vector A m) n ≝
     134match n return λn.Vector ? (n * m) → Vector (Vector ? m) n with
     135[ O ⇒ λ_.VEmpty ?
     136| S k ⇒
     137  λv.let 〈pre,post〉 ≝ vsplit … m (k*m) v in
     138  pre ::: rvsplit … post
     139].
    70140(* CSC: use vectors in place of lists? Or even better products of tuples
    71141   (more easily pattern matchable in the finite case)? *)
    72 let rec bevals_of_pointer_aux (p:pointer) (part: nat) (n: nat) (pr: plus part n = size_pointer (*ptype p*)) on n: list beval ≝
     142let rec bevals_of_pointer_aux (p:pointer) (part: nat) (n: nat) on n: n + part = size_pointer (*ptype p*) → list beval ≝
    73143 match n with
    74144  [ O ⇒ λ_.[]
    75   | S m ⇒ λpr':n=S m.(BVptr p (mk_part … part …))::bevals_of_pointer_aux p (S part) m ?] (refl ? n).
    76 /3/ (*Andrea: by _ cannot be re-parsed*) qed.
     145  | S m ⇒ λpr': S m + part = ?.
     146    let postfix ≝ rvsplit … (\snd (vsplit bool (m*8) (S part*8) (offv (poff p) ⌈BitVector ?↦?⌉))) in
     147    (BVptr (pblock p) (mk_part … part …) postfix)::bevals_of_pointer_aux p (S part) m ?
     148  ].
     149@hide_prf
     150[3: change with (?*?) in match offset_size;
     151  <pr' >(commutative_times_fast ? 8) >(commutative_times_fast ? 8)
     152  <distributive_times_plus_fast <plus_n_Sm_fast %
     153] -postfix
     154/3 by lt_plus_to_minus_r, lt_plus_to_lt_l/ qed.
    77155
    78156definition bevals_of_pointer: pointer → list beval ≝
    79157 λp. bevals_of_pointer_aux p 0 (size_pointer (*ptype p*)) ….
    80 // qed.
     158@hide_prf @plus_n_O qed.
     159
     160lemma vflatten_rvsplit : ∀A,n,m,v.vflatten A n m (rvsplit A n m v) = v.
     161#A #n elim n -n
     162[ #m #v >(Vector_O ? v) %
     163| #n #IH #m #v
     164  whd in match (rvsplit ????);
     165  @vsplit_elim #pre #post #EQ
     166  normalize nodelta
     167  whd in match (vflatten ????); >IH >EQ %
     168]
     169qed.
     170
     171lemma v_invert_append : ∀A,n,m.∀v,v' : Vector A n.∀u,u' : Vector A m.
     172  v @@ u = v' @@ u' → v = v' ∧ u = u'.
     173#A #n #m #v elim v -n
     174[ #v' >(Vector_O ? v') #u #u' normalize #EQ %{EQ} %
     175| #n #hd #tl #IH #v' elim (Vector_Sn ?? v') #hd' * #tl' #EQv' >EQv' -v'
     176  #u #u' normalize #EQ destruct(EQ) elim (IH … e0) #EQ' #EQ'' %{EQ''}
     177  >EQ' %
     178]
     179qed.
     180
     181lemma rvsplit_vflatten : ∀A,n,m,v.rvsplit A n m (vflatten A n m v) = v.
     182#A #n #m #v elim v -n
     183[ %
     184| #n #hd #tl #IH
     185  whd in match (vflatten ????);
     186  whd in match (rvsplit ????);
     187  @vsplit_elim #pre #post #EQ
     188  elim (v_invert_append … EQ) #EQ1 #EQ2 <EQ1 <EQ2
     189  normalize nodelta >IH %
     190]
     191qed.
     192
    81193
    82194lemma pointer_of_bevals_bevals_of_pointer:
    83195 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p.
    84 * #pbl #poff
    85 try %
    86 whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 1) (*[2,3: %]*)
    87 whd in ⊢ (??%?);(* >reflexive_eq_pointer >(eqb_n_n 2)*) %
     196* #pbl * #voff
     197whd in match (bevals_of_pointer ?);
     198@vsplit_elim #pre #post
     199normalize nodelta
     200#EQ >EQ
     201whd in match (bevals_of_pointer_aux ????);
     202@vsplit_elim #pre' #post'
     203normalize nodelta
     204>(Vector_O … pre') #EQ' normalize in EQ'; <EQ' -pre' -post'
     205whd in ⊢ (??%?);
     206>eq_block_b_b >eqb_n_n
     207>vflatten_rvsplit >vflatten_rvsplit
     208>(subvector_with_refl0 … post ? pre) [2: * %]
     209normalize nodelta %
    88210qed.
    89211
     
    134256 λv.match v with
    135257  [ BVundef ⇒ Error … [MSG ValueNotABoolean]
     258  | BVnonzero ⇒ OK … true
    136259  | BVByte b ⇒ OK … (eq_bv … (zero …) b)
    137260  | BVnull y ⇒  OK … false
    138   | BVptr p q ⇒ OK ? true ].
    139 
    140 axiom BadByte: String.
    141 
    142 definition Byte_of_val: beval → res Byte ≝ (*CSC: move elsewhere *)
    143  λb.match b with
     261  | BVptr p q o ⇒ OK ? true ].
     262
     263definition Byte_of_val: String → beval → res Byte ≝ (*CSC: move elsewhere *)
     264 λerr,b.match b with
    144265  [ BVByte b ⇒ OK … b
    145   | _ ⇒ Error … [MSG BadByte]].
     266  | _ ⇒ Error … [MSG err]].
    146267
    147268axiom NotAnInt32Val: String.
     
    151272   match l with
    152273    [ nil ⇒ Error ? [MSG NotAnInt32Val]
    153     | cons hd tl ⇒ do b ← Byte_of_val hd ; OK ? 〈b,tl〉 ] in
     274    | cons hd tl ⇒ do b ← Byte_of_val NotAnInt32Val hd ; OK ? 〈b,tl〉 ] in
    154275  do 〈b1,l〉 ← first_byte l ;
    155276  do 〈b2,l〉 ← first_byte l ;
     
    160281    | _ ⇒ Error ? [MSG NotAnInt32Val] ].
    161282
    162 (* CSC: maybe we should introduce a type of 1-bit-sized values *)
    163 definition BVtrue: beval ≝ BVByte [[false;false;false;false;false;false;false;true]].
    164 definition BVfalse: beval ≝ BVByte (zero …).
    165 definition beval_of_bool : bool → beval ≝ λb. if b then BVtrue else BVfalse.
     283inductive bebit : Type[0] ≝
     284| BBbit : bool → bebit
     285| BBundef : bebit
     286| BBptrcarry :
     287  (* is add *) bool → block → ∀p : part.Vector Byte (S p) → Vector Byte (S p) → bebit.
     288
     289definition eq_bebit: bebit → bebit → bool ≝
     290 λv1,v2.
     291  match v1 with
     292   [ BBundef      ⇒ match v2 with [ BBundef      ⇒ true                           | _ ⇒ false ]
     293   | BBbit b1    ⇒ match v2 with [ BBbit b2    ⇒ eq_b b1 b2                  | _ ⇒ false ]
     294   | BBptrcarry is_add1 b1 p1 o1 by1  ⇒
     295      match v2 with
     296      [ BBptrcarry is_add2 b2 p2 o2 by2  ⇒
     297        eq_b is_add1 is_add2 ∧ eq_block … b1 b2 ∧ eqb p1 p2 ∧
     298          (* equivalent to equality if p1 = p2 *)
     299          subvector_with … (eq_bv 8) o1 o2 ∧
     300          subvector_with … (eq_bv 8) by1 by2
     301      | _ ⇒ false
     302      ]
     303   ].
     304
     305axiom UnsupportedOp : String.
     306
     307definition be_opaccs : OpAccs → beval → beval → res (beval × beval) ≝
     308  λop,a,b.
     309  ! a' ← Byte_of_val UnsupportedOp a ;
     310  ! b' ← Byte_of_val UnsupportedOp b ;
     311  let 〈a'',b''〉 ≝ opaccs eval op a' b' in
     312  return 〈BVByte a'', BVByte b''〉.
     313
     314definition be_op1 : Op1 → beval → res beval ≝
     315  λop,a.
     316  ! a' ← Byte_of_val UnsupportedOp a ;
     317  return BVByte (op1 eval op a').
     318
     319definition Bit_of_val: String → bebit → res Bit ≝ (*CSC: move elsewhere *)
     320 λerr,b.match b with
     321  [ BBbit b ⇒ OK … b
     322  | _ ⇒ Error … [MSG err]].
     323
     324definition op2_bytes : Op2 → ∀n.Bit → Vector Byte n → Vector Byte n → (Vector Byte n) × Bit ≝
     325λop,n,carry.
     326  let f ≝ λn,b1,b2.λpr : (Vector Byte n) × Bit.
     327    let 〈res_tl, carry〉 ≝ pr in
     328    let 〈res_hd,carry'〉 ≝ op2 eval carry op b1 b2 in
     329    〈res_hd ::: res_tl, carry'〉 in
     330  fold_right2_i … f 〈[[ ]],carry〉 n.
     331
     332definition be_add_sub_byte : bool → bebit → beval → Byte → res (beval × bebit) ≝
     333  λis_add,carry,a1,b2.
     334  let op ≝ if is_add then Addc else Sub in
     335  match a1 with
     336  [ BVByte b1 ⇒
     337    ! carry' ← Bit_of_val UnsupportedOp carry ;
     338    let 〈rslt, carry''〉 ≝ op2 eval carry' op b1 b2 in
     339    return 〈BVByte rslt, BBbit carry''〉
     340  | BVptr b p o ⇒
     341    match p with
     342    [ O ⇒ λ_:0<size_pointer.λo : Vector Byte 1.
     343      if eq_bebit carry (BBbit false) then
     344        let o' ≝ from_singl … o in
     345        let 〈rslt,carry〉 ≝ op2 eval false op b2 o' in
     346        let p' : part ≝ mk_part 0 ? in
     347        return 〈BVptr b p' [[rslt]], BBptrcarry is_add b p' o [[b2]]〉
     348      else
     349        Error … [MSG UnsupportedOp]
     350    | S k ⇒ λSk_ok:S k<size_pointer.λo : Vector Byte (S (S k)).
     351      match carry with
     352      [ BBptrcarry is_add' b' p' o' by' ⇒
     353        if eq_b is_add is_add' ∧ eq_block b b' ∧ subvector_with … (eq_bv 8) o' o then
     354          If eqb k p' then with prf do
     355            let by' ≝ by' ⌈Vector ?? ↦ Vector Byte (S k)⌉ in
     356            let 〈rslt,ignore〉 ≝ op2_bytes op … false o (b2 ::: by') in
     357            let Sk_part ≝ mk_part (S k) Sk_ok in
     358            OK … 〈BVptr b Sk_part rslt,
     359                     BBptrcarry is_add b Sk_part o (b2 ::: by')〉
     360          else Error … [MSG UnsupportedOp]
     361        else Error … [MSG UnsupportedOp]
     362      | _ ⇒ Error … [MSG UnsupportedOp]
     363      ]
     364    ] (part_no_ok p) o
     365  | _ ⇒ Error … [MSG UnsupportedOp]
     366  ].
     367@hide_prf [//]
     368lapply prf @eqb_elim #H * >H %
     369qed.
     370
     371(* This tables shows what binary ops may be defined on bevals depending on
     372   the arguments (columns marked by 1st argument, rows by 2nd). Further
     373   checks for definedness are done for pointer parts taking into account
     374   blocks, parts and the carry value.
     375            | BVByte    | BVptr          | BVnull | BVnonzero | BVundef |
     376  ----------+-----------+----------------+--------+-----------+---------|
     377  BVByte    | all       | Add, Addc, Sub | none   | Or        | none    |
     378  ----------+-----------+----------------+--------+-----------+---------|
     379  BVptr     | Add, Addc | Sub, Xor       | Xor    | none      | none    |
     380  ----------+-----------+----------------+--------+-----------+---------|
     381  BVnull    | none      | Xor            | Xor    | none      | none    |
     382  ----------+-----------+----------------+--------+-----------+---------|
     383  BVnonzero | Or        | none           | none   | Or        | none    |
     384  ----------+-----------+----------------+--------+-----------+---------|
     385  BVundef   | none      | none           | none   | none      | none    |
     386  ----------------------------------------------------------------------+
     387*)
     388definition be_op2 : bebit → Op2 → beval → beval → res (beval × bebit) ≝
     389  λcarry,op,a1,a2.
     390  match a1 with
     391  [ BVByte b1 ⇒
     392    match a2 with
     393    [ BVByte b2 ⇒
     394      ! carry ← Bit_of_val UnsupportedOp carry ;
     395      let 〈result, carry〉 ≝ op2 eval carry op b1 b2 in
     396      return 〈BVByte result, BBbit carry〉
     397    | BVptr bl2 p2 o2 ⇒
     398      match op with
     399      [ Add ⇒ be_add_sub_byte true (BBbit false) a2 b1
     400      | Addc ⇒ be_add_sub_byte true carry a2 b1
     401      | _ ⇒ Error … [MSG UnsupportedOp]
     402      ]
     403    | BVnonzero ⇒
     404      match op with
     405      [ Or ⇒ return 〈BVnonzero, carry〉
     406      | _ ⇒ Error … [MSG UnsupportedOp]
     407      ]
     408    | _ ⇒ Error … [MSG UnsupportedOp]
     409    ]
     410  | BVptr bl1 p1 o1 ⇒
     411    match a2 with
     412    [ BVByte b2 ⇒
     413      match op with
     414      [ Add ⇒ be_add_sub_byte true (BBbit false) a1 b2
     415      | Addc ⇒ be_add_sub_byte true carry a1 b2
     416      | Sub ⇒ be_add_sub_byte false carry a1 b2
     417      | _ ⇒ Error … [MSG UnsupportedOp]
     418      ]
     419    | BVptr bl2 p2 o2 ⇒
     420      match op with
     421      [ Sub ⇒
     422        if eq_block bl1 bl2 ∧ eqb p1 p2 then
     423          ! carry ← Bit_of_val UnsupportedOp carry ;
     424          let by1 ≝ head' … o1 in
     425          let by2 ≝ head' … o2 in
     426          let 〈result, carry〉 ≝ op2 eval carry Sub by1 by2 in
     427          return 〈BVByte result, BBbit carry〉
     428        else Error … [MSG UnsupportedOp]
     429      | Xor ⇒
     430        if eq_block bl1 bl2 ∧ eqb p1 p2 then
     431          if subvector_with … (eq_bv 8) o1 o2 (* equivalent to equality *) then
     432            return 〈BVByte (bv_zero …), carry〉
     433          else
     434            return 〈BVnonzero, carry〉
     435        else Error … [MSG UnsupportedOp]
     436      | _ ⇒ Error … [MSG UnsupportedOp]
     437      ]
     438    | BVnull p2 ⇒
     439      match op with
     440      [ Xor ⇒
     441        if eqb p1 p2 then
     442          return 〈BVnonzero, carry〉
     443        else
     444          Error … [MSG UnsupportedOp]
     445      | _ ⇒ Error … [MSG UnsupportedOp]
     446      ]
     447    | _ ⇒ Error … [MSG UnsupportedOp]
     448    ]
     449  | BVnonzero ⇒
     450    match op with
     451    [ Or ⇒
     452      match a2 with
     453      [ BVByte _ ⇒ return 〈BVnonzero, carry〉
     454      | BVnonzero ⇒ return 〈BVnonzero, carry〉
     455      | _ ⇒ Error … [MSG UnsupportedOp]
     456      ]
     457    | _ ⇒ Error … [MSG UnsupportedOp]
     458    ]
     459  | BVnull p1 ⇒
     460    match op with
     461    [ Xor ⇒
     462      match a2 with
     463      [ BVptr _ p2 _ ⇒
     464        if eqb p1 p2 then
     465          return 〈BVnonzero, carry〉
     466        else
     467          Error … [MSG UnsupportedOp]
     468      | BVnull p2 ⇒
     469        if eqb p1 p2 then
     470          return 〈BVByte (bv_zero …), carry〉
     471        else
     472          Error … [MSG UnsupportedOp]
     473      | _ ⇒ Error … [MSG UnsupportedOp]
     474      ]
     475    | _ ⇒ Error … [MSG UnsupportedOp]
     476    ]
     477  | _ ⇒ Error … [MSG UnsupportedOp]
     478  ].
     479
     480record hw_register_env : Type[0] ≝
     481  { reg_env : BitVectorTrie beval 6
     482  ; carry_bit : bebit
     483  ; other_bit : bebit
     484  }.
     485
     486definition empty_hw_register_env: hw_register_env ≝
     487  mk_hw_register_env (Stub …) BBundef BBundef.
     488
     489definition hwreg_retrieve: hw_register_env → Register → beval ≝
     490 λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef.
     491
     492definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
     493 λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env))
     494  (carry_bit env) (other_bit env).
     495
     496definition hwreg_set_carry : bebit → hw_register_env → hw_register_env ≝
     497λv,env.mk_hw_register_env (reg_env env) v (other_bit env).
     498
     499definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
     500λv,env.mk_hw_register_env (reg_env env) (carry_bit env) v.
     501
     502
Note: See TracChangeset for help on using the changeset viewer.