Evenint case study

Co-authored-by: Lennard Gäher <lennard.gaeher@ibm.com>

Makefile

@@ -2,7 +2,7 @@ COQ_PATH =	_build/lib/coq/user-contrib
 RUST_TARGET = $(shell rustc -vV | sed -n 's|host: ||p')
 RUST_PATH =	target/$(RUST_TARGET)/release
 
-CASE_STUDIES = case_studies/paper_examples case_studies/tests case_studies/minivec
+CASE_STUDIES = case_studies/paper_examples case_studies/tests case_studies/minivec case_studies/evenint
 
 ### Project setup
 setup-nix:
@@ -38,8 +38,8 @@ all: frontend typesystem stdlib.proof
 .PHONY: all
 
 ### case studies
-case_studies.proof: typesystem
-case_studies.proof:	$(CASE_STUDIES:=.proof)
+case_studies.proof: typesystem generate_case_studies
+	cd case_studies && dune build --display short
 .PHONY: case_studies.proof
 
 clean_case_studies: $(CASE_STUDIES:=.clean)

case_studies/evenint/Cargo.toml

+[package]
+name = "evenint"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]

case_studies/evenint/RefinedRust.toml

+output_dir = "./output"
+lib_load_paths = ["../../stdlib"]

case_studies/evenint/output/evenint/.gitignore

+generated
+proofs/dune
+interface.rrlib
\ No newline at end of file

case_studies/evenint/output/evenint/proofs/proof_EvenInt_add.v

+From caesium Require Import lang notation.
+From refinedrust Require Import typing shims.
+From refinedrust.examples.evenint.generated Require Import generated_code_evenint generated_specs_evenint generated_template_EvenInt_add.
+
+Set Default Proof Using "Type".
+
+Section proof.
+Context `{!refinedrustGS Σ}.
+
+Lemma EvenInt_add_proof (π : thread_id) :
+  EvenInt_add_lemma π.
+Proof.
+  EvenInt_add_prelude.
+
+  repeat liRStep; liShow.
+
+  all: print_remaining_goal.
+  Unshelve. all: sidecond_solver.
+  Unshelve. all: sidecond_hammer.
+  Unshelve. all: print_remaining_sidecond.
+Qed.
+End proof.

case_studies/evenint/output/evenint/proofs/proof_EvenInt_add_even.v

+From caesium Require Import lang notation.
+From refinedrust Require Import typing shims.
+From refinedrust.examples.evenint.generated Require Import generated_code_evenint generated_specs_evenint generated_template_EvenInt_add_even.
+
+Set Default Proof Using "Type".
+
+Section proof.
+Context `{!refinedrustGS Σ}.
+
+Lemma EvenInt_add_even_proof (π : thread_id) :
+  EvenInt_add_even_lemma π.
+Proof.
+  EvenInt_add_even_prelude.
+
+  repeat liRStep; liShow.
+
+  all: print_remaining_goal.
+  Unshelve. all: sidecond_solver.
+  Unshelve. all: sidecond_hammer.
+  { by apply Zeven_plus_Zeven. }
+  Unshelve. all: print_remaining_sidecond.
+Qed.
+End proof.

case_studies/evenint/output/evenint/proofs/proof_EvenInt_add_two.v

+From caesium Require Import lang notation.
+From refinedrust Require Import typing shims.
+From refinedrust.examples.evenint.generated Require Import generated_code_evenint generated_specs_evenint generated_template_EvenInt_add_two.
+
+Set Default Proof Using "Type".
+
+Section proof.
+Context `{!refinedrustGS Σ}.
+
+Lemma EvenInt_add_two_proof (π : thread_id) :
+  EvenInt_add_two_lemma π.
+Proof.
+  EvenInt_add_two_prelude.
+
+  repeat liRStep; liShow.
+
+  all: print_remaining_goal.
+  Unshelve. all: sidecond_solver.
+  Unshelve. all: sidecond_hammer.
+  { rewrite -Z.add_assoc. apply Zeven_plus_Zeven; done. }
+  Unshelve. all: print_remaining_sidecond.
+Qed.
+End proof.

case_studies/evenint/output/evenint/proofs/proof_EvenInt_check_invariant.v

+From caesium Require Import lang notation.
+From refinedrust Require Import typing shims.
+From refinedrust.examples.evenint.generated Require Import generated_code_evenint generated_specs_evenint generated_template_EvenInt_check_invariant.
+
+Set Default Proof Using "Type".
+
+Section proof.
+Context `{!refinedrustGS Σ}.
+
+Lemma EvenInt_check_invariant_proof (π : thread_id) :
+  EvenInt_check_invariant_lemma π.
+Proof.
+  EvenInt_check_invariant_prelude.
+
+  repeat liRStep; liShow.
+
+  all: print_remaining_goal.
+  Unshelve. all: sidecond_solver.
+  Unshelve. all: sidecond_hammer.
+  { unsafe_unfold_common_caesium_defs. simpl. lia. }
+  { revert select (Zeven z). revert select (z `rem` 2 ≠ 0).
+    rewrite Zeven_ex_iff Z.rem_divide; last done.
+    setoid_rewrite Z.mul_comm; done. }
+  Unshelve. all: print_remaining_sidecond.
+Qed.
+End proof.

