Merge pull request #772 from formal-land/guillaume-claret@add-simulate-get_or_zero-example

Simulate: add get_or_zero example

Author: clarus

CoqOfRust/core/links/array.v

@@ -26,6 +26,18 @@ Module ArrayPairs.
     | S length, {| ArrayPair.x := x; ArrayPair.xs := xs |} => φ x :: to_values xs
     end.
 
+  Fixpoint to_tuple_rev_Set (A : Set) (length : nat) : Set :=
+    match length with
+    | O => unit
+    | S length => to_tuple_rev_Set A length * A
+    end.
+
+  Fixpoint to_tuple_rev {A : Set} {length : nat} (xs : t A length) : to_tuple_rev_Set A length :=
+    match length, xs with
+    | O, ArrayEmpty.Make => tt
+    | S length, {| ArrayPair.x := x; ArrayPair.xs := xs |} => (to_tuple_rev xs, x)
+    end.
+
   Fixpoint of_list {A : Set} (xs : list A) : t A (List.length xs) :=
     match xs with
     | [] => ArrayEmpty.Make

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

@@ -1,6 +1,7 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import CoqOfRust.simulate.M.
+Require Import core.links.array.
 Require Import examples.default.examples.custom.links.loops_free.
 
 Definition max2 (a b : U32.t) : U32.t :=
@@ -61,3 +62,72 @@ Proof.
   { apply Run.Pure. }
 Qed.
 Global Opaque run_max2.
+
+Definition get_or_zero (xs : array.t U32.t {| Integer.value := 4 |}) (i : Usize.t) : U32.t :=
+  let i := i.(Integer.value) in
+  let xs := ArrayPairs.to_tuple_rev xs.(array.value) in
+  match xs with
+  | (tt, x3, x2, x1, x0) =>
+    if i =? 0 then
+      x0
+    else if i =? 1 then
+      x1
+    else if i =? 2 then
+      x2
+    else if i =? 3 then
+      x3
+    else
+      {| Integer.value := 0 |}
+  end.
+
+Lemma get_or_zero_eq
+    (xs : array.t U32.t {| Integer.value := 4 |}) (i : Usize.t)
+    (H_i : 0 <= i.(Integer.value)) :
+  let ref_xs := make_ref 0 in
+  let stack := (xs, tt) in
+  {{
+    SimulateM.eval_f (Stack := [_]) (run_get_or_zero ref_xs i) stack 🌲
+    (Output.Success (get_or_zero xs i), stack)
+  }}.
+Proof.
+  destruct xs as [[x0 [x1 [x2 [x3 []]]]]].
+  destruct i as [i]; cbn in H_i.
+  unfold get_or_zero; cbn.
+  eapply Run.Call; cbn. {
+    apply Run.Pure.
+  }
+  cbn.
+  eapply Run.Call; cbn. {
+    apply Run.Pure.
+  }
+  cbn.
+  destruct (_ <? 4) eqn:?; cbn.
+  { progress repeat get_can_access.
+    unfold ArrayPairs.to_tuple_rev, Pos.to_nat; cbn.
+    destruct (i =? 0) eqn:?. {
+      replace i with 0 by lia; cbn.
+      apply Run.Pure.
+    }
+    destruct (i =? 1) eqn:?. {
+      replace i with 1 by lia; cbn.
+      apply Run.Pure.
+    }
+    destruct (i =? 2) eqn:?. {
+      replace i with 2 by lia; cbn.
+      apply Run.Pure.
+    }
+    destruct (i =? 3) eqn:?. {
+      replace i with 3 by lia; cbn.
+      apply Run.Pure.
+    }
+    lia.
+  }
+  { unfold ArrayPairs.to_tuple_rev, Pos.to_nat; cbn.
+    destruct (i =? 0) eqn:?; [lia|].
+    destruct (i =? 1) eqn:?; [lia|].
+    destruct (i =? 2) eqn:?; [lia|].
+    destruct (i =? 3) eqn:?; [lia|].
+    apply Run.Pure.
+  }
+Qed.
+Global Opaque run_get_or_zero.