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
- Note the code prefix (
A01= parser,A02= resolve,A03= types, …). - Open the primary crate/files below (or
rg 'A0xxxx' crates --glob '*.rs'). - Do not fix a types error by changing the SMT backend unless the code is
A04/A11/A05100and the failure is genuinely solver-side. - For unknown codes not listed here:
rg 'A0xxxx' docs/SPECIFICATION.mdthenrg 'A0xxxx' crates. - Do not invent
Axxxxxnumbers until emit + catalog + index land in the same PR (guards sections 14–15). Planned work uses prose, not reserved codes.
By series (agent phase map)
| Prefix | Phase | Primary crate | Start here |
|---|---|---|---|
| A01xxx | parser | assura-parser | grammar/, lexer.rs, lower/ |
| A02xxx | resolve | assura-resolve | lib.rs, type_refs.rs, imports.rs |
| A03xxx | types | assura-types | inference.rs, clauses.rs, checks/ |
| A04xxx | smt+types | assura-smt / assura-types | entry/, z3_backend/, refinement paths |
| A05xxx | types | assura-types | checks/linear_typestate.rs, checkers/linear.rs |
| A06xxx | types | assura-types | checks/linear_typestate.rs, checkers/typestate.rs |
| A07xxx | types | assura-types | checks/effects.rs, checkers/effects.rs |
| A08xxx | types | assura-types | checks/info_flow.rs, checkers/taint.rs, checkers/info_flow.rs |
| A09xxx | types | assura-types | checks/meta.rs (match), checkers/totality.rs |
| A10xxx | types | assura-types | checks/meta.rs, match exhaustiveness |
| A11xxx | smt+types | assura-smt / assura-types | entry/, invariant checks |
| A12xxx | types | assura-types | checks/concurrency.rs, checkers/security/ |
| A13xxx | types | assura-types | checks/numeric.rs, domain/numeric.rs |
| A31xxx | types | assura-types | checks/core.rs (liveness prove/fairness) |
| A05 (impl) | smt+cli | assura-smt / assura-cli | A05100 CE, A05101 timeout, A05102 known limitation, A05103 inconclusive |
Codes from SPEC §7.2 (plus a few high-traffic impl codes)
| Code | Phase | Primary crate | Message | Cause (spec) | SPEC subsection | Start in tree |
|---|---|---|---|---|---|---|
| A01001 | parser | assura-parser | Unexpected token | Parser error | Syntax (A01xxx) | grammar/, lexer.rs, lower/ |
| A01002 | parser | assura-parser | Unterminated string literal | Missing closing quote | Syntax (A01xxx) | grammar/, lexer.rs, lower/ |
| A02001 | resolve | assura-resolve | Undefined identifier X | Name not in scope | Name Resolution (A02xxx) | lib.rs, type_refs.rs, imports.rs |
| A02003 | resolve | assura-resolve | Duplicate definition of X | Name collision | Name Resolution (A02xxx) | lib.rs, type_refs.rs, imports.rs |
| A02005 | resolve | assura-resolve | Circular import | Module A imports B imports A | Name Resolution (A02xxx) | lib.rs, type_refs.rs, imports.rs |
| A03001 | types | assura-types | Expected T1, found T2 / empty tuple / pattern arity | Incompatible types; invalid (,); constructor/tuple pattern field count | Type Mismatch (A03xxx) | inference.rs, clauses.rs, checks/ |
| A03002 | types | assura-types | Type parameter count mismatch | Wrong number of generics | Type Mismatch (A03xxx) | inference.rs, clauses.rs, checks/ |
| A03005 | types | assura-types | Unknown field F in type T | Field does not exist | Type Mismatch (A03xxx) | inference.rs, clauses.rs, checks/ |
| A03006 | types | assura-types | Clause not Bool / dependent index mismatch | Non-Bool clause body; or Vec<T,3> vs Vec<T,5> | Type Mismatch (A03xxx) | clauses.rs, checkers/info_flow.rs |
| A05001 | types | assura-types | Linear variable X used twice | Grade 1, used 2+ times | Linearity (A05xxx) | checks/linear_typestate.rs, checkers/linear.rs |
| A05002 | types | assura-types | Linear variable X not used | Grade 1, never consumed | Linearity (A05xxx) | checks/linear_typestate.rs, checkers/linear.rs |
| A05003 | types | assura-types | Grade mismatch: expected N, used M | Exact count violated | Linearity (A05xxx) | checks/linear_typestate.rs, checkers/linear.rs |
| A05004 | types | assura-types | Cannot copy linear value | Tried to duplicate | Linearity (A05xxx) | checks/linear_typestate.rs, checkers/linear.rs |
| A06001 | types | assura-types | Invalid transition: S1 -> S2 | Not in state machine | Typestate (A06xxx) | checks/linear_typestate.rs, checkers/typestate.rs |
| A06002 | types | assura-types | Operation requires state S, found S' | Wrong current state | Typestate (A06xxx) | checks/linear_typestate.rs, checkers/typestate.rs |
| A06003 | types | assura-types | Object not in final state at end of scope | Protocol incomplete | Typestate (A06xxx) | checks/linear_typestate.rs, checkers/typestate.rs |
| A06004 | types | assura-types | Ambiguous state after branch | Different states in if/else | Typestate (A06xxx) | checks/linear_typestate.rs, checkers/typestate.rs |
| A07001 | types | assura-types | Undeclared effect E | Effect not in function signature | Effect Violation (A07xxx) | checks/effects.rs, checkers/effects.rs |
| A07002 | types | assura-types | Pure function performs effect E | Side effect in pure context | Effect Violation (A07xxx) | checks/effects.rs, checkers/effects.rs |
| A07003 | types | assura-types | Effect E in must-not list | Explicitly forbidden effect | Effect Violation (A07xxx) | checks/effects.rs, checkers/effects.rs |
| A08001 | types | assura-types | Data flow violation: L1 to L2 | High to low flow | Information Flow (A08xxx) | checks/info_flow.rs, checkers/taint.rs, checkers/info_flow.rs |
| A08002 | types | assura-types | PII leaked to logs | Restricted data in Public sink | Information Flow (A08xxx) | checks/info_flow.rs, checkers/taint.rs, checkers/info_flow.rs |
| A08003 | types | assura-types | Implicit flow via branch | Secret in branch condition | Information Flow (A08xxx) | checks/info_flow.rs, checkers/taint.rs, checkers/info_flow.rs |
| A08004 | types | assura-types | Purpose violation | Data used for undeclared purpose | Information Flow (A08xxx) | checks/info_flow.rs, checkers/taint.rs, checkers/info_flow.rs |
| A08005 | types | assura-types | Missing declassification | Label downgrade without declassify | Information Flow (A08xxx) | checks/info_flow.rs, checkers/taint.rs, checkers/info_flow.rs |
| A09001 | types | assura-types | Non-exhaustive pattern match | Missing cases | Totality (A09xxx) | checks/meta.rs (match), checkers/totality.rs |
| A09002 | types | assura-types | Recursion may not terminate | No decreasing measure | Totality (A09xxx) | checks/meta.rs (match), checkers/totality.rs |
| A09003 | types | assura-types | Decreasing measure not well-founded | Measure does not decrease | Totality (A09xxx) | checks/meta.rs (match), checkers/totality.rs |
| A09004 | types | assura-types | Partial function called from total context | Missing trust | Totality (A09xxx) | checks/meta.rs (match), checkers/totality.rs |
| A11001 | smt+types | assura-smt / assura-types | Invariant violated | SMT found counterexample | Business Invariant (A11xxx) | entry/, invariant checks |
| A11002 | smt+types | assura-smt / assura-types | Invariant not preserved by operation | Mutation breaks invariant | Business Invariant (A11xxx) | entry/, invariant checks |
| A11003 | smt+types | assura-smt / assura-types | Invariant verification timeout | SMT solver timed out | Business Invariant (A11xxx) | entry/, invariant checks |
| A11004 | smt+types | assura-smt / assura-types | Rule clause violated | Business rule not satisfied | Business Invariant (A11xxx) | entry/, invariant checks |
| A12001 | types | assura-types | Exclusive resource accessed concurrently | Data race possible | Concurrency (A12xxx) | checks/concurrency.rs, checkers/security/ |
| A12002 | types | assura-types | Actor isolation violated | Cross-actor mutable access | Concurrency (A12xxx) | checks/concurrency.rs, checkers/security/ |
| A12003 | types | assura-types | Shared-read resource modified | Write in shared-read context | Concurrency (A12xxx) | checks/concurrency.rs, checkers/security/ |
| A13001 | types | assura-types | Unit mismatch: U1 vs U2 | e.g., USD + EUR | Numerical Precision (A13xxx) | checks/numeric.rs, domain/numeric.rs |
| A13002 | types | assura-types | Dimensionally invalid operation | e.g., Money * Money | Numerical Precision (A13xxx) | checks/numeric.rs, domain/numeric.rs |
| A13003 | types | assura-types | Float used where fixed-point required | Precision loss | Numerical Precision (A13xxx) | checks/numeric.rs, domain/numeric.rs |
| A16001 | ? | ? | Purpose violation | Data used outside declared purposes | Privacy (A16xxx) | rg code in crates |
| A16002 | ? | ? | Retention policy missing | No retention declared for PII | Privacy (A16xxx) | rg code in crates |
| A16003 | ? | ? | Anonymization required | Retention period expired | Privacy (A16xxx) | rg code in crates |
| A17001 | ? | ? | Breaking field removal | Required field removed | Schema Evolution (A17xxx) | rg code in crates |
| A17002 | ? | ? | Missing default for new field | Non-optional field added | Schema Evolution (A17xxx) | rg code in crates |
| A17003 | ? | ? | Type change without migration | Incompatible field type change | Schema Evolution (A17xxx) | rg code in crates |
| A21001 | ? | ? | Breaking response field removal | Client may depend on field | API Evolution (A21xxx) | rg code in crates |
| A21002 | ? | ? | New required request field | Existing clients will fail | API Evolution (A21xxx) | rg code in crates |
| A21003 | ? | ? | Error variant removed | Client handlers break | API Evolution (A21xxx) | rg code in crates |
| A22001 | ? | ? | Exceeds declared complexity | O(n^2) found, O(n) declared | Complexity Bounds (A22xxx) | rg code in crates |
| A22002 | ? | ? | Complexity analysis timeout | AARA solver timed out | Complexity Bounds (A22xxx) | rg code in crates |
| A22003 | ? | ? | Unbounded allocation detected | No allocation bound proved | Complexity Bounds (A22xxx) | rg code in crates |
| A05100 | smt+cli | assura-smt / assura-cli | SMT counterexample found (verification failed) | Fix the contract (real violation) | (impl) | check/report.rs |
| A05101 | cli | assura-cli | SMT solver timed out | Increase --timeout | (impl) | check/report.rs |
| A05102 | cli | assura-cli | Known compiler limitation (warning, exit 0; error under --strict) | Simplify ensures, add IR, or ignore until encoding lands | (impl) | check/report.rs |
| A05103 | cli | assura-cli | Solver inconclusive (error, exit 1) | Simplify the contract or raise --timeout | (impl) | check/report.rs |
| A10002 | types | assura-types | Match 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.
| Code | Phase | Primary crate | Typical meaning | Start in tree |
|---|---|---|---|---|
| A01000 | cli/pipeline | assura-cli / assura-pipeline | Source file read/IO failure | check/run.rs, pipeline |
| A02006 | resolve | assura-resolve | Duplicate import | imports.rs |
| A02007 | resolve | assura-resolve | Unused import | unused.rs |
| A02008 | resolve | assura-resolve | Invalid import path segment | imports.rs |
| A02010 | resolve | assura-resolve | Cannot resolve import (module not found) | imports.rs, lib.rs |
| A03006 | types | assura-types | Clause body not Bool where required | clauses.rs |
| A03007 | types | assura-types | Numeric / refinement constraint failure | checks/numeric.rs, domain/numeric.rs |
| A03010 | types | assura-types | Type / annotation mismatch (impl) | inference.rs, clauses.rs, checks/ |
| A07003 | types | assura-types | Unknown / denied effect | checks/effects.rs (known effect names only) |
| A08102 | types | assura-types | Info-flow / taint violation (impl) | checks/info_flow.rs, checkers/taint.rs |
| A10001 | types | assura-types | Non-exhaustive match | checks/meta.rs |
| A10101 | types | assura-types | Numeric / match interaction (impl) | checks/numeric.rs, checks/meta.rs |
| A11005 | types | assura-types | Invariant / FFI-related type issue | checks/ffi_error.rs, entry/invariant paths |
| A14001 | types | assura-types | Frame / modifies violation | checks/frame_totality.rs |
| A14002 | types | assura-types | Secret-dependent array index (timing) | checkers/error_propagation.rs, checks/frame_totality.rs |
| A04008 | types+cli | assura-types / assura-cli | Ensures references unconstrained output (result) | checks/clause_quality.rs; suppressed when IR present (#703) |
| A05025 | smt+types | assura-smt / assura-types | Unresolved prophecy variable | advanced/prophecy.rs; structural checker in types |
| A05026 | smt | assura-smt | Prophecy double-resolved / unconstrained | advanced/prophecy.rs |
| A08101 | types | assura-types | Buffer access without bounds check | checkers/memory.rs |
| A09101 | types | assura-types | Tainted data as array index | checkers/taint.rs |
| A23003 | types | assura-types | Circular buffer empty on read | domain/memory.rs |
| A26001 | types | assura-types | Binary format field offset exceeds buffer | domain/format/binary_format.rs |
| A43005 | types | assura-types | Precomputed table size not a standard domain | domain/numeric.rs |
| A17004 | types | assura-types | Decrypt without tag_verified (AEAD) | checks crypto conformance |
| A23016 | types | assura-types | Domain / feature checker (impl) | domain/, checks/ |
| A24001 | types | assura-types | Domain / feature checker (impl) | domain/, checks/ |
| A27003 | types | assura-types | Domain / feature checker (impl) | domain/, checks/ |
| A28001 | types | assura-types | Domain / feature checker (impl) | domain/, checks/ |
| A33001 | types | assura-types | Storage / resource checker | checks/storage.rs |
| A37003 | types | assura-types | Storage / resource checker | checks/storage.rs |
| A38001 | types | assura-types | Storage / resource checker | checks/storage.rs |
| A42003 | types | assura-types | Numeric precision / bounds | checks/numeric.rs |
| A43001 | types | assura-types | Numeric precision / bounds | checks/numeric.rs |
| A43002 | types | assura-types | Numeric precision / bounds | checks/numeric.rs |
| A44001 | types | assura-types | Platform / target checker | checks/platform.rs |
| A45001 | types | assura-types | Platform / target checker | checks/platform.rs |
| A47001 | types | assura-types | Safety / CVE pattern checker | checks/safety.rs |
| A48002 | types | assura-types | Meta / match / totality (impl) | checks/meta.rs |
| A49001 | types | assura-types | Meta / match / totality (impl) | checks/meta.rs |
| A49002 | types | assura-types | Meta / match / totality (impl) | checks/meta.rs |
| A50001 | types | assura-types | Meta / feature checker (impl) | checks/meta.rs, domain/ |
| A52001 | types | assura-types | Meta / feature checker (impl) | checks/meta.rs |
| A54001 | types | assura-types | Meta / feature checker (impl) | checks/meta.rs |
| A55001 | types | assura-types | Meta / feature checker (impl) | checks/meta.rs, domain/ |
| A64001 | types | assura-types | FFI / error propagation (impl) | checks/ffi_error.rs |
| A31006 | types | assura-types | Liveness block missing prove | checks/core.rs (run_liveness_checks) |
| A31007 | types | assura-types | leads_to without assume fair | checks/core.rs (run_liveness_checks); colon form splits prove/leads_to clauses |
| A32002 | types | assura-types | Opaque body access without reveal | domain/core/opaque_function.rs |
| A36003 | types | assura-types | Duplicate savepoint name | domain/storage/rollback.rs |
| A52002 | types | assura-types | Suspend undeclared invariant (also empty decoder name in codec registry) | domain/meta/scoped_invariant.rs, domain/format/codec_registry.rs |
| A46002 | types | assura-types | Unbounded resource usage | domain/platform.rs |
| A29001 | types | assura-types | Data used before checksum verification | domain/format/checksum.rs |
| A25003 | types | assura-types | Unbounded operation in deadline | domain/concurrency.rs |
| A09103 | types | assura-types | Tainted data flows to trusted sink | checkers/taint.rs |
| A53006 | types | assura-types | Quantifier missing trigger annotation | domain/core/quantifier_trigger.rs |
| A49003 | types | assura-types | Equivalence missing contract reference | domain/meta/behavioral_equivalence.rs |
| A35003 | types | assura-types | Phantom read | domain/storage/mvcc.rs |
| A34003 | types | assura-types | Page cache capacity exceeded | domain/storage/page_cache.rs |
| A30002 | types | assura-types | Protocol wrong state for message | domain/format/protocol_grammar.rs |
| A23001 | types | assura-types | Circular buffer index exceeds capacity | domain/memory.rs |
| A10104 | types | assura-types | Fixed-width division by zero | checkers/fixed_width.rs |
| A09102 | types | assura-types | Tainted data used as allocation size | checkers/taint.rs |
| A08103 | types | assura-types | Ghost region references missing buffer | checkers/memory.rs |
| A51003 | types | assura-types | Contract version gap | domain/meta/incremental_contract.rs |
| A46003 | types | assura-types | Resource near limit | domain/platform.rs |
| A36001 | types | assura-types | Rollback to unknown savepoint | domain/storage/rollback.rs |
| A35001 | types | assura-types | Write-write conflict | domain/storage/mvcc.rs |
| A10102 | types | assura-types | Unsafe narrowing cast | checkers/fixed_width.rs |
| A10103 | types | assura-types | Signed/unsigned comparison mismatch | checkers/fixed_width.rs |
| A42001 | types | assura-types | Numerical precision loss | domain/numeric.rs |
| A20001 | types | assura-types | Deterministic function uses non-deterministic source | checkers/security/determinism.rs |
| A20002 | types | assura-types | Deterministic function iterates hash collection | checkers/security/determinism.rs |
| A18001 | types | assura-types | Shared memory read without access mode | checkers/security/shared_mem.rs |
| A18003 | types | assura-types | Shared memory data race | checkers/security/shared_mem.rs |
| A24003 | types | assura-types | Callback depth exceeded | domain/concurrency.rs |
| A25001 | types | assura-types | Deadline exceeded | domain/concurrency.rs |
| A22004 | types | assura-types | Arena use after drop | domain/memory.rs |
| A44003 | types | assura-types | Unknown platform in abstraction | domain/platform.rs |
| A46001 | types | assura-types | Resource limit exceeded | domain/platform.rs |
| A55003 | types | assura-types | Duplicate library name | domain/meta/contract_library.rs |
| A32001 | types | assura-types | Opaque function called without contract | domain/core/opaque_function.rs |
| A48001 | types | assura-types | Complexity bound exceeded | domain/meta/complexity_bound.rs |
| A34001 | types | assura-types | Evict pinned page | domain/storage/page_cache.rs |
| A37001 | types | assura-types | Monotonicity violation | domain/storage/monotonic_state.rs |
| A30003 | types | assura-types | Protocol missing required field | domain/format/protocol_grammar.rs |
| A15004 | types | assura-types | Operation may violate invariant | checkers/security/structural_invariant.rs | | A15001 | types | assura-types | Structural invariant on non-recursive type | checkers/security/structural_invariant.rs | | A18002 | types | assura-types | Shared memory write without exclusive | checkers/security/shared_mem.rs | | A33003 | types | assura-types | Fsync before data write | domain/storage/crash_recovery.rs | | A03012 | types | assura-types | Index variable used at runtime | checkers/info_flow.rs | | A23002 | types | assura-types | Circular buffer zero capacity | domain/memory.rs | | A45003 | types | assura-types | Undeclared feature flag | domain/platform.rs | | A42002 | types | assura-types | ULP bound violation | domain/numeric.rs | | A31001 | types | assura-types | Undefined axiom reference | domain/core/axiomatic_def.rs | | A31003 | types | assura-types | Unused axiom | domain/core/axiomatic_def.rs | | A32003 | types | assura-types | Reveal outside proof context | domain/core/opaque_function.rs | | A51001 | types | assura-types | Precondition strengthened | domain/meta/incremental_contract.rs | | A48003 | types | assura-types | Exponential complexity warning | domain/meta/complexity_bound.rs | | A54003 | types | assura-types | Diamond inheritance in contracts | domain/meta/contract_composition.rs | | A30001 | types | assura-types | Protocol invalid transition | domain/format/protocol_grammar.rs | | A29003 | types | assura-types | Checksum range mismatch | domain/format/checksum.rs | | A28003 | types | assura-types | String truncation splits code unit | domain/format/string_encoding.rs | | A27001 | types | assura-types | Bit field out of bounds | domain/format/bit_level.rs | | A26004 | types | assura-types | Binary fields overlap | domain/format/binary_format.rs | | A26003 | types | assura-types | Binary field missing endianness | domain/format/binary_format.rs | | A15002 | types | assura-types | Tree invariant insufficient fields | checkers/security/structural_invariant.rs | | A15003 | types | assura-types | Sort invariant wrong field count | checkers/security/structural_invariant.rs | | A33002 | types | assura-types | Commit without fsync | domain/storage/crash_recovery.rs | | A03011 | types | assura-types | Dependent type index kind mismatch | checkers/info_flow.rs | | A03008 | types | assura-types | Invalid Bool index expression | checkers/info_flow.rs | | A25002 | types | assura-types | Nested deadline exceeds outer | domain/concurrency.rs | | A24002 | types | assura-types | Callback registered in non-reentrant context | domain/concurrency.rs | | A23019 | types | assura-types | Fence ordering mismatch | domain/memory.rs | | A47002 | types | assura-types | Undischarged safety obligation | domain/safety.rs | | A47003 | types | assura-types | Empty proof obligations | domain/safety.rs | | A45002 | types | assura-types | Conflicting feature flags | domain/platform.rs | | A38002 | types | assura-types | Handler for undeclared failure mode | domain/storage/storage_failure.rs | | A44002 | types | assura-types | Direct platform reference | domain/platform.rs | | A55002 | types | assura-types | Library self-dependency | domain/meta/contract_library.rs | | A54002 | types | assura-types | Circular contract extends chain | domain/meta/contract_composition.rs | | A43003 | types | assura-types | Zero-size table | domain/numeric.rs | | A43004 | types | assura-types | Invalid encoding: byte sequence not valid | domain/numeric.rs | | A31002 | types | assura-types | Circular axiom dependency | domain/core/axiomatic_def.rs | | A53003 | types | assura-types | After-all predicate not satisfied | domain/core/crud_auth.rs | | A53001 | types | assura-types | CRUD operation missing auth policy | domain/core/crud_auth.rs | | A53002 | types | assura-types | Delete without authentication | domain/core/crud_auth.rs | | A52003 | types | assura-types | Restore non-suspended invariant | domain/meta/scoped_invariant.rs | | A50002 | types | assura-types | Refinement chain gap | domain/meta/multi_pass_refinement.rs | | A50003 | types | assura-types | Trivial refinement pass | domain/meta/multi_pass_refinement.rs | | A36002 | types | assura-types | Resource leak after rollback | domain/storage/rollback.rs | | A38003 | types | assura-types | Critical failure mode unhandled | domain/storage/storage_failure.rs | | A35002 | types | assura-types | Snapshot isolation violation | domain/storage/mvcc.rs | | A34002 | types | assura-types | Evict dirty page without flush | domain/storage/page_cache.rs | | A29002 | types | assura-types | Checksum algorithm mismatch | domain/format/checksum.rs | | A28002 | types | assura-types | String encoding mismatch | domain/format/string_encoding.rs | | A27002 | types | assura-types | Bit field crosses byte boundary | domain/format/bit_level.rs | | A05200 | types | assura-types | Unbounded quantifier warning | assura-cli/src/check/report.rs | | A51002 | types | assura-types | Postcondition weakened | domain/meta/incremental_contract.rs | | A37002 | types | assura-types | Illegal monotonic variable reset | domain/storage/monotonic_state.rs | | A03009 | types | assura-types | Invalid Enum index expression | checkers/info_flow.rs |
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
| Symptom | First action |
|---|---|
A01xxx | Parser/grammar/lower; minimal reproduction in tests/fixtures/ |
A02xxx | assura-resolve; symbol table / imports / type_refs |
A03xxx | assura-types inference/clauses; check Type::is_indeterminate() footgun |
A04xxx / counterexample | assura-smt; unconstrained result/outputs; verify_typed |
A05xxx linearity | checks/linear_typestate.rs / checkers/linear.rs |
A06xxx typestate | checkers/typestate.rs |
A07xxx effects | checks/effects.rs; known effect names only (see AGENTS pipeline trap) |
A08xxx taint/flow | checks/info_flow.rs / checkers/taint.rs |
A09xxx / A10xxx match/totality | checks/meta.rs / checkers/totality.rs; parser arm trivia footgun |
A14xxx frame/modifies | checks/frame_totality.rs |
A31xxx liveness | checks/core.rs; parser may split prove: leads_to(...) into two clauses |
A05100 counterexample / A05101 timeout / A05102 limitation / A05103 inconclusive | check/report.rs; limitation (A05102) = warning, else error |
A52xxx / A54xxx / high A-series | domain/meta features: checks/meta.rs, domain/, then rg 'Axxxxx' crates |
| Wrong phase suspicion | bash scripts/guards.sh then re-read AGENTS decision tree |
Maintenance
- Source of truth for meanings:
docs/SPECIFICATION.md§7.2. - When adding a new
Axxxxxin 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.
Catalog placeholders (not emitted)
Pure-listing hollow error codes (catalog + SPEC, no production emit and no partial checker wiring) were removed. New codes must be implemented, emitted, cataloged, and indexed in the same PR. See AGENTS.md and guards sections 14–15.
If a code is only planned, describe it in prose without an Axxxxx number
until emit lands. Do not re-add rows here without a production emitter.