Guarded2Network's diagnostics: a single defense-in-depth catch-all. Every case it reports is one an earlier pass rules out — type checking establishes that a receive's channel reference resolves and is Channel(_)-shaped — but this pass has no proof of that to appeal to, so the checks are real ones.

inductive G2NError : Type

Guarded2Network's errors.

• internalInvariantViolated (pos : SourceSpan) (description : String) : G2NError

  Defense-in-depth: an input shape this pass's own invariants (or type checking's) guarantee can't occur (e.g. a receive's channel resolving to a non-Channel(_) type, or not resolving at all) still turned up. No proof of unreachability exists yet, just facts established by earlier passes, so this stays a runtime check, not absurd/nomatch. pos is SourceSpan.placeholder at callers past the point a real position is still available (GuardedPlusCal.Statement carries none), matching Typed2Computable.lean's precedent.

@[implicit_reducible]

instance instReprG2NError : Repr G2NError

Equations

• instReprG2NError = { reprPrec := instReprG2NError.repr }

def instReprG2NError.repr : G2NError → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instInhabitedG2NError : Inhabited G2NError

Equations

• instInhabitedG2NError = { default := instInhabitedG2NError.default }

@[implicit_reducible]

instance instBEqG2NError : BEq G2NError

Equations

• instBEqG2NError = { beq := instBEqG2NError.beq }

def instBEqG2NError.beq : G2NError → G2NError → Bool

Equations

• instBEqG2NError.beq (G2NError.internalInvariantViolated a a_1) (G2NError.internalInvariantViolated b b_1) = (a == b && a_1 == b_1)
• instBEqG2NError.beq x✝¹ x✝ = false

@[implicit_reducible]

instance instCompilerDiagnosticG2NErrorString : CompilerDiagnostic G2NError String

Equations

• One or more equations did not get rendered due to their size.