Merge branch 'main' into alex/blog-gcd

Author: karthikbhargavan

.gitignore

@@ -10,6 +10,7 @@ result
 .DS_Store
 .depend
 .cache
+.lake
 proof-libs/fstar/rust_primitives/#*#
 **/proofs/*/extraction/*
 !**/proofs/*/extraction/Makefile

CHANGELOG.md

@@ -22,14 +22,23 @@ Change to cargo-hax:
 
 Changes to hax-lib:
  - Add Lean core models for options, results, default (#1747)
+ - F* lib: improved while loops support, additions of some specific arithmetic operations and fixed `TryInto` for integer types (#1742)
 
 Changes to the Lean backend:
  - Support for constants with arbitrary computation (#1738)
  - 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)
+ - Add support for shift-left (#1785)
+ - Add support for default methods of traits (#1777)
+ - Add support for floats (#1784)
+ - Add support for pattern matching on constant literals (#1789)
+ - Add support for binding subpatterns in match constructs (#1790)
+ - Add error when using patterns in function parameters (#1792)
 
 Miscellaneous:
+- Reserve extraction folder for auto-generated files in Lean examples (#1754)
 
 ## 0.3.5
 

docs/blog/.authors.yml

@@ -2,20 +2,20 @@ authors:
   franziskus:
     name: Franziskus Kiefer
     description: Creator
-    avatar: https://cryspen.com/images/franziskus_hu8239521875621889102.jpg
+    avatar: /blog/avatars/franziskus.jpg
   lucas:
     name: Lucas Franceschino
     description: Creator
-    avatar: https://cryspen.com/images/lucas_hu1387702743353212719.jpg
+    avatar: /blog/avatars/lucas.jpg
   clement:
     name: Clement Blaudeau
     description: Engineer
-    avatar: https://cryspen.com/images/clement_hu_da447295a2bd189d.jpg
+    avatar: /blog/avatars/clement.jpg
   maxime:
     name: Maxime Buyse
     description: Engineer
-    avatar: https://cryspen.com/images/maxime_hu_8da610acc29fd826.png
+    avatar: /blog/avatars/maxime.png
   alex:
     name: Alexander Bentkamp
     description: Engineer
-    avatar: https://cryspen.com/images/posts/alex_hu_8751e8cc5106c694.jpg
+    avatar: /blog/avatars/alex.png

docs/blog/avatars/clement.jpg

@@ -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
 
 ```
 ///

docs/blog/avatars/franziskus.jpg

@@ -700,15 +700,31 @@ struct
         in
         F.term @@ F.AST.LetOperator ([ (F.id op, p, pexpr rhs) ], pexpr body)
     | Let { lhs; rhs; body; monadic = None } ->
-        let p =
-          (* TODO: temp patch that remove annotation when we see an associated type *)
-          if [%matches? TAssociatedType _] @@ U.remove_tuple1 lhs.typ then
-            ppat lhs
-          else
-            F.pat @@ F.AST.PatAscribed (ppat lhs, (pty lhs.span lhs.typ, None))
+        let rec ascribe_tuple_components pattern =
+          match pattern with
+          | { p = PConstruct { constructor = `TupleCons n1; fields; _ }; _ }
+            when n1 > 1 ->
+              (* F* type inference works better if the ascription is on each component intead of the whole tuple. *)
+              F.pat
+              @@ F.AST.PatTuple
+                   ( List.map
+                       ~f:(fun { pat } -> ascribe_tuple_components pat)
+                       fields,
+                     false )
+          | _ ->
+              (* TODO: temp patch that remove annotation when we see an associated type *)
+              if [%matches? TAssociatedType _] @@ U.remove_tuple1 pattern.typ
+              then ppat pattern
+              else
+                F.pat
+                @@ F.AST.PatAscribed
+                     (ppat pattern, (pty pattern.span pattern.typ, None))
         in
         F.term
-        @@ F.AST.Let (NoLetQualifier, [ (None, (p, pexpr rhs)) ], pexpr body)
+        @@ F.AST.Let
+             ( NoLetQualifier,
+               [ (None, (ascribe_tuple_components lhs, pexpr rhs)) ],
+               pexpr body )
     | EffectAction _ -> .
     | Match { scrutinee; arms } ->
         F.term
@@ -1643,7 +1659,13 @@ struct
           List.concat_map
             ~f:(fun { ii_span; ii_generics; ii_v; ii_ident } ->
               let name = (RenderId.render ii_ident).name in
-
+              let ii_generics =
+                {
+                  ii_generics with
+                  constraints =
+                    List.filter ~f:[%matches? GCType _] ii_generics.constraints;
+                }
+              in
               match ii_v with
               | IIFn { body; params } ->
                   let pats =

docs/blog/avatars/lucas.jpg

@@ -14,6 +14,8 @@ include
       include On.Quote
       include On.Dyn
       include On.Unsafe
+      include On.Trait_item_default
+      include On.As_pattern
     end)
     (struct
       let backend = Diagnostics.Backend.FStar
@@ -32,7 +34,7 @@ module SubtypeToInputLanguage
          and type raw_pointer = Features.Off.raw_pointer
          and type early_exit = Features.Off.early_exit
          and type question_mark = Features.Off.question_mark
-         and type as_pattern = Features.Off.as_pattern
+         and type as_pattern = Features.On.as_pattern
          and type lifetime = Features.Off.lifetime
          and type monadic_action = Features.Off.monadic_action
          and type arbitrary_lhs = Features.Off.arbitrary_lhs
@@ -45,7 +47,7 @@ module SubtypeToInputLanguage
          and type state_passing_loop = Features.Off.state_passing_loop
          and type fold_like_loop = Features.Off.fold_like_loop
          and type match_guard = Features.Off.match_guard
-         and type trait_item_default = Features.Off.trait_item_default) =
+         and type trait_item_default = Features.On.trait_item_default) =
 struct
   module FB = InputLanguage
 
@@ -116,11 +118,9 @@ module TransformToInputLanguage =
   |> Phases.Drop_return_break_continue
   |> Phases.Functionalize_loops
   |> Phases.Reject.Question_mark
-  |> Phases.Reject.As_pattern
   |> Phases.Traits_specs
   |> Phases.Simplify_hoisting
   |> Phases.Newtype_as_refinement
-  |> Phases.Reject.Trait_item_default
   |> Phases.Bundle_cycles
   |> Phases.Reorder_fields
   |> Phases.Sort_items