Merge pull request #768 from formal-land/guillaume-claret@add-link-simulate-example

Add links and simulate example

Author: clarus

CoqOfRust/examples/default/examples/custom/links/loops_free.v

@@ -0,0 +1,10 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import examples.default.examples.custom.loops_free.
+
+(* pub fn max2(a: u32, b: u32) -> u32 *)
+Instance run_max2 (a b : U32.t) : Run.Trait max2 [] [] [φ a; φ b] U32.t.
+Proof.
+  constructor.
+  run_symbolic.
+Defined.

CoqOfRust/examples/default/examples/custom/simulate/loops_free.v

@@ -0,0 +1,26 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import CoqOfRust.simulate.M.
+Require Import examples.default.examples.custom.links.loops_free.
+
+Definition max2 (a b : U32.t) : U32.t :=
+  if a.(Integer.value) <? b.(Integer.value) then
+    b
+  else
+    a.
+
+Lemma max2_eq (a b : U32.t) :
+  {{
+    SimulateM.eval_f (Stack := []) (run_max2 a b) tt 🌲
+    (Output.Success (max2 a b), tt)
+  }}.
+Proof.
+  unfold max2.
+  repeat (
+    cbn ||
+    get_can_access ||
+    eapply Run.Call ||
+    apply Run.Pure ||
+    destruct (_ <? _)
+  ).
+Qed.