Skip to content

Add Hello World example and spec design notes#3

Merged
aallan merged 1 commit into
mainfrom
spec-and-readme-updates
Feb 23, 2026
Merged

Add Hello World example and spec design notes#3
aallan merged 1 commit into
mainfrom
spec-and-readme-updates

Conversation

@aallan

@aallan aallan commented Feb 23, 2026

Copy link
Copy Markdown
Owner

Summary

  • Add Hello World as the first example in README "What Vera Looks Like" section — the example humans will look for first
  • Add three forward-looking design notes to spec Chapter 0.8:
    • Abilities — Roc-style restricted type constraints, auto-derivable, no HKTs
    • LLM Inference<Inference> as an algebraic effect for AI runtime calls
    • Stdlib collectionsSet<T>, Map<K, V>, Decimal

Tagged as v0.0.5-1 (spec/docs update, not a compiler release).

Test plan

  • Verify README renders correctly on GitHub
  • Verify spec design notes are consistent with Chapters 2 (types) and 7 (effects)
  • No compiler changes — all pre-commit hooks pass

🤖 Generated with Claude Code

Add Hello World as first example in README "What Vera Looks Like"
section. Add three design notes to spec Chapter 0.8: Roc-style
restricted abilities, LLM inference as an algebraic effect, and
standard library collections (Set, Map, Decimal).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@aallan aallan merged commit 5c35fce into main Feb 23, 2026
5 checks passed
@aallan aallan deleted the spec-and-readme-updates branch February 23, 2026 08:27
aallan added a commit that referenced this pull request May 7, 2026
1. HISTORY.md "137 tagged releases" -> 138 (line 315): the v0.0.138
   row was added but the rollup footer count still said 137.

2. ROADMAP.md stabilisation-gate sentence: "order #5 starts when
   #1-#4 are closed" -> "order #4 starts when #1-#3 are closed".
   The earlier deletion of the #593 row (now closed) shifted the
   stabilisation tier to three items; the agent-integration tier
   numbering is also renumbered 5/6/7 -> 4/5/6 to match.

3. New test: test_eager_gc_array_mapi_with_non_allocating_string_closure
   mirrors the existing array_map String eager-GC test for the
   array_mapi unwind path with a fn(@Bool, @nat -> @string) closure
   returning pick(@Bool.0).  The existing array_mapi ADT test
   (test_array_mapi_non_allocating_closure_emits_balanced_push)
   covered the i32 branch; this new test covers the i32-pair branch.

4. Tighten the structural #593 predicate.  Pre-fix it accepted any
   "global.set $gc_sp" + absent "call $alloc"; CodeRabbit observed
   that a bare "global.set $gc_sp" could in principle be a stack-
   restore rather than a push.  In practice the prologue's
   gc_sp_save/restore is gated on ctx.needs_alloc and the regex
   already excludes call $alloc, so a non-allocating body cannot
   contain a restore -- but the literal predicate was weaker than
   the intent.  Adds _has_gc_shadow_push helper that anchors on the
   canonical "i32.const 4 / i32.add / global.set $gc_sp" SP-increment
   sequence emitted by gc_shadow_push (vera/wasm/helpers.py).  Used
   by both the i32-pair and i32-ADT structural tests; a non-push
   artefact in the body can no longer satisfy the assertion.

Plus: HISTORY.md tooling section gains a v0.0.138 row for
VERA_EAGER_GC alongside the existing tooling milestones (cross-
linked to ENVIRONMENT.md, which already has the full reference
section for it).

