Merge pull request #1768 from cryspen/alex/rustm

refactor(lean): rename Result to RustM

Author: abentkamp

CHANGELOG.md

@@ -29,6 +29,7 @@ Changes to the Lean backend:
  - Add support for base-expressions of structs (#1736)
  - Use the explicit monadic phase to insert `pure` and `←` only on demand, and
    not introduce extra `do` block (#1746)
+ - Rename `Result` monad to `RustM` to avoid confusion with Rust `Result` type (#1768)
 
 Miscellaneous:
 - Reserve extraction folder for auto-generated files in Lean examples (#1754)

docs/manual/lean/internals.md

@@ -39,14 +39,14 @@ inductive Error where
    | panic: Error
    | undef: Error
 
-inductive Result.{u} (α : Type u) where
-  | ok (v: α): Result α
-  | fail (e: Error): Result α
+inductive RustM.{u} (α : Type u) where
+  | ok (v: α): RustM α
+  | fail (e: Error): RustM α
   | div
 ```
 
 This monadic encoding shows for simple expressions: the result of the lean
-extracted function is not `u32` but `Result u32`.
+extracted function is not `u32` but `RustM u32`.
 
 /// html | div[style='float: left; width: 48%;']
 ```rust
@@ -58,7 +58,7 @@ fn f (x: u32) -> u32 {
 
 /// html | div[style='float: right;width: 48%;']
 ```lean
-def f (x : u32) : Result u32
+def f (x : u32) : RustM u32
   := do (← x +? (1 : u32))
 ```
 ///
@@ -73,9 +73,9 @@ actually be understood as bindings in the monad, propagating potential
 errors to the top.
 
 The `do` keywords enables the lifting `←` and the `pure` operators. Intuitively,
-lifting turns a value of type `Result T` into a value of type `T` by turning the
+lifting turns a value of type `RustM T` into a value of type `T` by turning the
 rest of the program into a use of `bind`. Conversely, `pure` turns a value of
-type `T` into a value of type `Result T`. This shows also for let-bindings :
+type `T` into a value of type `RustM T`. This shows also for let-bindings :
 
 
 /// html | div[style='float: left; width: 48%;']
@@ -90,7 +90,7 @@ fn f (x: u32) -> u32 {
 
 /// html | div[style='float: right;width: 48%;']
 ```lean
-def f (x : u32) : Result u32 := do
+def f (x : u32) : RustM u32 := do
   let y : u32 ← (pure
     (← x +? (1 : u32)));
   let z : u32 ← (pure
@@ -327,7 +327,7 @@ match e_v1 {
 /// html | div[style='float: right;width: 48%;']
 ```lean
 def enums (_ : Tuple0)
-  : Result Tuple0
+  : RustM Tuple0
   := do
   let e_v1 : E ← (pure E.V1);
   let e_v2 : E ← (pure E.V2);
@@ -413,8 +413,8 @@ fn f<T: T1>(x: T) -> usize {
 /// html | div[style='float: right;width: 48%;']
 ```lean
 class T1 (Self : Type) where
-  f1 : Self -> Result usize
-  f2 : Self -> Self -> Result usize
+  f1 : Self -> RustM usize
+  f2 : Self -> Self -> RustM usize
 
 structure S where
 
@@ -425,7 +425,7 @@ instance Impl : T1 S where
     := do (43 : usize)
 
 def f (T : Type) [(T1 T)] (x : T)
-  : Result usize
+  : RustM usize
   := do
   (← (← T1.f1 x) +? (← T1.f2 x x))
 ```
@@ -459,7 +459,7 @@ class Test
   [_constr_7570495343596639253 :
     (T1 T)]
   f_test :
-    Self -> T -> Result usize
+    Self -> T -> RustM usize
 ```
 ///
 
@@ -507,7 +507,7 @@ class Bar (Self : Type) where
 
 class T1 (Self : Type) where
   T : Type
-  f : Self -> T -> Result T
+  f : Self -> T -> RustM T
 
 class T3 (Self : Type) where
   T : Type
@@ -516,12 +516,12 @@ class T3 (Self : Type) where
   Tp : Type
   [_constr_15450263461214744089 : (Foo Tp T)]
   f (A : Type) [(Bar A)] :
-    Self -> T -> Tp -> Result usize
+    Self -> T -> Tp -> RustM usize
 
 class T2 (Self : Type) where
   T : Type
   [_constr_18277713886489441014 : (T1 T)]
-  f : Self -> T -> Result usize
+  f : Self -> T -> RustM usize
 
 ```
 ///

examples/lean_chacha20/src/lib.rs

@@ -50,7 +50,7 @@ theorem Lean_chacha20.chacha20_quarter_round_spec a b c d state:
   intros
   mvcgen [Lean_chacha20.chacha20_quarter_round,
           Lean_chacha20.chacha20_line,
-          Result.ofOption, ]
+          RustM.ofOption, ]
   <;> try omega
 "
 )]

hax-lib/proof-libs/lean/Hax/Core/Clone.lean

@@ -12,7 +12,7 @@ namespace Core.Clone
 
 class Clone (Self : Type) where
 
-def Clone.clone {Self: Type} : Self -> Result Self :=
+def Clone.clone {Self: Type} : Self -> RustM Self :=
   fun x => pure x
 
 end Core.Clone

hax-lib/proof-libs/lean/Hax/Core/Convert.lean

@@ -14,7 +14,7 @@ set_option mvcgen.warning false
 
 /- Warning : this function has been specialized, it should be turned into a typeclass -/
 def Core.Convert.TryInto.try_into {α n} (a: Array α) :
-   Result (Core.Result.Result (Vector α n) Core.Array.TryFromSliceError) :=
+   RustM (Core.Result.Result (Vector α n) Core.Array.TryFromSliceError) :=
    pure (
      if h: a.size = n then
        Core.Result.Result.Ok (a.toVector.cast h)

hax-lib/proof-libs/lean/Hax/Core/Default.lean

@@ -12,6 +12,6 @@ open Rust_primitives.Hax
 namespace Core.Default
 
 class Default (Self : Type) where
-  default : Tuple0 -> Result Self
+  default : Tuple0 -> RustM Self
 
 end Core.Default

hax-lib/proof-libs/lean/Hax/Core/Ops/Function.lean

@@ -11,30 +11,30 @@ open Rust_primitives.Hax
 namespace Core.Ops.Function
 
 class FnOnce (Self Args : Type) {Output: Type} where
-  call_once : Self -> Args -> Result Output
+  call_once : Self -> Args -> RustM Output
   Output : Type := Output
 
 class Fn (Self Args : Type) {Output: Type} where
   [_constr_10219838627318688691 : (FnOnce Self Args (Output := Output))]
-  call : Self -> Args -> Result Output
+  call : Self -> Args -> RustM Output
 
-instance {α β} : FnOnce (α → Result β) α (Output := β) where
+instance {α β} : FnOnce (α → RustM β) α (Output := β) where
   Output := β
   call_once f x := f x
 
-instance {α β} : FnOnce (α → Result β) (Tuple1 α) (Output := β) where
+instance {α β} : FnOnce (α → RustM β) (Tuple1 α) (Output := β) where
   Output := β
   call_once f x := f x._0
 
-instance {α β γ : Type} : FnOnce (α → β → Result γ) (Tuple2 α β) (Output := γ) where
+instance {α β γ : Type} : FnOnce (α → β → RustM γ) (Tuple2 α β) (Output := γ) where
   Output := γ
   call_once f x := f x._0 x._1
 
-instance {α β} : Fn (α → Result β) α (Output := β) where
+instance {α β} : Fn (α → RustM β) α (Output := β) where
   call f x := (FnOnce.call_once) f x
 
-instance {α β} : Fn (α → Result β) (Tuple1 α) (Output := β) where
+instance {α β} : Fn (α → RustM β) (Tuple1 α) (Output := β) where
   call f x := (FnOnce.call_once) f x
 
-instance {α β γ} : Fn (α → β → Result γ) (Tuple2 α β) (Output := γ) where
+instance {α β γ} : Fn (α → β → RustM γ) (Tuple2 α β) (Output := γ) where
   call f x := (FnOnce.call_once) f x

hax-lib/proof-libs/lean/Hax/Core/Option.lean

@@ -13,6 +13,7 @@ import Hax.Core.Panicking
 import Hax.Core.Result
 open Rust_primitives.Hax
 open Core.Ops
+open Core.Result
 open Std.Do
 set_option mvcgen.warning false
 
@@ -26,7 +27,7 @@ def Impl.is_some_and
   (T : Type) (F : Type) [(Function.FnOnce (Output := Bool) F T)] (self :
   (Option T))
   (f : F)
-  : Result Bool
+  : RustM Bool
   := do
   match self with
     | (Option.None ) => (pure false)
@@ -37,7 +38,7 @@ def Impl.is_none_or
   (T : Type) (F : Type) [(Function.FnOnce (Output := Bool) F T)] (self :
   (Option T))
   (f : F)
-  : Result Bool
+  : RustM Bool
   := do
   match self with
     | (Option.None ) => (pure true)
@@ -46,7 +47,7 @@ def Impl.is_none_or
 
 def Impl.as_ref
   (T : Type) (self : (Option T))
-  : Result (Option T)
+  : RustM (Option T)
   := do
   match self with
     | (Option.Some x)
@@ -56,7 +57,7 @@ def Impl.as_ref
 def Impl.unwrap_or
   (T : Type) (self : (Option T))
   (default : T)
-  : Result T
+  : RustM T
   := do
   match self with
     | (Option.Some x) => (pure x)
@@ -68,7 +69,7 @@ def Impl.unwrap_or_else
   [(Function.FnOnce F Rust_primitives.Hax.Tuple0 (Output := T))]
   (self : (Option T))
   (f : F)
-  : Result T
+  : RustM T
   := do
   match self with
     | (Option.Some x) => (pure x)
@@ -77,7 +78,7 @@ def Impl.unwrap_or_else
 def Impl.unwrap_or_default
   (T : Type) [(Core.Default.Default T)] (self :
   (Option T))
-  : Result T
+  : RustM T
   := do
   match self with
     | (Option.Some x) => (pure x)
@@ -90,7 +91,7 @@ def Impl.map
   [(Function.FnOnce F T (Output := U))]
   (self : (Option T))
   (f : F)
-  : Result (Option U)
+  : RustM (Option U)
   := do
   match self with
     | (Option.Some x) => (pure (Option.Some (← (Function.FnOnce.call_once f x))))
@@ -104,7 +105,7 @@ def Impl.map_or
   (self : (Option T))
   (default : U)
   (f : F)
-  : Result U
+  : RustM U
   := do
   match self with
     | (Option.Some t) => (Function.FnOnce.call_once f t)
@@ -120,7 +121,7 @@ def Impl.map_or_else
   (self : (Option T))
   (default : D)
   (f : F)
-  : Result U
+  : RustM U
   := do
   match self with
     | (Option.Some t) => (Function.FnOnce.call_once f t)
@@ -134,7 +135,7 @@ def Impl.map_or_default
   [(Core.Default.Default U)]
   (self : (Option T))
   (f : F)
-  : Result U
+  : RustM U
   := do
   match self with
     | (Option.Some t)
@@ -146,13 +147,13 @@ def Impl.map_or_default
 def Impl.ok_or
   (T : Type) (E : Type) (self : (Option T))
   (err : E)
-  : Result (Core.Result.Result T E)
+  : RustM (Result T E)
   := do
   match self with
     | (Option.Some v)
-      => (pure (Core.Result.Result.Ok v))
+      => (pure (Result.Ok v))
     | (Option.None )
-      => (pure (Core.Result.Result.Err err))
+      => (pure (Result.Err err))
 
 def Impl.ok_or_else
   (T : Type)
@@ -161,14 +162,14 @@ def Impl.ok_or_else
   [(Function.FnOnce F Rust_primitives.Hax.Tuple0 (Output := E))]
   (self : (Option T))
   (err : F)
-  : Result (Core.Result.Result T E)
+  : RustM (Result T E)
   := do
   match self with
     | (Option.Some v)
-      => (pure (Core.Result.Result.Ok v))
+      => (pure (Result.Ok v))
     | (Option.None )
       =>
-        (pure (Core.Result.Result.Err
+        (pure (Result.Err
           (← (Function.FnOnce.call_once
             err
             Rust_primitives.Hax.Tuple0.mk))))
@@ -180,7 +181,7 @@ def Impl.and_then
   [(Function.FnOnce F T (Output := Option U))]
   (self : (Option T))
   (f : F)
-  : Result (Option U)
+  : RustM (Option U)
   := do
   match self with
     | (Option.Some x)
@@ -189,7 +190,7 @@ def Impl.and_then
 
 def Impl.take
   (T : Type) (self : (Option T))
-  : Result
+  : RustM
   (Rust_primitives.Hax.Tuple2
     (Option T)
     (Option T))
@@ -198,7 +199,7 @@ def Impl.take
 
 def Impl.is_some
   (T : Type) (self : (Option T))
-  : Result Bool
+  : RustM Bool
   := do
   match self with
     | (Option.Some _) => (pure true)
@@ -217,7 +218,7 @@ def Impl.is_some.spec
 
 def Impl.is_none
   (T : Type) (self : (Option T))
-  : Result Bool
+  : RustM Bool
   := do
   match self with
     | (Option.Some _) => (pure false)
@@ -226,7 +227,7 @@ def Impl.is_none
 def Impl.expect
   (T : Type) (self : (Option T))
   (_msg : String)
-  : Result T
+  : RustM T
   := do
   match self with
     | (Option.Some val) => (pure val)
@@ -235,13 +236,13 @@ def Impl.expect
 
 def Impl.unwrap._.requires
   (T : Type) (self_ : (Option T))
-  : Result Bool
+  : RustM Bool
   := do
   (Impl.is_some T self_)
 
 def Impl.unwrap
   (T : Type) (self : (Option T))
-  : Result T
+  : RustM T
   := do
   match self with
     | (Option.Some val) => (pure val)

hax-lib/proof-libs/lean/Hax/Core/Panicking.lean

@@ -9,7 +9,7 @@ open Core.Ops
 namespace Core.Panicking.Internal
 
 def panic (T : Type) (_ : Rust_primitives.Hax.Tuple0)
-  : Result T
+  : RustM T
   := do .fail .panic
 
 end Core.Panicking.Internal