From 00e9cd8ce3e50b2dc7889a8ddb357e253fc21b04 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 21 May 2024 14:29:02 +0200
Subject: [PATCH] fix(proof-libs): fix implicits

Since we are now printing types explicitely, the F* library has no more freedom in term of implicits.

For example, operations on vectors always take two implicits: the type
of the items held by the vector, but also the type of the
allocator. In F*, we don't care about the allocator, thus, we model
any allocator with unit. In this setting, taking an implicit allocator
each time we take a vector is useless in F*. But now, the extraction gives (as an implicit) the allocator, so we need to expect an allocator.
---
 .../core/Alloc.Collections.Binary_heap.fsti   | 20 +++++++++----------
 proof-libs/fstar/core/Alloc.Vec.fst           |  3 ++-
 proof-libs/fstar/core/Core.Cmp.fsti           |  9 +++++++--
 proof-libs/fstar/core/Core.Option.fst         |  2 +-
 4 files changed, 20 insertions(+), 14 deletions(-)

diff --git a/proof-libs/fstar/core/Alloc.Collections.Binary_heap.fsti b/proof-libs/fstar/core/Alloc.Collections.Binary_heap.fsti
index d925c6db5..dc96bd380 100644
--- a/proof-libs/fstar/core/Alloc.Collections.Binary_heap.fsti
+++ b/proof-libs/fstar/core/Alloc.Collections.Binary_heap.fsti
@@ -3,25 +3,25 @@ open Rust_primitives
 
 val t_BinaryHeap: Type -> unit -> eqtype
 
-val impl_10__new: #t:Type -> t_BinaryHeap t ()
-val impl_10__push: #t:Type -> t_BinaryHeap t () -> t -> t_BinaryHeap t ()
-val impl_11__len: #t:Type -> t_BinaryHeap t () -> usize
-val impl_11__iter: #t:Type -> t_BinaryHeap t () -> t_Slice t
+val impl_10__new: #t:Type -> (#[(Tactics.exact (`()))]_:unit) -> t_BinaryHeap t ()
+val impl_10__push: #t:Type -> (#[(Tactics.exact (`()))]_:unit) -> t_BinaryHeap t () -> t -> t_BinaryHeap t ()
+val impl_11__len: #t:Type -> (#[(Tactics.exact (`()))]_:unit) -> t_BinaryHeap t () -> usize
+val impl_11__iter: #t:Type -> (#[(Tactics.exact (`()))]_:unit) -> t_BinaryHeap t () -> t_Slice t
 
 open Core.Option
 
-val impl_11__peek: #t:Type -> t_BinaryHeap t () -> t_Option t
-val impl_10__pop: #t:Type -> t_BinaryHeap t () -> t_BinaryHeap t () & t_Option t
+val impl_11__peek: #t:Type -> (#[(Tactics.exact (`()))]_:unit) -> t_BinaryHeap t () -> t_Option t
+val impl_10__pop: #t:Type -> (#[(Tactics.exact (`()))]_:unit) -> t_BinaryHeap t () -> t_BinaryHeap t () & t_Option t
 
 unfold
 let nonempty h = v (impl_11__len h) > 0
 
-val lemma_peek_len: #t:Type -> h: t_BinaryHeap t ()
+val lemma_peek_len: #t:Type -> (#[(Tactics.exact (`()))]_:unit) -> h: t_BinaryHeap t ()
   -> Lemma (Option_Some? (impl_11__peek h) <==> nonempty h)
   
-val lemma_pop_len: #t:Type -> h: t_BinaryHeap t ()
+val lemma_pop_len: #t:Type -> (#[(Tactics.exact (`()))]_:unit) -> h: t_BinaryHeap t ()
   -> Lemma (Option_Some? (snd (impl_10__pop h)) <==> nonempty h)
 
-val lemma_peek_pop: #t:Type -> h: t_BinaryHeap t ()
+val lemma_peek_pop: #t:Type -> (#[(Tactics.exact (`()))]_u:unit) -> h: t_BinaryHeap t ()
   -> Lemma (impl_11__peek h == snd (impl_10__pop h))
-          [SMTPat (impl_11__peek h)]
+          [SMTPat (impl_11__peek #t #_u h)]
diff --git a/proof-libs/fstar/core/Alloc.Vec.fst b/proof-libs/fstar/core/Alloc.Vec.fst
index 34b6fb87f..1a0784185 100644
--- a/proof-libs/fstar/core/Alloc.Vec.fst
+++ b/proof-libs/fstar/core/Alloc.Vec.fst
@@ -14,13 +14,14 @@ let impl__with_capacity (_capacity: usize) = impl__new ()
 // semantics: pushing on a "full" vector does nothing. It should panic
 // instead.
 let impl_1__push #t
+  (#[(Tactics.exact (`()))]_unit:unit)
   (v: t_Vec t ())// Removed: {Seq.length v + 1 <= max_usize})
   (x: t)
    : t_Vec t () = 
      if Seq.length v <= max_usize then v else
      FStar.Seq.append v (FStar.Seq.create 1 x)
 
-let impl_1__len #t (v: t_Vec t ()) =
+let impl_1__len #t (#[(Tactics.exact (`()))]_unit:unit) (v: t_Vec t ()) =
   let n = Seq.length v in
   assert (n <= maxint usize_inttype);
   mk_int #usize_inttype (Seq.length v)
diff --git a/proof-libs/fstar/core/Core.Cmp.fsti b/proof-libs/fstar/core/Core.Cmp.fsti
index 58fc8df97..967291795 100644
--- a/proof-libs/fstar/core/Core.Cmp.fsti
+++ b/proof-libs/fstar/core/Core.Cmp.fsti
@@ -1,8 +1,13 @@
 module Core.Cmp
 open Rust_primitives
 
-let min (#t:inttype) (a:int_t t) (b:int_t t) =
-  if a <. b then a else b
+class min_tc t = {
+  min: t -> t -> t
+}
+
+instance min_inttype (#t:inttype): min_tc (int_t t) = {
+  min = fun a b -> if a <. b then a else b
+}
 
 type t_Ordering =
   | Ordering_Less : t_Ordering
diff --git a/proof-libs/fstar/core/Core.Option.fst b/proof-libs/fstar/core/Core.Option.fst
index 77e65eff4..08d8bed2d 100644
--- a/proof-libs/fstar/core/Core.Option.fst
+++ b/proof-libs/fstar/core/Core.Option.fst
@@ -2,7 +2,7 @@ module Core.Option
 
 type t_Option t = | Option_Some of t | Option_None
 
-let impl__and_then #t #t_Self (self: t_Option t_Self) (f: t_Self -> t_Option t): t_Option t = 
+let impl__and_then #t_Self #t (self: t_Option t_Self) (f: t_Self -> t_Option t): t_Option t = 
   match self with
   | Option_Some x -> f x
   | Option_None -> Option_None