spec: fix alwaysHostNetwork invariant to be relational, not hardcoded

[abienkowski]

Problem

Reviewed all 9 Quint invariants against the actual guard/mutator behavior in Go, Rust, and TypeScript (issue #5). Result: 7 of 9 map cleanly and identically across all three languages. One real spec-vs-code mismatch found:

alwaysHostNetwork (spec/docker_socket_policy.qnt:384) checked c.networkMode == "host" — a hardcoded literal. But none of the three implementations hardcode "host"; ContainerConfigMutator copies whatever network_mode the matched policy configures. spec/README.md even documented it as "ContainerConfigMutator enforces networkMode=host", implying it's hardcoded like privileged=false" — it isn't. It only held because the one existing policy (config/beacon.yaml) happens to set network_mode: host`.

Fix

Changed the invariant to be relational — matching the pattern already used by volumesInWhitelist/flagsInAllowlist — checking that each container's networkMode equals its matched policy's configured value, rather than a hardcoded literal:

val alwaysHostNetwork = containers.forall(c =>
  policies.exists(p =>
    p.serviceName == c.serviceName
      and c.networkMode == p.containerConfig.networkMode
  )
)

The real security property is "the untrusted create-request body cannot override the policy-configured network mode" — not "network mode must always be the string host". Behavior under simulation is unchanged (beacon.yaml still sets host); this just makes the model check the actual guarantee instead of an incidental property of the one config file that currently exists.

Also updated spec/README.md:

• Corrected the alwaysHostNetwork row to describe the relational check
• Added a Modeling Notes section documenting that proxyLives and routingTableComplete are structurally tautological in the model (can't be falsified by any action sequence the simulator generates) and what actually provides real coverage for each guarantee outside the model

Verification

quint typecheck spec/docker_socket_policy.qnt   # passes
quint run --invariants allInvariants spec/docker_socket_policy.qnt
# [ok] No violation found (6192ms at 1615 traces/second)

Other issue #5 findings (no code change needed)

• Invariant count discrepancy ("spec says 7, CHANGELOG says 9") was already fixed by PR feat: gate releases on verification + test-parity fixes #13 — every doc currently says 9.
• Exec is unconditionally denied in all three languages (router + middleware, defense-in-depth).
• Routing table (26 endpoints) has no functional mismatches across Go/Rust/TS.
• Found a real (separate, out-of-scope) cross-language parity bug: Go's extractContainerName doesn't exclude reserved path segments (json/create/exec) the way Rust/TS do — filing a follow-up issue for this.

Closes #5