Repository: cryspen/hax (language: rust)

Issue:
Engine: F*: Missing `rec` qualifier in a mutually recursive top-level `let`
In some situations (likely connected to mutual bundles), mutual recursive functions get translated to `let ... and ...` bundles, but without the `rec`.
We need a reproducer here.


Discussion / hints:
Here is a simple reproducer:
```rust

mod a {
    pub trait A{
        fn f(&self);
    }
    impl A for i32 {

        fn f(&self){
            g(*self)
        }
    }
    pub fn g(x: i32) {super::b::h(x)}
}
mod b {
    pub fn h(x: impl super::a::A){x.f()}
}
```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/de59826b83/gist=b77a26fff7632965121d6a74a2dfca86)

This happens because the trait impl is considered to be part of the item-wise bundle. We should force item-wise bundles to contain either only functions or only types.
This is actually tricky. We can minimize further to:
```rust

pub trait A{
    fn f(&self);
}
impl A for i32 {

    fn f(&self){
        g(*self)
    }
}
pub fn g(x: i32) {x.f()}

```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/18ac15e70b/gist=34b7fa6f23630a961f722aff9584de29)
This is translated to the following F*: 
```
class t_A (v_Self: Type0) = {
  f_f_pre:v_Self -> Type0;
  f_f_post:v_Self -> Prims.unit -> Type0;
  f_f:x0: v_Self
    -> Prims.Pure Prims.unit
        (f_f_pre x0)
        (fun result -> f_f_post x0 result)
}

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_A_for_i32: t_A i32 =
  {
    f_f_pre = (fun (self: i32) -> true);
    f_f_post
    =
    (fun (self: i32) (out: Prims.unit) ->
        true);
    f_f = fun (self: i32) -> g self
  }

and g (x: i32) : Prims.unit =
  f_f #i32
    #FStar.Tactics.Typeclasses.solve
    x
```
Here there is a mutual recursion between a method from a trait impl, and a top-level function. At the item level we have a cyclic dependency between `g` and `impl_A_for_i32` but we cannot declare the impl with a `let rec`. 

I think the only way to solve this would be to hoist the method outside the impl. That can at least give a workaround (hoisting manually). 
After more investigation the reproducer is for a different problem. We should investigate more, there could be a bug in how we compute the dependency graph.
Here is a reproducer: https://github.com/hacspec/hax/issues/1186.

This is linked to naming (clash of names with bundling).
```rust
trait T { fn f(); }

pub mod a {
    impl super::T for u8{ fn f(){g()}}
    pub fn g(){super::b::g()}
}

pub mod b {
    impl super::T for i8 { fn f(){}}
    pub fn g(){super::a::g()}
}
```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/62f7bfabe3/gist=491e7719d1c6a774ef1ff774e5ffec01)

Here is another interesting reproducer without bundles:
```rust


fn f () {g()}

fn f_2(){f()}

fn g () {f()}

```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/98ded931ba/gist=0e13f4bd0b682989d1055214ec8c6a20)

The problem is that mutual recursion is treated by inserting a `rec` in front of the first item in the mutual recursion and an `and` in front of the others. But we assume that they will come next to one another in the ordering which is apparently not true. So this is an issue in items sorting.
I tried using https://github.com/hacspec/hax/pull/1140 which doesn't fix the problem. We probably need to add some dependencies in the dependency graph to treat a set of mutually recursive items as atomic.
I believe this comes from a bug in ocamlgraph. I opened https://github.com/backtracking/ocamlgraph/issues/149
I implemented a simple fix to ocamlgraph so if we don't get an answer quickly we have something we can use in a fork.

Actually it might be a good thing not to rely on a standard implementation for this (except if we know what it does), because if you think of a graph like a <->c   b <->d and want a stable topological sort with lexical order, then a, b, c, d could be considered the best answer but in our case we want elements that belong to the same cycle grouped together. My fork would behave well (for us) with respect to this but let's see if whatever solution that gets into ocamlgraph has this property.

