contracts: DstackKms.initialize accepts a zero appImplementation, which docs/specification.md §3.1 says must revert

Compare dstack/kms/auth-eth/docs/specification.md §3.1 and INV-4 with contracts/DstackKms.sol:72, then run forge test --match-path dstack/kms/auth-eth/test/SpecConformance.t.sol -vv. Confirm the intended zero-implementation behavior with maintainers, update the specification or implementation accordingly, and leave the conformance test aligned and passing.

Label: BUG (demonstrated). A test written against docs/specification.md §3.1 fails against the current contracts. Low severity; the fix may well be to the document rather than the code.

What the specification says

dstack/kms/auth-eth/docs/specification.md §3.1, for DstackKms.initialize(address initialOwner, address _appImplementation):

• pre: contract is not yet initialized; initialOwner != address(0);
  _appImplementation != address(0).
• post: owner() == initialOwner; appImplementation == _appImplementation; …
• reverts: already-initialized; either address is zero.

What the code does

// contracts/DstackKms.sol:72
function initialize(address initialOwner, address _appImplementation) public initializer {
    __Ownable_init(initialOwner);
    __UUPSUpgradeable_init();
    __ERC165_init();

    // Set DstackApp implementation if provided
    if (_appImplementation != address(0)) {
        appImplementation = _appImplementation;
        emit AppImplementationSet(_appImplementation);
        _emitPolicy("app-implementation", bytes32(uint256(uint160(_appImplementation))), true);
    }
}

Zero is not rejected; it takes the else of the if and the contract initializes with appImplementation == address(0). The initialOwner == address(0) half of the spec clause does hold, via __Ownable_init.

Written as the spec states it, in the new test/SpecConformance.t.sol:

$ forge test --match-path test/SpecConformance.t.sol -vv
[FAIL: next call did not revert as expected] test_Spec_3_1_InitializeRevertsOnZeroAppImplementation() (gas: 2535483)
Suite result: FAILED. 3 passed; 1 failed; 0 skipped

The committed version of that test is flipped to pin actual behaviour so the suite stays green:

[PASS] test_Spec_3_1_InitializeAcceptsZeroAppImplementation_DivergesFromSpec() (gas: 2541992)
       assertEq(kms.appImplementation(), address(0), "spec 3.1 says this reverts; it does not");
       vm.expectRevert("DstackApp implementation not set");
       kms.deployAndRegisterApp(owner, false, false, true, bytes32(0), bytes32(0));

Note the sibling: setAppImplementation does enforce require(_implementation != address(0), "Invalid implementation address"). The initializer and the setter disagree about the same storage slot.

docs/specification.md INV-4 notices half of this — "Currently only setAppImplementation enforces _implementation != address(0); the initializer sets it from input without re-checking" — and then records the invariant as holding modulo owner trust. What INV-4 does not notice is that §3.1's reverts clause, three pages earlier, states the opposite.

Steelman, and why this is probably a documentation fix

Permitting zero at initialization is defensible and may be deliberate. Deploy.s.sol:DeployKmsOnly takes APP_IMPLEMENTATION from the environment, and a deployment that intends to set the implementation later — or that does not use the factory at all, registering apps with registerApp instead — has no reason to be blocked at initialize. The failure mode is loud, immediate and recoverable: deployAndRegisterApp reverts with "DstackApp implementation not set" until the owner calls setAppImplementation, which is a one-transaction fix available at any time.

So the honest reading is that §3.1 was written more strictly than the code and nobody re-derived it. That still matters: docs/specification.md is explicitly "the deliverable an external formal-verification engagement (Runtime Verification, ChainSecurity, Certora) would build against", and an engagement building against it would either report this as a finding or, worse, encode the wrong precondition and verify around it.

What it costs

Bounded and recoverable. A DstackKms initialized with appImplementation == address(0) has a non-functional factory until the owner notices. No authorization decision is affected: isAppAllowed and isKmsAllowed never read appImplementation.

The real cost is to the specification's credibility as an audit input — one clause in the pre/post/frame tables is demonstrably untrue, and there is no test in the repo that would have caught it. The four tests in test/SpecConformance.t.sol are a start at closing that gap generally; the other three pass, including both hardcoded ERC-165 interface ids (0x1e079198, 0x8fd37527), which are correct.

Reachability: who — whoever deploys the KMS; credential — the deployment key; frequency — once, at deployment. Not attacker-triggered.

Improvement direction

Redeployment status: the documentation fix needs no contract change at all. The code fix would be an implementation upgrade behind the existing DstackKms proxy with no storage-layout change — but it would only affect future deployments, since an already-initialized proxy never runs initialize again. That asymmetry is the argument for fixing the document.

Options:

1. Amend the spec (docs only). Change §3.1's pre to drop _appImplementation != address(0), change reverts to "already-initialized; initialOwner is zero", and add a post clause: appImplementation == _appImplementation (which is true for zero too). Cross-reference INV-4, which already describes the actual behaviour. Zero cost, and it makes the two statements in the document agree with each other.
2. Tighten the code to match the spec (impl upgrade, no storage change). One require. Only helps future deployments, and forecloses the deploy-then-set-implementation workflow above, so it needs a check that no deployment relies on that first.
3. Split the difference (impl upgrade, no storage change). Keep zero permitted but make the posture legible — e.g. emit _emitPolicy("app-implementation", bytes32(0), false) on the zero path so the audit log records that the factory was left unconfigured, rather than emitting nothing.
4. Keep the conformance suite, whichever is chosen. test/SpecConformance.t.sol exists to make the spec executable. Extending it to the rest of §3's pre/post/frame clauses is the durable fix for this class — the divergence survived because no test read the document.

(1) plus (4) looks right unless the team actually wants the stricter constructor, in which case (2) plus (4).

Found during a scenario-driven review of the authorization contracts; full walk in .agent/CONTRACT-SCENARIOS.md (scenario 6, "spec conformance"), tests in dstack/kms/auth-eth/test/SpecConformance.t.sol.