Previously, the routing policy language
gave cloud network engineers a way to express topology intent through four
algebraic primitives. Declare
deny > allow > segments > default, run
terraform plan, and the compiler emits the correct route set. The algebra and
its mental model should simplify cloud network topology. And it does.
But correctness by construction answers “is this valid?” It doesn’t answer “is this what I meant?” A policy can be structurally correct and semantically wrong. When segments, allows, and denies interact across 9 VPCs in 3 regions, the algebra’s output isn’t obvious from reading the declaration. Navigating those interactions and refactoring topology with confidence requires more than the compiler itself. You need to see what the compiler decided, not just what it emitted.
The compiler generates routes. The semantic toolchain makes those decisions observable, auditable, and provable.
Five Semantic Outputs
The toolchain adds five inspection outputs to every IR module (Centralized
Router, Full Mesh Trio, Super Router). Enable them through the inspect field
and the compiler dumps structured JSON alongside the route set:
centralized_router = {
name = "mystique"
routing_policy = local.routing_policy
vpcs = module.vpcs
inspect = {
reachability = true
diagnostics = true
provenance = true
policy_diff = {
previous_reachability = jsondecode(file("inspect/myrouter-reachability.json"))
}
equivalence = {
equivalent_routing_policy = {
...
}
}
}
Each output operates on reachability meaning, not route resources. They answer different questions about the same compilation. And like the policy language itself, the toolchain is scope-invariant: the same five outputs work at Regional IR, Global IR, and Domain IR.
The Reachability Matrix
This is the algebra’s per-pair verdict as structured data. Every VPC pair resolves to one of six outcomes mapping directly to the precedence chain:
{
"app3:general3" : "permitted:segment",
"app3:infra3" : "permitted:allow",
"general3:infra3" : "denied:default"
}
Each entry represents bidirectional routes so "app3:general3" covers both
app3 -> general3 and general3 -> app3. The output is deduplicated: only the
lexicographically-first key is shown, no mirror entries. Three VPCs produce
three pairs, not six.
Six verdicts, no ambiguity:
permitted:segmentdenied:cross-segmentpermitted:allowdenied:denypermitted:defaultdenied:default
This is the compiled intermediate representation made inspectable. It separates “what the policy decided” from “what routes were emitted.”
When a policy has two segments, three allow rules, and a deny interacting across regions, the reachability matrix is the ground truth. No mental algebra required. Just read the JSON.
Diagnostics: -Wall for Network Policy
Compiler warnings for policy states that are valid but likely unintentional:
[
"VPC \"monitoring\" has zero connectivity. It is unsegmented under default=\"deny\" with no allow rules.",
"Segment \"isolated\" contains only 1 VPC. Single-member segments have no routing effect under default=\"deny\".",
"Deny rule { app -> db } is redundant: this pair would already be denied without it."
]
These are the errors that pass validation but produce a topology that doesn’t
match intent. A VPC with zero reachability. A redundant deny that clutters the
policy without changing behavior. A solo-member segment that looks like it does
something but algebraically does nothing under default = "deny".
The compiler catches them during plan, not after an incident.
That said, warnings are not errors. Sometimes a solo-member segment or a
redundant deny is intentional. Engineers may prefer the code organization: a
segment named management with one VPC documents intent even if it has no
routing effect under default = "deny". A redundant deny makes the policy
self-documenting for reviewers who shouldn’t have to reason about the algebra to
see that a pair is blocked. Diagnostics surfaces these states so you can make a
deliberate choice to keep them, not because you missed them.
Provenance: Debug Symbols for Routes
Every emitted route carries metadata tracing it back to the source VPC pair and the policy primitive that authorized it:
{
"route_table_id": "rtb-abc",
"destination_cidr_block": "10.0.64.0/18",
"from": "app",
"to": "db",
"verdict": "permitted",
"reason": "segment"
}
This is the link between compiled output and source program. When you see a route in a VPC route table and need to know why it exists, provenance traces it back to the exact policy primitive that caused it. No reverse-engineering the algebra from route table entries. No guessing. Just look it up.
Policy Diff: Source-Level vs. Assembly-Level
terraform plan shows route additions and removals. That’s the assembly diff.
When a one-line policy edit produces dozens of route changes, the plan tells you
what changed in infrastructure. It doesn’t tell you what changed in
connectivity.
Policy diff does. Given a previous reachability matrix, it computes the semantic delta:
{
"added": ["app:monitor"],
"removed": ["app:db"],
"unchanged": ["api:app", "api:web"]
}
inspect = {
policy_diff = {
previous_reachability = jsondecode(file("inspect/TEST-centralized-router-mystique-use1-reachability.json"))
}
}
Save the reachability matrix, change the policy, pass the old matrix back. The diff tells you exactly which VPC pairs gained or lost connectivity. Source-level changes, not assembly-level noise. Now you can actually see the consequence of that one-line edit before it hits anything.
Equivalence: Proving Two Policies Are the Same Program
The routing policy language post described algebraic equivalences. A solo-member
segment under default = "deny" is a no-op. default = "allow" with strategic
denies can produce the same reachability as default = "deny" with explicit
allows.
Equivalence takes a second policy declaration and compares permit/deny outcomes for every VPC pair:
centralized_router = {
routing_policy = {
default = "allow"
deny = [{ from = vpcs["app"], to = vpcs["db"] }]
}
inspect = {
equivalence = {
equivalent_routing_policy = {
default = "deny"
allow = [
{ from = vpcs["app"], to = vpcs["web"] },
{ from = vpcs["db"], to = vpcs["web"] },
]
}
}
}
}
{
"equivalent": true,
"mismatches": {}
}
Two different policy declarations, same reachability. The network policy equivalent of “these two programs compute the same function.”
When mismatches exist, the output shows exactly which pairs diverge and how:
{
"equivalent": false,
"mismatches": {
"app:db": {
"routing_policy": "permitted:default",
"equivalent_routing_policy": "denied:deny"
}
}
}
This is how you refactor routing topology with confidence. Rewrite from allow-with-denies to deny-with-allows. Reorganize segments into explicit allows. Simplify a verbose policy into a shorter one. Equivalence proves the rewrite didn’t change behavior. No route-by-route comparison, no hoping the plan output looks right. Mathematical proof.
Why This Is Possible: Pure Functions and Compile Time
The semantic toolchain exists because the compiler is a pure function.
generate_routes_to_other_vpcs is a zero-resource Terraform module: same
inputs, same outputs, no side effects, referential transparency. That
determinism is what makes provenance traceable, equivalence provable, and diffs
computable. If the compilation step were opaque or stateful, structured semantic
inspection would not be feasible.
The compiler itself is backed by 103 passing terraform test cases covering
the full policy algebra: deny rules, segments, precedence interactions, edge
cases, IPv4 and IPv6. Each test asserts on the exact route set. The semantic
toolchain builds on that tested foundation.
Audit and Compliance Evidence
The routing policy language already made the policy declaration the compliance artifact. The semantic toolchain takes this further by producing the structured evidence that auditors actually ask for.
-
PCI-DSS: The reachability matrix is the segmentation proof, generated directly from the compiler as a build artifact.
-
SOC 2: Policy diff provides the change audit trail, showing which VPC pairs gained or lost connectivity between compilations.
-
HIPAA / NIST 800-53 / FedRAMP: Provenance links every emitted route back to the policy primitive that authorized it. When an auditor asks “why can system A reach system B?”, the answer is a JSON lookup.
-
NIS2 / GDPR-adjacent: Equivalence proves that policy refactors preserve the required isolation posture. The compliance guarantee survives the rewrite because the proof is mathematical.
Diagnostics adds a preventive layer across all of these. The compiler flags misconfigurations (zero connectivity, redundant rules, no-effect segments) before apply, not during an audit finding.
The Toolchain Closes the Loop
The routing policy language gave engineers a way to declare intent. The compiler guarantees correctness by construction. The semantic toolchain makes that correctness observable:
- Reachability shows what the compiler decided
- Diagnostics warns when decisions look unintentional
- Provenance links decisions back to source
- Policy diff shows what changed between compilations
- Equivalence proves two declarations are the same program
Together, they close the gap between writing a policy and understanding its consequences. The algebra is small. Its interactions across regions are not. The semantic toolchain is how you navigate that complexity without trusting your mental model of a four-level precedence chain across a multi-region mesh.
Every output is structured JSON, so reachability can be asserted in CI, diffs surfaced in PR reviews, and equivalence used as a merge gate.
Declare intent, compile routes, inspect semantics, refactor with proof.