Fix patch:
diff --git a/engine/default.nix b/engine/default.nix
index 1a676c743..adc4eb5f2 100644
--- a/engine/default.nix
+++ b/engine/default.nix
@@ -1,24 +1,16 @@
-{
-  ocamlPackages,
-  fetchzip,
-  hax-rust-frontend,
-  hax-engine-names-extract,
-  rustc,
-  nodejs,
-  jq,
-  closurecompiler,
-  gnused,
-  lib,
-  removeReferencesTo,
-}: let
+{ ocamlPackages, fetchzip, hax-rust-frontend, hax-engine-names-extract, rustc
+, nodejs, jq, closurecompiler, gnused, lib, removeReferencesTo, fetchFromGitHub
+}:
+let
   non_empty_list = ocamlPackages.buildDunePackage rec {
     pname = "non_empty_list";
     version = "0.1";
     src = fetchzip {
-      url = "https://github.com/johnyob/ocaml-non-empty-list/archive/refs/tags/${version}.zip";
+      url =
+        "https://github.com/johnyob/ocaml-non-empty-list/archive/refs/tags/${version}.zip";
       sha256 = "sha256-BJlEi0yG2DRT5vuU9ulucMD5MPFt9duWgcNO1YsigiA=";
     };
-    buildInputs = with ocamlPackages; [base ppxlib ppx_deriving];
+    buildInputs = with ocamlPackages; [ base ppxlib ppx_deriving ];
     duneVersion = "3";
     minimalOCamlVersion = "4.08";
     doCheck = false;
@@ -28,13 +20,12 @@
     version = "0.1";
 
     src = fetchzip {
-      url = "https://github.com/wrbs/ppx_matches/archive/refs/tags/${version}.zip";
+      url =
+        "https://github.com/wrbs/ppx_matches/archive/refs/tags/${version}.zip";
       sha256 = "sha256-nAmWF8MgW0odKkRiFcHGsvJyIxNHaZpnOlNPsef89Fo=";
     };
 
-    buildInputs = [
-      ocamlPackages.ppxlib
-    ];
+    buildInputs = [ ocamlPackages.ppxlib ];
     duneVersion = "3";
     minimalOCamlVersion = "4.04";
     doCheck = false;
@@ -43,7 +34,17 @@
     pname = "hax-engine";
     version = "0.0.1";
     duneVersion = "3";
-    src = lib.sourceFilesBySuffices ./. [".ml" ".mli" ".js" "dune" "dune-js" "dune-project" "sh" "rs" "mld"];
+    src = lib.sourceFilesBySuffices ./. [
+      ".ml"
+      ".mli"
+      ".js"
+      "dune"
+      "dune-js"
+      "dune-project"
+      "sh"
+      "rs"
+      "mld"
+    ];
     buildInputs = with ocamlPackages;
       [
         base
@@ -65,18 +66,17 @@
         stdio
         re
         js_of_ocaml
-        ocamlgraph
-      ]
-      ++
+        (ocamlgraph.overrideAttrs (_: {
+          src = fetchFromGitHub {
+            owner = "maximebuyse";
+            repo = "ocamlgraph";
+            rev = "fix-stable-topological-sort";
+            sha256 = "sha256-l7v7Kxjaz3xP6T91peAzloyusxpsIOYHXLIiiRHa490=";
+          };
+        }))
+      ] ++
       # F* dependencies
