diff options
Diffstat (limited to 'backends/lean/Base/Primitives/Scalar.lean')
| -rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 169 |
1 files changed, 143 insertions, 26 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index fecb0d1d..f74fecd4 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -230,6 +230,20 @@ def Scalar.cMax (ty : ScalarTy) : Int := | .Usize => Scalar.max .U32 | _ => Scalar.max ty +theorem Scalar.min_lt_max (ty : ScalarTy) : Scalar.min ty < Scalar.max ty := by + cases ty <;> simp [Scalar.min, Scalar.max] + . simp [Isize.min, Isize.max] + have h1 := Isize.refined_min.property + have h2 := Isize.refined_max.property + cases h1 <;> cases h2 <;> simp [*] + . simp [Usize.max] + have h := Usize.refined_max.property + cases h <;> simp [*] + +theorem Scalar.min_le_max (ty : ScalarTy) : Scalar.min ty ≤ Scalar.max ty := by + have := Scalar.min_lt_max ty + int_tac + theorem Scalar.cMin_bound ty : Scalar.min ty ≤ Scalar.cMin ty := by cases ty <;> simp [Scalar.min, Scalar.max, Scalar.cMin, Scalar.cMax] at * have h := Isize.refined_min.property @@ -372,10 +386,28 @@ def Scalar.sub {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar def Scalar.mul {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) := Scalar.tryMk ty (x.val * y.val) --- TODO: instances of +, -, * etc. for scalars +-- TODO: shift left +def Scalar.shiftl {ty0 ty1 : ScalarTy} (x : Scalar ty0) (y : Scalar ty1) : Result (Scalar ty0) := + sorry + +-- TODO: shift right +def Scalar.shiftr {ty0 ty1 : ScalarTy} (x : Scalar ty0) (y : Scalar ty1) : Result (Scalar ty0) := + sorry + +-- TODO: xor +def Scalar.xor {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Scalar ty := + sorry + +-- TODO: and +def Scalar.and {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Scalar ty := + sorry + +-- TODO: or +def Scalar.or {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Scalar ty := + sorry -- Cast an integer from a [src_ty] to a [tgt_ty] --- TODO: check the semantics of casts in Rust +-- TODO: double-check the semantics of casts in Rust def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Result (Scalar tgt_ty) := Scalar.tryMk tgt_ty x.val @@ -398,6 +430,34 @@ def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Re instance (ty : ScalarTy) : Inhabited (Scalar ty) := by constructor; cases ty <;> apply (Scalar.ofInt 0) +-- TODO: reducible? +@[reducible] def core_isize_min : Isize := Scalar.ofInt Isize.min (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize)) +@[reducible] def core_isize_max : Isize := Scalar.ofInt Isize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize)) +@[reducible] def core_i8_min : I8 := Scalar.ofInt I8.min +@[reducible] def core_i8_max : I8 := Scalar.ofInt I8.max +@[reducible] def core_i16_min : I16 := Scalar.ofInt I16.min +@[reducible] def core_i16_max : I16 := Scalar.ofInt I16.max +@[reducible] def core_i32_min : I32 := Scalar.ofInt I32.min +@[reducible] def core_i32_max : I32 := Scalar.ofInt I32.max +@[reducible] def core_i64_min : I64 := Scalar.ofInt I64.min +@[reducible] def core_i64_max : I64 := Scalar.ofInt I64.max +@[reducible] def core_i128_min : I128 := Scalar.ofInt I128.min +@[reducible] def core_i128_max : I128 := Scalar.ofInt I128.max + +-- TODO: reducible? +@[reducible] def core_usize_min : Usize := Scalar.ofInt Usize.min +@[reducible] def core_usize_max : Usize := Scalar.ofInt Usize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Usize)) +@[reducible] def core_u8_min : U8 := Scalar.ofInt U8.min +@[reducible] def core_u8_max : U8 := Scalar.ofInt U8.max +@[reducible] def core_u16_min : U16 := Scalar.ofInt U16.min +@[reducible] def core_u16_max : U16 := Scalar.ofInt U16.max +@[reducible] def core_u32_min : U32 := Scalar.ofInt U32.min +@[reducible] def core_u32_max : U32 := Scalar.ofInt U32.max +@[reducible] def core_u64_min : U64 := Scalar.ofInt U64.min +@[reducible] def core_u64_max : U64 := Scalar.ofInt U64.max +@[reducible] def core_u128_min : U128 := Scalar.ofInt U128.min +@[reducible] def core_u128_max : U128 := Scalar.ofInt U128.max + -- TODO: below: not sure this is the best way. -- Should we rather overload operations like +, -, etc.? -- Also, it is possible to automate the generation of those definitions @@ -447,6 +507,26 @@ instance {ty} : HDiv (Scalar ty) (Scalar ty) (Result (Scalar ty)) where instance {ty} : HMod (Scalar ty) (Scalar ty) (Result (Scalar ty)) where hMod x y := Scalar.rem x y +-- Shift left +instance {ty0 ty1} : HShiftLeft (Scalar ty0) (Scalar ty1) (Result (Scalar ty0)) where + hShiftLeft x y := Scalar.shiftl x y + +-- Shift right +instance {ty0 ty1} : HShiftRight (Scalar ty0) (Scalar ty1) (Result (Scalar ty0)) where + hShiftRight x y := Scalar.shiftr x y + +-- Xor +instance {ty} : HXor (Scalar ty) (Scalar ty) (Scalar ty) where + hXor x y := Scalar.xor x y + +-- Or +instance {ty} : HOr (Scalar ty) (Scalar ty) (Scalar ty) where + hOr x y := Scalar.or x y + +-- And +instance {ty} : HAnd (Scalar ty) (Scalar ty) (Scalar ty) where + hAnd x y := Scalar.and x y + -- Generic theorem - shouldn't be used much @[cpspec] theorem Scalar.add_spec {ty} {x y : Scalar ty} @@ -864,33 +944,33 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S -- ofIntCore -- TODO: typeclass? -@[reducible] def Isize.ofIntCore := @Scalar.ofIntCore .Isize -@[reducible] def I8.ofIntCore := @Scalar.ofIntCore .I8 -@[reducible] def I16.ofIntCore := @Scalar.ofIntCore .I16 -@[reducible] def I32.ofIntCore := @Scalar.ofIntCore .I32 -@[reducible] def I64.ofIntCore := @Scalar.ofIntCore .I64 -@[reducible] def I128.ofIntCore := @Scalar.ofIntCore .I128 -@[reducible] def Usize.ofIntCore := @Scalar.ofIntCore .Usize -@[reducible] def U8.ofIntCore := @Scalar.ofIntCore .U8 -@[reducible] def U16.ofIntCore := @Scalar.ofIntCore .U16 -@[reducible] def U32.ofIntCore := @Scalar.ofIntCore .U32 -@[reducible] def U64.ofIntCore := @Scalar.ofIntCore .U64 -@[reducible] def U128.ofIntCore := @Scalar.ofIntCore .U128 +def Isize.ofIntCore := @Scalar.ofIntCore .Isize +def I8.ofIntCore := @Scalar.ofIntCore .I8 +def I16.ofIntCore := @Scalar.ofIntCore .I16 +def I32.ofIntCore := @Scalar.ofIntCore .I32 +def I64.ofIntCore := @Scalar.ofIntCore .I64 +def I128.ofIntCore := @Scalar.ofIntCore .I128 +def Usize.ofIntCore := @Scalar.ofIntCore .Usize +def U8.ofIntCore := @Scalar.ofIntCore .U8 +def U16.ofIntCore := @Scalar.ofIntCore .U16 +def U32.ofIntCore := @Scalar.ofIntCore .U32 +def U64.ofIntCore := @Scalar.ofIntCore .U64 +def U128.ofIntCore := @Scalar.ofIntCore .U128 -- ofInt -- TODO: typeclass? -@[reducible] def Isize.ofInt := @Scalar.ofInt .Isize -@[reducible] def I8.ofInt := @Scalar.ofInt .I8 -@[reducible] def I16.ofInt := @Scalar.ofInt .I16 -@[reducible] def I32.ofInt := @Scalar.ofInt .I32 -@[reducible] def I64.ofInt := @Scalar.ofInt .I64 -@[reducible] def I128.ofInt := @Scalar.ofInt .I128 -@[reducible] def Usize.ofInt := @Scalar.ofInt .Usize -@[reducible] def U8.ofInt := @Scalar.ofInt .U8 -@[reducible] def U16.ofInt := @Scalar.ofInt .U16 -@[reducible] def U32.ofInt := @Scalar.ofInt .U32 -@[reducible] def U64.ofInt := @Scalar.ofInt .U64 -@[reducible] def U128.ofInt := @Scalar.ofInt .U128 +abbrev Isize.ofInt := @Scalar.ofInt .Isize +abbrev I8.ofInt := @Scalar.ofInt .I8 +abbrev I16.ofInt := @Scalar.ofInt .I16 +abbrev I32.ofInt := @Scalar.ofInt .I32 +abbrev I64.ofInt := @Scalar.ofInt .I64 +abbrev I128.ofInt := @Scalar.ofInt .I128 +abbrev Usize.ofInt := @Scalar.ofInt .Usize +abbrev U8.ofInt := @Scalar.ofInt .U8 +abbrev U16.ofInt := @Scalar.ofInt .U16 +abbrev U32.ofInt := @Scalar.ofInt .U32 +abbrev U64.ofInt := @Scalar.ofInt .U64 +abbrev U128.ofInt := @Scalar.ofInt .U128 postfix:max "#isize" => Isize.ofInt postfix:max "#i8" => I8.ofInt @@ -908,9 +988,46 @@ postfix:max "#u128" => U128.ofInt -- Testing the notations example : Result Usize := 0#usize + 1#usize +-- TODO: factor those lemmas out @[simp] theorem Scalar.ofInt_val_eq {ty} (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : (Scalar.ofInt x h).val = x := by simp [Scalar.ofInt, Scalar.ofIntCore] +@[simp] theorem Isize.ofInt_val_eq (h : Scalar.min ScalarTy.Isize ≤ x ∧ x ≤ Scalar.max ScalarTy.Isize) : (Isize.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem I8.ofInt_val_eq (h : Scalar.min ScalarTy.I8 ≤ x ∧ x ≤ Scalar.max ScalarTy.I8) : (I8.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem I16.ofInt_val_eq (h : Scalar.min ScalarTy.I16 ≤ x ∧ x ≤ Scalar.max ScalarTy.I16) : (I16.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem I32.ofInt_val_eq (h : Scalar.min ScalarTy.I32 ≤ x ∧ x ≤ Scalar.max ScalarTy.I32) : (I32.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem I64.ofInt_val_eq (h : Scalar.min ScalarTy.I64 ≤ x ∧ x ≤ Scalar.max ScalarTy.I64) : (I64.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem I128.ofInt_val_eq (h : Scalar.min ScalarTy.I128 ≤ x ∧ x ≤ Scalar.max ScalarTy.I128) : (I128.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem Usize.ofInt_val_eq (h : Scalar.min ScalarTy.Usize ≤ x ∧ x ≤ Scalar.max ScalarTy.Usize) : (Usize.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem U8.ofInt_val_eq (h : Scalar.min ScalarTy.U8 ≤ x ∧ x ≤ Scalar.max ScalarTy.U8) : (U8.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem U16.ofInt_val_eq (h : Scalar.min ScalarTy.U16 ≤ x ∧ x ≤ Scalar.max ScalarTy.U16) : (U16.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem U32.ofInt_val_eq (h : Scalar.min ScalarTy.U32 ≤ x ∧ x ≤ Scalar.max ScalarTy.U32) : (U32.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem U64.ofInt_val_eq (h : Scalar.min ScalarTy.U64 ≤ x ∧ x ≤ Scalar.max ScalarTy.U64) : (U64.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + +@[simp] theorem U128.ofInt_val_eq (h : Scalar.min ScalarTy.U128 ≤ x ∧ x ≤ Scalar.max ScalarTy.U128) : (U128.ofInt x h).val = x := by + apply Scalar.ofInt_val_eq h + -- Comparisons instance {ty} : LT (Scalar ty) where lt a b := LT.lt a.val b.val |