diff options
| author | Jonathan Protzenko | 2023-10-22 16:34:46 -0700 |
|---|---|---|
| committer | Jonathan Protzenko | 2023-10-22 16:34:46 -0700 |
| commit | c27c3052ec3f9a093b06a41f56b3a361cb65e950 (patch) | |
| tree | 200c96364b0fb9ea05f7ac3877ce496c1b6a285e /backends/fstar | |
| parent | 61368028027a7c160c33b05ec605c26833212667 (diff) | |
Add more support for numeric operations, xor, rotate
Diffstat (limited to 'backends/fstar')
| -rw-r--r-- | backends/fstar/Primitives.fst | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst index e9391834..7d0845ed 100644 --- a/backends/fstar/Primitives.fst +++ b/backends/fstar/Primitives.fst @@ -100,6 +100,11 @@ type scalar_ty = | U64 | U128 +let is_unsigned = function +| Isize | I8 | I16 | I32 | I64 | I128 -> false +| Usize | U8 | U16 | U32 | U64 | U128 -> true + + let scalar_min (ty : scalar_ty) : int = match ty with | Isize -> isize_min @@ -162,6 +167,15 @@ let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = mk_scalar ty (x * y) +let scalar_lxor (#ty : scalar_ty { is_unsigned ty && ty <> Usize }) + (x : scalar ty) (y : scalar ty) : scalar ty = + match ty with + | U8 -> FStar.UInt.logxor #8 x y + | U16 -> FStar.UInt.logxor #16 x y + | U32 -> FStar.UInt.logxor #32 x y + | U64 -> FStar.UInt.logxor #64 x y + | U128 -> FStar.UInt.logxor #128 x y + (** Cast an integer from a [src_ty] to a [tgt_ty] *) // TODO: check the semantics of casts in Rust let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = @@ -258,7 +272,7 @@ let u32_add = scalar_add #U32 let u64_add = scalar_add #U64 let u128_add = scalar_add #U128 -/// Substraction +/// Subtraction let isize_sub = scalar_sub #Isize let i8_sub = scalar_sub #I8 let i16_sub = scalar_sub #I16 @@ -286,6 +300,13 @@ let u32_mul = scalar_mul #U32 let u64_mul = scalar_mul #U64 let u128_mul = scalar_mul #U128 +/// Logical operators, defined for unsigned types only, so far +let u8_xor = scalar_lxor #U8 +let u16_xor = scalar_lxor #U16 +let u32_xor = scalar_lxor #U32 +let u64_xor = scalar_lxor #U64 +let u128_xor = scalar_lxor #U128 + (*** Range *) type range (a : Type0) = { start : a; |