More examples, with a loop invariant

Author: pgiarrusso-sl

rocq-brick-libstdcpp/test/dune.inc

@@ -35,6 +35,24 @@
                          (run cpp2v -v %{input} -o N2_input_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ )))
  (alias (name srcs) (deps N2_input.cpp))
 )
+(subdir geeks_for_geeks_examples
+ (rule
+  (targets N3_sum_cpp.v)
+  (alias test_ast)
+  (deps (:input N3_sum.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+                         (run cpp2v -v %{input} -o N3_sum_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ )))
+ (alias (name srcs) (deps N3_sum.cpp))
+)
+(subdir geeks_for_geeks_examples
+ (rule
+  (targets N3_sum_a_cpp.v)
+  (alias test_ast)
+  (deps (:input N3_sum_a.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+                         (run cpp2v -v %{input} -o N3_sum_a_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ )))
+ (alias (name srcs) (deps N3_sum_a.cpp))
+)
 (subdir geeks_for_geeks_examples
  (rule
   (targets iostream_cpp.v)

rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N3_sum.cpp

@@ -0,0 +1,11 @@
+#include <iostream>
+using namespace std;
+
+int main() {
+    int a = 11, b = 9;
+
+    // Adding the two numbers and printing
+    // their sum
+    cout << a + b;
+    return 0;
+}

rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N3_sum.v

@@ -0,0 +1,20 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.spec.
+
+Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N3_sum_cpp.
+
+Import linearity.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  cpp.spec "main()" from source as main_spec with (
+    \prepost{osM} _global "std::cout" |-> ostreamR 1$m osM
+    \pre{str} _global "std::cout" |-> ostream_contentR 1$m str
+    \post[Vint 0]
+      _global "std::cout" |-> ostream_contentR 1$m (str ++ Z_to_string 20)
+  ).
+
+  Lemma main_ok : verify?[source] main_spec.
+  Proof. verify_spec; go. Qed.
+End with_cpp.

rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N3_sum_a.cpp

@@ -0,0 +1,18 @@
+#include <iostream>
+using namespace std;
+
+int main() {
+    int a = 11, b = 9;
+
+    // If b is positive, increment a to b times
+    for (int i = 0; i < b; i++)
+        a++;
+
+    // If b is negative, decrement a to |b| times
+    for (int i = 0; i > b; i--)
+        a--;
+
+    cout << a;
+
+    return 0;
+}

rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N3_sum_a.v

@@ -0,0 +1,37 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.spec.
+
+Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N3_sum_a_cpp.
+
+Import linearity.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  cpp.spec "main()" from source as main_spec with (
+    \prepost{osM} _global "std::cout" |-> ostreamR 1$m osM
+    \pre{str} _global "std::cout" |-> ostream_contentR 1$m str
+    \post[Vint 0]
+      _global "std::cout" |-> ostream_contentR 1$m (str ++ Z_to_string 20)
+  ).
+
+  #[global] Declare Instance Z_to_string_inj : Inj eq eq Z_to_string.
+
+  Lemma main_ok : verify?[source] main_spec.
+  Proof.
+    verify_spec; go.
+
+    wp_for (fun ρ =>
+      \pre{i1} _local ρ "i" |-> intR 1$m i1
+      \pre _local ρ "a" |-> intR 1$m (11 + i1)
+      \require 0 <= i1 <= 9
+      \post* _local ρ "i" |-> anyR "int" 1$m
+      \post* _local ρ "a" |-> intR 1$m 20
+      \post emp
+    ).
+
+    go.
+    wp_if; go.
+    wp_for (fun ρ => emp); go.
+  Qed.
+End with_cpp.