-      [
-        batteries
-        menhirLib
-        ppx_deriving
-        ppxlib
-        sedlex
-        stdint
-      ];
+      [ batteries menhirLib ppx_deriving ppxlib sedlex stdint ];
     nativeBuildInputs = [
       rustc
       hax-rust-frontend
@@ -92,23 +92,19 @@
       find "$bin" -type f -exec remove-references-to -t ${ocamlPackages.ocaml} '{}' +
     '';
 
-    outputs = ["out" "bin" "lib"];
+    outputs = [ "out" "bin" "lib" ];
     passthru = {
       docs = hax-engine.overrideAttrs (old: {
         name = "hax-engine-docs";
-        nativeBuildInputs =
-          old.nativeBuildInputs
-          ++ [
-            ocamlPackages.odoc
-          ];
-        buildPhase = ''dune build @doc'';
+        nativeBuildInputs = old.nativeBuildInputs ++ [ ocamlPackages.odoc ];
+        buildPhase = "dune build @doc";
         installPhase = "cp -rf _build/default/_doc/_html $out";
-        outputs = ["out"];
+        outputs = [ "out" ];
       });
       js = hax-engine.overrideAttrs (old: {
         name = "hax-engine.js";
-        nativeBuildInputs = old.nativeBuildInputs ++ [closurecompiler gnused];
-        outputs = ["out"];
+        nativeBuildInputs = old.nativeBuildInputs ++ [ closurecompiler gnused ];
+        outputs = [ "out" ];
         buildPhase = ''
           # Enable JS build
           sed -i "s/; (include dune-js)/(include dune-js)/g" bin/dune
@@ -125,5 +121,4 @@
       });
     };
   };
-in
-  hax-engine.overrideAttrs (_: {name = "hax-engine";})
+in hax-engine.overrideAttrs (_: { name = "hax-engine"; })
diff --git a/engine/hax-engine.opam b/engine/hax-engine.opam
index e317a03f5..56b671995 100644
--- a/engine/hax-engine.opam
+++ b/engine/hax-engine.opam
@@ -59,4 +59,7 @@ build: [
 dev-repo: "git+https://github.com/hacspec/hax.git"
 depexts: [
   ["nodejs"] {}
+]
+pin-depends: [
+  ["ocamlgraph" "git+https://github.com/maximebuyse/ocamlgraph.git#fix-stable-topological-sort"]
 ]
\ No newline at end of file
diff --git a/engine/hax-engine.opam.template b/engine/hax-engine.opam.template
index 43794c9a8..593f86aaa 100644
--- a/engine/hax-engine.opam.template
+++ b/engine/hax-engine.opam.template
@@ -1,3 +1,6 @@
 depexts: [
   ["nodejs"] {}
+]
+pin-depends: [
+  ["ocamlgraph" "git+https://github.com/maximebuyse/ocamlgraph.git#fix-stable-topological-sort"]
 ]
\ No newline at end of file


Test patch:
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index 8705e5981..9eb7c82e7 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
@@ -516,6 +516,8 @@ let add3_lemma (x: u32)
         x <=. 10ul || x >=. (u32_max /! 3ul <: u32) || (add3 x x x <: u32) =. (x *! 3ul <: u32)) =
   ()
 
+unfold let some_function _ = "hello from F*"
+
 let before_inlined_code = "example before"
 
 let inlined_code (foo: t_Foo) : Prims.unit =
@@ -528,6 +530,4 @@ let inlined_code (foo: t_Foo) : Prims.unit =
   ()
 
 let inlined_code_after = "example after"
-
-unfold let some_function _ = "hello from F*"
 '''
diff --git a/test-harness/src/snapshots/toolchain__reordering into-coq.snap b/test-harness/src/snapshots/toolchain__reordering into-coq.snap
index d3b0567d8..42cbf0bbf 100644
--- a/test-harness/src/snapshots/toolchain__reordering into-coq.snap
+++ b/test-harness/src/snapshots/toolchain__reordering into-coq.snap
@@ -67,6 +67,8 @@ Definition t_Foo_cast_to_repr (x : t_Foo) : t_isize :=
 
 (* NotImplementedYet *)
 
+(* NotImplementedYet *)
+
 Definition f (_ : t_u32) : t_Foo :=
   Foo_A.
 
@@ -79,3 +81,25 @@ Definition no_dependency_1_ (_ : unit) : unit :=
 Definition no_dependency_2_ (_ : unit) : unit :=
   tt.
 '''
