| 1 | (* include "arithmetics/Z.ma". *) |
|---|
| 2 | include "arithmetics/exp.ma". |
|---|
| 3 | include "basics/list.ma". |
|---|
| 4 | include "common/AST.ma". |
|---|
| 5 | include "common/Order.ma". |
|---|
| 6 | |
|---|
| 7 | definition bvint ≝ λsize. BitVector (bitsize_of_intsize size). |
|---|
| 8 | |
|---|
| 9 | definition bitsize_of_intsize: intsize → nat ≝ |
|---|
| 10 | λsize. |
|---|
| 11 | S (match size with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31]). |
|---|
| 12 | |
|---|
| 13 | definition of_int ≝ |
|---|
| 14 | λsize. |
|---|
| 15 | λn. |
|---|
| 16 | bitvector_of_nat (bitsize_of_intsize size) n. |
|---|
| 17 | |
|---|
| 18 | axiom compare: ∀size: intsize. bvint size → bvint size → order. |
|---|
| 19 | axiom zero: ∀size: intsize. bvint size. |
|---|
| 20 | axiom one: ∀size: intsize. bvint size. |
|---|
| 21 | axiom to_signed_int_repr: ∀size: intsize. bvint size → bvint_int_repr. |
|---|
| 22 | axiom to_unsigned_int_repr: ∀size: intsize. bvint size → bvint_int_repr. |
|---|
| 23 | axiom succ: ∀size: intsize. bvint size → bvint size. |
|---|
| 24 | axiom pred: ∀size: intsize. bvint size → bvint size. |
|---|
| 25 | axiom add: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 26 | axiom add_of: ∀size: intsize. bvint size → bvint size → bool. |
|---|
| 27 | axiom sub: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 28 | axiom sub_uf: ∀size: intsize. bvint size → bvint size → bool. |
|---|
| 29 | axiom mul: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 30 | axiom div: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 31 | axiom divu: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 32 | axiom modulo: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 33 | axiom modulou: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 34 | axiom eq: ∀size: intsize. bvint size → bvint size → bool. |
|---|
| 35 | axiom neq: ∀size: intsize. bvint size → bvint size → bool. |
|---|
| 36 | axiom lt: ∀size: intsize. bvint size → bvint size → bool. |
|---|
| 37 | axiom ltu: ∀size: intsize. bvint size → bvint size → bool. |
|---|
| 38 | axiom le: ∀size: intsize. bvint size → bvint size → bool. |
|---|
| 39 | axiom leu: ∀size: intsize. bvint size → bvint size → bool. |
|---|
| 40 | axiom gt: ∀size: intsize. bvint size → bvint size → bool. |
|---|
| 41 | axiom gtu: ∀size: intsize. bvint size → bvint size → bool. |
|---|
| 42 | axiom ge: ∀size: intsize. bvint size → bvint size → bool. |
|---|
| 43 | axiom geu: ∀size: intsize. bvint size → bvint size → bool. |
|---|
| 44 | axiom neg: ∀size: intsize. bvint size → bvint size. |
|---|
| 45 | axiom lognot: ∀size: intsize. bvint size → bvint size. |
|---|
| 46 | axiom logand: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 47 | axiom logor: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 48 | axiom logxor: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 49 | axiom shl: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 50 | axiom shr: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 51 | axiom shrl: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 52 | axiom max: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 53 | axiom maxu: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 54 | axiom min: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 55 | axiom minu: ∀size: intsize. bvint size → bvint size → bvint size. |
|---|
| 56 | axiom cast: ∀size: intsize. bvint_int_repr → bvint size. |
|---|
| 57 | axiom to_int: ∀size: intsize. bvint size → nat. (*dpm: """" *) |
|---|
| 58 | axiom zero_ext: ∀size: intsize. nat → bvint size → bvint size. (* nat here correct *) |
|---|
| 59 | axiom sign_ext: ∀size: intsize. nat → bvint size → bvint size. (* nat here correct *) |
|---|
| 60 | axiom break: ∀size: intsize. bvint size → nat → list (bvint size). |
|---|
| 61 | axiom merge: ∀size: intsize. list (bvint size) → bvint size. |
|---|
