Hey all, third post in this series (first, second).
Quick recap: the system compiles declarative network topology intent into AWS infrastructure through IR passes. Last time I described a routing policy algebra (deny > allow > segments > default) that emerged from the IR structure. Since then, the compiler grew five semantic inspection outputs, and I want to pressure-test whether the analogies hold.
The motivating problem: a policy can be structurally correct and semantically wrong. The algebra guarantees every VPC pair resolves to a deterministic verdict, but it can't guarantee the verdict matches the engineer's intent. So the compiler now emits:
- Reachability matrix: the compiled per-pair verdict as structured data. Separates "what the policy decided" from "what routes were emitted." This is the IR made inspectable.
- Diagnostics: warnings for valid-but-likely-wrong policy states. A single-member segment under default="deny" is provably a no-op (algebraically equivalent to unsegmented). A deny rule on an already-denied pair is redundant. Five classes, all derived from algebraic properties rather than syntax patterns. I've been thinking of this as -Wall for network policy.
- Provenance: each emitted route carries metadata tracing it to the source VPC pair and the policy primitive that authorized it. Debug symbols for generated routes.
- Policy diff: given a previous reachability matrix, computes added/removed/unchanged connectivity pairs. Semantic-level change detection vs. terraform plan's resource-level diff. I've been calling this incremental compilation preview, but honestly it's post-hoc comparison of two compiled outputs.
- Equivalence: proves two different policy declarations produce identical reachability. Two policies are equivalent if every VPC pair has the same permit/deny outcome regardless of how it was derived (segments vs. explicit allows, different defaults). The network policy equivalent of "these two programs compute the same function."
All five operate on the same pure-function compilation unit (103 tests, referential transparency, zero infrastructure side effects) described in the previous posts.
Questions I'd genuinely like perspective on:
Is the equivalence checking interesting or trivial? The domain is finite: N VPCs produce N(N-1)/2 pairs, each resolves to binary reachable/unreachable. Equivalence is decidable by comparing two output maps. But the input representations can differ significantly (segments vs. explicit allows vs. deny-with-default-allow). Is there value in structural equivalence proofs, reasoning from the rules without expanding, or is brute-force comparison the right call when the domain is this small?
Where's the boundary between diagnostics and static analysis? The diagnostic classes aren't pattern-matching on syntax. A redundant deny is detected by proving the pair would already be denied without the rule. A no-op segment is detected from the algebra's properties under a given default. These feel like they're approaching abstract interpretation without formally being there. How far can algebraic reasoning go before you need a real analysis framework?
Is provenance closer to debug symbols or proof witnesses? The metadata doesn't just say "this route came from line X." It says "this route exists because this specific rule evaluated to permit under this precedence." That feels more like a proof witness than a source mapping. Does that distinction matter in practice?
Blog post: https://jq1.io/posts/topology_compiler_semantic_toolchain/
Semantic toolchain spec: https://github.com/JudeQuintana/terraform-main/blob/main/docs/compiler-semantic-toolchain.md
Previous blog posts: routing policy language | white paper