+"Reordering_Mut_rec.v" = '''
+(* File automatically generated by Hacspec *)
+From Coq Require Import ZArith.
+Require Import List.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+Require Import Ascii.
+Require Import String.
+Require Import Coq.Floats.Floats.
+From RecordUpdate Require Import RecordSet.
+Import RecordSetNotations.
+
+Definition f (_ : unit) : unit :=
+  g (tt).
+
+Definition g (_ : unit) : unit :=
+  f (tt).
+
+Definition ff_2_ (_ : unit) : unit :=
+  f (tt).
+'''
diff --git a/test-harness/src/snapshots/toolchain__reordering into-fstar.snap b/test-harness/src/snapshots/toolchain__reordering into-fstar.snap
index 50d0e39c8..d2d516b69 100644
--- a/test-harness/src/snapshots/toolchain__reordering into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__reordering into-fstar.snap
@@ -26,6 +26,18 @@ exit = 0
 diagnostics = []
 
 [stdout.files]
+"Reordering.Mut_rec.fst" = '''
+module Reordering.Mut_rec
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let rec f (_: Prims.unit) : Prims.unit = g ()
+
+and g (_: Prims.unit) : Prims.unit = f ()
+
+let ff_2_ (_: Prims.unit) : Prims.unit = f ()
+'''
 "Reordering.fst" = '''
 module Reordering
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
diff --git a/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap b/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap
index b6655f747..e0130182c 100644
--- a/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap
+++ b/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap
@@ -92,6 +92,8 @@ Fail Next Obligation.
 
 (*Not implemented yet? todo(item)*)
 
+(*Not implemented yet? todo(item)*)
+
 Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 int32) : both L1 I1 t_Foo :=
   f _  :=
     Foo_A : both L1 I1 t_Foo.
@@ -112,3 +114,45 @@ Equations no_dependency_2_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1
     solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
 Fail Next Obligation.
 '''
+"Reordering_Mut_rec.v" = '''
+(* File automatically generated by Hacspec *)
+Set Warnings "-notation-overridden,-ambiguous-paths".
+From Crypt Require Import choice_type Package Prelude.
+Import PackageNotation.
+From extructures Require Import ord fset.
+From mathcomp Require Import word_ssrZ word.
+From Jasmin Require Import word.
+
+From Coq Require Import ZArith.
+From Coq Require Import Strings.String.
+Import List.ListNotations.
+Open Scope list_scope.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+From Hacspec Require Import ChoiceEquality.
+From Hacspec Require Import LocationUtility.
+From Hacspec Require Import Hacspec_Lib_Comparable.
+From Hacspec Require Import Hacspec_Lib_Pre.
+From Hacspec Require Import Hacspec_Lib.
+
+Open Scope hacspec_scope.
+Import choice.Choice.Exports.
+
+Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
+
+Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  f _  :=
+    solve_lift (g (ret_both (tt : 'unit))) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations g {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  g _  :=
+    solve_lift (f (ret_both (tt : 'unit))) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations ff_2_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  ff_2_ _  :=
+    solve_lift (f (ret_both (tt : 'unit))) : both L1 I1 'unit.
+Fail Next Obligation.
+'''
diff --git a/tests/reordering/src/lib.rs b/tests/reordering/src/lib.rs
index 03e4d0ea8..fb03140e2 100644
--- a/tests/reordering/src/lib.rs
+++ b/tests/reordering/src/lib.rs
@@ -17,3 +17,17 @@ enum Foo {
     A,
     B,
 }
+
+mod mut_rec {
+    fn f() {
+        g()
+    }
+
+    fn f_2() {
+        f()
+    }
+
+    fn g() {
+        f()
+    }
+}