feat(inference): add xAI Grok provider (#425)

.github/workflows/ci.yml

@@ -150,6 +150,9 @@ jobs:
       - name: Check spec code blocks parse correctly
         run: python scripts/check_spec_examples.py
 
+      - name: Check spec EBNF and Lark grammar agree on rule names (#683)
+        run: python scripts/check_grammar_alignment.py
+
       - name: Check README code blocks parse correctly
         run: python scripts/check_readme_examples.py
 
@@ -159,6 +162,9 @@ jobs:
       - name: Check FAQ code blocks parse correctly
         run: python scripts/check_faq_examples.py
 
+      - name: Check DE_BRUIJN.md code blocks parse correctly
+        run: python scripts/check_debruijn_examples.py
+
       - name: Check PYPI_README code blocks parse, check, and verify
         run: python scripts/check_pypi_readme_examples.py
 
@@ -171,6 +177,9 @@ jobs:
       - name: Check no unexpected [E602]/[E604] silent skips (Layer 1 of #626)
         run: python scripts/check_e602_clean.py
 
+      - name: Check editor grammars and READMEs carry every built-in effect (#1156)
+        run: python scripts/check_editor_grammars.py
+
       - name: Check every diagnostic carries rationale/fix/spec_ref (#682)
         run: python scripts/check_diagnostic_fields.py
 

.gitignore

@@ -62,3 +62,13 @@ node_modules/
 # interrupted run can strand one in the repo root.  Backstop only — the checkers
 # now write to the system tempdir, not here.
 /tmp*.vera
+
+# Run artifacts from the example corpus.  `examples/file_io.vera` writes the
+# RELATIVE path `hello.txt`, and the host resolves it against the process CWD
+# — so the documented invocation `vera run examples/file_io.vera` from the
+# repository root drops it in the ROOT, and running it from inside `examples/`
+# drops it there.  Both are ignored; a `git add -A` has twice picked the root
+# one up.  It is output, not source.  (`scripts/check_examples.py` only checks
+# and verifies, so it produces neither; `pytest tests/` leaves the tree clean.)
+/hello.txt
+/examples/hello.txt

.pre-commit-config.yaml

@@ -77,7 +77,7 @@ repos:
         pass_filenames: false
         files: '(examples/README\.md$|examples/.*\.vera$)'
 
-      # The six doc-block gates below read the inline vera:skip fence
+      # The seven doc-block gates below read the inline vera:skip fence
       # annotations via scripts/doc_annotations.py (#538), so an edit to
       # that shared module (or the gate script itself) re-runs the gate.
       - id: readme-examples
@@ -108,6 +108,13 @@ repos:
         pass_filenames: false
         files: '(FAQ\.md$|vera/.*\.py$|vera/grammar\.lark$|scripts/(check_faq_examples|doc_annotations)\.py$)'
 
+      - id: debruijn-examples
+        name: de bruijn examples
+        entry: .venv/bin/python scripts/check_debruijn_examples.py
+        language: system
+        pass_filenames: false
+        files: '(DE_BRUIJN\.md$|vera/.*\.py$|vera/grammar\.lark$|scripts/(check_debruijn_examples|doc_annotations)\.py$)'
+
       - id: pypi-readme-examples
         name: pypi readme examples
         entry: .venv/bin/python scripts/check_pypi_readme_examples.py
@@ -132,6 +139,34 @@ repos:
         pass_filenames: false
         files: '(\.md$|vera/environment\.py$|vera/prelude\.py$)'
 
+      # #683 — fails when a rule name exists in spec/10-grammar.md's EBNF but
+      # not in vera/grammar.lark, or the other way round.  Chapter 10 is the
+      # published map of the parse tree and drifted from it: the spec still
+      # called the assertion forms assert_stmt/assume_stmt after they became
+      # expressions, and three Lark rules (pure_effect, effect_set,
+      # with_clause) appeared in no EBNF block at all.  Rule names only — the
+      # bodies are not compared.
+      - id: grammar-alignment
+        name: grammar rule-name alignment
+        entry: .venv/bin/python scripts/check_grammar_alignment.py
+        language: system
+        pass_filenames: false
+        files: '(vera/grammar\.lark$|spec/10-grammar\.md$|scripts/check_grammar_alignment\.py$)'
+
+      # #1156 — fails when an editor grammar under editors/, or one of the two
+      # extension READMEs that repeat the list in prose, omits a built-in
+      # effect name.  Both enumerate them by hand and drifted four effects
+      # behind the registry silently (an unknown capitalised name just falls
+      # through to the generic type rule), so nothing failed when adding an
+      # effect skipped them.  Triggered by the effect registry as well as
+      # the grammars, since a new effect is what puts them out of date.
+      - id: editor-grammars
+        name: editor grammars
+        entry: .venv/bin/python scripts/check_editor_grammars.py
+        language: system
+        pass_filenames: false
+        files: '(editors/.*|vera/environment\.py$|vera/introspect\.py$|scripts/check_editor_grammars\.py$)'
+
       # Layer 1 of #626 — fails when any compile of an example or
       # conformance program emits [E602] (body unsupported) or
       # [E604] (param unsupported) outside the explicit allowlist

AGENTS.md

@@ -8,7 +8,7 @@ Read `SKILL.md` for the full language reference. It covers syntax, slot referenc
 
 ### Conformance programs as reference
 
-The conformance suite in `tests/conformance/` contains 179 small, self-contained programs — often one per language feature — that serve as minimal working examples (most are fully self-contained; the cross-module programs of Chapters 7–9 import companion `_lib`/module fixtures). Each positive program must pass its declared verification level (see `manifest.json` for mappings: `parse`, `check`, `verify`, or `run`); the twenty-five negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`) instead must *fail* `check` with the E-code in their `expected_error` field. When you need to see how a specific construct works (e.g. effect handlers, match expressions, closures), check the corresponding conformance program before reading the spec.
+The conformance suite in `tests/conformance/` contains 214 small, self-contained programs — often one per language feature — that serve as minimal working examples (most are fully self-contained; the cross-module programs of Chapters 7–9 import companion `_lib`/module fixtures). Each positive program must pass its declared verification level (see `manifest.json` for mappings: `parse`, `check`, `verify`, or `run`); the thirty-two negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_reserved_resume_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`, `ch02_alias_cycle_rejected`) instead must *fail* `check` with the E-code in their `expected_error` field. When you need to see how a specific construct works (e.g. effect handlers, match expressions, closures), check the corresponding conformance program before reading the spec.
 
 ### Workflow
 
@@ -52,7 +52,7 @@ vera version                      # Print the installed version (also --version,
 vera lsp                          # Serve LSP over stdio (needs the [lsp] extra; see LSP_SERVER.md)
 vera builtins [--json]            # List the built-in function registry (no file needed)
 vera effects [--json]             # List the effect and ability registry (no file needed)
-vera errors [--json]              # List the diagnostic error-code registry E001–E702 (no file needed)
+vera errors [--json]              # List the diagnostic-code registry: E001–E702 + W001/W002 (no file needed)
 ```
 
 See [TOOLCHAIN.md](TOOLCHAIN.md) for the CLI cookbook — driving the toolchain to write, verify, test, run, and debug Vera, including the `builtins`/`effects`/`errors` introspection commands.
@@ -134,13 +134,15 @@ The `verify --json` output includes a verification summary:
 }
 ```
 
+Alongside it, an `obligations` array carries one entry per reified proof obligation (`kind`, `status`, `description`, `location`). The summary is derived from that array by `status` — `verified` counts as `tier1_verified`, `tier3`/`timeout` as `tier3_runtime`, and `total` is their sum. Reproduce the counts by *filtering on `status`*, not by taking the array's length: a `violated` or `tier3_unguarded` obligation discharged to no tier, so it is counted nowhere and is surfaced as an error or warning diagnostic instead. On a program with one refuted contract, `total: 2` beside a three-entry array is the expected partition.
+
 ### Essential rules
 
 1. Every function needs `requires()`, `ensures()`, and `effects()` between the signature and body
 2. Use `@Type.index` to reference bindings (`@Int.0` = most recent Int, `@Int.1` = one before)
 3. Declare all effects: `effects(pure)` for pure functions, `effects(<IO>)` for IO, `effects(<Http>)` for network, `effects(<Inference>)` for LLM calls
 4. `Http.get(@String.0)` and `Http.post(@String.0, @String.1)` return `Result<String, String>`; match the result
-5. `Inference.complete(@String.0)` returns `Result<String, String>`; requires `VERA_ANTHROPIC_API_KEY`, `VERA_OPENAI_API_KEY`, `VERA_MOONSHOT_API_KEY` (Kimi), or `VERA_MISTRAL_API_KEY` to run; provider auto-detected from whichever key is set.  See [`ENVIRONMENT.md`](ENVIRONMENT.md) for the full env-var reference, including `VERA_INFERENCE_PROVIDER` / `VERA_INFERENCE_MODEL` overrides
+5. `Inference.complete(@String.0)` returns `Result<String, String>`; requires `VERA_ANTHROPIC_API_KEY`, `VERA_OPENAI_API_KEY`, `VERA_MOONSHOT_API_KEY` (Kimi), `VERA_MISTRAL_API_KEY`, or `VERA_XAI_API_KEY` (Grok) to run; provider auto-detected from whichever key is set.  See [`ENVIRONMENT.md`](ENVIRONMENT.md) for the full env-var reference, including `VERA_INFERENCE_PROVIDER` / `VERA_INFERENCE_MODEL` overrides
 6. Recursive functions need a `decreases()` clause
 7. Match expressions must be exhaustive
 8. `DB.query` / `DB.execute` (effect `<DB>`) take a **literal** SQL string — a query assembled from a runtime value is a compile-time error (`E207`). Every runtime value goes through a `?` placeholder and the `Array<Option<String>>` params array (`DB.query("SELECT ... WHERE id = ?", [Some(@String.0)])`); a placeholder/params count mismatch with a literal params array is `E208`. The connection comes from `VERA_DB_URL` (default: in-memory SQLite) — see [`ENVIRONMENT.md`](ENVIRONMENT.md)
@@ -185,9 +187,9 @@ Each stage is a module with a single public API function (`parse_file`, `transfo
 pytest tests/ -v                       # Run all tests (see TESTING.md)
 pytest tests/test_conformance.py -v    # Conformance suite only
 mypy vera/                             # Type-check the compiler
-python scripts/check_conformance.py    # All 179 conformance programs hold (positives pass; negatives fail with their E-code)
+python scripts/check_conformance.py    # All 214 conformance programs hold (positives pass; negatives fail with their E-code)
 python scripts/check_examples.py       # All 42 examples must pass
-python scripts/check_corpus_canonical.py # All 227 corpus programs in canonical form
+python scripts/check_corpus_canonical.py # All 262 corpus programs in canonical form
 ```
 
 Test helpers follow a pattern: `_check_ok(source)` / `_check_err(source, match)` / `_verify_ok(source)` / `_verify_err(source, match)`. See existing tests for examples.
@@ -196,7 +198,7 @@ When implementing a new language feature, write the conformance program *first*
 
 ### Invariants
 
-- All 179 conformance programs in `tests/conformance/` must hold at their declared level — positive entries pass, and the negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`) must *fail* `check` with their `expected_error` E-code
+- All 214 conformance programs in `tests/conformance/` must hold at their declared level — positive entries pass, and the negative fixtures (`ch02_generic_over_unit_rejected`, `ch02_map_unit_value_rejected`, `ch04_let_unit_rejected`, `ch05_apply_fn_arity`, `ch05_decreases_float_rejected`, `ch05_reserved_fn_name_rejected`, `ch05_reserved_keyword_fn_rejected`, `ch05_reserved_resume_fn_rejected`, `ch05_where_helper_outer_slot_rejected`, `ch07_handler_state_body_scope_rejected`, `ch07_old_outside_ensures_rejected`, `ch07_state_unit_op_param_read_rejected`, `ch08_circular_import`, `ch08_reserved_vera_prefix_rejected`, `ch08_reserved_vera_prefix_reference_rejected`, `ch08_reserved_vera_prefix_binder_rejected`, `ch08_reserved_vera_prefix_effect_rejected`, `ch08_reserved_vera_prefix_ability_rejected`, `ch08_reserved_vera_prefix_constructor_rejected`, `ch08_visibility_private`, `ch09_builtin_effect_redefinition_rejected`, `ch09_builtin_redefinition`, `ch09_ord_adt_rejected`, `ch09_eq_non_derivable_rejected`, `ch09_sql_injection_rejected`, `ch09_sql_placeholder_mismatch_rejected`, `ch09_sql_placeholder_let_mismatch_rejected`, `ch09_sql_numbered_placeholder_rejected`, `ch07_bare_effect_op_rejected`, `ch06_quantifier_array_domain_rejected`, `ch07_handler_state_type_mismatch_rejected`, `ch02_alias_cycle_rejected`) must *fail* `check` with their `expected_error` E-code
 - All 42 examples in `examples/` must pass `vera check` and `vera verify`
 - `mypy vera/` must be clean
 - `pytest tests/ -v` must pass