Suite: 3,747 passed (+1 from new array_mapi String test), 14 skipped.

Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan added a commit that referenced this pull request May 7, 2026
Two Conway's Life agent experiments on --target browser surfaced
five concrete blockers (issues #602/#603/#604/#609/#610) and an
explicit design memo (#608) mapping each obstacle to a concrete
runtime-only fix.  The current stabilisation framing covers
codegen reliability and walker completeness but treats browser-
target reliability as a separate concern.  The agent's diagnosis
makes that split harder to defend: "write once, run anywhere"
is currently true for pure computation and approximate-to-false
for anything with timing or screen output.  Two of the fixes
(#609 JSPI-driven IO.sleep, #610 ANSI subset interpreter) close
the timing and rendering halves of the seam without language
changes -- adding them to the stabilisation tier commits to
"browser-target Vera is something you'd actually use" before
the agent-integration push.

Changes:
- Expanded the campaign-pattern list from two patterns to three;
  third pattern documents the browser-target seam with links to
  the umbrella issue (#608) and the five concrete blockers.
- Added #609 (JSPI-driven IO.sleep) as item 3 in the stabilisation
  tier, with rationale + the WebAssembly JSPI / Asyncify mechanism.
- Added #610 (ANSI subset interpreter) as item 4 in the same tier,
  paired with #609 -- together they close the seam and let life.vera
  (terminal version) run unchanged on --target browser.
- Renumbered #595 from item 3 to item 5 (now last in stabilisation,
  since it's contingent on an upstream wasmtime-py release).
- Renumbered the agent-integration tier items 4/5/6 -> 6/7/8 to
  match.
- Updated the "What moves when" gate from "#4 starts when #1-#3
  are closed" to "#6 starts when #1-#5 are closed".

Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan added a commit that referenced this pull request May 8, 2026
PR #629 patched eight distinct triggers of the same canonical-name
canonicalisation drift, each one fixed locally. The underlying
pattern — five overlapping canonicalisation helpers in
`vera/wasm/inference.py` plus a silent fallthrough at
`vera/wasm/operators.py:482` that amplifies any inference miss
into invalid WASM — remains exposed.  The 9th trigger is a matter
of when, not if.

Filed #630 to close the bug class structurally:

  - Tier 1: fold the five helpers (`_format_named_type`,
    `_format_named_type_canonical`, `_resolve_i32_pair_ret_te`,
    `_resolve_base_type_name`, ad-hoc while-loops) into a single
    `_canonical_vera_type` covering RefinementType unwrap +
    alias-chain follow + generic substitution + format-with-args.
    Apply at every type-walking inference site.

  - Tier 2: convert the silent fallthrough at operators.py:482
    to a hard compile-time error. Dovetails with #626 Layer 1.

Together they make the 9th trigger either impossible (T1) or
instantly diagnosable (T2). Pure refactor + diagnostic
conversion — no behavioural change for any valid program; all
8 existing regression tests in TestStringInterpolation continue
to pin the now-fixed triggers.

Added to ROADMAP stabilisation tier as item #3 (after #604 and
#626; #630 is a sibling of #626 — single canonicalisation site
rather than the broader translator-returns-None pattern).
Renumbered the rest of the table.

Added to KNOWN_ISSUES.md "Bugs" section alongside #628 — both
are latent bug-class entries where individual instances are
patched but the underlying pattern remains exposed.

Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan added a commit that referenced this pull request May 8, 2026
…ents + CodeRabbit

Four review agents (code-reviewer, pr-test-analyzer, comment-analyzer,
silent-failure-hunter) plus three CodeRabbit comments produced a
batch of cross-cutting findings.  This commit addresses them all
in one pass to avoid the iterative round-trip cost the bug class
itself was filed to eliminate.

**Critical fixes:**

1. **Closure body E615 harvest gap (silent-failure-hunter C1).**
   `_compile_lifted_closure` constructed its own WasmContext but
   never harvested `_interp_inference_failures` — closure bodies
   with E615-triggering interpolation segments were silently
   dropped, producing call_indirect→missing-table-entry WASM
   validation traps with no source-located diagnostic.  Extracted
   the harvest into `CodeGenerator._harvest_interp_inference_failures`
   on the codegen base and called it from both functions.py and
   closures.py.  Removed the now-disproved `# pragma: no cover —
   defensive` claim on closures.py's body-instrs-None path.  New
   regression test `test_e615_in_closure_body_emits_diagnostic`.

2. **`_canonical_named_type` type_args from terminal NamedType
   (CodeRabbit #3 + code-reviewer I1).**  The walker's
   `outer_type_args` capture rule (always read from first NamedType)
   lost type_args when alias_map substitution bound a generic
   param to a parameterised type.  Empirically reachable today via
   `type Mapper<A, B> = fn(A -> B); Mapper<Int, Array<Int>>` etc.
   Fix: drop the "outermost" rule, return type_args from the
   terminal NamedType reached.  All 21 existing #602-class
   regression tests still pass.  New regression test
   `test_canonical_named_type_terminal_args_propagation`.

3. **HISTORY.md footer (CodeRabbit #1).**  141 tagged releases →
   142 to match the v0.0.142 row added in PR #631.

**UX fix:**

4. **Multiple E615 per function (silent-failure-hunter H2).**
   Pre-this-fix `_translate_interpolated_string` returned None on
   the first failing segment, requiring N round-trips for N bad
   segments in one interpolation.  Now collects every failing
   segment via `had_failure` flag, then bails at the end.  New
   regression test `test_multiple_e615_in_one_interpolation`.

**Doc-quality fixes (comment-analyzer):**

5. **Trigger-count drift** in `operators.py:491-494` —
   "every canonicalisation gap (#602 and ten subsequent triggers)"
   implied 11; rewrote to "the ten triggers of the #602 bug class
   accumulated across PRs #627 + #629".

6. **`_format_named_type_canonical` docstring drift** — claim
   "matches the pre-#630 fallback shape" was empirically wrong
   (pre-#630 resolved through aliases, post-#630 fallback doesn't).
   Rewrote to acknowledge the deliberate behavioural change.

7. **"Future closure-arg shapes plug in here without further
   dispatch ladder"** — overstatement.  Adding a `FnCall`
   returning a closure still needs an `elif`; what's saved is
   canonicalisation logic, not dispatch logic.  `IfExpr` between
   closures has no single `return_type` field — example was
   misleading.  Rewrote in both `_infer_fncall_vera_type` and
   `_infer_apply_fn_return_type`.

8. **`_canonical_wasm_type` docstring** — added explicit `Unit →
   None` documentation; clarified that `None` (no WASM type) and
   `"i64"` (unreachable-NamedType default) are distinct return
   shapes that callers must not conflate.

**Tests added (besides the regressions tied to fixes):**

9. **`test_per_function_isolation_of_failures_list`** — pins
   that a clean function and a dirty function in the same source
   produce independent `_interp_inference_failures` lists.

10. **`test_e615_fires_on_result_in_interpolation`** — adjacent
    ADT shape (Result vs Option) so a future Option-handling
    broadening doesn't accidentally regress the parallel Result
    path.

11. **`test_array_map_refinement_returning_closure`** — pins the
    previously-unaudited `_infer_closure_return_vera_type` path
    in `calls_arrays.py`, which the #630 migration broadened to
    handle refinements.

**Test enhancements:**

12. **E615 ordering before matching E602** in the existing test
    (CodeRabbit #2) — pinned via `warnings.index(e615[0])` <
    `warnings.index(matching_e602)`.  Filtered to the E602 that
    mentions the offending function so prelude-skip E602s don't
    confound the assertion.

13. **E615 source-location attached** in the existing test —
    softened to "line > 0" (any location) because SlotRef-inside-
    InterpolatedString spans are unreliable today (#634, separate
    follow-up).  Tightening to "line points at the segment" is
    the natural acceptance test for that follow-up.

**Skipped with reasons:**

- **Cycle-guard regression on `_resolve_base_type_name`** —
  test-analyzer C1 / code-reviewer S4.  Verified pre-existing
  and dead-code-safe today (cycles crash an upstream resolver
  first).  Filed as #633.

- **`_canonical_wasm_type`'s `i64` default for unhandled
  apply_fn / call_indirect shapes** — silent-failure-hunter H1.
  Bigger refactor parallel to Tier 2 but for the WASM-side
  dispatch.  Filed as #632.

- **SlotRef-inside-InterpolatedString span fidelity** —
  surfaced when writing the E615 source-location assertion.
  Diagnostic-quality concern, separate from #630's
  canonicalisation scope.  Filed as #634.

- **`_canonical_named_type` worked-example docstring**
  (comment-analyzer I6) — superseded by fix #2 above (semantics
  changed; docstring rewritten with concrete examples).

- **Per-context isolation prose-vs-test** (comment-analyzer I4)
  — addressed via fix #9 (test added).

- **`_resolve_i32_pair_ret_te` 30-line upper docstring** —
  comment-analyzer style nit.  The prose is load-bearing
  context (#628 cross-module narrative); trimming would lose
  history without obvious gain.  Defer.

**Follow-ups:** #632 (apply_fn / call_indirect E616), #633
(_resolve_base_type_name cycle guard), #634 (interpolation
SlotRef source spans).  Added to KNOWN_ISSUES.md alongside #628.

Counts: 3,792 tests (3,778 passed, 14 skipped) — six new tests
under `TestE615LoudInterpolationFallthrough630`.  CHANGELOG +
KNOWN_ISSUES + ROADMAP + TESTING.md + HISTORY footer all
synced.  mypy clean.

Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan added a commit that referenced this pull request May 11, 2026
…isted file (#626 Layer 1)

CodeRabbit found that the manifest-driven conformance filter silently
masked two state-inconsistency cases:

1. Missing `tests/conformance/manifest.json` → conformance list
   stayed empty; the gate scanned only examples.  No error surfaced.

2. Manifest entry referencing a file that doesn't exist on disk →
   silently dropped.  A partial scan set hides regressions in the
   missing program.

Both cases now fail fast with clear stderr messages:

- Missing manifest: "ERROR: conformance manifest not found at <path>"
  before any compile work.
- Missing files: collect all manifest entries with missing files
  first, then print one row per missing file with its entry id +
  filename, then refuse to run with rationale.  Collecting first
  surfaces the full discrepancy in one message rather than aborting
  on the first missing file.

Validated both paths by (a) temporarily moving the manifest aside
and (b) appending a fake entry referencing a nonexistent file —
both produce the expected error and exit 1.
aallan added a commit that referenced this pull request May 11, 2026
CodeRabbit found that the gate's stderr summary collapsed two
distinct failure categories into a single "unexpected [E602]/[E604]
skips" message: per-function silent skips (the gate's core
purpose) and file-level hard failures (PARSE_ERROR / TIMEOUT /
COMPILE_ERROR — file couldn't be evaluated at all).  The wording
was inaccurate when hard failures were present; a user reading
the summary couldn't tell whether the gate had found a new
silent skip or whether the compile pipeline itself was broken.

Split into two categories with distinct semantics + reporting:

- `skip_failures` — unexpected per-function [E602]/[E604]
  warnings outside the allowlist.  The core silent-skip detection
  the gate exists for.
- `hard_failures` — file-level: COMPILE_ERROR, PARSE_ERROR,
  TIMEOUT.  File couldn't be evaluated at all.

`_scan_paths` now returns `(clean, skip_failures, hard_failures)`
instead of `(clean, failures)`.  `main` prints hard failures
first (file-level problems before per-function detail), each
section with its own rationale paragraph.  Exit code 1 if either
category is non-empty.

Verified both empty (clean run) and non-empty (manifest-listed
missing file from CodeRabbit #3 testing) produce the expected
output.
aallan added a commit that referenced this pull request May 11, 2026
Both findings are reason-string quality on user-facing [E602]
diagnostics — the same lens the comment-analyzer flagged in the
PR review, refined to specific sites.

CR-2 (line 1688): `_translate_array_any_all_common` is a shared
implementation helper for `array_any` and `array_all`.  It was
passing `role="array_any_all"` into `_array_elem_triad_or_skip`
and emitting `"no load op for array_any_all_common element"` in
its body load-op raise.  Both strings leaked the internal helper
name into user-visible diagnostics.

Fix: thread a `name: str` kwarg through the helper from each
caller (`name="array_any"` / `name="array_all"`), use it for the
triad helper's `role=` and the body load-op raise.  Diagnostics
now mention `array_any` or `array_all` — the source-level builtin
the user wrote — rather than the internal dispatch helper.

CR-3 (lines 504-507): `_translate_array_slice`'s inference-failure
raise used to read "could not infer array_slice element type
(non-empty array literal required)".  The parenthetical implied
the fix was "use a literal", but the branch fires whenever
`_infer_concat_elem_type()` can't recover the element type — that
includes non-literal expressions that happen to be inference-opaque,
not just non-empty literals.

Fix: rephrase to "(provide an explicit element type or ensure
elements are recoverable from the expression)".  Neutral on the
literal/non-literal distinction; covers both reachable paths.

Validation
- mypy clean
- pytest 3789 passed, 14 skipped

Refs #626 #658

Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan added a commit that referenced this pull request May 13, 2026
Following user direction to pull all 7 deferred pr-review
findings into this PR rather than file a follow-up.  The 4
small code fixes (items 2/3/5/8) plus 2 new test files
(items 6/7) land here.

Code fixes:

- **#2 ModuleCall path-drop** (`vera/wasm/inference.py:289-292`
  and `:~973`) — both `_infer_expr_wasm_type::ModuleCall` and
  `_infer_vera_type::ModuleCall` previously synthesised a fake
  `ast.FnCall(name=expr.name, args=expr.args)` for dispatch,
  silently dropping `expr.path: tuple[str, ...]`.  If a
  regression ever flowed a ModuleCall to either helper, the
  fake-FnCall lookup could match a same-name local fn from a
  different module — silent wrong-answer rather than safe
  failure.  Now both return `None` so the unknown-type surfaces
  cleanly.

- **#3 AnonFn placeholder** (`vera/wasm/inference.py:~967`) —
  `_infer_vera_type::AnonFn` previously returned the literal
  string `"Fn"` as a placeholder.  No callsite recognised
  `"Fn"` as a real Vera type; downstream type-arg mangling
  paths (`vera/wasm/calls.py:1525,1533`) would feed it into
  mangled names like `option_map$Int_Fn`.  Now returns `None`
  for the same reason.

- **#5 Factually wrong "closure pipeline" comments**
  (`vera/codegen/compilability.py:~236, ~393`, both WALKER_
  COVERAGE checklists + inline pre-branch comments) — the
  `AnonFn` defensive branches were described as "masked today
  by closure pipeline running its own scan", but pr-review
  surfaced that `vera/codegen/closures.py::_compile_lifted_
  closure` does NOT call `_scan_io_ops` or
  `_scan_body_for_state_handlers` on lifted bodies.  The
  AnonFn branch is the PRIMARY defence, not redundant.
  Comments now state this directly.

- **#8 Dead `is not None` guards** (`vera/wasm/inference.py:~954,
  ~961`) — `Block.expr` and `HandleExpr.body.expr` are non-
  Optional in the AST schema (`vera/ast.py:470, 481`).  The
  guards in the `_infer_vera_type` defensive branches were
  unreachable defensive code.  Removed; direct calls now.

Test additions:

- **#6 Synthetic-AST tests for defensive branches**
  (`tests/test_walker_defensive_branches_597.py`, 21 tests,
  296 lines) — direct AST invocation pinning each of the 11
  defensive branches plus the 5 pr-review fixes.  Without
  these the defensive branches have 0% coverage (`coverage
  run` confirmed) — a future refactor breaking one would
  land silently.

- **#7 Unit tests for the enforcement script**
  (`tests/test_check_walker_coverage_597.py`, 12 tests, 255
  lines) — pins the script's parsing logic: Expr subclass
  extraction, isinstance flattening (incl. tuple form),
  checklist-block anchoring (incl. CR-3 regression test:
  `# Foo → bar` outside the WALKER_COVERAGE block must not
  be counted), section-header tolerance, auto-discovery
  invariants, end-to-end exit code.

CHANGELOG/HISTORY:

- Extended the v0.0.151 entry with two new sub-sections under
  "Fixed" (pr-review follow-ups) and a new "Tests" section
  documenting the two regression-test files.

Doc counts (auto-validated by `check_doc_counts.py`):

- TESTING.md total: 3,827 → 3,860 tests (+33), 29 → 31 files
- TESTING.md table: two new rows for the test files
- ROADMAP.md: 3,827 → 3,860
- README.md: 3,827 → 3,860

Validation:

- `pytest tests/ -q` → 3,846 passed, 14 skipped (+33 net new)
- `mypy vera/` → clean
- `python scripts/check_walker_coverage.py` → 9 walkers cover
  all 29 Expr subclasses (clean)
- `python scripts/check_doc_counts.py` → consistent across all
  surfaces

Refs #597 #668

Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan added a commit that referenced this pull request May 13, 2026
**Finding 1: TESTING.md stress count inconsistency** (valid) —
header table said `test_stress.py` has 16 instances but the
detailed section still read "8 initial test programs" and
"14 parametrised instances".  Fixed cohesively:
- `### The 8 initial test programs` → `### The 9 initial test
  programs` so the section claim matches the header.
- Added entry **9. `test_tco_with_allocation_1m_iterations`** so
  the section actually enumerates what it claims to.
- Updated test #3's stale narrative — this PR switched its body
  from `let @string = "stress"` (which doesn't trigger
  needs_alloc because string-pool literals don't allocate) to
  `let @array<Int> = [_, _]` (genuine heap alloc).  Old text
  asserted == 6,000 from `string_length("stress")`; new text
  asserts == 2,000 from `array_length([_, _])`.  Without this
  update the doc described a test that no longer exists.
- "Six of the eight" → "Seven of the nine" in the eager-GC lane
  paragraph (math now adds up to 16 with the 9th test).
- CLI examples and Budget line updated from 14/8 to 16/9.

**Finding 2: boundary-safe regex in WAT searches** (valid) — the
three #549 tests used plain `.find("(func $build")` and
`"return_call $build" in body` substring matches.  Today's test
source defines only `$build` and `$f` so there's no false-match
risk, but a future symbol like `$build_helper` would match
falsely.  Switched all three tests to `re.search` with
boundary-safe patterns:
- `re.search(r"\(func \$build\b", ...)` for function-start.
- `re.search(r"return_call \$build\b", ...)` for return_call
  sites (trailing `\b` excludes `$build_anything`).
- `re.search(r"\bcall \$build\b", ...)` for plain call sites
  (leading `\b` rules out `return_call $build`; trailing `\b`
  rules out `$build_anything`).
- Same boundary-safe extraction applied to `$overflow` in
  `test_shadow_stack_overflow_traps`.

Note on CR's literal suggested pattern `r'\b\(func \$build\b'`:
the leading `\b\(` is incorrect — `\b` requires a word-char on
one side, but `(` is preceded by whitespace or newline (both
non-word) at WAT indentation depths, so that anchor wouldn't
match.  Dropped the leading anchor; kept the substantive
trailing `\b`.

Scope decline: did NOT update the pre-existing tests in the
file that use the same substring-search pattern (the #517 tests
on lines 1899/1934/1949/1968/2016/2027 etc.).  Those existed
before this PR and changing them is out of scope for #549.
CR's relayed wording said "apply the same replacement to the
analogous checks later in the file" — interpreted as the
analogous checks in MY new/modified tests, not the entire pre-
existing test suite.

Validation: pytest passes (3862/3862), mypy clean, ruff S
rules clean, doc-counts consistent (test_codegen.py grew by
+39 lines from the regex switchover; TESTING.md updated to
match).

Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan added a commit that referenced this pull request May 26, 2026
Third CodeRabbit finding on #697 (not flagged by user — they
mentioned 2 — but real and important to fix).  I fabricated
the URL https://x.com/jasisz1/status/1796358291235291136 when
filing #698 and the ROADMAP entry, guessing at a plausible
X.com URL format from the screenshot.  CodeRabbit ran a web
query confirming the URL does not resolve.

Fix in this commit: ROADMAP.md vera shape entry now says
"\Szymon Teżewski (@jasisz1)'s 24 May 2026 tweet"\ (full
name, full date, no fake URL — the user has the screenshot
if anyone wants the actual link).

Also fixed (outside this commit):
- Issue #698 body — same URL, same fix.  Per memory note
  feedback_issue_history.md the exception list allows body
  edits for "factual error in just-filed issue under active
  review" — and CodeRabbit is the active reviewer.
- Issue #523 comment — my own earlier comment had the same
  URL.  Edited via gh api PATCH (comments are mutable
  surfaces, unlike issue bodies).

Docs-only — no version bump.

Co-Authored-By: Claude <noreply@anthropic.invalid>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant