Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Error Code Index (quick lookup)

Purpose: Use this table to find the compiler phase and primary crate/files for any error code. Full catalog is in docs/SPECIFICATION.md §7.2 / Appendix D.

How to use

  1. Note the code prefix (A01 = parser, A02 = resolve, A03 = types, …).
  2. Open the primary crate/files below (or rg 'A0xxxx' crates --glob '*.rs').
  3. Do not fix a types error by changing the SMT backend unless the code is A04/A11/A05100 and the failure is genuinely solver-side.
  4. For unknown codes not listed here: rg 'A0xxxx' docs/SPECIFICATION.md then rg 'A0xxxx' crates.

By series (agent phase map)

PrefixPhasePrimary crateStart here
A01xxxparserassura-parsergrammar/, lexer.rs, lower/
A02xxxresolveassura-resolvelib.rs, type_refs.rs, imports.rs
A03xxxtypesassura-typesinference.rs, clauses.rs, checks/
A04xxxsmt+typesassura-smt / assura-typesentry/, z3_backend/, refinement paths
A05xxxtypesassura-typeschecks/linear_typestate.rs, checkers/linear.rs
A06xxxtypesassura-typeschecks/linear_typestate.rs, checkers/typestate.rs
A07xxxtypesassura-typeschecks/effects.rs, checkers/effects.rs
A08xxxtypesassura-typeschecks/info_flow.rs, checkers/taint.rs, checkers/info_flow.rs
A09xxxtypesassura-typeschecks/meta.rs (match), checkers/totality.rs
A10xxxtypesassura-typeschecks/meta.rs, match exhaustiveness
A11xxxsmt+typesassura-smt / assura-typesentry/, invariant checks
A12xxxtypesassura-typeschecks/concurrency.rs, checkers/security/
A13xxxtypesassura-typeschecks/numeric.rs, domain/numeric.rs
A31xxxtypesassura-typeschecks/core.rs (liveness prove/fairness)
A05 (impl)smt+cliassura-smt / assura-cliA05100 SMT inconclusive / limitation

Codes from SPEC §7.2 (plus a few high-traffic impl codes)

