ENG-162 add Kani invariant coverage

.github/workflows/kani.yml

@@ -0,0 +1,197 @@
+name: Kani
+
+on:
+  schedule:
+    # Nightly verification on the default branch.
+    - cron: "0 2 * * *"
+  workflow_dispatch:
+  pull_request:
+    branches: [main, dev]
+    paths:
+      - ".github/workflows/kani.yml"
+      - "Cargo.toml"
+      - "Cargo.lock"
+      - "common/**"
+      - "contract/universal-account/**"
+      - "contract/vault/kernel/**"
+      - "fuzz/fuzz_targets/fuzz_fee_math.rs"
+      - "test-utils/src/controller/universal_account.rs"
+      - "universal-account/**"
+
+concurrency:
+  group: kani-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+env:
+  KANI_VERSION: "0.67.0"
+  CARGO_TERM_COLOR: always
+  CARGO_INCREMENTAL: 0
+
+jobs:
+  universal-account:
+    name: Universal Account
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5
+        with:
+          persist-credentials: false
+
+      - name: Run Universal Account Kani proofs
+        uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126
+        with:
+          kani-version: ${{ env.KANI_VERSION }}
+          command: cargo-kani
+          args: -p templar-universal-account
+
+  vault-kernel:
+    name: Vault Kernel
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5
+        with:
+          persist-credentials: false
+
+      - name: Run Vault Kernel Kani proofs
+        uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126
+        with:
+          kani-version: ${{ env.KANI_VERSION }}
+          command: cargo-kani
+          args: -p templar-vault-kernel
+
+  vault-kernel-sync-external:
+    name: Vault Kernel / Sync External
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5
+        with:
+          persist-credentials: false
+
+      - name: Run Vault Kernel external sync immutability Kani proofs
+        uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126
+        with:
+          kani-version: ${{ env.KANI_VERSION }}
+          command: cargo-kani
+          args: >-
+            -p templar-vault-kernel
+            --features action-sync-external
+            --harness rebalance_withdraw_conserves_total_assets_and_moves_external_to_idle
+            --harness sync_external_assets_preserves_total_as_idle_plus_external
+            --harness bounded_sync_then_rebalance_conserves_accounting_across_actions
+            --harness sync_external_assets_allocating_only_mutates_external_and_total_assets
+            --harness sync_external_assets_withdrawing_preserves_share_supply_queue_and_actor_fields
+            --harness sync_external_assets_refreshing_only_mutates_external_and_total_assets
+            --harness sync_external_assets_rejects_wrong_op_id_and_disallowed_states
+
+  vault-kernel-withdraw-escrow:
+    name: Vault Kernel / Withdraw Escrow
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5
+        with:
+          persist-credentials: false
+
+      - name: Run Vault Kernel withdraw escrow Kani proof
+        uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126
+        with:
+          kani-version: ${{ env.KANI_VERSION }}
+          command: cargo-kani
+          args: >-
+            -p templar-vault-kernel
+            --harness post_deposit_request_withdraw_preserves_accounting_and_escrows_previewed_shares
+
+  vault-kernel-allocation-lifecycle:
+    name: Vault Kernel / Allocation Lifecycle
+    runs-on: ubuntu-latest
+    timeout-minutes: 25
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5
+        with:
+          persist-credentials: false
+
+      - name: Run Vault Kernel allocation lifecycle Kani proofs
+        uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126
+        with:
+          kani-version: ${{ env.KANI_VERSION }}
+          command: cargo-kani
+          args: >-
+            -p templar-vault-kernel
+            --features action-allocation-lifecycle,action-sync-external,action-recovery
+            --harness allocation_partial_sync_then_abort_restores_unallocated_assets
+            --harness allocation_full_sync_then_finish_conserves_assets
+            --harness allocation_wrong_op_id_is_rejected_without_progress
+
+  vault-kernel-refresh-lifecycle:
+    name: Vault Kernel / Refresh Lifecycle
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5
+        with:
+          persist-credentials: false
+
+      - name: Run Vault Kernel refresh lifecycle Kani proofs
+        uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126
+        with:
+          kani-version: ${{ env.KANI_VERSION }}
+          command: cargo-kani
+          args: >-
+            -p templar-vault-kernel
+            --features action-refresh-lifecycle,action-sync-external
+            --harness refresh_lifecycle_mutates_only_external_assets_and_returns_idle
+
+  vault-kernel-recovery:
+    name: Vault Kernel / Recovery
+    runs-on: ubuntu-latest
+    timeout-minutes: 25
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5
+        with:
+          persist-credentials: false
+
+      - name: Run Vault Kernel emergency recovery Kani proofs
+        uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126
+        with:
+          kani-version: ${{ env.KANI_VERSION }}
+          command: cargo-kani
+          args: >-
+            -p templar-vault-kernel
+            --features action-recovery
+            --harness emergency_reset_allocating_restores_remaining_assets_to_idle
+            --harness emergency_reset_withdrawing_restores_collected_assets_and_refunds_escrow
+            --harness emergency_reset_payout_restores_payout_assets_and_refunds_escrow
+            --harness emergency_reset_refreshing_returns_idle_without_accounting_mutation
+
+  vault-kernel-refresh-fees:
+    name: Vault Kernel / Refresh Fees
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5
+        with:
+          persist-credentials: false
+
+      - name: Run Vault Kernel refresh fee Kani proofs
+        uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126
+        with:
+          kani-version: ${{ env.KANI_VERSION }}
+          command: cargo-kani
+          args: >-
+            -p templar-vault-kernel
+            --features action-refresh-fees
+            --harness refresh_fees_zero_fee_rates_only_update_anchor
+            --harness refresh_fees_active_rates_only_mint_fee_shares_and_update_anchor

Cargo.toml

@@ -202,6 +202,9 @@ doc_markdown = "allow"
 result_large_err = "allow"
 ignore_without_reason = "allow"
 
+[workspace.lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
+
 [profile.dev]
 incremental = true
 

README.md

@@ -1,6 +1,7 @@
 # Templar Protocol
 
 [![Test](https://github.com/Templar-Protocol/contracts/actions/workflows/test.yml/badge.svg)](https://github.com/Templar-Protocol/contracts/actions/workflows/test.yml)
+[![Kani](https://github.com/Templar-Protocol/contracts/actions/workflows/kani.yml/badge.svg)](https://github.com/Templar-Protocol/contracts/actions/workflows/kani.yml)
 [![Coverage](https://codecov.io/gh/Templar-Protocol/contracts/branch/dev/graph/badge.svg)](https://codecov.io/gh/Templar-Protocol/contracts)
 [![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT)