From 3dfa0309f4325757d971c6322bff28c84d0726a0 Mon Sep 17 00:00:00 2001 From: Mark Dittmer Date: Wed, 22 Jul 2026 14:27:11 +0000 Subject: [PATCH 1/5] Introduce `ub` variant for `Result` This change introduces a `Result` variant intended to model undefined behaviour (UB). The intent is to allow unsafe definitions and theorems to introduce proof obligations that formalize the conditions under which unsafe operations introduce undefined behaviour. Using a `Result` variant provides a natural abstraction asserting that undefined behaviour at a particular step determines all subsequent behaviour as undefined. Towards #1225 --- backends/lean/Aeneas/Std/Primitives.lean | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/backends/lean/Aeneas/Std/Primitives.lean b/backends/lean/Aeneas/Std/Primitives.lean index e7712225d..93c950e34 100644 --- a/backends/lean/Aeneas/Std/Primitives.lean +++ b/backends/lean/Aeneas/Std/Primitives.lean @@ -63,6 +63,7 @@ open Error inductive Result (α : Type u) where | ok (v: α): Result α | fail (e: Error): Result α + | ub | div deriving Repr, BEq @@ -82,12 +83,12 @@ instance Result_Nonempty (α : Type u) : Nonempty (Result α) := def ok? {α: Type u} (r: Result α): Bool := match r with | ok _ => true - | fail _ | div => false + | fail _ | ub | div => false def div? {α: Type u} (r: Result α): Bool := match r with | div => true - | ok _ | fail _ => false + | ok _ | fail _ | ub => false def massert (b : Prop) [Decidable b] : Result Unit := if b then ok () else fail assertionFailure @@ -119,6 +120,7 @@ def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Resu match x with | ok v => f v | fail v => fail v + | ub => ub | div => div -- Allows using Result in do-blocks @@ -131,6 +133,7 @@ instance : Pure Result where @[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_ub (f : α → Result β) : bind .ub f = .ub := by simp [bind] @[simp] theorem bind_div (f : α → Result β) : bind .div f = .div := by simp [bind] @[simp] theorem bind_tc_ok (x : α) (f : α → Result β) : @@ -139,6 +142,9 @@ instance : Pure Result where @[simp] theorem bind_tc_fail (x : Error) (f : α → Result β) : (do let y ← fail x; f y) = fail x := by simp [Bind.bind, bind] +@[simp] theorem bind_tc_ub (f : α → Result β) : + (do let y ← ub; f y) = ub := by simp [Bind.bind, bind] + @[simp] theorem bind_tc_div (f : α → Result β) : (do let y ← div; f y) = div := by simp [Bind.bind, bind] @@ -178,6 +184,7 @@ noncomputable instance : MonoBind Result where · exact h _ · exact FlatOrder.rel.refl · exact FlatOrder.rel.refl + . exact FlatOrder.rel.refl end Order @@ -284,6 +291,7 @@ def loop {α : Type u} {β : Type v} (body : α → Result (ControlFlow α β)) | ControlFlow.cont x => loop body x | ControlFlow.done x => ok x | fail e => fail e + | ub => ub | div => div partial_fixpoint From aede11d2faca56543c03f66f5ba2825b77d8f28d Mon Sep 17 00:00:00 2001 From: Mark Dittmer Date: Wed, 22 Jul 2026 19:56:13 +0000 Subject: [PATCH 2/5] Repair cases in `WP` and `Ops` to support `Result.ub` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Repairs deliberately map `.ub => ⟨False⟩` in `mvcgen` bindings for `Result.instWP`. This matches the intuition that UB should be forbidden rather than another case for reasoning about weakest preconditions. Towards #1225 --- backends/lean/Aeneas/Std/Core/Ops.lean | 1 + backends/lean/Aeneas/Std/WP.lean | 17 ++++++++++++++++- 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/backends/lean/Aeneas/Std/Core/Ops.lean b/backends/lean/Aeneas/Std/Core/Ops.lean index 2063c3e3d..3e291b6c6 100644 --- a/backends/lean/Aeneas/Std/Core/Ops.lean +++ b/backends/lean/Aeneas/Std/Core/Ops.lean @@ -77,6 +77,7 @@ def BuiltinFnMut (Inputs : Type u) (Outputs : Type v) : core.ops.function.FnMut match f x with | ok y => ok (y, f) | fail e => fail e + | ub => ub | div => div } diff --git a/backends/lean/Aeneas/Std/WP.lean b/backends/lean/Aeneas/Std/WP.lean index 84b6a8404..6cdf76618 100644 --- a/backends/lean/Aeneas/Std/WP.lean +++ b/backends/lean/Aeneas/Std/WP.lean @@ -19,6 +19,7 @@ def theta (m:Result α) : Wp α := match m with | ok x => wp_return x | fail _ => fun _ => False + | ub => fun _ => False | div => fun _ => False def spec {α} (x:Result α) (p:Post α) := @@ -28,6 +29,7 @@ def dspec {α} (x:Result α) (p:Post α) := match x with | ok x => p x | fail _ => False + | ub => False | div => True theorem spec_dspec (α) (x : Result α) (p: Post α) : spec x p → dspec x p := by @@ -61,6 +63,9 @@ theorem spec_ok (x : α) : spec (ok x) p ↔ p x := by simp [spec, theta, wp_ret @[simp, grind =, agrind =] theorem spec_fail (e : Error) : spec (fail e) p ↔ False := by simp [spec, theta] +@[simp, grind =, agrind =] +theorem spec_ub : spec ub p ↔ False := by simp [spec, theta] + @[simp, grind =, agrind =] theorem spec_div : spec div p ↔ False := by simp [spec, theta] @@ -77,6 +82,10 @@ theorem spec_ok_pair {α β} (a : α) (b : β) (f : α → β → Prop) : theorem spec_fail_pair (e : Error) (f : α → β → Prop) : spec (fail e) (uncurry f) ↔ False := by simp +@[simp, grind =, agrind =] +theorem spec_ub_pair (f : α → β → Prop) : + spec ub (uncurry f) ↔ False := by simp + @[simp, grind =, agrind =] theorem spec_div_pair (f : α → β → Prop) : spec div (uncurry f) ↔ False := by simp @@ -101,6 +110,8 @@ theorem spec_bind {α β} {k : α -> Result β} {Pₖ : Post β} {m : Result α} apply Hm · simp apply Hm + · simp + apply Hm /-- Small helper to currify functions -/ def curry {α β γ} (f : α × β → γ) (x : α) : β → γ := fun y => f (x, y) @@ -149,6 +160,8 @@ theorem spec_bind' {α β} {k : α -> Result β} {Pₖ : Post β} {m : Result α apply Hm · simp apply Hm + · simp + apply Hm /-- We use this lemma to decompose nested `uncurry'` predicates into a sequence of universal quantifiers. -/ @[simp] @@ -216,6 +229,8 @@ theorem dspec_bind' {α β} {k : α -> Result β} {Pₖ : Post β} {m : Result apply Hm · simp apply Hm + · simp + apply Hm @[simp] def qimp_dspec_uncurry' {α₀ α₁ β} (P : α₀ → α₁ → Prop) (k : α₀ × α₁ → Result β) (Q : β → Prop) : @@ -791,7 +806,7 @@ open Std.Do instance Result.instWP : WP Result.{u} (.except (ULift Error) (.except PUnit .pure)) where wp x := { - trans Q := match x with | .ok a => Q.1 a | .fail e => Q.2.1 (ULift.up e) | .div => Q.2.2.1 .unit + trans Q := match x with | .ok a => Q.1 a | .fail e => Q.2.1 (ULift.up e) | .ub => ⟨False⟩ | .div => Q.2.2.1 .unit conjunctiveRaw Q₁ Q₂ := by apply SPred.bientails.of_eq cases x <;> simp From 733cb792fcce8574668388a01d3c28401ab025db Mon Sep 17 00:00:00 2001 From: Mark Dittmer Date: Wed, 22 Jul 2026 20:27:25 +0000 Subject: [PATCH 3/5] Repair cases in `Mul` and `Core` to support `Result.ub` Towards #1225 --- backends/lean/Aeneas/Std/Array/Core.lean | 1 + backends/lean/Aeneas/Std/Scalar/Ops/Mul.lean | 6 ++-- tests/lean/Adt.lean | 4 +-- tests/lean/AdtBorrows.lean | 8 ++--- tests/lean/ArraySliceIndex.lean | 3 +- tests/lean/Arrays.lean | 11 +++---- tests/lean/Avl/Funs.lean | 6 ++-- tests/lean/ChunksExact.lean | 3 +- tests/lean/Closures.lean | 6 ++-- tests/lean/Demo/Demo.lean | 4 +-- tests/lean/Drop.lean | 3 +- tests/lean/Issue789LoopCtxMatch.lean | 4 +-- tests/lean/IterAdapters.lean | 30 ++++++------------ tests/lean/Iterators.lean | 12 +++---- tests/lean/Joins.lean | 12 +++---- tests/lean/LoopSharedLoanInJoin.lean | 4 +-- tests/lean/Loops.lean | 33 +++++++------------- tests/lean/LoopsAdts.lean | 10 +++--- tests/lean/LoopsIssues.lean | 4 +-- tests/lean/LoopsNested.lean | 26 +++++++-------- tests/lean/LoopsRec.lean | 31 ++++++------------ tests/lean/LoopsSequences.lean | 8 ++--- tests/lean/NestedBorrows.lean | 11 +++---- tests/lean/OverflowingOps.lean | 24 +++++--------- tests/lean/RustBorrowCheckIssues.lean | 7 ++--- tests/lean/Scalars.lean | 3 +- tests/lean/Tutorial/Tutorial.lean | 7 ++--- 27 files changed, 113 insertions(+), 168 deletions(-) diff --git a/backends/lean/Aeneas/Std/Array/Core.lean b/backends/lean/Aeneas/Std/Array/Core.lean index 9d2cdf044..41ff6efee 100644 --- a/backends/lean/Aeneas/Std/Array/Core.lean +++ b/backends/lean/Aeneas/Std/Array/Core.lean @@ -37,6 +37,7 @@ def List.clone (clone : α → Result α) (l : List α) : Result ({ l' : List α match h :List.mapM clone l with | ok v => ok ⟨ v, by have := List.mapM_Result_length h; scalar_tac ⟩ | fail e => fail e + | ub => ub | div => div @[step] diff --git a/backends/lean/Aeneas/Std/Scalar/Ops/Mul.lean b/backends/lean/Aeneas/Std/Scalar/Ops/Mul.lean index fc1ab6f61..fae2695f7 100644 --- a/backends/lean/Aeneas/Std/Scalar/Ops/Mul.lean +++ b/backends/lean/Aeneas/Std/Scalar/Ops/Mul.lean @@ -43,7 +43,8 @@ theorem UScalar.mul_equiv {ty} (x y : UScalar ty) : match mul x y with | ok z => x.val * y.val ≤ UScalar.max ty ∧ (↑z : Nat) = ↑x * ↑y ∧ z.bv = x.bv * y.bv | fail _ => UScalar.max ty < x.val * y.val - | .div => False := by + | ub => False + | div => False := by simp only [mul] have := tryMk_eq ty (x.val * y.val) split <;> simp_all only [inBounds, true_and, not_lt, gt_iff_lt] @@ -73,7 +74,8 @@ theorem IScalar.mul_equiv {ty} (x y : IScalar ty) : match mul x y with | ok z => IScalar.min ty ≤ x.val * y.val ∧ x.val * y.val ≤ IScalar.max ty ∧ z.val = x.val * y.val ∧ z.bv = x.bv * y.bv | fail _ => ¬(IScalar.min ty ≤ x.val * y.val ∧ x.val * y.val ≤ IScalar.max ty) - | .div => False := by + | ub => False + | div => False := by simp only [mul, not_and, not_le] have := tryMk_eq ty (x.val * y.val) split <;> simp_all only [inBounds, min, max, true_and, not_and, not_lt] <;> diff --git a/tests/lean/Adt.lean b/tests/lean/Adt.lean index f99cbd9c1..b4f063030 100644 --- a/tests/lean/Adt.lean +++ b/tests/lean/Adt.lean @@ -37,7 +37,7 @@ def BigStructName := Unit /-- [adt::BigStruct] Source: 'tests/src/adt.rs', lines 17:0-24:2 -/ def BigStruct := - BigStructName × BigStructName × BigStructName × BigStructName × - BigStructName × BigStructName + BigStructName × BigStructName × BigStructName × BigStructName × BigStructName + × BigStructName end adt diff --git a/tests/lean/AdtBorrows.lean b/tests/lean/AdtBorrows.lean index 455ecdc5b..674c35aaa 100644 --- a/tests/lean/AdtBorrows.lean +++ b/tests/lean/AdtBorrows.lean @@ -204,8 +204,8 @@ def MutWrapper2.unwrap Source: 'tests/src/adt-borrows.rs', lines 143:4-145:5 -/ def MutWrapper2.id {T : Type} (self : MutWrapper2 T) : - Result ((MutWrapper2 T) × (MutWrapper2 T → MutWrapper2 T) × (MutWrapper2 - T → MutWrapper2 T)) + Result ((MutWrapper2 T) × (MutWrapper2 T → MutWrapper2 T) × (MutWrapper2 T → + MutWrapper2 T)) := do let back'a := fun mw => { self with x := mw.x } let back'b := fun mw => { self with y := mw.y } @@ -227,8 +227,8 @@ def use_mut_wrapper2 : Result Unit := do Source: 'tests/src/adt-borrows.rs', lines 159:0-161:1 -/ def use_mut_wrapper2_id {T : Type} (x : MutWrapper2 T) : - Result ((MutWrapper2 T) × (MutWrapper2 T → MutWrapper2 T) × (MutWrapper2 - T → MutWrapper2 T)) + Result ((MutWrapper2 T) × (MutWrapper2 T → MutWrapper2 T) × (MutWrapper2 T → + MutWrapper2 T)) := do let (mw, id_back, id_back1) ← MutWrapper2.id x let back'a := fun mw1 => { x with x := (id_back { mw with x := mw1.x }).x } diff --git a/tests/lean/ArraySliceIndex.lean b/tests/lean/ArraySliceIndex.lean index 51415b432..ae649732d 100644 --- a/tests/lean/ArraySliceIndex.lean +++ b/tests/lean/ArraySliceIndex.lean @@ -61,8 +61,7 @@ def slice_use_index_mut_range_from Visibility: public -/ def slice_use_get_mut_range_from (s : Slice Std.U32) : - Result ((Option (Slice Std.U32)) × (Option (Slice Std.U32) → Slice - Std.U32)) + Result ((Option (Slice Std.U32)) × (Option (Slice Std.U32) → Slice Std.U32)) := do core.slice.Slice.get_mut (core.slice.index.SliceIndexRangeFromUsizeSlice Std.U32) s { start := 0#usize } diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index 00b7716b6..6e05cdbae 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -103,9 +103,7 @@ def index_slice {T : Type} (s : Slice T) (i : Std.Usize) : Result T := do Source: 'tests/src/arrays.rs', lines 65:0-67:1 Visibility: public -/ def index_mut_slice - {T : Type} (s : Slice T) (i : Std.Usize) : - Result (T × (T → Slice T)) - := do + {T : Type} (s : Slice T) (i : Std.Usize) : Result (T × (T → Slice T)) := do Slice.index_mut_usize s i /-- [arrays::slice_subslice_shared_]: @@ -504,8 +502,7 @@ def sum2 (s : Slice Std.U32) (s2 : Slice Std.U32) : Result Std.U32 := do Source: 'tests/src/arrays.rs', lines 294:0-297:1 Visibility: public -/ def f0 : Result Unit := do - let (s, _) ← - lift (Array.to_slice_mut (Array.make 2#usize [ 1#u32, 2#u32 ])) + let (s, _) ← lift (Array.to_slice_mut (Array.make 2#usize [ 1#u32, 2#u32 ])) let _ ← Slice.index_mut_usize s 0#usize ok () @@ -669,8 +666,8 @@ def sum_mut_slice def add_acc_loop.body (paSrc : Array Std.U32 256#usize) (peDst : Array Std.U32 256#usize) (i : Std.Usize) : - Result (ControlFlow ((Array Std.U32 256#usize) × (Array Std.U32 256#usize) - × Std.Usize) ((Array Std.U32 256#usize) × (Array Std.U32 256#usize))) + Result (ControlFlow ((Array Std.U32 256#usize) × (Array Std.U32 256#usize) × + Std.Usize) ((Array Std.U32 256#usize) × (Array Std.U32 256#usize))) := do if i < 256#usize then diff --git a/tests/lean/Avl/Funs.lean b/tests/lean/Avl/Funs.lean index 34be2c16a..1dcd1c4f8 100644 --- a/tests/lean/Avl/Funs.lean +++ b/tests/lean/Avl/Funs.lean @@ -131,8 +131,7 @@ def Node.insert_in_left let left ← core.option.Option.unwrap o1 if left.balance_factor <= 0#i8 then - let node1 ← - Node.rotate_right (Node.mk node.value o2 node.right i) left + let node1 ← Node.rotate_right (Node.mk node.value o2 node.right i) left ok (false, node1) else let node1 ← @@ -158,8 +157,7 @@ def Node.insert_in_right let right ← core.option.Option.unwrap o1 if right.balance_factor >= 0#i8 then - let node1 ← - Node.rotate_left (Node.mk node.value node.left o2 i) right + let node1 ← Node.rotate_left (Node.mk node.value node.left o2 i) right ok (false, node1) else let node1 ← diff --git a/tests/lean/ChunksExact.lean b/tests/lean/ChunksExact.lean index 4e6dab516..c73472e07 100644 --- a/tests/lean/ChunksExact.lean +++ b/tests/lean/ChunksExact.lean @@ -118,8 +118,7 @@ def test_chunks_exact_remainder_2 : Result Unit := do Source: 'tests/src/chunks_exact.rs', lines 61:0-73:1 Visibility: public -/ def test_chunks_exact_size_1 : Result Unit := do - let s ← - lift (Array.to_slice (Array.make 3#usize [ 10#u32, 20#u32, 30#u32 ])) + let s ← lift (Array.to_slice (Array.make 3#usize [ 10#u32, 20#u32, 30#u32 ])) let it ← core.slice.Slice.chunks_exact s 1#usize let (o, it1) ← core.slice.iter.IteratorChunksExact.next it let c1 ← core.option.Option.unwrap o diff --git a/tests/lean/Closures.lean b/tests/lean/Closures.lean index 75ee34250..a36f15d33 100644 --- a/tests/lean/Closures.lean +++ b/tests/lean/Closures.lean @@ -239,8 +239,7 @@ def call_closure2.closure_1.Insts.CoreOpsFunctionFnMutTupleU32.call_mut (state : call_closure2.closure_1) (_ : Unit) : Result (Std.U32 × call_closure2.closure_1) := do - let i ← - call_closure2.closure_1.Insts.CoreOpsFunctionFnTupleU32.call state () + let i ← call_closure2.closure_1.Insts.CoreOpsFunctionFnTupleU32.call state () ok (i, state) /-- [closures::call_closure2::{impl core::ops::function::FnOnce<(), u32> for closures::call_closure2::closure#1}::call_once]: @@ -337,8 +336,7 @@ def call_closure2.closure.Insts.CoreOpsFunctionFnTupleU32 : /-- [closures::call_closure2]: Source: 'tests/src/closures.rs', lines 38:0-41:1 -/ def call_closure2 : Result Std.U32 := do - let _ ← - call_closure call_closure2.closure.Insts.CoreOpsFunctionFnTupleU32 () + let _ ← call_closure call_closure2.closure.Insts.CoreOpsFunctionFnTupleU32 () call_closure call_closure2.closure_1.Insts.CoreOpsFunctionFnTupleU32 () /-- [closures::u8_id]: diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean index f4d1c0d29..63a805247 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -165,9 +165,7 @@ def Usize.Insts.DemoCounter : Counter Std.Usize := { Source: 'tests/src/demo.rs', lines 112:0-114:1 Visibility: public -/ def use_counter - {T : Type} (CounterInst : Counter T) (cnt : T) : - Result (Std.Usize × T) - := do + {T : Type} (CounterInst : Counter T) (cnt : T) : Result (Std.Usize × T) := do CounterInst.incr cnt /-- [demo::mod_add]: diff --git a/tests/lean/Drop.lean b/tests/lean/Drop.lean index a0119232e..795885c55 100644 --- a/tests/lean/Drop.lean +++ b/tests/lean/Drop.lean @@ -20,8 +20,7 @@ namespace drop def fill_loop.body {T : Type} (corecloneCloneInst : core.clone.Clone T) (value : T) (iter : core.ops.range.Range Std.Usize) (s : Slice T) : - Result (ControlFlow ((core.ops.range.Range Std.Usize) × (Slice T)) (Slice - T)) + Result (ControlFlow ((core.ops.range.Range Std.Usize) × (Slice T)) (Slice T)) := do let (o, iter1) ← core.iter.range.IteratorRange.next core.iter.range.StepUsize iter diff --git a/tests/lean/Issue789LoopCtxMatch.lean b/tests/lean/Issue789LoopCtxMatch.lean index afeb5baf5..9ad03a790 100644 --- a/tests/lean/Issue789LoopCtxMatch.lean +++ b/tests/lean/Issue789LoopCtxMatch.lean @@ -36,8 +36,8 @@ def f @[rust_loop_body] def the_loop_loop.body (s : S) (next_in : Slice Std.U8) : - Result (ControlFlow (S × (Slice Std.U8)) (Std.U8 × (Array Std.U8 4#usize) - × (Slice Std.U8) × Bool)) + Result (ControlFlow (S × (Slice Std.U8)) (Std.U8 × (Array Std.U8 4#usize) × + (Slice Std.U8) × Bool)) := do let (s1, to_slice_mut_back) ← lift (Array.to_slice_mut s.y) let ((done1, n), i, s2) ← f s.x next_in s1 diff --git a/tests/lean/IterAdapters.lean b/tests/lean/IterAdapters.lean index f1aee0526..9d4419a7d 100644 --- a/tests/lean/IterAdapters.lean +++ b/tests/lean/IterAdapters.lean @@ -18,8 +18,7 @@ namespace iter_adapters Source: 'tests/src/iter_adapters.rs', lines 14:0-24:1 Visibility: public -/ def test_enumerate_slice : Result Unit := do - let s ← - lift (Array.to_slice (Array.make 3#usize [ 10#u32, 20#u32, 30#u32 ])) + let s ← lift (Array.to_slice (Array.make 3#usize [ 10#u32, 20#u32, 30#u32 ])) let i ← core.slice.Slice.iter s let it ← core.iter.traits.iterator.Iterator.enumerate.trait_default @@ -103,8 +102,7 @@ def test_take_2 : Result Unit := do Source: 'tests/src/iter_adapters.rs', lines 50:0-54:1 Visibility: public -/ def test_take_0 : Result Unit := do - let s ← - lift (Array.to_slice (Array.make 3#usize [ 10#u32, 20#u32, 30#u32 ])) + let s ← lift (Array.to_slice (Array.make 3#usize [ 10#u32, 20#u32, 30#u32 ])) let i ← core.slice.Slice.iter s let it ← core.iter.traits.iterator.Iterator.take.trait_default @@ -303,8 +301,7 @@ def test_range_u64 : Result Unit := do @[rust_loop_body] def test_range_usize_loop.body (iter : core.ops.range.Range Std.Usize) (count : Std.Usize) : - Result (ControlFlow ((core.ops.range.Range Std.Usize) × Std.Usize) - Std.Usize) + Result (ControlFlow ((core.ops.range.Range Std.Usize) × Std.Usize) Std.Usize) := do let (o, iter1) ← core.iter.range.IteratorRange.next core.iter.range.StepUsize iter @@ -375,8 +372,7 @@ def test_range_empty : Result Unit := do Source: 'tests/src/iter_adapters.rs', lines 137:0-144:1 Visibility: public -/ def test_array_into_iter : Result Unit := do - let s ← - lift (Array.to_slice (Array.make 3#usize [ 10#u32, 20#u32, 30#u32 ])) + let s ← lift (Array.to_slice (Array.make 3#usize [ 10#u32, 20#u32, 30#u32 ])) let it ← core.slice.Slice.iter s let (o, it1) ← core.slice.iter.IteratorSliceIter.next it let i ← core.option.Option.unwrap o @@ -587,16 +583,14 @@ def test_range_u16_boundary : Result Unit := do { start := 0#u16, «end» := 3#u16 } let i ← core.option.Option.unwrap o massert (i = 0#u16) - let (o1, it1) ← - core.iter.range.IteratorRange.next core.iter.range.StepU16 it + let (o1, it1) ← core.iter.range.IteratorRange.next core.iter.range.StepU16 it let i1 ← core.option.Option.unwrap o1 massert (i1 = 1#u16) let (o2, it2) ← core.iter.range.IteratorRange.next core.iter.range.StepU16 it1 let i2 ← core.option.Option.unwrap o2 massert (i2 = 2#u16) - let (o3, _) ← - core.iter.range.IteratorRange.next core.iter.range.StepU16 it2 + let (o3, _) ← core.iter.range.IteratorRange.next core.iter.range.StepU16 it2 let b := core.option.Option.is_none o3 massert b @@ -612,12 +606,10 @@ def test_range_u32_boundary : Result Unit := do { start := 0#u32, «end» := 2#u32 } let i ← core.option.Option.unwrap o massert (i = 0#u32) - let (o1, it1) ← - core.iter.range.IteratorRange.next core.iter.range.StepU32 it + let (o1, it1) ← core.iter.range.IteratorRange.next core.iter.range.StepU32 it let i1 ← core.option.Option.unwrap o1 massert (i1 = 1#u32) - let (o2, _) ← - core.iter.range.IteratorRange.next core.iter.range.StepU32 it1 + let (o2, _) ← core.iter.range.IteratorRange.next core.iter.range.StepU32 it1 let b := core.option.Option.is_none o2 massert b @@ -633,16 +625,14 @@ def test_range_u64_boundary : Result Unit := do { start := 100#u64, «end» := 103#u64 } let i ← core.option.Option.unwrap o massert (i = 100#u64) - let (o1, it1) ← - core.iter.range.IteratorRange.next core.iter.range.StepU64 it + let (o1, it1) ← core.iter.range.IteratorRange.next core.iter.range.StepU64 it let i1 ← core.option.Option.unwrap o1 massert (i1 = 101#u64) let (o2, it2) ← core.iter.range.IteratorRange.next core.iter.range.StepU64 it1 let i2 ← core.option.Option.unwrap o2 massert (i2 = 102#u64) - let (o3, _) ← - core.iter.range.IteratorRange.next core.iter.range.StepU64 it2 + let (o3, _) ← core.iter.range.IteratorRange.next core.iter.range.StepU64 it2 let b := core.option.Option.is_none o3 massert b diff --git a/tests/lean/Iterators.lean b/tests/lean/Iterators.lean index cbf8daac3..c382c4847 100644 --- a/tests/lean/Iterators.lean +++ b/tests/lean/Iterators.lean @@ -101,8 +101,8 @@ def slice_iter_mut_while_loop0.body (back : core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) (b : Bool) : Result (ControlFlow ((core.slice.iter.IterMut Std.U16) × - (core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) × - Bool) (core.slice.iter.IterMut Std.U16)) + (core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) × Bool) + (core.slice.iter.IterMut Std.U16)) := do let (o, it1, next_back) ← core.slice.iter.IteratorIterMut.next it match o with @@ -205,8 +205,8 @@ def slice_iter_mut_while_early_return_loop0.body (back : core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) (b : Bool) : Result (ControlFlow ((core.slice.iter.IterMut Std.U16) × - (core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) × - Bool) (core.slice.iter.IterMut Std.U16)) + (core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) × Bool) + (core.slice.iter.IterMut Std.U16)) := do let (o, it1, next_back) ← core.slice.iter.IteratorIterMut.next it match o with @@ -270,8 +270,8 @@ def slice_iter_mut_while_early_return_two_bools_loop0.body (back : core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) (b0 : Bool) (b1 : Bool) : Result (ControlFlow ((core.slice.iter.IterMut Std.U16) × - (core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) × - Bool × Bool) (core.slice.iter.IterMut Std.U16)) + (core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) × Bool + × Bool) (core.slice.iter.IterMut Std.U16)) := do let (o, it1, next_back) ← core.slice.iter.IteratorIterMut.next it match o with diff --git a/tests/lean/Joins.lean b/tests/lean/Joins.lean index 4fad829e1..461cea13f 100644 --- a/tests/lean/Joins.lean +++ b/tests/lean/Joins.lean @@ -18,19 +18,19 @@ namespace joins Source: 'tests/src/joins.rs', lines 4:0-7:1 -/ def opt_add_1 (b : Bool) (x : Std.U32) : Result Std.U32 := do let y ← if b - then ok 1#u32 - else ok 0#u32 + then ok 1#u32 + else ok 0#u32 x + y /-- [joins::opt_add_2]: Source: 'tests/src/joins.rs', lines 9:0-13:1 -/ def opt_add_2 (b : Bool) (x : Std.U32) : Result Std.U32 := do let y ← if b - then ok 1#u32 - else ok 0#u32 + then ok 1#u32 + else ok 0#u32 let z ← if b - then ok 1#u32 - else ok 0#u32 + then ok 1#u32 + else ok 0#u32 let i ← x + y i + z diff --git a/tests/lean/LoopSharedLoanInJoin.lean b/tests/lean/LoopSharedLoanInJoin.lean index aab74d806..5166a7e6a 100644 --- a/tests/lean/LoopSharedLoanInJoin.lean +++ b/tests/lean/LoopSharedLoanInJoin.lean @@ -69,8 +69,8 @@ def State.extract_loop.body (a : Array Std.U64 4#usize) (i1 : Std.U32) (result : Slice Std.U64) (lane_index : Std.Usize) : Result (ControlFlow ((core.ops.range.Range Std.Usize) × (Array Std.U64 - 4#usize) × Std.U32 × (Slice Std.U64) × Std.Usize) ((Array Std.U64 - 4#usize) × Std.U32 × (Slice Std.U64))) + 4#usize) × Std.U32 × (Slice Std.U64) × Std.Usize) ((Array Std.U64 4#usize) + × Std.U32 × (Slice Std.U64))) := do let (o, iter1) ← core.iter.range.IteratorRange.next core.iter.range.StepUsize iter diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index a84c0f1b6..845ebaa2a 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -450,9 +450,7 @@ def list_nth_mut_pair Visibility: public -/ @[rust_loop] def list_nth_shared_pair_loop - {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : - Result (T × T) - := do + {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : Result (T × T) := do match ls0 with | List.Cons x0 tl0 => match ls1 with @@ -470,9 +468,7 @@ partial_fixpoint Visibility: public -/ @[reducible] def list_nth_shared_pair - {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : - Result (T × T) - := do + {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : Result (T × T) := do list_nth_shared_pair_loop ls0 ls1 i /-- [loops::list_nth_mut_pair_merge]: loop 0: @@ -522,9 +518,7 @@ def list_nth_mut_pair_merge Visibility: public -/ @[rust_loop] def list_nth_shared_pair_merge_loop - {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : - Result (T × T) - := do + {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : Result (T × T) := do match ls0 with | List.Cons x0 tl0 => match ls1 with @@ -542,9 +536,7 @@ partial_fixpoint Visibility: public -/ @[reducible] def list_nth_shared_pair_merge - {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : - Result (T × T) - := do + {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : Result (T × T) := do list_nth_shared_pair_merge_loop ls0 ls1 i /-- [loops::list_nth_mut_shared_pair]: loop 0: @@ -909,8 +901,8 @@ def issue270 (v : List (List Std.U8)) : Result (Option (List Std.U8)) := do def issue400_1_loop.body (cond : Bool) (back : Std.I32 → (Std.I32 × Std.I32)) (y : Std.I32) (i : Std.I32) : - Result (ControlFlow ((Std.I32 → (Std.I32 × Std.I32)) × Std.I32 × - Std.I32) (Std.I32 × Std.I32)) + Result (ControlFlow ((Std.I32 → (Std.I32 × Std.I32)) × Std.I32 × Std.I32) + (Std.I32 × Std.I32)) := do if i < 32#i32 then @@ -949,11 +941,11 @@ def issue400_1 @[rust_loop_body] def issue400_2_loop.body (conds : Slice Bool) - (back : Std.I32 → Std.I32 → (Std.I32 × Std.I32 × Std.I32)) - (y : Std.I32) (z : Std.I32) (i : Std.Usize) : - Result (ControlFlow ((Std.I32 → Std.I32 → (Std.I32 × Std.I32 × - Std.I32)) × Std.I32 × Std.I32 × Std.Usize) (Std.I32 × Std.I32 × - (Std.I32 → Std.I32 → (Std.I32 × Std.I32 × Std.I32)))) + (back : Std.I32 → Std.I32 → (Std.I32 × Std.I32 × Std.I32)) (y : Std.I32) + (z : Std.I32) (i : Std.Usize) : + Result (ControlFlow ((Std.I32 → Std.I32 → (Std.I32 × Std.I32 × Std.I32)) × + Std.I32 × Std.I32 × Std.Usize) (Std.I32 × Std.I32 × (Std.I32 → Std.I32 → + (Std.I32 × Std.I32 × Std.I32)))) := do let i1 := Slice.len conds if i < i1 @@ -988,8 +980,7 @@ def issue400_2 (a : Std.I32) (b : Std.I32) (c : Std.I32) (conds : Slice Bool) : Result (Std.I32 × Std.I32 × Std.I32) := do - let (y, z, back) ← - issue400_2_loop (fun i i1 => (i, i1, c)) conds a b 0#usize + let (y, z, back) ← issue400_2_loop (fun i i1 => (i, i1, c)) conds a b 0#usize let y1 ← y + 3#i32 let z1 ← z + 5#i32 ok (back y1 z1) diff --git a/tests/lean/LoopsAdts.lean b/tests/lean/LoopsAdts.lean index 5e3d80e40..c0d74be41 100644 --- a/tests/lean/LoopsAdts.lean +++ b/tests/lean/LoopsAdts.lean @@ -97,8 +97,8 @@ def update_array_mut_borrow def array_mut_borrow_loop1_loop.body (back : Array Std.U32 32#usize → Array Std.U32 32#usize) (b : Bool) (a : Array Std.U32 32#usize) : - Result (ControlFlow ((Array Std.U32 32#usize → Array Std.U32 32#usize) × - Bool × (Array Std.U32 32#usize)) (Array Std.U32 32#usize)) + Result (ControlFlow ((Array Std.U32 32#usize → Array Std.U32 32#usize) × Bool + × (Array Std.U32 32#usize)) (Array Std.U32 32#usize)) := do if b then @@ -137,9 +137,9 @@ def array_mut_borrow_loop1 def array_mut_borrow_loop2_loop.body (back : Array Std.U32 32#usize → Array Std.U32 32#usize) (b : Bool) (a : Array Std.U32 32#usize) : - Result (ControlFlow ((Array Std.U32 32#usize → Array Std.U32 32#usize) × - Bool × (Array Std.U32 32#usize)) ((Array Std.U32 32#usize) × (Array - Std.U32 32#usize → Array Std.U32 32#usize))) + Result (ControlFlow ((Array Std.U32 32#usize → Array Std.U32 32#usize) × Bool + × (Array Std.U32 32#usize)) ((Array Std.U32 32#usize) × (Array Std.U32 + 32#usize → Array Std.U32 32#usize))) := do if b then diff --git a/tests/lean/LoopsIssues.lean b/tests/lean/LoopsIssues.lean index 93dd4b548..1644d2913 100644 --- a/tests/lean/LoopsIssues.lean +++ b/tests/lean/LoopsIssues.lean @@ -178,8 +178,8 @@ def test_loop.body if b0 then let buf1 ← if b1 - then write buf - else ok buf + then write buf + else ok buf read buf1 ok (cont (true, buf1)) else ok (done ()) diff --git a/tests/lean/LoopsNested.lean b/tests/lean/LoopsNested.lean index dfc2dd8f0..29723cf46 100644 --- a/tests/lean/LoopsNested.lean +++ b/tests/lean/LoopsNested.lean @@ -97,10 +97,9 @@ def sum_loop0.body Result (ControlFlow (Std.U32 × Std.U32) Std.U32) := do if i < m - then - let s1 ← sum_loop0_loop0 n s 0#u32 - let i1 ← i + 1#u32 - ok (cont (s1, i1)) + then let s1 ← sum_loop0_loop0 n s 0#u32 + let i1 ← i + 1#u32 + ok (cont (s1, i1)) else ok (done s) /-- [loops_nested::sum]: loop 0: @@ -131,10 +130,9 @@ def update_array_loop0_loop0.body 4#usize)) := do if j < 4#usize - then - let a ← Array.update out j 1#u8 - let j1 ← j + 1#usize - ok (cont (a, j1)) + then let a ← Array.update out j 1#u8 + let j1 ← j + 1#usize + ok (cont (a, j1)) else ok (done out) /-- [loops_nested::update_array]: loop 1: @@ -336,8 +334,8 @@ def sample_ntt @[rust_loop_body] def generate_matrix_inner_loop.body (key : Key) (state : Array Std.U8 8#usize) (j : Std.Usize) : - Result (ControlFlow (Key × (Array Std.U8 8#usize) × Std.Usize) (Key × - (Array Std.U8 8#usize))) + Result (ControlFlow (Key × (Array Std.U8 8#usize) × Std.Usize) (Key × (Array + Std.U8 8#usize))) := do if j < 4#usize then @@ -377,8 +375,8 @@ def generate_matrix_loop0_loop0.body (state_base : Array Std.U8 8#usize) (i : Std.U8) (key : Key) (state_work : Array Std.U8 8#usize) (coordinates : Array Std.U8 2#usize) (j : Std.U8) : - Result (ControlFlow (Key × (Array Std.U8 8#usize) × (Array Std.U8 2#usize) - × Std.U8) (Key × (Array Std.U8 8#usize) × (Array Std.U8 2#usize))) + Result (ControlFlow (Key × (Array Std.U8 8#usize) × (Array Std.U8 2#usize) × + Std.U8) (Key × (Array Std.U8 8#usize) × (Array Std.U8 2#usize))) := do if j < 4#u8 then @@ -420,8 +418,8 @@ def generate_matrix_loop0.body (state_base : Array Std.U8 8#usize) (key : Key) (state_work : Array Std.U8 8#usize) (coordinates : Array Std.U8 2#usize) (i : Std.U8) : - Result (ControlFlow (Key × (Array Std.U8 8#usize) × (Array Std.U8 2#usize) - × Std.U8) (Key × (Array Std.U8 8#usize))) + Result (ControlFlow (Key × (Array Std.U8 8#usize) × (Array Std.U8 2#usize) × + Std.U8) (Key × (Array Std.U8 8#usize))) := do if i < 4#u8 then diff --git a/tests/lean/LoopsRec.lean b/tests/lean/LoopsRec.lean index 83d649316..b75f99b0a 100644 --- a/tests/lean/LoopsRec.lean +++ b/tests/lean/LoopsRec.lean @@ -58,10 +58,9 @@ def sum (max : Std.U32) : Result Std.U32 := do def sum_with_mut_borrows_loop (max : Std.U32) (i : Std.U32) (s : Std.U32) : Result Std.U32 := do if i < max - then - let ms ← s + i - let mi ← i + 1#u32 - sum_with_mut_borrows_loop max mi ms + then let ms ← s + i + let mi ← i + 1#u32 + sum_with_mut_borrows_loop max mi ms else ok s partial_fixpoint @@ -387,9 +386,7 @@ def list_nth_mut_pair Visibility: public -/ @[rust_loop] def list_nth_shared_pair_loop - {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : - Result (T × T) - := do + {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : Result (T × T) := do match ls0 with | List.Cons x0 tl0 => match ls1 with @@ -407,9 +404,7 @@ partial_fixpoint Visibility: public -/ @[reducible] def list_nth_shared_pair - {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : - Result (T × T) - := do + {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : Result (T × T) := do list_nth_shared_pair_loop ls0 ls1 i /-- [loops_rec::list_nth_mut_pair_merge]: loop 0: @@ -459,9 +454,7 @@ def list_nth_mut_pair_merge Visibility: public -/ @[rust_loop] def list_nth_shared_pair_merge_loop - {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : - Result (T × T) - := do + {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : Result (T × T) := do match ls0 with | List.Cons x0 tl0 => match ls1 with @@ -479,9 +472,7 @@ partial_fixpoint Visibility: public -/ @[reducible] def list_nth_shared_pair_merge - {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : - Result (T × T) - := do + {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : Result (T × T) := do list_nth_shared_pair_merge_loop ls0 ls1 i /-- [loops_rec::list_nth_mut_shared_pair]: loop 0: @@ -765,9 +756,8 @@ def issue270.box_get_borrow {T : Type} (x : T) : Result T := do def issue270_loop (t : List (List Std.U8)) (last : List Std.U8) : Result (List Std.U8) := do match t with - | List.Cons ht tt => - let t1 ← issue270.box_get_borrow tt - issue270_loop t1 ht + | List.Cons ht tt => let t1 ← issue270.box_get_borrow tt + issue270_loop t1 ht | List.Nil => ok last partial_fixpoint @@ -839,8 +829,7 @@ def issue400_2 (a : Std.I32) (b : Std.I32) (c : Std.I32) (conds : Slice Bool) : Result (Std.I32 × Std.I32 × Std.I32) := do - let (y, z, back) ← - issue400_2_loop (fun i i1 => (i, i1, c)) conds a b 0#usize + let (y, z, back) ← issue400_2_loop (fun i i1 => (i, i1, c)) conds a b 0#usize let y1 ← y + 3#i32 let z1 ← z + 5#i32 ok (back y1 z1) diff --git a/tests/lean/LoopsSequences.lean b/tests/lean/LoopsSequences.lean index beda7f8d0..4473f9538 100644 --- a/tests/lean/LoopsSequences.lean +++ b/tests/lean/LoopsSequences.lean @@ -74,8 +74,8 @@ def key_expand_loop0.body (state_base : Array Std.U8 8#usize) (key : Key) (state_work : Array Std.U8 8#usize) (sample_buffer : Array Std.U8 1#usize) (i : Std.I32) : - Result (ControlFlow (Key × (Array Std.U8 8#usize) × (Array Std.U8 1#usize) - × Std.I32) (Key × (Array Std.U8 8#usize) × (Array Std.U8 1#usize))) + Result (ControlFlow (Key × (Array Std.U8 8#usize) × (Array Std.U8 1#usize) × + Std.I32) (Key × (Array Std.U8 8#usize) × (Array Std.U8 1#usize))) := do if i < 32#i32 then @@ -116,8 +116,8 @@ def key_expand_loop1.body (state_base : Array Std.U8 8#usize) (key : Key) (state_work : Array Std.U8 8#usize) (sample_buffer : Array Std.U8 1#usize) (i : Std.I32) : - Result (ControlFlow (Key × (Array Std.U8 8#usize) × (Array Std.U8 1#usize) - × Std.I32) (Key × (Array Std.U8 8#usize))) + Result (ControlFlow (Key × (Array Std.U8 8#usize) × (Array Std.U8 1#usize) × + Std.I32) (Key × (Array Std.U8 8#usize))) := do if i < 32#i32 then diff --git a/tests/lean/NestedBorrows.lean b/tests/lean/NestedBorrows.lean index 61b3b2b31..bcb8adb7e 100644 --- a/tests/lean/NestedBorrows.lean +++ b/tests/lean/NestedBorrows.lean @@ -45,8 +45,7 @@ def call_inner_mut : Result Unit := do Source: 'tests/src/nested-borrows.rs', lines 28:0-32:1 -/ def inner_mut_swap (ppx : Std.U32) (py : Std.U32) : - Result (Std.U32 × (Std.U32 → Std.U32) × (Std.U32 → (Std.U32 × - Std.U32))) + Result (Std.U32 × (Std.U32 → Std.U32) × (Std.U32 → (Std.U32 × Std.U32))) := do let back'b := fun ppx1 => (10#u32, ppx1) ok (py, fun ppx1 => ppx1, back'b) @@ -150,8 +149,8 @@ def iter_mut_loop {T : Type} (it : IterMut T) : Result (IterMut T) := do @[rust_loop_body] def iter_mut_incr_loop.body (back : IterMut Std.U32 → Option Std.U32) (it : IterMut Std.U32) : - Result (ControlFlow ((IterMut Std.U32 → Option Std.U32) × (IterMut - Std.U32)) (Option Std.U32)) + Result (ControlFlow ((IterMut Std.U32 → Option Std.U32) × (IterMut Std.U32)) + (Option Std.U32)) := do let (o, it1, next_back) ← IterMut.next it match o with @@ -312,8 +311,8 @@ def iter_list_while_loop0_loop0 (b : Bool) : Result Unit := do @[rust_loop_body] def iter_list_while_loop0.body {T : Type} (l : List T) (back : List T → List T) (b : Bool) : - Result (ControlFlow ((List T) × (List T → List T) × Bool) ((List T) × - (List T → List T))) + Result (ControlFlow ((List T) × (List T → List T) × Bool) ((List T) × (List T + → List T))) := do let (o, l1, next1_back) ← next1 l match o with diff --git a/tests/lean/OverflowingOps.lean b/tests/lean/OverflowingOps.lean index 341c93ba4..8fa7f62ab 100644 --- a/tests/lean/OverflowingOps.lean +++ b/tests/lean/OverflowingOps.lean @@ -16,8 +16,7 @@ namespace overflowing_ops /-- [overflowing_ops::u8_overflowing_add]: Source: 'tests/src/overflowing-ops.rs', lines 3:0-5:1 -/ -def u8_overflowing_add - (x : Std.U8) (y : Std.U8) : Result (Std.U8 × Bool) := do +def u8_overflowing_add (x : Std.U8) (y : Std.U8) : Result (Std.U8 × Bool) := do ok (core.num.U8.overflowing_add x y) /-- [overflowing_ops::u16_overflowing_add]: @@ -52,8 +51,7 @@ def usize_overflowing_add /-- [overflowing_ops::i8_overflowing_add]: Source: 'tests/src/overflowing-ops.rs', lines 22:0-24:1 -/ -def i8_overflowing_add - (x : Std.I8) (y : Std.I8) : Result (Std.I8 × Bool) := do +def i8_overflowing_add (x : Std.I8) (y : Std.I8) : Result (Std.I8 × Bool) := do ok (core.num.I8.overflowing_add x y) /-- [overflowing_ops::i16_overflowing_add]: @@ -88,8 +86,7 @@ def isize_overflowing_add /-- [overflowing_ops::u8_overflowing_sub]: Source: 'tests/src/overflowing-ops.rs', lines 41:0-43:1 -/ -def u8_overflowing_sub - (x : Std.U8) (y : Std.U8) : Result (Std.U8 × Bool) := do +def u8_overflowing_sub (x : Std.U8) (y : Std.U8) : Result (Std.U8 × Bool) := do ok (core.num.U8.overflowing_sub x y) /-- [overflowing_ops::u16_overflowing_sub]: @@ -124,8 +121,7 @@ def usize_overflowing_sub /-- [overflowing_ops::i8_overflowing_sub]: Source: 'tests/src/overflowing-ops.rs', lines 60:0-62:1 -/ -def i8_overflowing_sub - (x : Std.I8) (y : Std.I8) : Result (Std.I8 × Bool) := do +def i8_overflowing_sub (x : Std.I8) (y : Std.I8) : Result (Std.I8 × Bool) := do ok (core.num.I8.overflowing_sub x y) /-- [overflowing_ops::i16_overflowing_sub]: @@ -160,8 +156,7 @@ def isize_overflowing_sub /-- [overflowing_ops::u8_overflowing_mul]: Source: 'tests/src/overflowing-ops.rs', lines 79:0-81:1 -/ -def u8_overflowing_mul - (x : Std.U8) (y : Std.U8) : Result (Std.U8 × Bool) := do +def u8_overflowing_mul (x : Std.U8) (y : Std.U8) : Result (Std.U8 × Bool) := do ok (core.num.U8.overflowing_mul x y) /-- [overflowing_ops::u16_overflowing_mul]: @@ -196,8 +191,7 @@ def usize_overflowing_mul /-- [overflowing_ops::i8_overflowing_mul]: Source: 'tests/src/overflowing-ops.rs', lines 98:0-100:1 -/ -def i8_overflowing_mul - (x : Std.I8) (y : Std.I8) : Result (Std.I8 × Bool) := do +def i8_overflowing_mul (x : Std.I8) (y : Std.I8) : Result (Std.I8 × Bool) := do ok (core.num.I8.overflowing_mul x y) /-- [overflowing_ops::i16_overflowing_mul]: @@ -232,8 +226,7 @@ def isize_overflowing_mul /-- [overflowing_ops::u8_overflowing_div]: Source: 'tests/src/overflowing-ops.rs', lines 117:0-119:1 -/ -def u8_overflowing_div - (x : Std.U8) (y : Std.U8) : Result (Std.U8 × Bool) := do +def u8_overflowing_div (x : Std.U8) (y : Std.U8) : Result (Std.U8 × Bool) := do core.num.U8.overflowing_div x y /-- [overflowing_ops::u16_overflowing_div]: @@ -268,8 +261,7 @@ def usize_overflowing_div /-- [overflowing_ops::i8_overflowing_div]: Source: 'tests/src/overflowing-ops.rs', lines 136:0-138:1 -/ -def i8_overflowing_div - (x : Std.I8) (y : Std.I8) : Result (Std.I8 × Bool) := do +def i8_overflowing_div (x : Std.I8) (y : Std.I8) : Result (Std.I8 × Bool) := do core.num.I8.overflowing_div x y /-- [overflowing_ops::i16_overflowing_div]: diff --git a/tests/lean/RustBorrowCheckIssues.lean b/tests/lean/RustBorrowCheckIssues.lean index c2d0c0cc1..bf99020bc 100644 --- a/tests/lean/RustBorrowCheckIssues.lean +++ b/tests/lean/RustBorrowCheckIssues.lean @@ -21,8 +21,7 @@ namespace rust_borrow_check_issues Source: '/rustc/library/core/src/mem/mod.rs', lines 1000:0-1002:24 Name pattern: [core::mem::drop] Visibility: public -/ -@[rust_fun "core::mem::drop"] -axiom core.mem.drop {T : Type} : T → Result Unit +@[rust_fun "core::mem::drop"] axiom core.mem.drop {T : Type} : T → Result Unit /-- [core::option::{core::option::Option}::as_mut]: Source: '/rustc/library/core/src/option.rs', lines 763:4-763:52 @@ -43,8 +42,8 @@ def unnecessary_error : Result Unit := do Source: 'tests/src/rust-borrow-check-issues.rs', lines 35:0-52:1 -/ def unnecessary_error_2 (b0 : Bool) (b1 : Bool) : Result Unit := do let i ← if b0 - then ok 0#u32 - else ok 1#u32 + then ok 0#u32 + else ok 1#u32 let _ ← if b1 then do diff --git a/tests/lean/Scalars.lean b/tests/lean/Scalars.lean index b08de12b1..455284238 100644 --- a/tests/lean/Scalars.lean +++ b/tests/lean/Scalars.lean @@ -215,8 +215,7 @@ def test_is_multiple_of_zero_divisor : Result Unit := do Source: 'tests/src/scalars.rs', lines 158:0-160:1 Visibility: public -/ def test_try_from_usize_u32_ok : Result Unit := do - let r ← - core.convert.num.ptr_try_from_impls.TryFromU32Usize.try_from 5#usize + let r ← core.convert.num.ptr_try_from_impls.TryFromU32Usize.try_from 5#usize let b ← core.result.Result.is_ok r massert b diff --git a/tests/lean/Tutorial/Tutorial.lean b/tests/lean/Tutorial/Tutorial.lean index 7fc8cc012..aff766601 100644 --- a/tests/lean/Tutorial/Tutorial.lean +++ b/tests/lean/Tutorial/Tutorial.lean @@ -175,9 +175,7 @@ def Usize.Insts.TutorialCounter : Counter Std.Usize := { Source: 'src/lib.rs', lines 117:0-119:1 Visibility: public -/ def use_counter - {T : Type} (CounterInst : Counter T) (cnt : T) : - Result (Std.Usize × T) - := do + {T : Type} (CounterInst : Counter T) (cnt : T) : Result (Std.Usize × T) := do CounterInst.incr cnt /-- [tutorial::list_nth_mut1]: loop 0: @@ -211,8 +209,7 @@ def list_nth_mut1 Source: 'src/lib.rs', lines 135:4-137:5 Visibility: public -/ @[rust_loop] -def list_tail_loop - {T : Type} (l : CList T) : Result (CList T → CList T) := do +def list_tail_loop {T : Type} (l : CList T) : Result (CList T → CList T) := do match l with | CList.CCons t tl => let back ← list_tail_loop tl From f5ee235f52ec2a252c8835dcc91a4d52bcce0ac6 Mon Sep 17 00:00:00 2001 From: Mark Dittmer Date: Thu, 23 Jul 2026 02:08:09 +0000 Subject: [PATCH 4/5] Repair cases in `Slice` and `Vec` to support `Result.ub` Towards #1225 --- backends/lean/Aeneas/Std/Slice.lean | 5 +++++ backends/lean/Aeneas/Std/Vec.lean | 2 ++ 2 files changed, 7 insertions(+) diff --git a/backends/lean/Aeneas/Std/Slice.lean b/backends/lean/Aeneas/Std/Slice.lean index 16da42b2a..572cbad70 100644 --- a/backends/lean/Aeneas/Std/Slice.lean +++ b/backends/lean/Aeneas/Std/Slice.lean @@ -1012,6 +1012,7 @@ def Slice.mapM {α β} (f : α → Result β) (x : Slice α) : Result (Slice β match h : x.val.mapM f with | ok xs => ok ⟨xs, List.mapM_Result_length h ▸ x.prop⟩ | fail e => fail e + | ub => ub | div => div @[step] @@ -1047,6 +1048,7 @@ theorem Slice.mapM_spec {α β} {f : α → Result β} {s : Slice α} {post : Na exact hf case h_2 e heq => simp [hl'] at heq case h_3 heq => simp [hl'] at heq + case h_4 heq => simp [hl'] at heq -- ============================================================================ -- Slice.fill — overwrite every element with a clone of `v` @@ -1060,6 +1062,7 @@ def core.slice.Slice.fill {T : Type} (cloneInst : core.clone.Clone T) match h : s.val.mapM (fun _ => cloneInst.clone v) with | .ok val => .ok ⟨val, List.mapM_Result_length h ▸ s.property⟩ | .fail e => .fail e + | .ub => .ub | .div => .div private theorem List.mapM_const_ok {T : Type} (l : List T) @@ -1087,11 +1090,13 @@ theorem core.slice.Slice.fill.spec {T : Type} (cloneInst : core.clone.Clone T) | .ok v' => congr 1; have := hclone; rw [hc] at this; simp [WP.wp_return] at this; exact this | .fail _ => exfalso; have := hclone; rw [hc] at this; simp at this + | .ub => exfalso; have := hclone; rw [hc] at this; simp at this | .div => exfalso; have := hclone; rw [hc] at this; simp at this have hmapM := List.mapM_const_ok s.val hcl split · rename_i val heq; rw [hmapM] at heq; cases heq; simp [spec_ok, Slice.length, List.length_replicate] · exfalso; simp_all · exfalso; simp_all + · exfalso; simp_all end Aeneas.Std diff --git a/backends/lean/Aeneas/Std/Vec.lean b/backends/lean/Aeneas/Std/Vec.lean index c58199c4b..db7da624b 100644 --- a/backends/lean/Aeneas/Std/Vec.lean +++ b/backends/lean/Aeneas/Std/Vec.lean @@ -182,6 +182,7 @@ def Vec.index_mut_usize {α : Type u} (v: Vec α) (i: Usize) : | ok x => ok (x, Vec.set v i) | fail e => fail e + | ub => ub | div => div @[step] @@ -357,6 +358,7 @@ def alloc.vec.Vec.extend_from_slice {T : Type} (cloneInst : core.clone.Clone T) | ok s' => ok ⟨ v.val ++ s'.val , by have := Slice.clone_length h'; scalar_tac ⟩ | fail e => fail e + | ub => ub | div => div else fail .panic From c64320b45e12c0653779b21dc332805c1bcc0c2c Mon Sep 17 00:00:00 2001 From: Mark Dittmer Date: Thu, 23 Jul 2026 13:25:09 +0000 Subject: [PATCH 5/5] Format test files after `Result.ub` changes Towards #1225 --- tests/lean/Adt.lean | 4 ++-- tests/lean/AdtBorrows.lean | 8 +++---- tests/lean/ArraySliceIndex.lean | 3 ++- tests/lean/Arrays.lean | 11 +++++---- tests/lean/Avl/Funs.lean | 6 +++-- tests/lean/ChunksExact.lean | 3 ++- tests/lean/Closures.lean | 6 +++-- tests/lean/Demo/Demo.lean | 4 +++- tests/lean/Drop.lean | 3 ++- tests/lean/Issue789LoopCtxMatch.lean | 4 ++-- tests/lean/IterAdapters.lean | 30 ++++++++++++++++-------- tests/lean/Iterators.lean | 12 +++++----- tests/lean/Joins.lean | 12 +++++----- tests/lean/LoopSharedLoanInJoin.lean | 4 ++-- tests/lean/Loops.lean | 33 +++++++++++++++++---------- tests/lean/LoopsAdts.lean | 10 ++++---- tests/lean/LoopsIssues.lean | 4 ++-- tests/lean/LoopsNested.lean | 26 +++++++++++---------- tests/lean/LoopsRec.lean | 31 +++++++++++++++++-------- tests/lean/LoopsSequences.lean | 8 +++---- tests/lean/NestedBorrows.lean | 11 +++++---- tests/lean/OverflowingOps.lean | 24 ++++++++++++------- tests/lean/RustBorrowCheckIssues.lean | 7 +++--- tests/lean/Scalars.lean | 3 ++- tests/lean/Tutorial/Tutorial.lean | 7 ++++-- 25 files changed, 166 insertions(+), 108 deletions(-) diff --git a/tests/lean/Adt.lean b/tests/lean/Adt.lean index b4f063030..f99cbd9c1 100644 --- a/tests/lean/Adt.lean +++ b/tests/lean/Adt.lean @@ -37,7 +37,7 @@ def BigStructName := Unit /-- [adt::BigStruct] Source: 'tests/src/adt.rs', lines 17:0-24:2 -/ def BigStruct := - BigStructName × BigStructName × BigStructName × BigStructName × BigStructName - × BigStructName + BigStructName × BigStructName × BigStructName × BigStructName × + BigStructName × BigStructName end adt diff --git a/tests/lean/AdtBorrows.lean b/tests/lean/AdtBorrows.lean index 674c35aaa..455ecdc5b 100644 --- a/tests/lean/AdtBorrows.lean +++ b/tests/lean/AdtBorrows.lean @@ -204,8 +204,8 @@ def MutWrapper2.unwrap Source: 'tests/src/adt-borrows.rs', lines 143:4-145:5 -/ def MutWrapper2.id {T : Type} (self : MutWrapper2 T) : - Result ((MutWrapper2 T) × (MutWrapper2 T → MutWrapper2 T) × (MutWrapper2 T → - MutWrapper2 T)) + Result ((MutWrapper2 T) × (MutWrapper2 T → MutWrapper2 T) × (MutWrapper2 + T → MutWrapper2 T)) := do let back'a := fun mw => { self with x := mw.x } let back'b := fun mw => { self with y := mw.y } @@ -227,8 +227,8 @@ def use_mut_wrapper2 : Result Unit := do Source: 'tests/src/adt-borrows.rs', lines 159:0-161:1 -/ def use_mut_wrapper2_id {T : Type} (x : MutWrapper2 T) : - Result ((MutWrapper2 T) × (MutWrapper2 T → MutWrapper2 T) × (MutWrapper2 T → - MutWrapper2 T)) + Result ((MutWrapper2 T) × (MutWrapper2 T → MutWrapper2 T) × (MutWrapper2 + T → MutWrapper2 T)) := do let (mw, id_back, id_back1) ← MutWrapper2.id x let back'a := fun mw1 => { x with x := (id_back { mw with x := mw1.x }).x } diff --git a/tests/lean/ArraySliceIndex.lean b/tests/lean/ArraySliceIndex.lean index ae649732d..51415b432 100644 --- a/tests/lean/ArraySliceIndex.lean +++ b/tests/lean/ArraySliceIndex.lean @@ -61,7 +61,8 @@ def slice_use_index_mut_range_from Visibility: public -/ def slice_use_get_mut_range_from (s : Slice Std.U32) : - Result ((Option (Slice Std.U32)) × (Option (Slice Std.U32) → Slice Std.U32)) + Result ((Option (Slice Std.U32)) × (Option (Slice Std.U32) → Slice + Std.U32)) := do core.slice.Slice.get_mut (core.slice.index.SliceIndexRangeFromUsizeSlice Std.U32) s { start := 0#usize } diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index 6e05cdbae..00b7716b6 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -103,7 +103,9 @@ def index_slice {T : Type} (s : Slice T) (i : Std.Usize) : Result T := do Source: 'tests/src/arrays.rs', lines 65:0-67:1 Visibility: public -/ def index_mut_slice - {T : Type} (s : Slice T) (i : Std.Usize) : Result (T × (T → Slice T)) := do + {T : Type} (s : Slice T) (i : Std.Usize) : + Result (T × (T → Slice T)) + := do Slice.index_mut_usize s i /-- [arrays::slice_subslice_shared_]: @@ -502,7 +504,8 @@ def sum2 (s : Slice Std.U32) (s2 : Slice Std.U32) : Result Std.U32 := do Source: 'tests/src/arrays.rs', lines 294:0-297:1 Visibility: public -/ def f0 : Result Unit := do - let (s, _) ← lift (Array.to_slice_mut (Array.make 2#usize [ 1#u32, 2#u32 ])) + let (s, _) ← + lift (Array.to_slice_mut (Array.make 2#usize [ 1#u32, 2#u32 ])) let _ ← Slice.index_mut_usize s 0#usize ok () @@ -666,8 +669,8 @@ def sum_mut_slice def add_acc_loop.body (paSrc : Array Std.U32 256#usize) (peDst : Array Std.U32 256#usize) (i : Std.Usize) : - Result (ControlFlow ((Array Std.U32 256#usize) × (Array Std.U32 256#usize) × - Std.Usize) ((Array Std.U32 256#usize) × (Array Std.U32 256#usize))) + Result (ControlFlow ((Array Std.U32 256#usize) × (Array Std.U32 256#usize) + × Std.Usize) ((Array Std.U32 256#usize) × (Array Std.U32 256#usize))) := do if i < 256#usize then diff --git a/tests/lean/Avl/Funs.lean b/tests/lean/Avl/Funs.lean index 1dcd1c4f8..34be2c16a 100644 --- a/tests/lean/Avl/Funs.lean +++ b/tests/lean/Avl/Funs.lean @@ -131,7 +131,8 @@ def Node.insert_in_left let left ← core.option.Option.unwrap o1 if left.balance_factor <= 0#i8 then - let node1 ← Node.rotate_right (Node.mk node.value o2 node.right i) left + let node1 ← + Node.rotate_right (Node.mk node.value o2 node.right i) left ok (false, node1) else let node1 ← @@ -157,7 +158,8 @@ def Node.insert_in_right let right ← core.option.Option.unwrap o1 if right.balance_factor >= 0#i8 then - let node1 ← Node.rotate_left (Node.mk node.value node.left o2 i) right + let node1 ← + Node.rotate_left (Node.mk node.value node.left o2 i) right ok (false, node1) else let node1 ← diff --git a/tests/lean/ChunksExact.lean b/tests/lean/ChunksExact.lean index c73472e07..4e6dab516 100644 --- a/tests/lean/ChunksExact.lean +++ b/tests/lean/ChunksExact.lean @@ -118,7 +118,8 @@ def test_chunks_exact_remainder_2 : Result Unit := do Source: 'tests/src/chunks_exact.rs', lines 61:0-73:1 Visibility: public -/ def test_chunks_exact_size_1 : Result Unit := do - let s ← lift (Array.to_slice (Array.make 3#usize [ 10#u32, 20#u32, 30#u32 ])) + let s ← + lift (Array.to_slice (Array.make 3#usize [ 10#u32, 20#u32, 30#u32 ])) let it ← core.slice.Slice.chunks_exact s 1#usize let (o, it1) ← core.slice.iter.IteratorChunksExact.next it let c1 ← core.option.Option.unwrap o diff --git a/tests/lean/Closures.lean b/tests/lean/Closures.lean index a36f15d33..75ee34250 100644 --- a/tests/lean/Closures.lean +++ b/tests/lean/Closures.lean @@ -239,7 +239,8 @@ def call_closure2.closure_1.Insts.CoreOpsFunctionFnMutTupleU32.call_mut (state : call_closure2.closure_1) (_ : Unit) : Result (Std.U32 × call_closure2.closure_1) := do - let i ← call_closure2.closure_1.Insts.CoreOpsFunctionFnTupleU32.call state () + let i ← + call_closure2.closure_1.Insts.CoreOpsFunctionFnTupleU32.call state () ok (i, state) /-- [closures::call_closure2::{impl core::ops::function::FnOnce<(), u32> for closures::call_closure2::closure#1}::call_once]: @@ -336,7 +337,8 @@ def call_closure2.closure.Insts.CoreOpsFunctionFnTupleU32 : /-- [closures::call_closure2]: Source: 'tests/src/closures.rs', lines 38:0-41:1 -/ def call_closure2 : Result Std.U32 := do - let _ ← call_closure call_closure2.closure.Insts.CoreOpsFunctionFnTupleU32 () + let _ ← + call_closure call_closure2.closure.Insts.CoreOpsFunctionFnTupleU32 () call_closure call_closure2.closure_1.Insts.CoreOpsFunctionFnTupleU32 () /-- [closures::u8_id]: diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean index 63a805247..f4d1c0d29 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -165,7 +165,9 @@ def Usize.Insts.DemoCounter : Counter Std.Usize := { Source: 'tests/src/demo.rs', lines 112:0-114:1 Visibility: public -/ def use_counter - {T : Type} (CounterInst : Counter T) (cnt : T) : Result (Std.Usize × T) := do + {T : Type} (CounterInst : Counter T) (cnt : T) : + Result (Std.Usize × T) + := do CounterInst.incr cnt /-- [demo::mod_add]: diff --git a/tests/lean/Drop.lean b/tests/lean/Drop.lean index 795885c55..a0119232e 100644 --- a/tests/lean/Drop.lean +++ b/tests/lean/Drop.lean @@ -20,7 +20,8 @@ namespace drop def fill_loop.body {T : Type} (corecloneCloneInst : core.clone.Clone T) (value : T) (iter : core.ops.range.Range Std.Usize) (s : Slice T) : - Result (ControlFlow ((core.ops.range.Range Std.Usize) × (Slice T)) (Slice T)) + Result (ControlFlow ((core.ops.range.Range Std.Usize) × (Slice T)) (Slice + T)) := do let (o, iter1) ← core.iter.range.IteratorRange.next core.iter.range.StepUsize iter diff --git a/tests/lean/Issue789LoopCtxMatch.lean b/tests/lean/Issue789LoopCtxMatch.lean index 9ad03a790..afeb5baf5 100644 --- a/tests/lean/Issue789LoopCtxMatch.lean +++ b/tests/lean/Issue789LoopCtxMatch.lean @@ -36,8 +36,8 @@ def f @[rust_loop_body] def the_loop_loop.body (s : S) (next_in : Slice Std.U8) : - Result (ControlFlow (S × (Slice Std.U8)) (Std.U8 × (Array Std.U8 4#usize) × - (Slice Std.U8) × Bool)) + Result (ControlFlow (S × (Slice Std.U8)) (Std.U8 × (Array Std.U8 4#usize) + × (Slice Std.U8) × Bool)) := do let (s1, to_slice_mut_back) ← lift (Array.to_slice_mut s.y) let ((done1, n), i, s2) ← f s.x next_in s1 diff --git a/tests/lean/IterAdapters.lean b/tests/lean/IterAdapters.lean index 9d4419a7d..f1aee0526 100644 --- a/tests/lean/IterAdapters.lean +++ b/tests/lean/IterAdapters.lean @@ -18,7 +18,8 @@ namespace iter_adapters Source: 'tests/src/iter_adapters.rs', lines 14:0-24:1 Visibility: public -/ def test_enumerate_slice : Result Unit := do - let s ← lift (Array.to_slice (Array.make 3#usize [ 10#u32, 20#u32, 30#u32 ])) + let s ← + lift (Array.to_slice (Array.make 3#usize [ 10#u32, 20#u32, 30#u32 ])) let i ← core.slice.Slice.iter s let it ← core.iter.traits.iterator.Iterator.enumerate.trait_default @@ -102,7 +103,8 @@ def test_take_2 : Result Unit := do Source: 'tests/src/iter_adapters.rs', lines 50:0-54:1 Visibility: public -/ def test_take_0 : Result Unit := do - let s ← lift (Array.to_slice (Array.make 3#usize [ 10#u32, 20#u32, 30#u32 ])) + let s ← + lift (Array.to_slice (Array.make 3#usize [ 10#u32, 20#u32, 30#u32 ])) let i ← core.slice.Slice.iter s let it ← core.iter.traits.iterator.Iterator.take.trait_default @@ -301,7 +303,8 @@ def test_range_u64 : Result Unit := do @[rust_loop_body] def test_range_usize_loop.body (iter : core.ops.range.Range Std.Usize) (count : Std.Usize) : - Result (ControlFlow ((core.ops.range.Range Std.Usize) × Std.Usize) Std.Usize) + Result (ControlFlow ((core.ops.range.Range Std.Usize) × Std.Usize) + Std.Usize) := do let (o, iter1) ← core.iter.range.IteratorRange.next core.iter.range.StepUsize iter @@ -372,7 +375,8 @@ def test_range_empty : Result Unit := do Source: 'tests/src/iter_adapters.rs', lines 137:0-144:1 Visibility: public -/ def test_array_into_iter : Result Unit := do - let s ← lift (Array.to_slice (Array.make 3#usize [ 10#u32, 20#u32, 30#u32 ])) + let s ← + lift (Array.to_slice (Array.make 3#usize [ 10#u32, 20#u32, 30#u32 ])) let it ← core.slice.Slice.iter s let (o, it1) ← core.slice.iter.IteratorSliceIter.next it let i ← core.option.Option.unwrap o @@ -583,14 +587,16 @@ def test_range_u16_boundary : Result Unit := do { start := 0#u16, «end» := 3#u16 } let i ← core.option.Option.unwrap o massert (i = 0#u16) - let (o1, it1) ← core.iter.range.IteratorRange.next core.iter.range.StepU16 it + let (o1, it1) ← + core.iter.range.IteratorRange.next core.iter.range.StepU16 it let i1 ← core.option.Option.unwrap o1 massert (i1 = 1#u16) let (o2, it2) ← core.iter.range.IteratorRange.next core.iter.range.StepU16 it1 let i2 ← core.option.Option.unwrap o2 massert (i2 = 2#u16) - let (o3, _) ← core.iter.range.IteratorRange.next core.iter.range.StepU16 it2 + let (o3, _) ← + core.iter.range.IteratorRange.next core.iter.range.StepU16 it2 let b := core.option.Option.is_none o3 massert b @@ -606,10 +612,12 @@ def test_range_u32_boundary : Result Unit := do { start := 0#u32, «end» := 2#u32 } let i ← core.option.Option.unwrap o massert (i = 0#u32) - let (o1, it1) ← core.iter.range.IteratorRange.next core.iter.range.StepU32 it + let (o1, it1) ← + core.iter.range.IteratorRange.next core.iter.range.StepU32 it let i1 ← core.option.Option.unwrap o1 massert (i1 = 1#u32) - let (o2, _) ← core.iter.range.IteratorRange.next core.iter.range.StepU32 it1 + let (o2, _) ← + core.iter.range.IteratorRange.next core.iter.range.StepU32 it1 let b := core.option.Option.is_none o2 massert b @@ -625,14 +633,16 @@ def test_range_u64_boundary : Result Unit := do { start := 100#u64, «end» := 103#u64 } let i ← core.option.Option.unwrap o massert (i = 100#u64) - let (o1, it1) ← core.iter.range.IteratorRange.next core.iter.range.StepU64 it + let (o1, it1) ← + core.iter.range.IteratorRange.next core.iter.range.StepU64 it let i1 ← core.option.Option.unwrap o1 massert (i1 = 101#u64) let (o2, it2) ← core.iter.range.IteratorRange.next core.iter.range.StepU64 it1 let i2 ← core.option.Option.unwrap o2 massert (i2 = 102#u64) - let (o3, _) ← core.iter.range.IteratorRange.next core.iter.range.StepU64 it2 + let (o3, _) ← + core.iter.range.IteratorRange.next core.iter.range.StepU64 it2 let b := core.option.Option.is_none o3 massert b diff --git a/tests/lean/Iterators.lean b/tests/lean/Iterators.lean index c382c4847..cbf8daac3 100644 --- a/tests/lean/Iterators.lean +++ b/tests/lean/Iterators.lean @@ -101,8 +101,8 @@ def slice_iter_mut_while_loop0.body (back : core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) (b : Bool) : Result (ControlFlow ((core.slice.iter.IterMut Std.U16) × - (core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) × Bool) - (core.slice.iter.IterMut Std.U16)) + (core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) × + Bool) (core.slice.iter.IterMut Std.U16)) := do let (o, it1, next_back) ← core.slice.iter.IteratorIterMut.next it match o with @@ -205,8 +205,8 @@ def slice_iter_mut_while_early_return_loop0.body (back : core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) (b : Bool) : Result (ControlFlow ((core.slice.iter.IterMut Std.U16) × - (core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) × Bool) - (core.slice.iter.IterMut Std.U16)) + (core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) × + Bool) (core.slice.iter.IterMut Std.U16)) := do let (o, it1, next_back) ← core.slice.iter.IteratorIterMut.next it match o with @@ -270,8 +270,8 @@ def slice_iter_mut_while_early_return_two_bools_loop0.body (back : core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) (b0 : Bool) (b1 : Bool) : Result (ControlFlow ((core.slice.iter.IterMut Std.U16) × - (core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) × Bool - × Bool) (core.slice.iter.IterMut Std.U16)) + (core.slice.iter.IterMut Std.U16 → core.slice.iter.IterMut Std.U16) × + Bool × Bool) (core.slice.iter.IterMut Std.U16)) := do let (o, it1, next_back) ← core.slice.iter.IteratorIterMut.next it match o with diff --git a/tests/lean/Joins.lean b/tests/lean/Joins.lean index 461cea13f..4fad829e1 100644 --- a/tests/lean/Joins.lean +++ b/tests/lean/Joins.lean @@ -18,19 +18,19 @@ namespace joins Source: 'tests/src/joins.rs', lines 4:0-7:1 -/ def opt_add_1 (b : Bool) (x : Std.U32) : Result Std.U32 := do let y ← if b - then ok 1#u32 - else ok 0#u32 + then ok 1#u32 + else ok 0#u32 x + y /-- [joins::opt_add_2]: Source: 'tests/src/joins.rs', lines 9:0-13:1 -/ def opt_add_2 (b : Bool) (x : Std.U32) : Result Std.U32 := do let y ← if b - then ok 1#u32 - else ok 0#u32 + then ok 1#u32 + else ok 0#u32 let z ← if b - then ok 1#u32 - else ok 0#u32 + then ok 1#u32 + else ok 0#u32 let i ← x + y i + z diff --git a/tests/lean/LoopSharedLoanInJoin.lean b/tests/lean/LoopSharedLoanInJoin.lean index 5166a7e6a..aab74d806 100644 --- a/tests/lean/LoopSharedLoanInJoin.lean +++ b/tests/lean/LoopSharedLoanInJoin.lean @@ -69,8 +69,8 @@ def State.extract_loop.body (a : Array Std.U64 4#usize) (i1 : Std.U32) (result : Slice Std.U64) (lane_index : Std.Usize) : Result (ControlFlow ((core.ops.range.Range Std.Usize) × (Array Std.U64 - 4#usize) × Std.U32 × (Slice Std.U64) × Std.Usize) ((Array Std.U64 4#usize) - × Std.U32 × (Slice Std.U64))) + 4#usize) × Std.U32 × (Slice Std.U64) × Std.Usize) ((Array Std.U64 + 4#usize) × Std.U32 × (Slice Std.U64))) := do let (o, iter1) ← core.iter.range.IteratorRange.next core.iter.range.StepUsize iter diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index 845ebaa2a..a84c0f1b6 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -450,7 +450,9 @@ def list_nth_mut_pair Visibility: public -/ @[rust_loop] def list_nth_shared_pair_loop - {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : Result (T × T) := do + {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : + Result (T × T) + := do match ls0 with | List.Cons x0 tl0 => match ls1 with @@ -468,7 +470,9 @@ partial_fixpoint Visibility: public -/ @[reducible] def list_nth_shared_pair - {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : Result (T × T) := do + {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : + Result (T × T) + := do list_nth_shared_pair_loop ls0 ls1 i /-- [loops::list_nth_mut_pair_merge]: loop 0: @@ -518,7 +522,9 @@ def list_nth_mut_pair_merge Visibility: public -/ @[rust_loop] def list_nth_shared_pair_merge_loop - {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : Result (T × T) := do + {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : + Result (T × T) + := do match ls0 with | List.Cons x0 tl0 => match ls1 with @@ -536,7 +542,9 @@ partial_fixpoint Visibility: public -/ @[reducible] def list_nth_shared_pair_merge - {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : Result (T × T) := do + {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : + Result (T × T) + := do list_nth_shared_pair_merge_loop ls0 ls1 i /-- [loops::list_nth_mut_shared_pair]: loop 0: @@ -901,8 +909,8 @@ def issue270 (v : List (List Std.U8)) : Result (Option (List Std.U8)) := do def issue400_1_loop.body (cond : Bool) (back : Std.I32 → (Std.I32 × Std.I32)) (y : Std.I32) (i : Std.I32) : - Result (ControlFlow ((Std.I32 → (Std.I32 × Std.I32)) × Std.I32 × Std.I32) - (Std.I32 × Std.I32)) + Result (ControlFlow ((Std.I32 → (Std.I32 × Std.I32)) × Std.I32 × + Std.I32) (Std.I32 × Std.I32)) := do if i < 32#i32 then @@ -941,11 +949,11 @@ def issue400_1 @[rust_loop_body] def issue400_2_loop.body (conds : Slice Bool) - (back : Std.I32 → Std.I32 → (Std.I32 × Std.I32 × Std.I32)) (y : Std.I32) - (z : Std.I32) (i : Std.Usize) : - Result (ControlFlow ((Std.I32 → Std.I32 → (Std.I32 × Std.I32 × Std.I32)) × - Std.I32 × Std.I32 × Std.Usize) (Std.I32 × Std.I32 × (Std.I32 → Std.I32 → - (Std.I32 × Std.I32 × Std.I32)))) + (back : Std.I32 → Std.I32 → (Std.I32 × Std.I32 × Std.I32)) + (y : Std.I32) (z : Std.I32) (i : Std.Usize) : + Result (ControlFlow ((Std.I32 → Std.I32 → (Std.I32 × Std.I32 × + Std.I32)) × Std.I32 × Std.I32 × Std.Usize) (Std.I32 × Std.I32 × + (Std.I32 → Std.I32 → (Std.I32 × Std.I32 × Std.I32)))) := do let i1 := Slice.len conds if i < i1 @@ -980,7 +988,8 @@ def issue400_2 (a : Std.I32) (b : Std.I32) (c : Std.I32) (conds : Slice Bool) : Result (Std.I32 × Std.I32 × Std.I32) := do - let (y, z, back) ← issue400_2_loop (fun i i1 => (i, i1, c)) conds a b 0#usize + let (y, z, back) ← + issue400_2_loop (fun i i1 => (i, i1, c)) conds a b 0#usize let y1 ← y + 3#i32 let z1 ← z + 5#i32 ok (back y1 z1) diff --git a/tests/lean/LoopsAdts.lean b/tests/lean/LoopsAdts.lean index c0d74be41..5e3d80e40 100644 --- a/tests/lean/LoopsAdts.lean +++ b/tests/lean/LoopsAdts.lean @@ -97,8 +97,8 @@ def update_array_mut_borrow def array_mut_borrow_loop1_loop.body (back : Array Std.U32 32#usize → Array Std.U32 32#usize) (b : Bool) (a : Array Std.U32 32#usize) : - Result (ControlFlow ((Array Std.U32 32#usize → Array Std.U32 32#usize) × Bool - × (Array Std.U32 32#usize)) (Array Std.U32 32#usize)) + Result (ControlFlow ((Array Std.U32 32#usize → Array Std.U32 32#usize) × + Bool × (Array Std.U32 32#usize)) (Array Std.U32 32#usize)) := do if b then @@ -137,9 +137,9 @@ def array_mut_borrow_loop1 def array_mut_borrow_loop2_loop.body (back : Array Std.U32 32#usize → Array Std.U32 32#usize) (b : Bool) (a : Array Std.U32 32#usize) : - Result (ControlFlow ((Array Std.U32 32#usize → Array Std.U32 32#usize) × Bool - × (Array Std.U32 32#usize)) ((Array Std.U32 32#usize) × (Array Std.U32 - 32#usize → Array Std.U32 32#usize))) + Result (ControlFlow ((Array Std.U32 32#usize → Array Std.U32 32#usize) × + Bool × (Array Std.U32 32#usize)) ((Array Std.U32 32#usize) × (Array + Std.U32 32#usize → Array Std.U32 32#usize))) := do if b then diff --git a/tests/lean/LoopsIssues.lean b/tests/lean/LoopsIssues.lean index 1644d2913..93dd4b548 100644 --- a/tests/lean/LoopsIssues.lean +++ b/tests/lean/LoopsIssues.lean @@ -178,8 +178,8 @@ def test_loop.body if b0 then let buf1 ← if b1 - then write buf - else ok buf + then write buf + else ok buf read buf1 ok (cont (true, buf1)) else ok (done ()) diff --git a/tests/lean/LoopsNested.lean b/tests/lean/LoopsNested.lean index 29723cf46..dfc2dd8f0 100644 --- a/tests/lean/LoopsNested.lean +++ b/tests/lean/LoopsNested.lean @@ -97,9 +97,10 @@ def sum_loop0.body Result (ControlFlow (Std.U32 × Std.U32) Std.U32) := do if i < m - then let s1 ← sum_loop0_loop0 n s 0#u32 - let i1 ← i + 1#u32 - ok (cont (s1, i1)) + then + let s1 ← sum_loop0_loop0 n s 0#u32 + let i1 ← i + 1#u32 + ok (cont (s1, i1)) else ok (done s) /-- [loops_nested::sum]: loop 0: @@ -130,9 +131,10 @@ def update_array_loop0_loop0.body 4#usize)) := do if j < 4#usize - then let a ← Array.update out j 1#u8 - let j1 ← j + 1#usize - ok (cont (a, j1)) + then + let a ← Array.update out j 1#u8 + let j1 ← j + 1#usize + ok (cont (a, j1)) else ok (done out) /-- [loops_nested::update_array]: loop 1: @@ -334,8 +336,8 @@ def sample_ntt @[rust_loop_body] def generate_matrix_inner_loop.body (key : Key) (state : Array Std.U8 8#usize) (j : Std.Usize) : - Result (ControlFlow (Key × (Array Std.U8 8#usize) × Std.Usize) (Key × (Array - Std.U8 8#usize))) + Result (ControlFlow (Key × (Array Std.U8 8#usize) × Std.Usize) (Key × + (Array Std.U8 8#usize))) := do if j < 4#usize then @@ -375,8 +377,8 @@ def generate_matrix_loop0_loop0.body (state_base : Array Std.U8 8#usize) (i : Std.U8) (key : Key) (state_work : Array Std.U8 8#usize) (coordinates : Array Std.U8 2#usize) (j : Std.U8) : - Result (ControlFlow (Key × (Array Std.U8 8#usize) × (Array Std.U8 2#usize) × - Std.U8) (Key × (Array Std.U8 8#usize) × (Array Std.U8 2#usize))) + Result (ControlFlow (Key × (Array Std.U8 8#usize) × (Array Std.U8 2#usize) + × Std.U8) (Key × (Array Std.U8 8#usize) × (Array Std.U8 2#usize))) := do if j < 4#u8 then @@ -418,8 +420,8 @@ def generate_matrix_loop0.body (state_base : Array Std.U8 8#usize) (key : Key) (state_work : Array Std.U8 8#usize) (coordinates : Array Std.U8 2#usize) (i : Std.U8) : - Result (ControlFlow (Key × (Array Std.U8 8#usize) × (Array Std.U8 2#usize) × - Std.U8) (Key × (Array Std.U8 8#usize))) + Result (ControlFlow (Key × (Array Std.U8 8#usize) × (Array Std.U8 2#usize) + × Std.U8) (Key × (Array Std.U8 8#usize))) := do if i < 4#u8 then diff --git a/tests/lean/LoopsRec.lean b/tests/lean/LoopsRec.lean index b75f99b0a..83d649316 100644 --- a/tests/lean/LoopsRec.lean +++ b/tests/lean/LoopsRec.lean @@ -58,9 +58,10 @@ def sum (max : Std.U32) : Result Std.U32 := do def sum_with_mut_borrows_loop (max : Std.U32) (i : Std.U32) (s : Std.U32) : Result Std.U32 := do if i < max - then let ms ← s + i - let mi ← i + 1#u32 - sum_with_mut_borrows_loop max mi ms + then + let ms ← s + i + let mi ← i + 1#u32 + sum_with_mut_borrows_loop max mi ms else ok s partial_fixpoint @@ -386,7 +387,9 @@ def list_nth_mut_pair Visibility: public -/ @[rust_loop] def list_nth_shared_pair_loop - {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : Result (T × T) := do + {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : + Result (T × T) + := do match ls0 with | List.Cons x0 tl0 => match ls1 with @@ -404,7 +407,9 @@ partial_fixpoint Visibility: public -/ @[reducible] def list_nth_shared_pair - {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : Result (T × T) := do + {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : + Result (T × T) + := do list_nth_shared_pair_loop ls0 ls1 i /-- [loops_rec::list_nth_mut_pair_merge]: loop 0: @@ -454,7 +459,9 @@ def list_nth_mut_pair_merge Visibility: public -/ @[rust_loop] def list_nth_shared_pair_merge_loop - {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : Result (T × T) := do + {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : + Result (T × T) + := do match ls0 with | List.Cons x0 tl0 => match ls1 with @@ -472,7 +479,9 @@ partial_fixpoint Visibility: public -/ @[reducible] def list_nth_shared_pair_merge - {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : Result (T × T) := do + {T : Type} (ls0 : List T) (ls1 : List T) (i : Std.U32) : + Result (T × T) + := do list_nth_shared_pair_merge_loop ls0 ls1 i /-- [loops_rec::list_nth_mut_shared_pair]: loop 0: @@ -756,8 +765,9 @@ def issue270.box_get_borrow {T : Type} (x : T) : Result T := do def issue270_loop (t : List (List Std.U8)) (last : List Std.U8) : Result (List Std.U8) := do match t with - | List.Cons ht tt => let t1 ← issue270.box_get_borrow tt - issue270_loop t1 ht + | List.Cons ht tt => + let t1 ← issue270.box_get_borrow tt + issue270_loop t1 ht | List.Nil => ok last partial_fixpoint @@ -829,7 +839,8 @@ def issue400_2 (a : Std.I32) (b : Std.I32) (c : Std.I32) (conds : Slice Bool) : Result (Std.I32 × Std.I32 × Std.I32) := do - let (y, z, back) ← issue400_2_loop (fun i i1 => (i, i1, c)) conds a b 0#usize + let (y, z, back) ← + issue400_2_loop (fun i i1 => (i, i1, c)) conds a b 0#usize let y1 ← y + 3#i32 let z1 ← z + 5#i32 ok (back y1 z1) diff --git a/tests/lean/LoopsSequences.lean b/tests/lean/LoopsSequences.lean index 4473f9538..beda7f8d0 100644 --- a/tests/lean/LoopsSequences.lean +++ b/tests/lean/LoopsSequences.lean @@ -74,8 +74,8 @@ def key_expand_loop0.body (state_base : Array Std.U8 8#usize) (key : Key) (state_work : Array Std.U8 8#usize) (sample_buffer : Array Std.U8 1#usize) (i : Std.I32) : - Result (ControlFlow (Key × (Array Std.U8 8#usize) × (Array Std.U8 1#usize) × - Std.I32) (Key × (Array Std.U8 8#usize) × (Array Std.U8 1#usize))) + Result (ControlFlow (Key × (Array Std.U8 8#usize) × (Array Std.U8 1#usize) + × Std.I32) (Key × (Array Std.U8 8#usize) × (Array Std.U8 1#usize))) := do if i < 32#i32 then @@ -116,8 +116,8 @@ def key_expand_loop1.body (state_base : Array Std.U8 8#usize) (key : Key) (state_work : Array Std.U8 8#usize) (sample_buffer : Array Std.U8 1#usize) (i : Std.I32) : - Result (ControlFlow (Key × (Array Std.U8 8#usize) × (Array Std.U8 1#usize) × - Std.I32) (Key × (Array Std.U8 8#usize))) + Result (ControlFlow (Key × (Array Std.U8 8#usize) × (Array Std.U8 1#usize) + × Std.I32) (Key × (Array Std.U8 8#usize))) := do if i < 32#i32 then diff --git a/tests/lean/NestedBorrows.lean b/tests/lean/NestedBorrows.lean index bcb8adb7e..61b3b2b31 100644 --- a/tests/lean/NestedBorrows.lean +++ b/tests/lean/NestedBorrows.lean @@ -45,7 +45,8 @@ def call_inner_mut : Result Unit := do Source: 'tests/src/nested-borrows.rs', lines 28:0-32:1 -/ def inner_mut_swap (ppx : Std.U32) (py : Std.U32) : - Result (Std.U32 × (Std.U32 → Std.U32) × (Std.U32 → (Std.U32 × Std.U32))) + Result (Std.U32 × (Std.U32 → Std.U32) × (Std.U32 → (Std.U32 × + Std.U32))) := do let back'b := fun ppx1 => (10#u32, ppx1) ok (py, fun ppx1 => ppx1, back'b) @@ -149,8 +150,8 @@ def iter_mut_loop {T : Type} (it : IterMut T) : Result (IterMut T) := do @[rust_loop_body] def iter_mut_incr_loop.body (back : IterMut Std.U32 → Option Std.U32) (it : IterMut Std.U32) : - Result (ControlFlow ((IterMut Std.U32 → Option Std.U32) × (IterMut Std.U32)) - (Option Std.U32)) + Result (ControlFlow ((IterMut Std.U32 → Option Std.U32) × (IterMut + Std.U32)) (Option Std.U32)) := do let (o, it1, next_back) ← IterMut.next it match o with @@ -311,8 +312,8 @@ def iter_list_while_loop0_loop0 (b : Bool) : Result Unit := do @[rust_loop_body] def iter_list_while_loop0.body {T : Type} (l : List T) (back : List T → List T) (b : Bool) : - Result (ControlFlow ((List T) × (List T → List T) × Bool) ((List T) × (List T - → List T))) + Result (ControlFlow ((List T) × (List T → List T) × Bool) ((List T) × + (List T → List T))) := do let (o, l1, next1_back) ← next1 l match o with diff --git a/tests/lean/OverflowingOps.lean b/tests/lean/OverflowingOps.lean index 8fa7f62ab..341c93ba4 100644 --- a/tests/lean/OverflowingOps.lean +++ b/tests/lean/OverflowingOps.lean @@ -16,7 +16,8 @@ namespace overflowing_ops /-- [overflowing_ops::u8_overflowing_add]: Source: 'tests/src/overflowing-ops.rs', lines 3:0-5:1 -/ -def u8_overflowing_add (x : Std.U8) (y : Std.U8) : Result (Std.U8 × Bool) := do +def u8_overflowing_add + (x : Std.U8) (y : Std.U8) : Result (Std.U8 × Bool) := do ok (core.num.U8.overflowing_add x y) /-- [overflowing_ops::u16_overflowing_add]: @@ -51,7 +52,8 @@ def usize_overflowing_add /-- [overflowing_ops::i8_overflowing_add]: Source: 'tests/src/overflowing-ops.rs', lines 22:0-24:1 -/ -def i8_overflowing_add (x : Std.I8) (y : Std.I8) : Result (Std.I8 × Bool) := do +def i8_overflowing_add + (x : Std.I8) (y : Std.I8) : Result (Std.I8 × Bool) := do ok (core.num.I8.overflowing_add x y) /-- [overflowing_ops::i16_overflowing_add]: @@ -86,7 +88,8 @@ def isize_overflowing_add /-- [overflowing_ops::u8_overflowing_sub]: Source: 'tests/src/overflowing-ops.rs', lines 41:0-43:1 -/ -def u8_overflowing_sub (x : Std.U8) (y : Std.U8) : Result (Std.U8 × Bool) := do +def u8_overflowing_sub + (x : Std.U8) (y : Std.U8) : Result (Std.U8 × Bool) := do ok (core.num.U8.overflowing_sub x y) /-- [overflowing_ops::u16_overflowing_sub]: @@ -121,7 +124,8 @@ def usize_overflowing_sub /-- [overflowing_ops::i8_overflowing_sub]: Source: 'tests/src/overflowing-ops.rs', lines 60:0-62:1 -/ -def i8_overflowing_sub (x : Std.I8) (y : Std.I8) : Result (Std.I8 × Bool) := do +def i8_overflowing_sub + (x : Std.I8) (y : Std.I8) : Result (Std.I8 × Bool) := do ok (core.num.I8.overflowing_sub x y) /-- [overflowing_ops::i16_overflowing_sub]: @@ -156,7 +160,8 @@ def isize_overflowing_sub /-- [overflowing_ops::u8_overflowing_mul]: Source: 'tests/src/overflowing-ops.rs', lines 79:0-81:1 -/ -def u8_overflowing_mul (x : Std.U8) (y : Std.U8) : Result (Std.U8 × Bool) := do +def u8_overflowing_mul + (x : Std.U8) (y : Std.U8) : Result (Std.U8 × Bool) := do ok (core.num.U8.overflowing_mul x y) /-- [overflowing_ops::u16_overflowing_mul]: @@ -191,7 +196,8 @@ def usize_overflowing_mul /-- [overflowing_ops::i8_overflowing_mul]: Source: 'tests/src/overflowing-ops.rs', lines 98:0-100:1 -/ -def i8_overflowing_mul (x : Std.I8) (y : Std.I8) : Result (Std.I8 × Bool) := do +def i8_overflowing_mul + (x : Std.I8) (y : Std.I8) : Result (Std.I8 × Bool) := do ok (core.num.I8.overflowing_mul x y) /-- [overflowing_ops::i16_overflowing_mul]: @@ -226,7 +232,8 @@ def isize_overflowing_mul /-- [overflowing_ops::u8_overflowing_div]: Source: 'tests/src/overflowing-ops.rs', lines 117:0-119:1 -/ -def u8_overflowing_div (x : Std.U8) (y : Std.U8) : Result (Std.U8 × Bool) := do +def u8_overflowing_div + (x : Std.U8) (y : Std.U8) : Result (Std.U8 × Bool) := do core.num.U8.overflowing_div x y /-- [overflowing_ops::u16_overflowing_div]: @@ -261,7 +268,8 @@ def usize_overflowing_div /-- [overflowing_ops::i8_overflowing_div]: Source: 'tests/src/overflowing-ops.rs', lines 136:0-138:1 -/ -def i8_overflowing_div (x : Std.I8) (y : Std.I8) : Result (Std.I8 × Bool) := do +def i8_overflowing_div + (x : Std.I8) (y : Std.I8) : Result (Std.I8 × Bool) := do core.num.I8.overflowing_div x y /-- [overflowing_ops::i16_overflowing_div]: diff --git a/tests/lean/RustBorrowCheckIssues.lean b/tests/lean/RustBorrowCheckIssues.lean index bf99020bc..c2d0c0cc1 100644 --- a/tests/lean/RustBorrowCheckIssues.lean +++ b/tests/lean/RustBorrowCheckIssues.lean @@ -21,7 +21,8 @@ namespace rust_borrow_check_issues Source: '/rustc/library/core/src/mem/mod.rs', lines 1000:0-1002:24 Name pattern: [core::mem::drop] Visibility: public -/ -@[rust_fun "core::mem::drop"] axiom core.mem.drop {T : Type} : T → Result Unit +@[rust_fun "core::mem::drop"] +axiom core.mem.drop {T : Type} : T → Result Unit /-- [core::option::{core::option::Option}::as_mut]: Source: '/rustc/library/core/src/option.rs', lines 763:4-763:52 @@ -42,8 +43,8 @@ def unnecessary_error : Result Unit := do Source: 'tests/src/rust-borrow-check-issues.rs', lines 35:0-52:1 -/ def unnecessary_error_2 (b0 : Bool) (b1 : Bool) : Result Unit := do let i ← if b0 - then ok 0#u32 - else ok 1#u32 + then ok 0#u32 + else ok 1#u32 let _ ← if b1 then do diff --git a/tests/lean/Scalars.lean b/tests/lean/Scalars.lean index 455284238..b08de12b1 100644 --- a/tests/lean/Scalars.lean +++ b/tests/lean/Scalars.lean @@ -215,7 +215,8 @@ def test_is_multiple_of_zero_divisor : Result Unit := do Source: 'tests/src/scalars.rs', lines 158:0-160:1 Visibility: public -/ def test_try_from_usize_u32_ok : Result Unit := do - let r ← core.convert.num.ptr_try_from_impls.TryFromU32Usize.try_from 5#usize + let r ← + core.convert.num.ptr_try_from_impls.TryFromU32Usize.try_from 5#usize let b ← core.result.Result.is_ok r massert b diff --git a/tests/lean/Tutorial/Tutorial.lean b/tests/lean/Tutorial/Tutorial.lean index aff766601..7fc8cc012 100644 --- a/tests/lean/Tutorial/Tutorial.lean +++ b/tests/lean/Tutorial/Tutorial.lean @@ -175,7 +175,9 @@ def Usize.Insts.TutorialCounter : Counter Std.Usize := { Source: 'src/lib.rs', lines 117:0-119:1 Visibility: public -/ def use_counter - {T : Type} (CounterInst : Counter T) (cnt : T) : Result (Std.Usize × T) := do + {T : Type} (CounterInst : Counter T) (cnt : T) : + Result (Std.Usize × T) + := do CounterInst.incr cnt /-- [tutorial::list_nth_mut1]: loop 0: @@ -209,7 +211,8 @@ def list_nth_mut1 Source: 'src/lib.rs', lines 135:4-137:5 Visibility: public -/ @[rust_loop] -def list_tail_loop {T : Type} (l : CList T) : Result (CList T → CList T) := do +def list_tail_loop + {T : Type} (l : CList T) : Result (CList T → CList T) := do match l with | CList.CCons t tl => let back ← list_tail_loop tl