diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/coq/Primitives.v | 46 | ||||
| -rw-r--r-- | backends/fstar/Primitives.fst | 56 | ||||
| -rw-r--r-- | backends/lean/Base/Diverge/Base.lean | 102 | ||||
| -rw-r--r-- | backends/lean/Base/Diverge/Elab.lean | 50 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Alloc.lean | 4 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/ArraySlice.lean | 54 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Base.lean | 30 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 142 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Vec.lean | 26 | ||||
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 22 |
10 files changed, 265 insertions, 267 deletions
diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v index 990e27e4..e84d65ce 100644 --- a/backends/coq/Primitives.v +++ b/backends/coq/Primitives.v @@ -19,19 +19,19 @@ Inductive error := | OutOfFuel. Inductive result A := - | Return : A -> result A + | Ok : A -> result A | Fail_ : error -> result A. -Arguments Return {_} a. +Arguments Ok {_} a. Arguments Fail_ {_}. Definition bind {A B} (m: result A) (f: A -> result B) : result B := match m with | Fail_ e => Fail_ e - | Return x => f x + | Ok x => f x end. -Definition return_ {A: Type} (x: A) : result A := Return x. +Definition return_ {A: Type} (x: A) : result A := Ok x. Definition fail_ {A: Type} (e: error) : result A := Fail_ e. Notation "x <- c1 ; c2" := (bind c1 (fun x => c2)) @@ -39,27 +39,27 @@ Notation "x <- c1 ; c2" := (bind c1 (fun x => c2)) (** Monadic assert *) Definition massert (b: bool) : result unit := - if b then Return tt else Fail_ Failure. + if b then Ok tt else Fail_ Failure. (** Normalize and unwrap a successful result (used for globals) *) -Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A := - match a as r return (r = Return x -> A) with - | Return a' => fun _ => a' +Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A := + match a as r return (r = Ok x -> A) with + | Ok a' => fun _ => a' | Fail_ e => fun p' => False_rect _ (eq_ind (Fail_ e) (fun e : result A => match e with - | Return _ => False + | Ok _ => False | Fail_ e => True end) - I (Return x) p') + I (Ok x) p') end p. Notation "x %global" := (eval_result_refl x eq_refl) (at level 40). Notation "x %return" := (eval_result_refl x eq_refl) (at level 40). (* Sanity check *) -Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3. +Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3. (*** Misc *) @@ -236,7 +236,7 @@ Import Sumbool. Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) := match sumbool_of_bool (scalar_in_bounds ty x) with - | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H)) + | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H)) | right _ => Fail_ Failure end. @@ -544,9 +544,9 @@ Arguments core_ops_range_Range_end_ {_}. (*** [alloc] *) -Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x. +Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x. Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) := - Return (x, fun x => Return x). + Ok (x, fun x => Ok x). (* Trait instance *) Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {| @@ -589,7 +589,7 @@ Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usi result (T * (T -> result (array T n))) := match array_index_usize T n a i with | Fail_ e => Fail_ e - | Return x => Return (x, array_update_usize T n a i) + | Ok x => Ok (x, array_update_usize T n a i) end. (*** Slice *) @@ -603,7 +603,7 @@ Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) : result (T * (T -> result (slice T))) := match slice_index_usize T s i with | Fail_ e => Fail_ e - | Return x => Return (x, slice_update_usize T s i) + | Ok x => Ok (x, slice_update_usize T s i) end. (*** Subslices *) @@ -615,7 +615,7 @@ Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) : result (slice T * (slice T -> result (array T n))) := match array_to_slice T n a with | Fail_ e => Fail_ e - | Return x => Return (x, array_from_slice T n a) + | Ok x => Ok (x, array_from_slice T n a) end. Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T). @@ -657,17 +657,17 @@ end end. Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) := l <- f (alloc_vec_Vec_to_list v) ; match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with - | left H => Return (exist _ l (scalar_le_max_valid _ _ H)) + | left H => Ok (exist _ l (scalar_le_max_valid _ _ H)) | right _ => Fail_ Failure end. Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) := - alloc_vec_Vec_bind v (fun l => Return (l ++ [x])). + alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])). Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) := alloc_vec_Vec_bind v (fun l => if to_Z i <? Z.of_nat (length l) - then Return (list_update l (usize_to_nat i) x) + then Ok (list_update l (usize_to_nat i) x) else Fail_ Failure). (* Helper *) @@ -679,8 +679,8 @@ Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : Definition alloc_vec_Vec_index_mut_usize {T : Type} (v: alloc_vec_Vec T) (i: usize) : result (T * (T -> result (alloc_vec_Vec T))) := match alloc_vec_Vec_index_usize v i with - | Return x => - Return (x, alloc_vec_Vec_update_usize v i) + | Ok x => + Ok (x, alloc_vec_Vec_update_usize v i) | Fail_ e => Fail_ e end. @@ -717,7 +717,7 @@ Definition core_slice_index_Slice_index x <- inst.(core_slice_index_SliceIndex_get) i s; match x with | None => Fail_ Failure - | Some x => Return x + | Some x => Ok x end. (* [core::slice::index::Range:::get]: forward function *) diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst index fca80829..acdb09dc 100644 --- a/backends/fstar/Primitives.fst +++ b/backends/fstar/Primitives.fst @@ -23,11 +23,11 @@ type error : Type0 = | OutOfFuel type result (a : Type0) : Type0 = -| Return : v:a -> result a +| Ok : v:a -> result a | Fail : e:error -> result a // Monadic return operator -unfold let return (#a : Type0) (x : a) : result a = Return x +unfold let return (#a : Type0) (x : a) : result a = Ok x // Monadic bind operator. // Allows to use the notation: @@ -36,17 +36,17 @@ unfold let return (#a : Type0) (x : a) : result a = Return x // ... // ``` unfold let (let*) (#a #b : Type0) (m: result a) - (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) : + (f: (x:a) -> Pure (result b) (requires (m == Ok x)) (ensures fun _ -> True)) : result b = match m with - | Return x -> f x + | Ok x -> f x | Fail e -> Fail e // Monadic assert(...) -let massert (b:bool) : result unit = if b then Return () else Fail Failure +let massert (b:bool) : result unit = if b then Ok () else Fail Failure // Normalize and unwrap a successful result (used for globals). -let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x +let eval_global (#a : Type0) (x : result a{Ok? (normalize_term x)}) : a = Ok?.v x (*** Misc *) type char = FStar.Char.char @@ -144,7 +144,7 @@ let scalar_max (ty : scalar_ty) : int = type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty} let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) = - if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure + if scalar_min ty <= x && scalar_max ty >= x then Ok x else Fail Failure let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x) @@ -498,9 +498,9 @@ type core_ops_range_Range (a : Type0) = { (*** [alloc] *) -let alloc_boxed_Box_deref (t : Type0) (x : t) : result t = Return x +let alloc_boxed_Box_deref (t : Type0) (x : t) : result t = Ok x let alloc_boxed_Box_deref_mut (t : Type0) (x : t) : result (t & (t -> result t)) = - Return (x, (fun x -> Return x)) + Ok (x, (fun x -> Ok x)) // Trait instance let alloc_boxed_Box_coreopsDerefInst (self : Type0) : core_ops_deref_Deref self = { @@ -528,20 +528,20 @@ let mk_array (a : Type0) (n : usize) l let array_index_usize (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = - if i < length x then Return (index x i) + if i < length x then Ok (index x i) else Fail Failure let array_update_usize (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) = - if i < length x then Return (list_update x i nx) + if i < length x then Ok (list_update x i nx) else Fail Failure let array_index_mut_usize (a : Type0) (n : usize) (x : array a n) (i : usize) : result (a & (a -> result (array a n))) = match array_index_usize a n x i with | Fail e -> Fail e - | Return v -> - Return (v, array_update_usize a n x i) + | Ok v -> + Ok (v, array_update_usize a n x i) (*** Slice *) type slice (a : Type0) = s:list a{length s <= usize_max} @@ -549,30 +549,30 @@ type slice (a : Type0) = s:list a{length s <= usize_max} let slice_len (a : Type0) (s : slice a) : usize = length s let slice_index_usize (a : Type0) (x : slice a) (i : usize) : result a = - if i < length x then Return (index x i) + if i < length x then Ok (index x i) else Fail Failure let slice_update_usize (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) = - if i < length x then Return (list_update x i nx) + if i < length x then Ok (list_update x i nx) else Fail Failure let slice_index_mut_usize (a : Type0) (s : slice a) (i : usize) : result (a & (a -> result (slice a))) = match slice_index_usize a s i with | Fail e -> Fail e - | Return x -> - Return (x, slice_update_usize a s i) + | Ok x -> + Ok (x, slice_update_usize a s i) (*** Subslices *) -let array_to_slice (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice (a : Type0) (n : usize) (x : array a n) : result (slice a) = Ok x let array_from_slice (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) = - if length s = n then Return s + if length s = n then Ok s else Fail Failure let array_to_slice_mut (a : Type0) (n : usize) (x : array a n) : result (slice a & (slice a -> result (array a n))) = - Return (x, array_from_slice a n x) + Ok (x, array_from_slice a n x) // TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *) let array_subslice (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) : result (slice a) = @@ -598,16 +598,16 @@ let alloc_vec_Vec_len (a : Type0) (v : alloc_vec_Vec a) : usize = length v // Helper let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail Failure + if i < length v then Ok (index v i) else Fail Failure // Helper let alloc_vec_Vec_update_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) = - if i < length v then Return (list_update v i x) else Fail Failure + if i < length v then Ok (list_update v i x) else Fail Failure let alloc_vec_Vec_index_mut_usize (#a : Type0) (v: alloc_vec_Vec a) (i: usize) : result (a & (a → result (alloc_vec_Vec a))) = match alloc_vec_Vec_index_usize v i with - | Return x -> - Return (x, alloc_vec_Vec_update_usize v i) + | Ok x -> + Ok (x, alloc_vec_Vec_update_usize v i) | Fail e -> Fail e let alloc_vec_Vec_push (a : Type0) (v : alloc_vec_Vec a) (x : a) : @@ -616,17 +616,17 @@ let alloc_vec_Vec_push (a : Type0) (v : alloc_vec_Vec a) (x : a) : (ensures (fun res -> match res with | Fail e -> e == Failure - | Return v' -> length v' = length v + 1)) = + | Ok v' -> length v' = length v + 1)) = if length v < usize_max then begin (**) assert_norm(length [x] == 1); (**) append_length v [x]; (**) assert(length (append v [x]) = length v + 1); - Return (append v [x]) + Ok (append v [x]) end else Fail Failure let alloc_vec_Vec_insert (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) = - if i < length v then Return (list_update v i x) else Fail Failure + if i < length v then Ok (list_update v i x) else Fail Failure // Trait declaration: [core::slice::index::private_slice_index::Sealed] type core_slice_index_private_slice_index_Sealed (self : Type0) = unit @@ -650,7 +650,7 @@ let core_slice_index_Slice_index let* x = inst.get i s in match x with | None -> Fail Failure - | Some x -> Return x + | Some x -> Ok x // [core::slice::index::Range:::get]: forward function let core_slice_index_RangeUsize_get (t : Type0) (i : core_ops_range_Range usize) (s : slice t) : diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean index 7521eecc..0f20125f 100644 --- a/backends/lean/Base/Diverge/Base.lean +++ b/backends/lean/Base/Diverge/Base.lean @@ -167,7 +167,7 @@ namespace Fix match x1 with | div => True | fail _ => x2 = x1 - | ret _ => x2 = x1 -- TODO: generalize + | ok _ => x2 = x1 -- TODO: generalize -- Monotonicity relation over monadic arrows (i.e., Kleisli arrows) def karrow_rel (k1 k2 : (x:a) → Result (b x)) : Prop := @@ -386,7 +386,7 @@ namespace Fix have Hgeq := Hgmono Hffmono simp [result_rel] at Hgeq cases Heq: g (fix_fuel n k) <;> rename_i y <;> simp_all - -- Remains the .ret case + -- Remains the .ok case -- Use Hdiv to prove that: ∀ n, h y (fix_fuel n f) = div -- We do this in two steps: first we prove it for m ≥ n have Hhdiv: ∀ m, h y (fix_fuel m k) = .div := by @@ -507,7 +507,7 @@ namespace FixI specific case. Remark: the index designates the function in the mutually recursive group - (it should be a finite type). We make the return type depend on the input + (it should be a finite type). We make the output type depend on the input type because we group the type parameters in the input type. -/ open Primitives Fix @@ -943,7 +943,7 @@ namespace Ex1 match ls with | [] => .fail .panic | hd :: tl => - if i = 0 then .ret hd + if i = 0 then .ok hd else k (tl, i - 1) theorem list_nth_body_is_valid: ∀ k x, is_valid_p k (λ k => @list_nth_body a k x) := by @@ -960,7 +960,7 @@ namespace Ex1 match ls with | [] => .fail .panic | hd :: tl => - if i = 0 then .ret hd + if i = 0 then .ok hd else list_nth tl (i - 1) := by have Heq := is_valid_fix_fixed_eq (@list_nth_body_is_valid a) @@ -981,11 +981,11 @@ namespace Ex2 match ls with | [] => .fail .panic | hd :: tl => - if i = 0 then .ret hd + if i = 0 then .ok hd else do let y ← k (tl, i - 1) - .ret y + .ok y theorem list_nth_body_is_valid: ∀ k x, is_valid_p k (λ k => @list_nth_body a k x) := by intro k x @@ -1002,11 +1002,11 @@ namespace Ex2 match ls with | [] => .fail .panic | hd :: tl => - if i = 0 then .ret hd + if i = 0 then .ok hd else do let y ← list_nth tl (i - 1) - .ret y) + .ok y) := by have Heq := is_valid_fix_fixed_eq (@list_nth_body_is_valid a) simp [list_nth] @@ -1023,9 +1023,9 @@ namespace Ex3 - inputs: the sum allows to select the function to call in the recursive calls (and the functions may not have the same input types) - outputs: this case is degenerate because `even` and `odd` have the same - return type `Bool`, but generally speaking we need a sum type because + output type `Bool`, but generally speaking we need a sum type because the functions in the mutually recursive group may have different - return types. + output types. -/ variable (k : (Int ⊕ Int) → Result (Bool ⊕ Bool)) @@ -1034,7 +1034,7 @@ namespace Ex3 | .inl i => -- Body of `is_even` if i = 0 - then .ret (.inl true) -- We use .inl because this is `is_even` + then .ok (.inl true) -- We use .inl because this is `is_even` else do let b ← @@ -1044,13 +1044,13 @@ namespace Ex3 let r ← k (.inr (i- 1)) match r with | .inl _ => .fail .panic -- Invalid output - | .inr b => .ret b - -- Wrap the return value - .ret (.inl b) + | .inr b => .ok b + -- Wrap the output value + .ok (.inl b) | .inr i => -- Body of `is_odd` if i = 0 - then .ret (.inr false) -- We use .inr because this is `is_odd` + then .ok (.inr false) -- We use .inr because this is `is_odd` else do let b ← @@ -1059,10 +1059,10 @@ namespace Ex3 -- extract the output value let r ← k (.inl (i- 1)) match r with - | .inl b => .ret b + | .inl b => .ok b | .inr _ => .fail .panic -- Invalid output - -- Wrap the return value - .ret (.inr b) + -- Wrap the output value + .ok (.inr b) theorem is_even_is_odd_body_is_valid: ∀ k x, is_valid_p k (λ k => is_even_is_odd_body k x) := by @@ -1078,7 +1078,7 @@ namespace Ex3 do let r ← fix is_even_is_odd_body (.inl i) match r with - | .inl b => .ret b + | .inl b => .ok b | .inr _ => .fail .panic def is_odd (i : Int): Result Bool := @@ -1086,11 +1086,11 @@ namespace Ex3 let r ← fix is_even_is_odd_body (.inr i) match r with | .inl _ => .fail .panic - | .inr b => .ret b + | .inr b => .ok b -- The unfolding equation for `is_even` - diverges if `i < 0` theorem is_even_eq (i : Int) : - is_even i = (if i = 0 then .ret true else is_odd (i - 1)) + is_even i = (if i = 0 then .ok true else is_odd (i - 1)) := by have Heq := is_valid_fix_fixed_eq is_even_is_odd_body_is_valid simp [is_even, is_odd] @@ -1108,7 +1108,7 @@ namespace Ex3 -- The unfolding equation for `is_odd` - diverges if `i < 0` theorem is_odd_eq (i : Int) : - is_odd i = (if i = 0 then .ret false else is_even (i - 1)) + is_odd i = (if i = 0 then .ok false else is_even (i - 1)) := by have Heq := is_valid_fix_fixed_eq is_even_is_odd_body_is_valid simp [is_even, is_odd] @@ -1134,17 +1134,17 @@ namespace Ex4 /- The bodies are more natural -/ def is_even_body (k : (i : Fin 2) → (x : input_ty i) → Result (output_ty i x)) (i : Int) : Result Bool := if i = 0 - then .ret true + then .ok true else do let b ← k 1 (i - 1) - .ret b + .ok b def is_odd_body (k : (i : Fin 2) → (x : input_ty i) → Result (output_ty i x)) (i : Int) : Result Bool := if i = 0 - then .ret false + then .ok false else do let b ← k 0 (i - 1) - .ret b + .ok b @[simp] def bodies : Funs (Fin 2) input_ty output_ty @@ -1177,19 +1177,19 @@ namespace Ex4 theorem is_even_eq (i : Int) : is_even i = (if i = 0 - then .ret true + then .ok true else do let b ← is_odd (i - 1) - .ret b) := by + .ok b) := by simp [is_even, is_odd]; conv => lhs; rw [body_fix_eq] theorem is_odd_eq (i : Int) : is_odd i = (if i = 0 - then .ret false + then .ok false else do let b ← is_even (i - 1) - .ret b) := by + .ok b) := by simp [is_even, is_odd]; conv => lhs; rw [body_fix_eq] end Ex4 @@ -1203,12 +1203,12 @@ namespace Ex5 /- An auxiliary function, which doesn't require the fixed-point -/ def map (f : a → Result b) (ls : List a) : Result (List b) := match ls with - | [] => .ret [] + | [] => .ok [] | hd :: tl => do let hd ← f hd let tl ← map f tl - .ret (hd :: tl) + .ok (hd :: tl) /- The validity theorem for `map`, generic in `f` -/ theorem map_is_valid @@ -1229,11 +1229,11 @@ namespace Ex5 def id_body (k : Tree a → Result (Tree a)) (t : Tree a) : Result (Tree a) := match t with - | .leaf x => .ret (.leaf x) + | .leaf x => .ok (.leaf x) | .node tl => do let tl ← map k tl - .ret (.node tl) + .ok (.node tl) theorem id_body_is_valid : ∀ k x, is_valid_p k (λ k => @id_body a k x) := by @@ -1254,11 +1254,11 @@ namespace Ex5 theorem id_eq (t : Tree a) : (id t = match t with - | .leaf x => .ret (.leaf x) + | .leaf x => .ok (.leaf x) | .node tl => do let tl ← map id tl - .ret (.node tl)) + .ok (.node tl)) := by have Heq := is_valid_fix_fixed_eq (@id_body_is_valid a) simp [id] @@ -1283,7 +1283,7 @@ namespace Ex6 match ls with | [] => .fail .panic | hd :: tl => - if i = 0 then .ret hd + if i = 0 then .ok hd else k 0 ⟨ a, tl, i - 1 ⟩ @[simp] def bodies : @@ -1314,7 +1314,7 @@ namespace Ex6 match ls with | [] => is_valid_p_same k (.fail .panic) | hd :: tl => - is_valid_p_ite k (Eq i 0) (is_valid_p_same k (.ret hd)) (is_valid_p_rec k 0 ⟨a, tl, i-1⟩) + is_valid_p_ite k (Eq i 0) (is_valid_p_same k (.ok hd)) (is_valid_p_rec k 0 ⟨a, tl, i-1⟩) theorem body_is_valid' : is_valid body := fun k => @@ -1330,7 +1330,7 @@ namespace Ex6 match ls with | [] => .fail .panic | hd :: tl => - if i = 0 then .ret hd + if i = 0 then .ok hd else list_nth tl (i - 1) := by have Heq := is_valid_fix_fixed_eq body_is_valid @@ -1345,7 +1345,7 @@ namespace Ex6 match ls with | [] => .fail .panic | hd :: tl => - if i = 0 then .ret hd + if i = 0 then .ok hd else list_nth tl (i - 1) := -- Use the fixed-point equation @@ -1376,7 +1376,7 @@ namespace Ex7 match ls with | [] => .fail .panic | hd :: tl => - if i = 0 then .ret hd + if i = 0 then .ok hd else k 0 a ⟨ tl, i - 1 ⟩ @[simp] def bodies : @@ -1407,7 +1407,7 @@ namespace Ex7 match ls with | [] => is_valid_p_same k (.fail .panic) | hd :: tl => - is_valid_p_ite k (Eq i 0) (is_valid_p_same k (.ret hd)) (is_valid_p_rec k 0 a ⟨tl, i-1⟩) + is_valid_p_ite k (Eq i 0) (is_valid_p_same k (.ok hd)) (is_valid_p_rec k 0 a ⟨tl, i-1⟩) theorem body_is_valid' : is_valid body := fun k => @@ -1423,7 +1423,7 @@ namespace Ex7 match ls with | [] => .fail .panic | hd :: tl => - if i = 0 then .ret hd + if i = 0 then .ok hd else list_nth tl (i - 1) := by have Heq := is_valid_fix_fixed_eq body_is_valid @@ -1438,7 +1438,7 @@ namespace Ex7 match ls with | [] => .fail .panic | hd :: tl => - if i = 0 then .ret hd + if i = 0 then .ok hd else list_nth tl (i - 1) := -- Use the fixed-point equation @@ -1464,12 +1464,12 @@ namespace Ex8 /- An auxiliary function, which doesn't require the fixed-point -/ def map {a : Type y} {b : Type z} (f : a → Result b) (ls : List a) : Result (List b) := match ls with - | [] => .ret [] + | [] => .ok [] | hd :: tl => do let hd ← f hd let tl ← map f tl - .ret (hd :: tl) + .ok (hd :: tl) /- The validity theorems for `map`, generic in `f` -/ @@ -1518,11 +1518,11 @@ namespace Ex9 def id_body.{u} (k : (i:Fin 1) → (t:ty i) → input_ty i t → Result (output_ty i t)) (a : Type u) (t : Tree a) : Result (Tree a) := match t with - | .leaf x => .ret (.leaf x) + | .leaf x => .ok (.leaf x) | .node tl => do let tl ← map (k 0 a) tl - .ret (.node tl) + .ok (.node tl) @[simp] def bodies : Funs (Fin 1) ty input_ty output_ty tys := @@ -1556,11 +1556,11 @@ namespace Ex9 theorem id_eq' {a : Type u} (t : Tree a) : id t = (match t with - | .leaf x => .ret (.leaf x) + | .leaf x => .ok (.leaf x) | .node tl => do let tl ← map id tl - .ret (.node tl)) + .ok (.node tl)) := -- The unfolding equation have Heq := is_valid_fix_fixed_eq body_is_valid.{u} diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean index 71eaba10..5db8ffed 100644 --- a/backends/lean/Base/Diverge/Elab.lean +++ b/backends/lean/Base/Diverge/Elab.lean @@ -35,7 +35,7 @@ def mkProd (x y : Expr) : MetaM Expr := def mkInOutTy (x y z : Expr) : MetaM Expr := do mkAppM ``FixII.mk_in_out_ty #[x, y, z] --- Return the `a` in `Return a` +-- Return the `a` in `Result a` def getResultTy (ty : Expr) : MetaM Expr := ty.withApp fun f args => do if ¬ f.isConstOf ``Result ∨ args.size ≠ 1 then @@ -411,7 +411,7 @@ structure TypeInfo where For `list_nth`: `λ a => List a × Int` -/ in_ty : Expr - /- The output type, without the `Return`. This is a function taking + /- The output type, without the `Result`. This is a function taking as input a value of type `params_ty`. For `list_nth`: `λ a => a` @@ -1479,9 +1479,9 @@ namespace Tests divergent def list_nth {a: Type u} (ls : List a) (i : Int) : Result a := match ls with | [] => .fail .panic - | x :: ls => - if i = 0 then return x - else return (← list_nth ls (i - 1)) + | x :: ls => do + if i = 0 then pure x + else pure (← list_nth ls (i - 1)) --set_option trace.Diverge false @@ -1490,7 +1490,7 @@ namespace Tests example {a: Type} (ls : List a) : ∀ (i : Int), 0 ≤ i → i < ls.length → - ∃ x, list_nth ls i = .ret x := by + ∃ x, list_nth ls i = .ok x := by induction ls . intro i hpos h; simp at h; linarith . rename_i hd tl ih @@ -1538,7 +1538,7 @@ namespace Tests if i > 10 then return (← foo (i / 10)) + (← bar i) else bar 10 divergent def bar (i : Int) : Result Nat := - if i > 20 then foo (i / 20) else .ret 42 + if i > 20 then foo (i / 20) else .ok 42 end #check foo.unfold @@ -1557,8 +1557,8 @@ namespace Tests divergent def iInBounds {a : Type} (ls : List a) (i : Int) : Result Bool := let i0 := ls.length if i < i0 - then Result.ret True - else Result.ret False + then Result.ok True + else Result.ok False #check iInBounds.unfold @@ -1566,8 +1566,8 @@ namespace Tests {a : Type} (ls : List a) : Result Bool := let ls1 := ls match ls1 with - | [] => Result.ret False - | _ :: _ => Result.ret True + | [] => Result.ok False + | _ :: _ => Result.ok True #check isCons.unfold @@ -1584,7 +1584,7 @@ namespace Tests divergent def infinite_loop : Result Unit := do let _ ← infinite_loop - Result.ret () + Result.ok () #check infinite_loop.unfold @@ -1604,51 +1604,51 @@ namespace Tests divergent def id {a : Type u} (t : Tree a) : Result (Tree a) := match t with - | .leaf x => .ret (.leaf x) + | .leaf x => .ok (.leaf x) | .node tl => do let tl ← map id tl - .ret (.node tl) + .ok (.node tl) #check id.unfold divergent def id1 {a : Type u} (t : Tree a) : Result (Tree a) := match t with - | .leaf x => .ret (.leaf x) + | .leaf x => .ok (.leaf x) | .node tl => do let tl ← map (fun x => id1 x) tl - .ret (.node tl) + .ok (.node tl) #check id1.unfold divergent def id2 {a : Type u} (t : Tree a) : Result (Tree a) := match t with - | .leaf x => .ret (.leaf x) + | .leaf x => .ok (.leaf x) | .node tl => do let tl ← map (fun x => do let _ ← id2 x; id2 x) tl - .ret (.node tl) + .ok (.node tl) #check id2.unfold divergent def incr (t : Tree Nat) : Result (Tree Nat) := match t with - | .leaf x => .ret (.leaf (x + 1)) + | .leaf x => .ok (.leaf (x + 1)) | .node tl => do let tl ← map incr tl - .ret (.node tl) + .ok (.node tl) -- We handle this by inlining the let-binding divergent def id3 (t : Tree Nat) : Result (Tree Nat) := match t with - | .leaf x => .ret (.leaf (x + 1)) + | .leaf x => .ok (.leaf (x + 1)) | .node tl => do let f := id3 let tl ← map f tl - .ret (.node tl) + .ok (.node tl) #check id3.unfold @@ -1658,12 +1658,12 @@ namespace Tests -- be parameterized by something). divergent def id4 (t : Tree Nat) : Result (Tree Nat) := match t with - | .leaf x => .ret (.leaf (x + 1)) + | .leaf x => .ok (.leaf (x + 1)) | .node tl => do - let f ← .ret id4 + let f ← .ok id4 let tl ← map f tl - .ret (.node tl) + .ok (.node tl) #check id4.unfold -/ diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean index 1f470fe1..15fe1ff9 100644 --- a/backends/lean/Base/Primitives/Alloc.lean +++ b/backends/lean/Base/Primitives/Alloc.lean @@ -11,8 +11,8 @@ namespace boxed -- alloc.boxed namespace Box -- alloc.boxed.Box -def deref (T : Type) (x : T) : Result T := ret x -def deref_mut (T : Type) (x : T) : Result (T × (T → Result T)) := ret (x, λ x => ret x) +def deref (T : Type) (x : T) : Result T := ok x +def deref_mut (T : Type) (x : T) : Result (T × (T → Result T)) := ok (x, λ x => ok x) /-- Trait instance -/ def coreopsDerefInst (Self : Type) : diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean index 3bd2aebb..91ca7284 100644 --- a/backends/lean/Base/Primitives/ArraySlice.lean +++ b/backends/lean/Base/Primitives/ArraySlice.lean @@ -49,7 +49,7 @@ abbrev Array.slice {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i def Array.index_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α := match v.val.indexOpt i.val with | none => fail .arrayOutOfBounds - | some x => ret x + | some x => ok x -- For initialization def Array.repeat (α : Type u) (n : Usize) (x : α) : Array α n := @@ -68,7 +68,7 @@ theorem Array.repeat_spec {α : Type u} (n : Usize) (x : α) : @[pspec] theorem Array.index_usize_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize) (hbound : i.val < v.length) : - ∃ x, v.index_usize α n i = ret x ∧ x = v.val.index i.val := by + ∃ x, v.index_usize α n i = ok x ∧ x = v.val.index i.val := by simp only [index_usize] -- TODO: dependent rewrite have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) @@ -78,12 +78,12 @@ def Array.update_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (x: match v.val.indexOpt i.val with | none => fail .arrayOutOfBounds | some _ => - .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩ + ok ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩ @[pspec] theorem Array.update_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α) (hbound : i.val < v.length) : - ∃ nv, v.update_usize α n i x = ret nv ∧ + ∃ nv, v.update_usize α n i x = ok nv ∧ nv.val = v.val.update i.val x := by simp only [update_usize] @@ -95,12 +95,12 @@ theorem Array.update_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Us def Array.index_mut_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result (α × (α -> Result (Array α n))) := do let x ← index_usize α n v i - ret (x, update_usize α n v i) + ok (x, update_usize α n v i) @[pspec] theorem Array.index_mut_usize_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize) (hbound : i.val < v.length) : - ∃ x back, v.index_mut_usize α n i = ret (x, back) ∧ + ∃ x back, v.index_mut_usize α n i = ok (x, back) ∧ x = v.val.index i.val ∧ back = update_usize α n v i := by simp only [index_mut_usize, Bind.bind, bind] @@ -147,7 +147,7 @@ abbrev Slice.slice {α : Type u} [Inhabited α] (s : Slice α) (i j : Int) : Lis def Slice.index_usize (α : Type u) (v: Slice α) (i: Usize) : Result α := match v.val.indexOpt i.val with | none => fail .arrayOutOfBounds - | some x => ret x + | some x => ok x /- In the theorems below: we don't always need the `∃ ..`, but we use one so that `progress` introduces an opaque variable and an equality. This @@ -157,7 +157,7 @@ def Slice.index_usize (α : Type u) (v: Slice α) (i: Usize) : Result α := @[pspec] theorem Slice.index_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize) (hbound : i.val < v.length) : - ∃ x, v.index_usize α i = ret x ∧ x = v.val.index i.val := by + ∃ x, v.index_usize α i = ok x ∧ x = v.val.index i.val := by simp only [index_usize] -- TODO: dependent rewrite have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) @@ -167,12 +167,12 @@ def Slice.update_usize (α : Type u) (v: Slice α) (i: Usize) (x: α) : Result ( match v.val.indexOpt i.val with | none => fail .arrayOutOfBounds | some _ => - .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩ + ok ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩ @[pspec] theorem Slice.update_usize_spec {α : Type u} (v: Slice α) (i: Usize) (x : α) (hbound : i.val < v.length) : - ∃ nv, v.update_usize α i x = ret nv ∧ + ∃ nv, v.update_usize α i x = ok nv ∧ nv.val = v.val.update i.val x := by simp only [update_usize] @@ -184,12 +184,12 @@ theorem Slice.update_usize_spec {α : Type u} (v: Slice α) (i: Usize) (x : α) def Slice.index_mut_usize (α : Type u) (v: Slice α) (i: Usize) : Result (α × (α → Result (Slice α))) := do let x ← Slice.index_usize α v i - ret (x, Slice.update_usize α v i) + ok (x, Slice.update_usize α v i) @[pspec] theorem Slice.index_mut_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize) (hbound : i.val < v.length) : - ∃ x back, v.index_mut_usize α i = ret (x, back) ∧ + ∃ x back, v.index_mut_usize α i = ok (x, back) ∧ x = v.val.index i.val ∧ back = Slice.update_usize α v i := by simp only [index_mut_usize, Bind.bind, bind] @@ -203,30 +203,30 @@ theorem Slice.index_mut_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i `progress` tactic), meaning `Array.to_slice` should be considered as opaque. All what the spec theorem reveals is that the "representative" lists are the same. -/ def Array.to_slice (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) := - ret ⟨ v.val, by simp [← List.len_eq_length]; scalar_tac ⟩ + ok ⟨ v.val, by simp [← List.len_eq_length]; scalar_tac ⟩ @[pspec] theorem Array.to_slice_spec {α : Type u} {n : Usize} (v : Array α n) : - ∃ s, to_slice α n v = ret s ∧ v.val = s.val := by simp [to_slice] + ∃ s, to_slice α n v = ok s ∧ v.val = s.val := by simp [to_slice] def Array.from_slice (α : Type u) (n : Usize) (_ : Array α n) (s : Slice α) : Result (Array α n) := if h: s.val.len = n.val then - ret ⟨ s.val, by simp [← List.len_eq_length, *] ⟩ + ok ⟨ s.val, by simp [← List.len_eq_length, *] ⟩ else fail panic @[pspec] theorem Array.from_slice_spec {α : Type u} {n : Usize} (a : Array α n) (ns : Slice α) (h : ns.val.len = n.val) : - ∃ na, from_slice α n a ns = ret na ∧ na.val = ns.val + ∃ na, from_slice α n a ns = ok na ∧ na.val = ns.val := by simp [from_slice, *] def Array.to_slice_mut (α : Type u) (n : Usize) (a : Array α n) : Result (Slice α × (Slice α → Result (Array α n))) := do let s ← Array.to_slice α n a - ret (s, Array.from_slice α n a) + ok (s, Array.from_slice α n a) @[pspec] theorem Array.to_slice_mut_spec {α : Type u} {n : Usize} (v : Array α n) : - ∃ s back, to_slice_mut α n v = ret (s, back) ∧ + ∃ s back, to_slice_mut α n v = ok (s, back) ∧ v.val = s.val ∧ back = Array.from_slice α n v := by simp [to_slice_mut, to_slice] @@ -234,7 +234,7 @@ theorem Array.to_slice_mut_spec {α : Type u} {n : Usize} (v : Array α n) : def Array.subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) := -- TODO: not completely sure here if r.start.val < r.end_.val ∧ r.end_.val ≤ a.val.len then - ret ⟨ a.val.slice r.start.val r.end_.val, + ok ⟨ a.val.slice r.start.val r.end_.val, by simp [← List.len_eq_length] have := a.val.slice_len_le r.start.val r.end_.val @@ -245,7 +245,7 @@ def Array.subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) @[pspec] theorem Array.subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) : - ∃ s, subslice α n a r = ret s ∧ + ∃ s, subslice α n a r = ok s ∧ s.val = a.val.slice r.start.val r.end_.val ∧ (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i)) := by @@ -269,7 +269,7 @@ def Array.update_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range . scalar_tac let na := s_beg.append (s.val.append s_end) have : na.len = a.val.len := by simp [na, *] - ret ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩ + ok ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩ else fail panic @@ -281,7 +281,7 @@ def Array.update_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range @[pspec] theorem Array.update_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α) (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : s.length = r.end_.val - r.start.val) : - ∃ na, update_subslice α n a r s = ret na ∧ + ∃ na, update_subslice α n a r s = ok na ∧ (∀ i, 0 ≤ i → i < r.start.val → na.index_s i = a.index_s i) ∧ (∀ i, r.start.val ≤ i → i < r.end_.val → na.index_s i = s.index_s (i - r.start.val)) ∧ (∀ i, r.end_.val ≤ i → i < n.val → na.index_s i = a.index_s i) := by @@ -305,7 +305,7 @@ theorem Array.update_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : def Slice.subslice (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) := -- TODO: not completely sure here if r.start.val < r.end_.val ∧ r.end_.val ≤ s.length then - ret ⟨ s.val.slice r.start.val r.end_.val, + ok ⟨ s.val.slice r.start.val r.end_.val, by simp [← List.len_eq_length] have := s.val.slice_len_le r.start.val r.end_.val @@ -316,7 +316,7 @@ def Slice.subslice (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slic @[pspec] theorem Slice.subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize) (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) : - ∃ ns, subslice α s r = ret ns ∧ + ∃ ns, subslice α s r = ok ns ∧ ns.val = s.slice r.start.val r.end_.val ∧ (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index_s i = s.index_s (r.start.val + i)) := by @@ -343,14 +343,14 @@ def Slice.update_subslice (α : Type u) (s : Slice α) (r : Range Usize) (ss : S . scalar_tac let ns := s_beg.append (ss.val.append s_end) have : ns.len = s.val.len := by simp [ns, *] - ret ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩ + ok ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩ else fail panic @[pspec] theorem Slice.update_subslice_spec {α : Type u} [Inhabited α] (a : Slice α) (r : Range Usize) (ss : Slice α) (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : ss.length = r.end_.val - r.start.val) : - ∃ na, update_subslice α a r ss = ret na ∧ + ∃ na, update_subslice α a r ss = ok na ∧ (∀ i, 0 ≤ i → i < r.start.val → na.index_s i = a.index_s i) ∧ (∀ i, r.start.val ≤ i → i < r.end_.val → na.index_s i = ss.index_s (i - r.start.val)) ∧ (∀ i, r.end_.val ≤ i → i < a.length → na.index_s i = a.index_s i) := by @@ -392,7 +392,7 @@ def core.slice.index.Slice.index let x ← inst.get i slice match x with | none => fail panic - | some x => ret x + | some x => ok x /- [core::slice::index::Range:::get]: forward function -/ def core.slice.index.RangeUsize.get (T : Type) (i : Range Usize) (slice : Slice T) : diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean index 0c64eca1..4c5b2795 100644 --- a/backends/lean/Base/Primitives/Base.lean +++ b/backends/lean/Base/Primitives/Base.lean @@ -41,7 +41,7 @@ deriving Repr, BEq open Error inductive Result (α : Type u) where - | ret (v: α): Result α + | ok (v: α): Result α | fail (e: Error): Result α | div deriving Repr, BEq @@ -56,31 +56,31 @@ instance Result_Nonempty (α : Type u) : Nonempty (Result α) := /- HELPERS -/ -def ret? {α: Type u} (r: Result α): Bool := +def ok? {α: Type u} (r: Result α): Bool := match r with - | ret _ => true + | ok _ => true | fail _ | div => false def div? {α: Type u} (r: Result α): Bool := match r with | div => true - | ret _ | fail _ => false + | ok _ | fail _ => false def massert (b:Bool) : Result Unit := - if b then ret () else fail assertionFailure + if b then ok () else fail assertionFailure macro "prove_eval_global" : tactic => `(tactic| first | apply Eq.refl | decide) -def eval_global {α: Type u} (x: Result α) (_: ret? x := by prove_eval_global) : α := +def eval_global {α: Type u} (x: Result α) (_: ok? x := by prove_eval_global) : α := match x with | fail _ | div => by contradiction - | ret x => x + | ok x => x /- DO-DSL SUPPORT -/ def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Result β := match x with - | ret v => f v + | ok v => f v | fail v => fail v | div => div @@ -88,11 +88,11 @@ def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Resu instance : Bind Result where bind := bind --- Allows using return x in do-blocks +-- Allows using pure x in do-blocks instance : Pure Result where - pure := fun x => ret x + pure := fun x => ok x -@[simp] theorem bind_ret (x : α) (f : α → Result β) : bind (.ret x) f = f x := by simp [bind] +@[simp] theorem bind_ok (x : α) (f : α → Result β) : bind (.ok x) f = f x := by simp [bind] @[simp] theorem bind_fail (x : Error) (f : α → Result β) : bind (.fail x) f = .fail x := by simp [bind] @[simp] theorem bind_div (f : α → Result β) : bind .div f = .div := by simp [bind] @@ -103,14 +103,14 @@ instance : Pure Result where -- rely on subtype, and a custom let-binding operator, in effect recreating our -- own variant of the do-dsl -def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } := +def Result.attach {α: Type} (o : Result α): Result { x : α // o = ok x } := match o with - | ret x => ret ⟨x, rfl⟩ + | ok x => ok ⟨x, rfl⟩ | fail e => fail e | div => div -@[simp] theorem bind_tc_ret (x : α) (f : α → Result β) : - (do let y ← .ret x; f y) = f x := by simp [Bind.bind, bind] +@[simp] theorem bind_tc_ok (x : α) (f : α → Result β) : + (do let y ← .ok x; f y) = f x := by simp [Bind.bind, bind] @[simp] theorem bind_tc_fail (x : Error) (f : α → Result β) : (do let y ← fail x; f y) = fail x := by simp [Bind.bind, bind] diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 7668bc59..98d695a4 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -350,7 +350,7 @@ def Scalar.tryMk (ty : ScalarTy) (x : Int) : Result (Scalar ty) := -- ``` -- then normalization blocks (for instance, some proofs which use reflexivity fail). -- However, the version below doesn't block reduction (TODO: investigate): - return Scalar.ofIntCore x (Scalar.check_bounds_prop h) + ok (Scalar.ofIntCore x (Scalar.check_bounds_prop h)) else fail integerOverflow def Scalar.neg {ty : ScalarTy} (x : Scalar ty) : Result (Scalar ty) := Scalar.tryMk ty (- x.val) @@ -584,7 +584,7 @@ instance {ty} : HAnd (Scalar ty) (Scalar ty) (Scalar ty) where theorem Scalar.add_spec {ty} {x y : Scalar ty} (hmin : Scalar.min ty ≤ ↑x + y.val) (hmax : ↑x + ↑y ≤ Scalar.max ty) : - (∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y) := by + (∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y) := by -- Applying the unfoldings only on the left conv => congr; ext; lhs; unfold HAdd.hAdd instHAddScalarResult; simp [add, tryMk] split @@ -593,7 +593,7 @@ theorem Scalar.add_spec {ty} {x y : Scalar ty} theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty} (hmax : ↑x + ↑y ≤ Scalar.max ty) : - ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by + ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by have hmin : Scalar.min ty ≤ ↑x + ↑y := by have hx := x.hmin have hy := y.hmin @@ -602,57 +602,57 @@ theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty} /- Fine-grained theorems -/ @[pspec] theorem Usize.add_spec {x y : Usize} (hmax : ↑x + ↑y ≤ Usize.max) : - ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by + ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *] @[pspec] theorem U8.add_spec {x y : U8} (hmax : ↑x + ↑y ≤ U8.max) : - ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by + ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *] @[pspec] theorem U16.add_spec {x y : U16} (hmax : ↑x + ↑y ≤ U16.max) : - ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by + ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *] @[pspec] theorem U32.add_spec {x y : U32} (hmax : ↑x + ↑y ≤ U32.max) : - ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by + ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *] @[pspec] theorem U64.add_spec {x y : U64} (hmax : ↑x + ↑y ≤ U64.max) : - ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by + ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *] @[pspec] theorem U128.add_spec {x y : U128} (hmax : ↑x + ↑y ≤ U128.max) : - ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by + ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *] @[pspec] theorem Isize.add_spec {x y : Isize} (hmin : Isize.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ Isize.max) : - ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := + ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := Scalar.add_spec hmin hmax @[pspec] theorem I8.add_spec {x y : I8} (hmin : I8.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I8.max) : - ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := + ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := Scalar.add_spec hmin hmax @[pspec] theorem I16.add_spec {x y : I16} (hmin : I16.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I16.max) : - ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := + ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := Scalar.add_spec hmin hmax @[pspec] theorem I32.add_spec {x y : I32} (hmin : I32.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I32.max) : - ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := + ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := Scalar.add_spec hmin hmax @[pspec] theorem I64.add_spec {x y : I64} (hmin : I64.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I64.max) : - ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := + ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := Scalar.add_spec hmin hmax @[pspec] theorem I128.add_spec {x y : I128} (hmin : I128.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I128.max) : - ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := + ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := Scalar.add_spec hmin hmax -- Generic theorem - shouldn't be used much @@ -660,7 +660,7 @@ theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty} theorem Scalar.sub_spec {ty} {x y : Scalar ty} (hmin : Scalar.min ty ≤ ↑x - ↑y) (hmax : ↑x - ↑y ≤ Scalar.max ty) : - ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by + ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by conv => congr; ext; lhs; simp [HSub.hSub, sub, tryMk, Sub.sub] split . simp [pure] @@ -669,7 +669,7 @@ theorem Scalar.sub_spec {ty} {x y : Scalar ty} theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned) {x y : Scalar ty} (hmin : Scalar.min ty ≤ ↑x - ↑y) : - ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by + ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by have : ↑x - ↑y ≤ Scalar.max ty := by have hx := x.hmin have hxm := x.hmax @@ -680,64 +680,64 @@ theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned) /- Fine-grained theorems -/ @[pspec] theorem Usize.sub_spec {x y : Usize} (hmin : Usize.min ≤ ↑x - ↑y) : - ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by + ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned] @[pspec] theorem U8.sub_spec {x y : U8} (hmin : U8.min ≤ ↑x - ↑y) : - ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by + ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned] @[pspec] theorem U16.sub_spec {x y : U16} (hmin : U16.min ≤ ↑x - ↑y) : - ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by + ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned] @[pspec] theorem U32.sub_spec {x y : U32} (hmin : U32.min ≤ ↑x - ↑y) : - ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by + ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned] @[pspec] theorem U64.sub_spec {x y : U64} (hmin : U64.min ≤ ↑x - ↑y) : - ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by + ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned] @[pspec] theorem U128.sub_spec {x y : U128} (hmin : U128.min ≤ ↑x - ↑y) : - ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by + ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned] @[pspec] theorem Isize.sub_spec {x y : Isize} (hmin : Isize.min ≤ ↑x - ↑y) (hmax : ↑x - ↑y ≤ Isize.max) : - ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := + ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := Scalar.sub_spec hmin hmax @[pspec] theorem I8.sub_spec {x y : I8} (hmin : I8.min ≤ ↑x - ↑y) (hmax : ↑x - ↑y ≤ I8.max) : - ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := + ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := Scalar.sub_spec hmin hmax @[pspec] theorem I16.sub_spec {x y : I16} (hmin : I16.min ≤ ↑x - ↑y) (hmax : ↑x - ↑y ≤ I16.max) : - ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := + ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := Scalar.sub_spec hmin hmax @[pspec] theorem I32.sub_spec {x y : I32} (hmin : I32.min ≤ ↑x - ↑y) (hmax : ↑x - ↑y ≤ I32.max) : - ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := + ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := Scalar.sub_spec hmin hmax @[pspec] theorem I64.sub_spec {x y : I64} (hmin : I64.min ≤ ↑x - ↑y) (hmax : ↑x - ↑y ≤ I64.max) : - ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := + ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := Scalar.sub_spec hmin hmax @[pspec] theorem I128.sub_spec {x y : I128} (hmin : I128.min ≤ ↑x - ↑y) (hmax : ↑x - ↑y ≤ I128.max) : - ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := + ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := Scalar.sub_spec hmin hmax -- Generic theorem - shouldn't be used much theorem Scalar.mul_spec {ty} {x y : Scalar ty} (hmin : Scalar.min ty ≤ ↑x * ↑y) (hmax : ↑x * ↑y ≤ Scalar.max ty) : - ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by + ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by conv => congr; ext; lhs; simp [HMul.hMul] simp [mul, tryMk] split @@ -747,7 +747,7 @@ theorem Scalar.mul_spec {ty} {x y : Scalar ty} theorem Scalar.mul_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty} (hmax : ↑x * ↑y ≤ Scalar.max ty) : - ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by + ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by have : Scalar.min ty ≤ ↑x * ↑y := by have hx := x.hmin have hy := y.hmin @@ -756,57 +756,57 @@ theorem Scalar.mul_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty} /- Fine-grained theorems -/ @[pspec] theorem Usize.mul_spec {x y : Usize} (hmax : ↑x * ↑y ≤ Usize.max) : - ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by + ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned] @[pspec] theorem U8.mul_spec {x y : U8} (hmax : ↑x * ↑y ≤ U8.max) : - ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by + ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned] @[pspec] theorem U16.mul_spec {x y : U16} (hmax : ↑x * ↑y ≤ U16.max) : - ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by + ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned] @[pspec] theorem U32.mul_spec {x y : U32} (hmax : ↑x * ↑y ≤ U32.max) : - ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by + ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned] @[pspec] theorem U64.mul_spec {x y : U64} (hmax : ↑x * ↑y ≤ U64.max) : - ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by + ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned] @[pspec] theorem U128.mul_spec {x y : U128} (hmax : ↑x * ↑y ≤ U128.max) : - ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by + ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned] @[pspec] theorem Isize.mul_spec {x y : Isize} (hmin : Isize.min ≤ ↑x * ↑y) (hmax : ↑x * ↑y ≤ Isize.max) : - ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := + ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := Scalar.mul_spec hmin hmax @[pspec] theorem I8.mul_spec {x y : I8} (hmin : I8.min ≤ ↑x * ↑y) (hmax : ↑x * ↑y ≤ I8.max) : - ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := + ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := Scalar.mul_spec hmin hmax @[pspec] theorem I16.mul_spec {x y : I16} (hmin : I16.min ≤ ↑x * ↑y) (hmax : ↑x * ↑y ≤ I16.max) : - ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := + ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := Scalar.mul_spec hmin hmax @[pspec] theorem I32.mul_spec {x y : I32} (hmin : I32.min ≤ ↑x * ↑y) (hmax : ↑x * ↑y ≤ I32.max) : - ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := + ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := Scalar.mul_spec hmin hmax @[pspec] theorem I64.mul_spec {x y : I64} (hmin : I64.min ≤ ↑x * ↑y) (hmax : ↑x * ↑y ≤ I64.max) : - ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := + ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := Scalar.mul_spec hmin hmax @[pspec] theorem I128.mul_spec {x y : I128} (hmin : I128.min ≤ ↑x * ↑y) (hmax : ↑x * ↑y ≤ I128.max) : - ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := + ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := Scalar.mul_spec hmin hmax -- Generic theorem - shouldn't be used much @@ -815,15 +815,14 @@ theorem Scalar.div_spec {ty} {x y : Scalar ty} (hnz : ↑y ≠ (0 : Int)) (hmin : Scalar.min ty ≤ scalar_div ↑x ↑y) (hmax : scalar_div ↑x ↑y ≤ Scalar.max ty) : - ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y := by + ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y := by simp [HDiv.hDiv, div, Div.div] simp [tryMk, *] - simp [pure] rfl theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : Scalar ty} (hnz : ↑y ≠ (0 : Int)) : - ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by + ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by have h : Scalar.min ty = 0 := by cases ty <;> simp [ScalarTy.isSigned, min] at * have hx := x.hmin have hy := y.hmin @@ -839,69 +838,69 @@ theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S /- Fine-grained theorems -/ @[pspec] theorem Usize.div_spec (x : Usize) {y : Usize} (hnz : ↑y ≠ (0 : Int)) : - ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by + ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *] @[pspec] theorem U8.div_spec (x : U8) {y : U8} (hnz : ↑y ≠ (0 : Int)) : - ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by + ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *] @[pspec] theorem U16.div_spec (x : U16) {y : U16} (hnz : ↑y ≠ (0 : Int)) : - ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by + ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *] @[pspec] theorem U32.div_spec (x : U32) {y : U32} (hnz : ↑y ≠ (0 : Int)) : - ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by + ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *] @[pspec] theorem U64.div_spec (x : U64) {y : U64} (hnz : ↑y ≠ (0 : Int)) : - ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by + ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *] @[pspec] theorem U128.div_spec (x : U128) {y : U128} (hnz : ↑y ≠ (0 : Int)) : - ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by + ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *] @[pspec] theorem Isize.div_spec (x : Isize) {y : Isize} (hnz : ↑y ≠ (0 : Int)) (hmin : Isize.min ≤ scalar_div ↑x ↑y) (hmax : scalar_div ↑x ↑y ≤ Isize.max): - ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y := + ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y := Scalar.div_spec hnz hmin hmax @[pspec] theorem I8.div_spec (x : I8) {y : I8} (hnz : ↑y ≠ (0 : Int)) (hmin : I8.min ≤ scalar_div ↑x ↑y) (hmax : scalar_div ↑x ↑y ≤ I8.max): - ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y := + ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y := Scalar.div_spec hnz hmin hmax @[pspec] theorem I16.div_spec (x : I16) {y : I16} (hnz : ↑y ≠ (0 : Int)) (hmin : I16.min ≤ scalar_div ↑x ↑y) (hmax : scalar_div ↑x ↑y ≤ I16.max): - ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y := + ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y := Scalar.div_spec hnz hmin hmax @[pspec] theorem I32.div_spec (x : I32) {y : I32} (hnz : ↑y ≠ (0 : Int)) (hmin : I32.min ≤ scalar_div ↑x ↑y) (hmax : scalar_div ↑x ↑y ≤ I32.max): - ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y := + ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y := Scalar.div_spec hnz hmin hmax @[pspec] theorem I64.div_spec (x : I64) {y : I64} (hnz : ↑y ≠ (0 : Int)) (hmin : I64.min ≤ scalar_div ↑x ↑y) (hmax : scalar_div ↑x ↑y ≤ I64.max): - ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y := + ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y := Scalar.div_spec hnz hmin hmax @[pspec] theorem I128.div_spec (x : I128) {y : I128} (hnz : ↑y ≠ (0 : Int)) (hmin : I128.min ≤ scalar_div ↑x ↑y) (hmax : scalar_div ↑x ↑y ≤ I128.max): - ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y := + ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y := Scalar.div_spec hnz hmin hmax -- Generic theorem - shouldn't be used much @@ -910,15 +909,14 @@ theorem Scalar.rem_spec {ty} {x y : Scalar ty} (hnz : ↑y ≠ (0 : Int)) (hmin : Scalar.min ty ≤ scalar_rem ↑x ↑y) (hmax : scalar_rem ↑x ↑y ≤ Scalar.max ty) : - ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y := by + ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y := by simp [HMod.hMod, rem] simp [tryMk, *] - simp [pure] rfl theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : Scalar ty} (hnz : ↑y ≠ (0 : Int)) : - ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by + ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by have h : Scalar.min ty = 0 := by cases ty <;> simp [ScalarTy.isSigned, min] at * have hx := x.hmin have hy := y.hmin @@ -934,62 +932,62 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S simp [*] @[pspec] theorem Usize.rem_spec (x : Usize) {y : Usize} (hnz : ↑y ≠ (0 : Int)) : - ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by + ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *] @[pspec] theorem U8.rem_spec (x : U8) {y : U8} (hnz : ↑y ≠ (0 : Int)) : - ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by + ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *] @[pspec] theorem U16.rem_spec (x : U16) {y : U16} (hnz : ↑y ≠ (0 : Int)) : - ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by + ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *] @[pspec] theorem U32.rem_spec (x : U32) {y : U32} (hnz : ↑y ≠ (0 : Int)) : - ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by + ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *] @[pspec] theorem U64.rem_spec (x : U64) {y : U64} (hnz : ↑y ≠ (0 : Int)) : - ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by + ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *] @[pspec] theorem U128.rem_spec (x : U128) {y : U128} (hnz : ↑y ≠ (0 : Int)) : - ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by + ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *] @[pspec] theorem I8.rem_spec (x : I8) {y : I8} (hnz : ↑y ≠ (0 : Int)) (hmin : I8.min ≤ scalar_rem ↑x ↑y) (hmax : scalar_rem ↑x ↑y ≤ I8.max): - ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y := + ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y := Scalar.rem_spec hnz hmin hmax @[pspec] theorem I16.rem_spec (x : I16) {y : I16} (hnz : ↑y ≠ (0 : Int)) (hmin : I16.min ≤ scalar_rem ↑x ↑y) (hmax : scalar_rem ↑x ↑y ≤ I16.max): - ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y := + ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y := Scalar.rem_spec hnz hmin hmax @[pspec] theorem I32.rem_spec (x : I32) {y : I32} (hnz : ↑y ≠ (0 : Int)) (hmin : I32.min ≤ scalar_rem ↑x ↑y) (hmax : scalar_rem ↑x ↑y ≤ I32.max): - ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y := + ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y := Scalar.rem_spec hnz hmin hmax @[pspec] theorem I64.rem_spec (x : I64) {y : I64} (hnz : ↑y ≠ (0 : Int)) (hmin : I64.min ≤ scalar_rem ↑x ↑y) (hmax : scalar_rem ↑x ↑y ≤ I64.max): - ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y := + ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y := Scalar.rem_spec hnz hmin hmax @[pspec] theorem I128.rem_spec (x : I128) {y : I128} (hnz : ↑y ≠ (0 : Int)) (hmin : I128.min ≤ scalar_rem ↑x ↑y) (hmax : scalar_rem ↑x ↑y ≤ I128.max): - ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y := + ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y := Scalar.rem_spec hnz hmin hmax -- ofIntCore diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean index 2b8425d8..8e2d65a8 100644 --- a/backends/lean/Base/Primitives/Vec.lean +++ b/backends/lean/Base/Primitives/Vec.lean @@ -60,34 +60,34 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α) simp [Usize.max] at * have hm := Usize.refined_max.property cases h <;> cases hm <;> simp [U32.max, U64.max] at * <;> try linarith - return ⟨ List.concat v.val x, by simp at *; assumption ⟩ + ok ⟨ List.concat v.val x, by simp at *; assumption ⟩ else fail maximumSizeExceeded -- This shouldn't be used def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit := if i.val < v.length then - .ret () + ok () else - .fail arrayOutOfBounds + fail arrayOutOfBounds -- This is actually the backward function def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) := if i.val < v.length then - .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩ + ok ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩ else - .fail arrayOutOfBounds + fail arrayOutOfBounds @[pspec] theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α) (hbound : i.val < v.length) : - ∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by + ∃ nv, v.insert α i x = ok nv ∧ nv.val = v.val.update i.val x := by simp [insert, *] def Vec.index_usize {α : Type u} (v: Vec α) (i: Usize) : Result α := match v.val.indexOpt i.val with | none => fail .arrayOutOfBounds - | some x => ret x + | some x => ok x /- In the theorems below: we don't always need the `∃ ..`, but we use one so that `progress` introduces an opaque variable and an equality. This @@ -97,7 +97,7 @@ def Vec.index_usize {α : Type u} (v: Vec α) (i: Usize) : Result α := @[pspec] theorem Vec.index_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) (hbound : i.val < v.length) : - ∃ x, v.index_usize i = ret x ∧ x = v.val.index i.val := by + ∃ x, v.index_usize i = ok x ∧ x = v.val.index i.val := by simp only [index_usize] -- TODO: dependent rewrite have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) @@ -107,12 +107,12 @@ def Vec.update_usize {α : Type u} (v: Vec α) (i: Usize) (x: α) : Result (Vec match v.val.indexOpt i.val with | none => fail .arrayOutOfBounds | some _ => - .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩ + ok ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩ @[pspec] theorem Vec.update_usize_spec {α : Type u} (v: Vec α) (i: Usize) (x : α) (hbound : i.val < v.length) : - ∃ nv, v.update_usize i x = ret nv ∧ + ∃ nv, v.update_usize i x = ok nv ∧ nv.val = v.val.update i.val x := by simp only [update_usize] @@ -124,15 +124,15 @@ theorem Vec.update_usize_spec {α : Type u} (v: Vec α) (i: Usize) (x : α) def Vec.index_mut_usize {α : Type u} (v: Vec α) (i: Usize) : Result (α × (α → Result (Vec α))) := match Vec.index_usize v i with - | ret x => - ret (x, Vec.update_usize v i) + | ok x => + ok (x, Vec.update_usize v i) | fail e => fail e | div => div @[pspec] theorem Vec.index_mut_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) (hbound : i.val < v.length) : - ∃ x back, v.index_mut_usize i = ret (x, back) ∧ + ∃ x back, v.index_mut_usize i = ok (x, back) ∧ x = v.val.index i.val ∧ -- Backward function back = v.update_usize i diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index dc30c441..ea38c630 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -136,7 +136,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) let _ ← tryTac (simpAt true [] - [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div] + [``Primitives.bind_tc_ok, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div] [hEq.fvarId!] (.targets #[] true)) -- It may happen that at this point the goal is already solved (though this is rare) -- TODO: not sure this is the best way of checking it @@ -397,33 +397,33 @@ namespace Test example {ty} {x y : Scalar ty} (hmin : Scalar.min ty ≤ x.val + y.val) (hmax : x.val + y.val ≤ Scalar.max ty) : - ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by + ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by progress keep _ as ⟨ z, h1 .. ⟩ simp [*, h1] example {ty} {x y : Scalar ty} (hmin : Scalar.min ty ≤ x.val + y.val) (hmax : x.val + y.val ≤ Scalar.max ty) : - ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by + ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by progress keep h with Scalar.add_spec as ⟨ z ⟩ simp [*, h] example {x y : U32} (hmax : x.val + y.val ≤ U32.max) : - ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by + ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by -- This spec theorem is suboptimal, but it is good to check that it works progress with Scalar.add_spec as ⟨ z, h1 .. ⟩ simp [*, h1] example {x y : U32} (hmax : x.val + y.val ≤ U32.max) : - ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by + ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by progress with U32.add_spec as ⟨ z, h1 .. ⟩ simp [*, h1] example {x y : U32} (hmax : x.val + y.val ≤ U32.max) : - ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by + ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by progress keep _ as ⟨ z, h1 .. ⟩ simp [*, h1] @@ -431,7 +431,7 @@ namespace Test `α : Type u` where u is quantified, while here we use `α : Type 0` -/ example {α : Type} (v: Vec α) (i: Usize) (x : α) (hbounds : i.val < v.length) : - ∃ nv, v.update_usize i x = ret nv ∧ + ∃ nv, v.update_usize i x = ok nv ∧ nv.val = v.val.update i.val x := by progress simp [*] @@ -443,8 +443,8 @@ namespace Test (do (do let _ ← v.update_usize i x - .ret ()) - .ret ()) = ret nv + .ok ()) + .ok ()) = ok nv := by progress simp [*] @@ -454,8 +454,8 @@ namespace Test not a constant. We also test the case where the function under scrutinee is not a constant. -/ example {x : U32} - (f : U32 → Result Unit) (h : ∀ x, f x = .ret ()) : - f x = ret () := by + (f : U32 → Result Unit) (h : ∀ x, f x = .ok ()) : + f x = ok () := by progress end Test |