Added Kani to CI. (#1)

* Added kani integration.

* Fix yaml problem.

* yaml hash problem

* No need to cd?

* Use new release, not the hash

* Added comment describing the unwind value.

Co-authored-by: Yoshiki Takashima <[email protected]>

.github/workflows/continuous-integration-workflow.yaml

@@ -96,6 +96,27 @@ jobs:
           command: test
           args: --no-default-features
 
+  kani:
+    runs-on: ubuntu-latest
+    steps:
+      - name: checkout
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - name: Verify with Kani
+        uses: model-checking/[email protected]
+        with:
+          enable-propproof: true
+          args: |
+            --tests -p prost-types --default-unwind 3 \
+            --harness "tests::check_timestamp_roundtrip_via_system_time"
+        # --default-unwind N roughly corresponds to how much effort
+        # Kani will spend trying to prove correctness of the
+        # program. Higher the number, more programs can be proven
+        # correct. However, Kani will require more time and memory. If
+        # Kani fails with "Failed Checks: unwinding assertion," this
+        # number may need to be raised for Kani to succeed.
+
   no-std:
     runs-on: ubuntu-latest
     steps: