Use ocamlgraph fork to fix missing rec bug.

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"]
 ]

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"]
 ]

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*"
 '''

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).
+'''

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"

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.
+'''

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()
+    }
+}