From b82387e0cbb5d96f13427bb6955648b4e9a68cc3 Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Thu, 31 Oct 2024 17:49:51 +0100 Subject: [PATCH] Add coq stack example --- examples/Cargo.toml | 2 +- .../proofs/coq/extraction/Coq_example.v | 170 ++++++++++++++++++ examples/coq-example/src/lib.rs | 86 +++++++++ 3 files changed, 257 insertions(+), 1 deletion(-) create mode 100644 examples/coq-example/proofs/coq/extraction/Coq_example.v create mode 100644 examples/coq-example/src/lib.rs diff --git a/examples/Cargo.toml b/examples/Cargo.toml index 7a79b49ba..a5b3a521b 100644 --- a/examples/Cargo.toml +++ b/examples/Cargo.toml @@ -6,7 +6,7 @@ members = [ "barrett", "kyber_compress", "proverif-psk" -] +, "coq-example"] resolver = "2" [workspace.dependencies] diff --git a/examples/coq-example/proofs/coq/extraction/Coq_example.v b/examples/coq-example/proofs/coq/extraction/Coq_example.v new file mode 100644 index 000000000..6a99f8795 --- /dev/null +++ b/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 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. diff --git a/examples/coq-example/src/lib.rs b/examples/coq-example/src/lib.rs new file mode 100644 index 000000000..2e44072c1 --- /dev/null +++ b/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, + ) { + 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 { + 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