diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/Demo/Properties.lean | 12 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Properties.lean | 14 | ||||
| -rw-r--r-- | tests/lean/Tutorial.lean | 22 |
3 files changed, 24 insertions, 24 deletions
diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean index e514ac3e..abdc2985 100644 --- a/tests/lean/Demo/Properties.lean +++ b/tests/lean/Demo/Properties.lean @@ -9,7 +9,7 @@ namespace demo -- @[pspec] theorem mul2_add1_spec (x : U32) (h : 2 * ↑x + 1 ≤ U32.max) - : ∃ y, mul2_add1 x = ret y ∧ + : ∃ y, mul2_add1 x = ok y ∧ ↑y = 2 * ↑x + (1 : Int) := by rw [mul2_add1] @@ -18,7 +18,7 @@ theorem mul2_add1_spec (x : U32) (h : 2 * ↑x + 1 ≤ U32.max) simp; scalar_tac theorem use_mul2_add1_spec (x : U32) (y : U32) (h : 2 * ↑x + 1 + ↑y ≤ U32.max) : - ∃ z, use_mul2_add1 x y = ret z ∧ + ∃ z, use_mul2_add1 x y = ok z ∧ ↑z = 2 * ↑x + (1 : Int) + ↑y := by rw [use_mul2_add1] progress with mul2_add1_spec as ⟨ i ⟩ @@ -34,7 +34,7 @@ open CList theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) (h : ↑i < l.to_list.len) : - ∃ x, list_nth T l i = ret x ∧ + ∃ x, list_nth T l i = ok x ∧ x = l.to_list.index ↑i := by rw [list_nth] @@ -52,7 +52,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) simp_all theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) : - ∃ y, i32_id x = ret y ∧ x.val = y.val := by + ∃ y, i32_id x = ok y ∧ x.val = y.val := by rw [i32_id] if hx : x = 0#i32 then simp_all @@ -66,8 +66,8 @@ termination_by x.val.toNat decreasing_by scalar_decr_tac theorem list_tail_spec {T : Type} [Inhabited T] (l : CList T) : - ∃ back, list_tail T l = ret (CList.CNil, back) ∧ - ∀ tl', ∃ l', back tl' = ret l' ∧ l'.to_list = l.to_list ++ tl'.to_list := by + ∃ back, list_tail T l = ok (CList.CNil, back) ∧ + ∀ tl', ∃ l', back tl' = ok l' ∧ l'.to_list = l.to_list ++ tl'.to_list := by rw [list_tail] match l with | CNil => diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index 4e0ca509..fcaf5806 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -59,7 +59,7 @@ def distinct_keys (ls : Core.List (Usize × α)) := ls.pairwise_rel (λ x y => x def hash_mod_key (k : Usize) (l : Int) : Int := match hash_key k with - | .ret k => k.val % l + | .ok k => k.val % l | _ => 0 @[simp] @@ -121,7 +121,7 @@ theorem insert_in_list_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) ( (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v) (hdk : distinct_keys l0.v) : ∃ b l1, - insert_in_list α key value l0 = ret (b, l1) ∧ + insert_in_list α key value l0 = ok (b, l1) ∧ -- The boolean is true ↔ we inserted a new binding (b ↔ (l0.lookup key = none)) ∧ -- We update the binding @@ -183,7 +183,7 @@ theorem insert_in_list_spec {α : Type} (l : Int) (key: Usize) (value: α) (l0: (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v) (hdk : distinct_keys l0.v) : ∃ b l1, - insert_in_list α key value l0 = ret (b, l1) ∧ + insert_in_list α key value l0 = ok (b, l1) ∧ (b ↔ (l0.lookup key = none)) ∧ -- We update the binding l1.lookup key = value ∧ @@ -240,7 +240,7 @@ set_option maxHeartbeats 2000000 theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value : α) (hinv : hm.inv) (hnsat : hm.lookup key = none → hm.len_s < Usize.max) : - ∃ nhm, hm.insert_no_resize α key value = ret nhm ∧ + ∃ nhm, hm.insert_no_resize α key value = ok nhm ∧ -- We preserve the invariant nhm.inv ∧ -- We updated the binding for key @@ -253,7 +253,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value | some _ => nhm.len_s = hm.len_s) := by rw [insert_no_resize] -- Simplify. Note that this also simplifies some function calls, like array index - simp [hash_key, bind_tc_ret] + simp [hash_key, bind_tc_ok] have _ : (alloc.vec.Vec.len (List α) hm.slots).val ≠ 0 := by intro simp_all [inv] @@ -281,7 +281,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value rw [if_update_eq] -- TODO: necessary because we don't have a join -- TODO: progress to ... have hipost : - ∃ i0, (if inserted = true then hm.num_entries + Usize.ofInt 1 else pure hm.num_entries) = ret i0 ∧ + ∃ i0, (if inserted = true then hm.num_entries + Usize.ofInt 1 else pure hm.num_entries) = ok i0 ∧ i0.val = if inserted then hm.num_entries.val + 1 else hm.num_entries.val := by if inserted then @@ -328,7 +328,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value -- TODO: we want to automate this simp only [k_hash_mod] have h := Int.emod_lt_of_pos k.val hvpos - simp_all only [ret.injEq, exists_eq_left', List.len_update, gt_iff_lt, + simp_all only [ok.injEq, exists_eq_left', List.len_update, gt_iff_lt, List.index_update_eq, ne_eq, not_false_eq_true, neq_imp] if h_hm : k_hash_mod = hash_mod.val then simp_all only [k_hash_mod, List.len_update, gt_iff_lt, List.index_update_eq, diff --git a/tests/lean/Tutorial.lean b/tests/lean/Tutorial.lean index d92b2dd7..94b70991 100644 --- a/tests/lean/Tutorial.lean +++ b/tests/lean/Tutorial.lean @@ -18,7 +18,7 @@ namespace Tutorial def mul2_add1 (x : U32) : Result U32 := do let x1 ← x + x let x2 ← x1 + 1#u32 - ret x2 + ok x2 /- There are several things to note. @@ -75,9 +75,9 @@ def mul2_add1 (x : U32) : Result U32 := do -/ def mul2_add1_desugared (x : U32) : Result U32 := match Scalar.add x x with - | ret x1 => -- Success case + | ok x1 => -- Success case match Scalar.add x1 (U32.ofInt 1) with - | ret x2 => ret x2 + | ok x2 => ok x2 | error => error | error => error -- Propagating the errors @@ -105,7 +105,7 @@ theorem mul2_add1_spec -/ (h : 2 * ↑x + 1 ≤ U32.max) /- The postcondition -/ - : ∃ y, mul2_add1 x = ret y ∧ -- The call succeeds + : ∃ y, mul2_add1 x = ok y ∧ -- The call succeeds ↑ y = 2 * ↑x + (1 : Int) -- The output has the expected value := by /- The proof -/ @@ -154,7 +154,7 @@ theorem mul2_add1_spec -/ @[pspec] -- the [pspec] attribute saves the theorem in a database, for [progress] to use it theorem mul2_add1_spec2 (x : U32) (h : 2 * ↑x + 1 ≤ U32.max) - : ∃ y, mul2_add1 x = ret y ∧ + : ∃ y, mul2_add1 x = ok y ∧ ↑ y = 2 * ↑x + (1 : Int) := by rw [mul2_add1] @@ -172,7 +172,7 @@ def use_mul2_add1 (x : U32) (y : U32) : Result U32 := do @[pspec] theorem use_mul2_add1_spec (x : U32) (y : U32) (h : 2 * ↑x + 1 + ↑y ≤ U32.max) : - ∃ z, use_mul2_add1 x y = ret z ∧ + ∃ z, use_mul2_add1 x y = ok z ∧ ↑z = 2 * ↑x + (1 : Int) + ↑y := by rw [use_mul2_add1] -- Here we use [progress] on [mul2_add1] @@ -230,7 +230,7 @@ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T := match l with | CCons x tl => if i = 0#u32 - then ret x + then ok x else do let i1 ← i - 1#u32 list_nth T tl i1 @@ -263,7 +263,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) -- Precondition: the index is in bounds (h : ↑i < l.to_list.len) -- Postcondition - : ∃ x, list_nth T l i = ret x ∧ + : ∃ x, list_nth T l i = ok x ∧ -- [x] is the ith element of [l] after conversion to [List] x = l.to_list.index ↑i := by @@ -340,7 +340,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) If in a theorem we state and prove that: ``` - ∃ y, i32_id x = ret x + ∃ y, i32_id x = ok x ``` we not only prove that the function doesn't fail, but also that it terminates. @@ -348,7 +348,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) annotates it with the [divergent] keyword. -/ divergent def i32_id (x : I32) : Result I32 := - if x = 0#i32 then ret 0#i32 + if x = 0#i32 then ok 0#i32 else do let x1 ← x - 1#i32 let x2 ← i32_id x1 @@ -356,7 +356,7 @@ divergent def i32_id (x : I32) : Result I32 := /- We can easily prove that [i32_id] behaves like the identity on positive inputs -/ theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) : - ∃ y, i32_id x = ret y ∧ x.val = y.val := by + ∃ y, i32_id x = ok y ∧ x.val = y.val := by rw [i32_id] if hx : x = 0#i32 then simp_all |