case_studies/evenint/output/evenint/proofs/proof_EvenInt_get.v

+From caesium Require Import lang notation.
+From refinedrust Require Import typing shims.
+From refinedrust.examples.evenint.generated Require Import generated_code_evenint generated_specs_evenint generated_template_EvenInt_get.
+
+Set Default Proof Using "Type".
+
+Section proof.
+Context `{!refinedrustGS Σ}.
+
+Lemma EvenInt_get_proof (π : thread_id) :
+  EvenInt_get_lemma π.
+Proof.
+  EvenInt_get_prelude.
+
+  repeat liRStep; liShow.
+
+  all: print_remaining_goal.
+  Unshelve. all: sidecond_solver.
+  Unshelve. all: sidecond_hammer.
+  Unshelve. all: print_remaining_sidecond.
+Qed.
+End proof.

case_studies/evenint/output/evenint/proofs/proof_EvenInt_new.v

+From caesium Require Import lang notation.
+From refinedrust Require Import typing shims.
+From refinedrust.examples.evenint.generated Require Import generated_code_evenint generated_specs_evenint generated_template_EvenInt_new.
+
+Set Default Proof Using "Type".
+
+Section proof.
+Context `{!refinedrustGS Σ}.
+
+Lemma EvenInt_new_proof (π : thread_id) :
+  EvenInt_new_lemma π.
+Proof.
+  EvenInt_new_prelude.
+
+  repeat liRStep; liShow.
+
+  all: print_remaining_goal.
+  Unshelve. all: sidecond_solver.
+  Unshelve. all: sidecond_hammer.
+  Unshelve. all: print_remaining_sidecond.
+Qed.
+End proof.

case_studies/evenint/output/evenint/proofs/proof_EvenInt_new_2.v

+From caesium Require Import lang notation.
+From refinedrust Require Import typing shims.
+From refinedrust.examples.evenint.generated Require Import generated_code_evenint generated_specs_evenint generated_template_EvenInt_new_2.
+
+Set Default Proof Using "Type".
+
+Section proof.
+Context `{!refinedrustGS Σ}.
+
+Lemma EvenInt_new_2_proof (π : thread_id) :
+  EvenInt_new_2_lemma π.
+Proof.
+  EvenInt_new_2_prelude.
+
+  repeat liRStep; liShow.
+
+  all: print_remaining_goal.
+  Unshelve. all: sidecond_solver.
+  Unshelve. all: sidecond_hammer.
+  { unsafe_unfold_common_caesium_defs; simpl. lia. }
+  { apply Zeven_ex_iff.
+    setoid_rewrite <-Z.mul_comm.
+    apply Z.rem_divide; done. }
+  { unsafe_unfold_common_caesium_defs; simpl. lia. }
+  { revert select (i `rem` 2 ≠ 0).
+    rewrite Z.rem_mod_eq_0; last done.
+    rewrite Zmod_odd. intros Hne.
+    apply Zeven_Sn, Zodd_bool_iff.
+    destruct Z.odd; done. }
+  { revert select (i `rem` 2 ≠ 0).
+    rewrite Z.rem_mod_eq_0; last done.
+    rewrite Zmod_odd. intros Hne.
+    apply Zeven_pred, Zodd_bool_iff.
+    destruct Z.odd; done. }
+  Unshelve. all: print_remaining_sidecond.
+Qed.
+End proof.

case_studies/evenint/output/evenint/proofs/proof_EvenInt_new_3.v

+From caesium Require Import lang notation.
+From refinedrust Require Import typing shims.
+From refinedrust.examples.evenint.generated Require Import generated_code_evenint generated_specs_evenint generated_template_EvenInt_new_3.
+
+Set Default Proof Using "Type".
+
+Section proof.
+Context `{!refinedrustGS Σ}.
+
+Lemma EvenInt_new_3_proof (π : thread_id) :
+  EvenInt_new_3_lemma π.
+Proof.
+  EvenInt_new_3_prelude.
+
+  repeat liRStep; liShow.
+
+  all: print_remaining_goal.
+  Unshelve. all: sidecond_solver.
+  Unshelve. all: sidecond_hammer.
+  { unsafe_unfold_common_caesium_defs. simpl. lia. }
+  { apply Zeven_ex_iff.
+    setoid_rewrite <-Z.mul_comm.
+    apply Z.rem_divide; done. }
+  Unshelve. all: print_remaining_sidecond.
+Qed.
+End proof.

