Add coq stack example

examples/Cargo.toml

@@ -6,7 +6,7 @@ members = [
     "barrett",
     "kyber_compress",
     "proverif-psk"
-]
+, "coq-example"]
 resolver = "2"
 
 [workspace.dependencies]

examples/coq-example/proofs/coq/extraction/Coq_example.v

@@ -0,0 +1,170 @@
+(* 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.
+
+(* LIBRARY CODE *)
+Definition t_isize := Z.
+Notation "'t_Vec' T '((t_Global))'" := (list T).
+Definition impl_1__push {A} (l : list A) (a : A) : list A := cons a l.
+Definition impl_1__pop {A} (l : list A) : list A * option A :=
+  match l with
+  | [] => ([], None)
+  | (x :: xs) => (xs, Some x)
+  end.
+Definition impl__unwrap {A} (x : option A) `{H : x <> None} : A :=
+  match x as k return k <> None -> _ with
+  | None => fun H => False_rect _ (H eq_refl)
+  | Some a => fun _ => a
+  end H.
+Definition t_Add_f_add := (fun x y => x + y).
+Definition t_Mul_f_mul := (fun x y => x * y).
+Definition t_PartialEq_f_eq := (fun x y => x =? y).
+Definition impl__isize__rem_euclid := fun x y => x mod y.
+Definition cast := fun (x : Z) => x.
+Definition ne := fun x y => negb (x =? y).
+Definition impl_1__len {A} (l : list A) := Z.of_nat (List.length l).
+Definition t_PartialOrd_f_lt := fun x y => x <? y.
+Notation "'Option_Some'" := Some.
+Notation "'Option_None'" := None.
+Definition sub := fun x y => x - y.
+Definition impl__new {A} (tt : unit) : list A := [].
+Definition f_fold {A B} (l : list A) (i : B) (f : B -> A -> B) : B := List.fold_left f l i.
+Definition f_into_iter {A} := @id A.
+(* /LIBRARY CODE *)
+
+
+
+Inductive t_Instruction : Type :=
+| Instruction_Push : t_isize -> _
+| Instruction_Pop
+| Instruction_Add
+| Instruction_Sub
+| Instruction_Mul
+| Instruction_Not
+| Instruction_Dup.
+Arguments t_Instruction:clear implicits.
+Arguments t_Instruction.
+
+(* NotImplementedYet *)
+
+Definition impl__Instruction__interpret (self : t_Instruction) (stack : t_Vec ((t_isize)) ((t_Global))) : t_Vec ((t_isize)) ((t_Global)) :=
+  let (stack,hax_temp_output) := match self with
+  | Instruction_Push (v) =>
+    (impl_1__push (stack) (v),tt)
+  | Instruction_Pop =>
+    let (tmp0,out) := impl_1__pop (stack) in
+    let stack := tmp0 in
+    let _ := out in
+    (stack,tt)
+  | Instruction_Add =>
+    let (tmp0,out) := impl_1__pop (stack) in
+    let stack := tmp0 in
+    let hoist2 := out in
+    let (tmp0,out) := impl_1__pop (stack) in
+    let stack := tmp0 in
+    let hoist1 := out in
+    let hoist3 := (hoist2,hoist1) in
+    match hoist3 with
+    | (Option_Some (a),Option_Some (b)) =>
+      (impl_1__push (stack) (t_Add_f_add (b) (a)),tt)
+    | _ =>
+      (stack,tt)
+    end
+  | Instruction_Sub =>
+    let (tmp0,out) := impl_1__pop (stack) in
+    let stack := tmp0 in
+    let hoist5 := out in
+    let (tmp0,out) := impl_1__pop (stack) in
+    let stack := tmp0 in
+    let hoist4 := out in
+    let hoist6 := (hoist5,hoist4) in
+    match hoist6 with
+    | (Option_Some (a),Option_Some (b)) =>
+      (impl_1__push (stack) (sub (b) (a)),tt)
+    | _ =>
+      (stack,tt)
+    end
+  | Instruction_Mul =>
+    let (tmp0,out) := impl_1__pop (stack) in
+    let stack := tmp0 in
+    let hoist8 := out in
+    let (tmp0,out) := impl_1__pop (stack) in
+    let stack := tmp0 in
+    let hoist7 := out in
+    let hoist9 := (hoist8,hoist7) in
+    match hoist9 with
+    | (Option_Some (a),Option_Some (b)) =>
+      (impl_1__push (stack) (t_Mul_f_mul (b) (a)),tt)
+    | _ =>
+      (stack,tt)
+    end
+  | Instruction_Not =>
+    let (tmp0,out) := impl_1__pop (stack) in
+    let stack := tmp0 in
+    let hoist10 := out in
+    match hoist10 with
+    | Option_Some (a) =>
+      (impl_1__push (stack) (if
+        t_PartialEq_f_eq (a) (0)
+      then
+        1
+      else
+        0),tt)
+    | _ =>
+      (stack,tt)
+    end
+  | Instruction_Dup =>
+    let (tmp0,out) := impl_1__pop (stack) in
+    let stack := tmp0 in
+    let hoist11 := out in
+    match hoist11 with
+    | Option_Some (a) =>
+      let stack := impl_1__push (stack) (a) in
+      let stack := impl_1__push (stack) (a) in
+      (stack,tt)
+    | _ =>
+      (stack,tt)
+    end
+  end in
+  stack.
+
+Definition example (_ : unit) : t_Vec ((t_isize)) ((t_Global)) :=
+  let stk := impl__new (tt) in
+  let stk := f_fold (f_into_iter ([Instruction_Push (1); Instruction_Push (1); Instruction_Add; Instruction_Push (1); Instruction_Push (1); Instruction_Push (1); Instruction_Add; Instruction_Add; Instruction_Dup; Instruction_Mul; Instruction_Sub])) (stk) (fun stk cmd =>
+    impl__Instruction__interpret (cmd) (stk)) in
+  stk.
+
+(* Handwritten Proofs *)
+
+(* Check example *)
+Example is_example_correct : example tt = [-7]. Proof. reflexivity. Qed.
+
+(* Proof composite operations *)
+Theorem dup_mul_is_square : forall x,
+    impl__Instruction__interpret Instruction_Mul (
+        impl__Instruction__interpret Instruction_Dup [x])
+    = [Z.pow x 2].
+Proof.
+  intros.
+  cbn.
+  rewrite Z.mul_1_r.
+  reflexivity.
+Qed.
+
+Theorem push_pop_cancel : forall l x,
+    impl__Instruction__interpret Instruction_Pop (
+        impl__Instruction__interpret (Instruction_Push x) l)
+    = l.
+Proof.
+  intros.
+  cbn.
+  reflexivity.
+Qed.

examples/coq-example/src/lib.rs

@@ -0,0 +1,86 @@
+enum Instruction {
+    Push(isize),
+    Pop,
+    Add,
+    Sub,
+    Mul,
+    Not,
+    Dup,
+}
+
+impl Instruction {
+    pub fn interpret(
+        self,
+        stack: &mut Vec<isize>,
+    ) {
+        match self {
+            Instruction::Push(v) => stack.push(v),
+            Instruction::Pop => {
+                stack.pop();
+            }
+            Instruction::Add => {
+                match (stack.pop(), stack.pop()) {
+                    (Some(a), Some(b)) => stack.push(b + a),
+                    _ => (),
+                }
+            }
+            Instruction::Sub => {
+                match (stack.pop(), stack.pop()) {
+                    (Some(a), Some(b)) => stack.push(b - a),
+                    _ => (),
+                }
+            }
+            Instruction::Mul => {
+                match (stack.pop(), stack.pop()) {
+                    (Some(a), Some(b)) => stack.push(b * a),
+                    _ => (),
+                }
+            }
+            Instruction::Not => {
+                match stack.pop() {
+                    Some(a) => stack.push(if a == 0 { 1 } else { 0 }),
+                    _ => (),
+                }
+            }
+            Instruction::Dup => {
+                match stack.pop() {
+                    Some(a) => {
+                        stack.push(a);
+                        stack.push(a);
+                    }
+                    _ => (),
+                }
+            }
+        }
+    }
+}
+
+fn example () -> Vec<isize> {
+    let mut stk = Vec::new();
+    for cmd in [
+        Instruction::Push(1),
+        Instruction::Push(1),
+        Instruction::Add,
+        Instruction::Push(1),
+        Instruction::Push(1),
+        Instruction::Push(1),
+        Instruction::Add,
+        Instruction::Add,
+        Instruction::Dup,
+        Instruction::Mul,
+        Instruction::Sub] {
+        cmd.interpret(&mut stk)
+    }
+    stk
+}
+// Push 1: 1
+// Push 1: 1, 1
+//    Add: 2
+// Push 1: 2, 1
+// Push 1: 2, 1, 1
+// Push 1: 2, 1, 1, 1
+//    Add: 2, 1, 2
+//    Add: 2, 3
+//    Dup: 2, 3, 3
+//    Mul: 2, 9
+//    Sub: -7