CodePhasePrimary crateMessageCause (spec)SPEC subsectionStart in tree
A01001parserassura-parserUnexpected tokenParser errorSyntax (A01xxx)grammar/, lexer.rs, lower/
A01002parserassura-parserUnterminated string literalMissing closing quoteSyntax (A01xxx)grammar/, lexer.rs, lower/
A01003parserassura-parserInvalid numeric literalMalformed numberSyntax (A01xxx)grammar/, lexer.rs, lower/
A01004parserassura-parserReserved keyword used as identifierNaming conflictSyntax (A01xxx)grammar/, lexer.rs, lower/
A01005parserassura-parserMismatched bracesUnbalanced {}Syntax (A01xxx)grammar/, lexer.rs, lower/
A02001resolveassura-resolveUndefined identifier XName not in scopeName Resolution (A02xxx)lib.rs, type_refs.rs, imports.rs
A02002resolveassura-resolveUndefined type XType not declaredName Resolution (A02xxx)lib.rs, type_refs.rs, imports.rs
A02003resolveassura-resolveDuplicate definition of XName collisionName Resolution (A02xxx)lib.rs, type_refs.rs, imports.rs
A02004resolveassura-resolveAmbiguous import XMultiple modules export same nameName Resolution (A02xxx)lib.rs, type_refs.rs, imports.rs
A02005resolveassura-resolveCircular importModule A imports B imports AName Resolution (A02xxx)lib.rs, type_refs.rs, imports.rs
A03001typesassura-typesExpected T1, found T2 / empty tuple / pattern arityIncompatible types; invalid (,); constructor/tuple pattern field countType Mismatch (A03xxx)inference.rs, clauses.rs, checks/
A03002typesassura-typesType parameter count mismatchWrong number of genericsType Mismatch (A03xxx)inference.rs, clauses.rs, checks/
A03003typesassura-typesCannot unify T1 with T2Failed unificationType Mismatch (A03xxx)inference.rs, clauses.rs, checks/
A03004typesassura-typesMissing field F in structIncomplete constructionType Mismatch (A03xxx)inference.rs, clauses.rs, checks/
A03005typesassura-typesUnknown field F in type TField does not existType Mismatch (A03xxx)inference.rs, clauses.rs, checks/
A03006typesassura-typesClause not Bool / dependent index mismatchNon-Bool clause body; or Vec<T,3> vs Vec<T,5>Type Mismatch (A03xxx)clauses.rs, checkers/info_flow.rs
A04001smt+typesassura-smt / assura-typesPrecondition may not holdrequires clause violatedRefinement Violation (A04xxx)entry/, z3_backend/, refinement paths
A04002smt+typesassura-smt / assura-typesPostcondition may not holdensures clause violatedRefinement Violation (A04xxx)entry/, z3_backend/, refinement paths
A04003smt+typesassura-smt / assura-typesRefinement subtype check failed`{v: T \Refinement Violation (A04xxx)entry/, z3_backend/, refinement paths
A04004smt+typesassura-smt / assura-typesDivision by zero possibleDivisor may be 0Refinement Violation (A04xxx)entry/, z3_backend/, refinement paths
A04005smt+typesassura-smt / assura-typesIndex out of bounds possibleIndex may exceed lengthRefinement Violation (A04xxx)entry/, z3_backend/, refinement paths
A04006smt+typesassura-smt / assura-typesArithmetic overflow possibleResult may exceed boundsRefinement Violation (A04xxx)entry/, z3_backend/, refinement paths
A04007smt+typesassura-smt / assura-typesRefinement timeoutSMT solver timed outRefinement Violation (A04xxx)entry/, z3_backend/, refinement paths
A05001typesassura-typesLinear variable X used twiceGrade 1, used 2+ timesLinearity (A05xxx)checks/linear_typestate.rs, checkers/linear.rs
A05002typesassura-typesLinear variable X not usedGrade 1, never consumedLinearity (A05xxx)checks/linear_typestate.rs, checkers/linear.rs
A05003typesassura-typesGrade mismatch: expected N, used MExact count violatedLinearity (A05xxx)checks/linear_typestate.rs, checkers/linear.rs
A05004typesassura-typesCannot copy linear valueTried to duplicateLinearity (A05xxx)checks/linear_typestate.rs, checkers/linear.rs
A05005typesassura-typesLinear value dropped without consumingResource leakLinearity (A05xxx)checks/linear_typestate.rs, checkers/linear.rs
A06001typesassura-typesInvalid transition: S1 -> S2Not in state machineTypestate (A06xxx)checks/linear_typestate.rs, checkers/typestate.rs
A06002typesassura-typesOperation requires state S, found S'Wrong current stateTypestate (A06xxx)checks/linear_typestate.rs, checkers/typestate.rs
A06003typesassura-typesObject not in final state at end of scopeProtocol incompleteTypestate (A06xxx)checks/linear_typestate.rs, checkers/typestate.rs
A06004typesassura-typesAmbiguous state after branchDifferent states in if/elseTypestate (A06xxx)checks/linear_typestate.rs, checkers/typestate.rs
A06005typesassura-typesMissing transition guardRequired predicate missingTypestate (A06xxx)checks/linear_typestate.rs, checkers/typestate.rs
A07001typesassura-typesUndeclared effect EEffect not in function signatureEffect Violation (A07xxx)checks/effects.rs, checkers/effects.rs
A07002typesassura-typesPure function performs effect ESide effect in pure contextEffect Violation (A07xxx)checks/effects.rs, checkers/effects.rs
A07003typesassura-typesEffect E in must-not listExplicitly forbidden effectEffect Violation (A07xxx)checks/effects.rs, checkers/effects.rs
A07004typesassura-typesEffect handler missing for EUnhandled effectEffect Violation (A07xxx)checks/effects.rs, checkers/effects.rs
A07005typesassura-typesEffect hierarchy violationSub-effect used but parent not declaredEffect Violation (A07xxx)checks/effects.rs, checkers/effects.rs
A08001typesassura-typesData flow violation: L1 to L2High to low flowInformation Flow (A08xxx)checks/info_flow.rs, checkers/taint.rs, checkers/info_flow.rs
A08002typesassura-typesPII leaked to logsRestricted data in Public sinkInformation Flow (A08xxx)checks/info_flow.rs, checkers/taint.rs, checkers/info_flow.rs
A08003typesassura-typesImplicit flow via branchSecret in branch conditionInformation Flow (A08xxx)checks/info_flow.rs, checkers/taint.rs, checkers/info_flow.rs
A08004typesassura-typesPurpose violationData used for undeclared purposeInformation Flow (A08xxx)checks/info_flow.rs, checkers/taint.rs, checkers/info_flow.rs
A08005typesassura-typesMissing declassificationLabel downgrade without declassifyInformation Flow (A08xxx)checks/info_flow.rs, checkers/taint.rs, checkers/info_flow.rs
A09001typesassura-typesNon-exhaustive pattern matchMissing casesTotality (A09xxx)checks/meta.rs (match), checkers/totality.rs
A09002typesassura-typesRecursion may not terminateNo decreasing measureTotality (A09xxx)checks/meta.rs (match), checkers/totality.rs
A09003typesassura-typesDecreasing measure not well-foundedMeasure does not decreaseTotality (A09xxx)checks/meta.rs (match), checkers/totality.rs
A09004typesassura-typesPartial function called from total contextMissing trustTotality (A09xxx)checks/meta.rs (match), checkers/totality.rs
A11001smt+typesassura-smt / assura-typesInvariant violatedSMT found counterexampleBusiness Invariant (A11xxx)entry/, invariant checks
A11002smt+typesassura-smt / assura-typesInvariant not preserved by operationMutation breaks invariantBusiness Invariant (A11xxx)entry/, invariant checks
A11003smt+typesassura-smt / assura-typesInvariant verification timeoutSMT solver timed outBusiness Invariant (A11xxx)entry/, invariant checks
A11004smt+typesassura-smt / assura-typesRule clause violatedBusiness rule not satisfiedBusiness Invariant (A11xxx)entry/, invariant checks
A12001typesassura-typesExclusive resource accessed concurrentlyData race possibleConcurrency (A12xxx)checks/concurrency.rs, checkers/security/
A12002typesassura-typesActor isolation violatedCross-actor mutable accessConcurrency (A12xxx)checks/concurrency.rs, checkers/security/
A12003typesassura-typesShared-read resource modifiedWrite in shared-read contextConcurrency (A12xxx)checks/concurrency.rs, checkers/security/
A13001typesassura-typesUnit mismatch: U1 vs U2e.g., USD + EURNumerical Precision (A13xxx)checks/numeric.rs, domain/numeric.rs
A13002typesassura-typesDimensionally invalid operatione.g., Money * MoneyNumerical Precision (A13xxx)checks/numeric.rs, domain/numeric.rs
A13003typesassura-typesFloat used where fixed-point requiredPrecision lossNumerical Precision (A13xxx)checks/numeric.rs, domain/numeric.rs
A13004typesassura-typesInteger overflow possibleArithmetic exceeds boundsNumerical Precision (A13xxx)checks/numeric.rs, domain/numeric.rs
A16001??Purpose violationData used outside declared purposesPrivacy (A16xxx)rg code in crates
A16002??Retention policy missingNo retention declared for PIIPrivacy (A16xxx)rg code in crates
A16003??Anonymization requiredRetention period expiredPrivacy (A16xxx)rg code in crates
A17001??Breaking field removalRequired field removedSchema Evolution (A17xxx)rg code in crates
A17002??Missing default for new fieldNon-optional field addedSchema Evolution (A17xxx)rg code in crates
A17003??Type change without migrationIncompatible field type changeSchema Evolution (A17xxx)rg code in crates
A21001??Breaking response field removalClient may depend on fieldAPI Evolution (A21xxx)rg code in crates
A21002??New required request fieldExisting clients will failAPI Evolution (A21xxx)rg code in crates
A21003??Error variant removedClient handlers breakAPI Evolution (A21xxx)rg code in crates
A22001??Exceeds declared complexityO(n^2) found, O(n) declaredComplexity Bounds (A22xxx)rg code in crates
A22002??Complexity analysis timeoutAARA solver timed outComplexity Bounds (A22xxx)rg code in crates
A22003??Unbounded allocation detectedNo allocation bound provedComplexity Bounds (A22xxx)rg code in crates
A05100smt+cliassura-smt / assura-cliSMT counterexample found (verification failed)Fix the contract (real violation)(impl)check/report.rs
A05101cliassura-cliSMT solver timed outIncrease --timeout(impl)check/report.rs
A05102cliassura-cliKnown compiler limitation (warning, exit 0)No action needed(impl)check/report.rs
A05103cliassura-cliSolver inconclusive (error, exit 1)Simplify the contract(impl)check/report.rs
A10002typesassura-typesMatch on unknown scrutinee without wildcard(implementation; see CLI/SMT Unknown policy)(impl)checks/meta.rs (match exhaustiveness)

High-traffic implementation codes (not always in SPEC §7.2 table above)

Agents often hit these in tests/checkers before finding them in Appendix D. Prefer this table over guessing the phase.

CodePhasePrimary crateTypical meaningStart in tree
A02006resolveassura-resolveDuplicate importimports.rs
A02007resolveassura-resolveUnused importunused.rs
A02008resolveassura-resolveInvalid import path segmentimports.rs
A02010resolveassura-resolveCannot resolve import (module not found)imports.rs, lib.rs
A03006typesassura-typesClause body not Bool where requiredclauses.rs
A03007typesassura-typesNumeric / refinement constraint failurechecks/numeric.rs, domain/numeric.rs
A03010typesassura-typesType / annotation mismatch (impl)inference.rs, clauses.rs, checks/
A07003typesassura-typesUnknown / denied effectchecks/effects.rs (known effect names only)
A08102typesassura-typesInfo-flow / taint violation (impl)checks/info_flow.rs, checkers/taint.rs
A10001typesassura-typesNon-exhaustive matchchecks/meta.rs
A10101typesassura-typesNumeric / match interaction (impl)checks/numeric.rs, checks/meta.rs
A11005typesassura-typesInvariant / FFI-related type issuechecks/ffi_error.rs, entry/invariant paths
A14001typesassura-typesFrame / modifies violationchecks/frame_totality.rs
A23016typesassura-typesDomain / feature checker (impl)domain/, checks/
A24001typesassura-typesDomain / feature checker (impl)domain/, checks/
A27003typesassura-typesDomain / feature checker (impl)domain/, checks/
A28001typesassura-typesDomain / feature checker (impl)domain/, checks/
A33001typesassura-typesStorage / resource checkerchecks/storage.rs
A37003typesassura-typesStorage / resource checkerchecks/storage.rs
A38001typesassura-typesStorage / resource checkerchecks/storage.rs
A42003typesassura-typesNumeric precision / boundschecks/numeric.rs
A43001typesassura-typesNumeric precision / boundschecks/numeric.rs
A43002typesassura-typesNumeric precision / boundschecks/numeric.rs
A44001typesassura-typesPlatform / target checkerchecks/platform.rs
A45001typesassura-typesPlatform / target checkerchecks/platform.rs
A47001typesassura-typesSafety / CVE pattern checkerchecks/safety.rs
A48002typesassura-typesMeta / match / totality (impl)checks/meta.rs
A49001typesassura-typesMeta / match / totality (impl)checks/meta.rs
A49002typesassura-typesMeta / match / totality (impl)checks/meta.rs
A50001typesassura-typesMeta / feature checker (impl)checks/meta.rs, domain/
A52001typesassura-typesMeta / feature checker (impl)checks/meta.rs
A54001typesassura-typesMeta / feature checker (impl)checks/meta.rs
A55001typesassura-typesMeta / feature checker (impl)checks/meta.rs, domain/
A64001typesassura-typesFFI / error propagation (impl)checks/ffi_error.rs
A31006typesassura-typesLiveness block missing provechecks/core.rs (run_liveness_checks)
A31007typesassura-typesleads_to without assume fairchecks/core.rs (run_liveness_checks); colon form splits prove/leads_to clauses

If a code is still missing: rg 'A0xxxx' crates --glob '*.rs' then add a row here in the same PR when agents are likely to hit it again.

Agent decision shortcuts

SymptomFirst action
A01xxxParser/grammar/lower; minimal reproduction in tests/fixtures/
A02xxxassura-resolve; symbol table / imports / type_refs
A03xxxassura-types inference/clauses; check Type::is_indeterminate() footgun
A04xxx / counterexampleassura-smt; unconstrained result/outputs; verify_typed
A05xxx linearitychecks/linear_typestate.rs / checkers/linear.rs
A06xxx typestatecheckers/typestate.rs
A07xxx effectschecks/effects.rs; known effect names only (see AGENTS pipeline trap)
A08xxx taint/flowchecks/info_flow.rs / checkers/taint.rs
A09xxx / A10xxx match/totalitychecks/meta.rs / checkers/totality.rs; parser arm trivia footgun
A14xxx frame/modifieschecks/frame_totality.rs
A31xxx livenesschecks/core.rs; parser may split prove: leads_to(...) into two clauses
A05100 counterexample / A05101 timeout / A05102 limitation / A05103 inconclusivecheck/report.rs; limitation (A05102) = warning, else error
A52xxx / A54xxx / high A-seriesdomain/meta features: checks/meta.rs, domain/, then rg 'Axxxxx' crates
Wrong phase suspicionbash scripts/guards.sh then re-read AGENTS decision tree

Maintenance

  • Source of truth for meanings: docs/SPECIFICATION.md §7.2.
  • When adding a new Axxxxx in code, add a row here (or in “High-traffic implementation codes”) in the same PR if agents are likely to hit it.
  • Do not try to generate all of Appendix D unless agents repeatedly miss phase; curated + high-traffic is enough.
  • Full phase/wiring rules: AGENTS.md, crates/assura-types/src/CHECKER-LAYERS.md.