test(auth-eth): add Halmos symbolic tests for DstackKms root epochs

Prove the root registry step invariant (append-only entries, chain
hash recursion, hash-bound activation and pop, kmsInfo following the
current epoch), canonical key encodings, authorization epoch bounds,
bootstrap-only authorization before registration, KMS and app
authorization matching epoch policy, epoch isolation of KMS policy
writes, and legacy entry points following the current epochs.
Mutation testing confirms each property catches a targeted bug.

Document that wrong-kind rejections report root epoch (0, 0x0),
unlike the README and the auth-simple and auth-mock backends.

Signed-off-by: Kevin Wang <wy721@qq.com>

Author: kvinwang

dstack/kms/auth-eth/README.md

@@ -150,6 +150,7 @@ slither .
 halmos --contract DstackAppSymbolicTest
 halmos --contract DstackAppEpochSymbolicTest
 halmos --contract DstackKmsSymbolicTest
+halmos --contract DstackKmsEpochSymbolicTest
 ```
 
 Forge 1.8 enables `dynamic_test_linking` by default, which compiles `new` in

dstack/kms/auth-eth/docs/formal-verification.md

@@ -151,6 +151,55 @@ counterexample. Dropping the inactive-epoch check in `_authorizeApp` does
 not: policy for an inactive epoch cannot be written, so that check is
 defense in depth.
 
+`test/DstackKmsEpoch.symbolic.t.sol` (root epochs; setUp registers epochs
+0-2, activates 1 so that 2 is pending, admits one KMS identity and OS image
+per epoch, and deploys an app at app epoch 1):
+- [x] `check_RootRegistry_StepInvariant` — after any single call to any
+      enumerated mutating function, by any caller with symbolic args: the
+      current epoch stays registered and moves only by one, through the
+      owner's activation naming its chain hash; the registry changes by at
+      most one entry at its end, and only the owner's pop of a pending
+      epoch naming its chain hash removes one; existing entries keep their
+      keys and hashes; every chain hash commits to its keys and the previous
+      hash; `kmsInfo` holds the current keys without legacy evidence.
+- [x] `check_RegisterRootEpoch_AcceptsOnlyCanonicalEncodings` — registration
+      succeeds exactly for a 91-byte uncompressed P-256 SPKI and a 33-byte
+      compressed secp256k1 key.
+- [x] `check_Authorize_EnforcesEpochBounds` — a wrong-kind operation, an app
+      root epoch above the current one, a KMS root epoch above the latest
+      registered one, or an app epoch above the app's current one is never
+      authorized; right-kind results report the current root epoch and hash.
+- [x] `check_Authorize_OnlyBootstrapBeforeRegistration` — with no root epoch
+      registered, only `kms_bootstrap` can be authorized.
+- [x] `check_AuthorizeKms_MatchesEpochPolicy` — after any one owner write,
+      KMS authorization allows exactly when the selected root epoch is
+      registered, the TCB is up to date, and that epoch's row admits the OS
+      image, aggregated MR and device.
+- [x] `check_AuthorizeApp_MatchesKmsAndAppPolicy` — app authorization allows
+      exactly when both epochs are active, the selected root epoch admits
+      the OS image, and the app's own `authorizeApp` admits it.
+- [x] `check_KmsPolicyWrite_PreservesOtherEpochDecisions` — a KMS policy
+      write at one root epoch, through the explicit or the latest-epoch
+      setters, never changes a KMS decision at another epoch.
+- [x] `check_LegacyEntryPoints_FollowCurrentEpochs` — `isKmsAllowed`
+      decides as `kms_serve` at the current root epoch, and `isAppAllowed`
+      denies an app that has left app epoch 0.
+
+Mutation-tested: a chain hash that ignores the previous epoch, activation
+that leaves `kmsInfo` stale, a pop that ignores the chain hash, app requests
+selecting a pending root epoch, KMS requests limited to the current epoch,
+`isKmsAllowed` checking the latest epoch, accepting an `0x04` k256 tag, an
+OS image row aliasing epoch 1 onto the legacy row, an app check skipping the
+OS image, and non-bootstrap operations before registration each produce a
+counterexample.
+
+Finding: a wrong-kind operation is rejected before the result is filled with
+the current root epoch and chain hash, so it reports `(0, 0x0)`, while the KMS
+README states that rejections carry the current epochs and auth-simple and
+auth-mock do return them. The KMS then reports "Root epoch not registered"
+instead of the rejection reason. A KMS never sends a wrong-kind operation, so
+this only affects error reporting.
+
 Single-call (`test/DstackKms.symbolic.t.sol`):
 - [x] `check_RegisterApp_AnyCallerCanRegisterNonZeroAddress` + `_RejectsZeroAddress`
       — codifies the permissionless-by-design behavior; see "Findings"