Add existing roundtrip test to Kani CI and avoid recursive submoduling (

tokio-rs#828)

* Add existing roundtrip test to Kani CI

* Bump up Kani version

* Remove `v` from GA version

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

@@ -103,15 +103,14 @@ jobs:
     steps:
       - name: checkout
         uses: actions/checkout@v3
-        with:
-          submodules: recursive
       - name: Verify with Kani
-        uses: model-checking/kani-github-action@v0.19
+        uses: model-checking/kani-github-action@0.23
         with:
           enable-propproof: true
           args: |
             --tests -p prost-types --default-unwind 3 \
-            --harness "tests::check_timestamp_roundtrip_via_system_time"
+            --harness "tests::check_timestamp_roundtrip_via_system_time" \
+            --harness "tests::check_duration_roundtrip_nanos"
         # --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

KANI.md

@@ -19,7 +19,7 @@ capabilities and limitations.
   from the Kani repository.
   ```bash
   git clone https://github.com/model-checking/kani.git --branch features/proptest propproof
-  cd propproof; git submodule update --init --recursive
+  cd propproof; git submodule update --init
   ```
 
   Then, use `.cargo/config.toml` enable it in the local directory you
@@ -34,7 +34,7 @@ capabilities and limitations.
 
 **Please Note**:
 - `features/proptest` branch under Kani is likely not the final
-  location for this code. If this instruction stops working, please
+  location for this code. If these instructions stop working, please
   consult the Kani documentation and file an issue on [the Kani
   repo](https://github.com/model-checking/kani.git).
 - The cargo config file will force cargo to always use PropProof. To