case_studies/evenint/src/lib.rs

+#![feature(register_tool)]
+#![register_tool(rr)]
+#![feature(custom_inner_attributes)]
+
+#![rr::include("option")]
+
+#[rr::skip]
+#[rr::returns("()")]
+fn test() {
+    let mut a;
+    let b;
+    unsafe {
+        a = EvenInt::new(0);
+        b = EvenInt::new(2);
+
+        // broken!!
+        let c = EvenInt::new(1);
+    }
+
+    //a.add_even(&b);
+    assert!(a.get() % 2 == 0);
+}
+
+/*
+fn get_even_int_from_user() -> Option<EvenInt> {
+    let a = input(); 
+
+    if a % 2 == 0 {
+        Some(EvenInt::new(a))
+    }
+    else {
+        None
+    }
+}
+*/
+
+
+
+#[rr::refined_by("x" : "Z")]
+#[rr::invariant("Zeven x")]
+struct EvenInt {
+    #[rr::field("x")]
+    num: i32,
+}
+
+
+impl EvenInt {
+    #[rr::params("i" : "Z")]
+    //#[rr::requires("i < MaxInt i32")]
+    #[rr::args("i")] 
+    #[rr::exists("j" : "Z")]
+    #[rr::returns("j")]
+    pub fn new_2(x: i32) -> Self {
+        if x % 2 == 0 {
+            Self {num: x}
+        }
+        else {
+            if x < 1000 {
+                Self { num : x + 1 } 
+            }
+            else {
+                Self { num : x - 1 } 
+            }
+        }
+    }
+
+    #[rr::params("i" : "Z")]
+    #[rr::args("i")] 
+    #[rr::exists("j" : "option Z")]
+    #[rr::returns("<#>@{option} j")]
+    pub fn new_3(x: i32) -> Option<Self> {
+        if x % 2 == 0 {
+            let y = unsafe { Self::new(x) };
+            Some(y)
+        }
+        else {
+            None
+        }
+    }
+
+    /// Create a new even integer.
+    #[rr::params("i" : "Z")]
+    #[rr::args("i")] 
+    #[rr::requires("Zeven i")]
+    #[rr::returns("i")]
+    pub unsafe fn new(x: i32) -> Self {
+        Self {num: x}
+    }
+
+    /// Internal function. Unsafely add 1, making the integer odd.
+    #[rr::params("i", "γ")]
+    #[rr::args(#raw "(# (-[ #i] : plist (λ X, place_rfn X) [_]), γ)")]
+    #[rr::requires("(i+1 ≤ MaxInt i32)%Z")]
+    #[rr::observe("γ": "-[ #(i+1)] : plist (λ X, place_rfn X) [_]")]
+    unsafe fn add(&mut self) {
+        self.num += 1;
+    }
+
+    /// Get the even integer
+    #[rr::params("z")]
+    #[rr::args("#z")]
+    #[rr::ensures("Zeven z")]
+    #[rr::returns("z")]
+    pub fn get(&self) -> i32 {
+        self.num
+    }
+
+    /// This should always succeed.
+    #[rr::params("z")]
+    #[rr::args("#z")]
+    pub fn check_invariant(&self) {
+        assert!(self.get() % 2 == 0);
+    }
+
+    /// Add another even integer.
+    #[rr::params("z", "y", "γ")]
+    #[rr::args("(#z, γ)", "#y")]
+    #[rr::requires("(z + y)%Z ∈ i32")]
+    #[rr::observe("γ": "z + y")]
+    pub fn add_even(&mut self, other: &EvenInt) {
+        self.num += other.num;
+    }
+
+    /// Add 2 to an even integer.
+    #[rr::params("z", "γ")]
+    #[rr::args("(#z, γ)")]
+    #[rr::requires("(z + 2 ≤ MaxInt i32)%Z")]
+    #[rr::observe("γ": "z + 2")]
+    pub fn add_two(&mut self) {
+        self.num;
+
+        unsafe {
+            self.add();
+            self.add();
+        }
+    }
+}

docs/tutorial.md

@@ -57,7 +57,7 @@ struct EvenInt {
 
 impl EvenInt {
     /// Create a new even integer.
-    unsafe pub fn new(x: i32) -> Self {
+    pub unsafe fn new(x: i32) -> Self {
         Self {num: x}
     }
 

stdlib/Makefile

@@ -10,7 +10,8 @@ generate_stdlib: $(STDLIB:=.crate)
 
 clean_stdlib: $(STDLIB:=.clean)
 
-stdlib.proof:	$(STDLIB:=.proof)
+stdlib.proof: generate_stdlib
+	dune build --display short
 
 %.proof:	%.crate
 	cd $* && dune build --display short