You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This commit was created on GitHub.com and signed with GitHub’s verified signature.
Added
Concurrent <Async>: async(Http.get/post(...)) now runs on a host worker thread (#841). The concurrency half deferred when #59 shipped the language surface: async(Http.get(url)) / async(Http.post(url, body)) — with call-free argument expressions — fuse into a single vera.async_http_get / vera.async_http_post host import that issues the request on a host ThreadPoolExecutor at the async(...) point (request issuance keeps program order) and returns the Future as a #578 bit-31-tagged handle wrapper (new wrap kind 4); await probes the value's first word for the wrapper tag and blocks on vera.async_await for fused handles, passing eager values through unchanged. Two overlapping async(Http.get)s are pinned by a server-side request-ordering test (no wall-clock). Every other async shape keeps the eager identity lowering (spec §9.5.4 now says an implementation MAY evaluate concurrently when the effect row is commutative; §7.4 records the ordering guarantee). The fusion predicate is strictly narrower than W002's whitelist, so a "evaluates eagerly" warning can never coexist with concurrent execution — and it lives in one shared module (vera/wasm/async_fusion.py) consumed by both import-emission passes, so the pre-scan and the translator cannot desync. GC follows the full opaque-handle contract, mutation-validated: the wrapper is shadow-rooted at the async site (operand-stack window pinned) and an unawaited future's wrapper is reclaimed by Phase 2c host_decref_handle(4, handle), cancelling the task and evicting the store entry (observable via ExecuteResult.host_store_sizes["future"]). Worker threads run only the pure fetch halves (fetch_get / fetch_post, split out of the Http host callbacks in vera/runtime/http.py) and never touch guest memory; the Result ADT is built at await time on the guest thread. Ctrl-C during a blocked await rides the wasmtime>=45 BaseException trampoline to the exit-130 handler, and the executor is torn down (shutdown(cancel_futures=True)) on every exit path. The browser runtime stays eager (spec-conformant; identical values, request fires synchronously at the async point, outcome buffered host-side until await). A function may now declare a Future<T> return type (previously [E605]-skipped — Future<T> is transparent in the type mapper). The await handle-check keys on the literal type Future<Result<String, String>> and covers slots, parameters, direct compositions, and calls — bare, imported, or module-qualified — whose declared return is that type (derived from the cross-module return-type registry — with module-qualified calls resolved by (path, name), so a colliding local of a different future shape cannot misclassify await(m::grab(...)) in either direction; the local-only first cut and the bare-name qualified keying were both caught in review with repros and fixed with RED-first tests). Alias-typed shapes are rejected before codegen today (an alias-typed let has no WASM representation → [E602] skip); the one unclassifiable shape — an indirectly-called closure returning this future type — is a documented limitation in KNOWN_ISSUES.md.
W002 — async concurrency-eligibility warning (#841). async(e) is only made concurrent when e's effect row stays within the commutative whitelist ({Http} in v1; the Async marker itself has no operations and cannot order anything). For any other row the checker now says so — async(IO.print(...)) warns that it evaluates eagerly at the async() site — instead of letting a program imply concurrency it does not get. The rule resolves effect-op calls to their parent effect and function calls to their declared rows, recursively, and treats anything unresolvable as conservatively non-commutative. Mutation-validated four ways (rule deleted, whitelist over-permissive, whitelist over-firing, fn-call rows ignored — each flips exactly its discriminating tests RED).
Changed
Split tests/test_checker.py into eight phase-focused test files (#420). The monolithic 6,752-line, 60-class checker test file is replaced by eight themed files — test_checker_types.py, test_checker_patterns.py, test_checker_functions.py, test_checker_effects.py, test_checker_modules.py, test_checker_errors.py, test_checker_builtins_collections.py, test_checker_builtins_strings.py — each under 1,200 lines, with the shared header (the _check / _errors / _warnings / _check_ok / _check_clean / _check_err helpers and the EXAMPLES_DIR / EXAMPLE_FILES / CLEAN_EXAMPLES / WARN_EXAMPLES constants) extracted to a new tests/checker_helpers.py imported by all eight (matching the repo's existing from tests.<module> import precedent). Mechanical and behaviour-preserving: all 572 tests are carried over unchanged and each class moves whole; no test is added, removed, or modified. (Companion to the #419test_codegen.py split.)
Split tests/test_verifier.py into nine theme-focused test files (#839). The 9,356-line, 38-class verifier test file — the largest remaining after the #419 split, and the verifier/SMT oracle for the mutation sweep — is replaced by nine theme files (test_verifier_contracts.py, _nat_obligations, _primitive_ops, _calls_modules, _adt_decreases, _refinements, _shadow_audits, _mutation_obligations, _mutation_gates_smt), each under 1,500 lines, alongside the pre-existing test_verifier_coverage.py (untouched). The shared harness — the _verify / _verify_ok / _verify_err / _verify_warn / _nat_sub_status helpers plus the EXAMPLES_DIR / ALL_EXAMPLES corpus constants and the _MK source template — moves to a new tests/verifier_helpers.py imported per file. Mechanical and behaviour-preserving: all 474 tests are carried over unchanged, every class / helper / constant moves byte-for-byte (46/46-block differential against the pre-split file), and the [tool.mutmut] oracle selection tracks the new files. The issue's 8-file plan became nine under the 1,500-line ceiling (the #746 refinement-predicate class alone is ~1,300 lines, and the #387 hardening battery split in two). Completes the oversized-test-oracle split program (#420, #419, #839).
Split tests/test_codegen.py into twenty-one feature-focused test files (#419). The monolithic 21,225-line, 161-class codegen test file — the largest file in the tree, and the codegen oracle for the mutation sweep — is replaced by twenty-one feature files (test_codegen_expressions.py, _calls, _infrastructure, _interpolation, _effects, _data_types, _arrays, _refinements, _strings, _string_builtins, _numeric, _io, _collections, _json, _decimal, _host_effects, _nat_guards, _translator_fixes, _gc_alloc, _gc_rooting, _gc_reclamation), each under 1,500 lines (the issue's acceptance criterion), alongside the six pre-existing test_codegen_* modules. The shared harness — the eleven _compile* / _run* / WAT-and-GC assertion helpers (four of which lived interspersed between classes) plus the _IO_PRELUDE / _INLINE_BUILTIN_NAMES fixture constants — moves to a new tests/codegen_helpers.py imported per file. Mechanical and behaviour-preserving: all 1,219 tests (including the 10 stress-marked) are carried over unchanged and every class, helper, and constant moves byte-for-byte; per-file import blocks are computed from actual usage, and the [tool.mutmut] oracle selection tracks the new files. The issue's original 9-file plan was drawn when the file was 10,019 lines / 118 classes; at 21,225 / 161 the same theme boundaries yield twenty-one files. This closes out roadmap Tier 1 (safety net and runtime robustness). (Companion to the #420test_checker.py split.)
Consolidated the triplicated _resolved() helper in tests/test_checker_modules.py (#835). TestCrossModuleTyping, TestVisibilityEnforcement, and TestModuleCallParsed each carried their own @staticmethod _resolved() that builds a ResolvedModule from source text, and the TestModuleCallParsed copy had drifted (file_path=Path("/fake") vs the others' Path(f"/fake/{'/'.join(path)}.vera")). Replaced all three with a single module-level _resolved_module() called directly, unifying on the non-drifted file_path form. Follow-up to the #420 split, which had deliberately preserved the duplication byte-for-byte (unifying changes the file_path value, which flows into diagnostic location.file via vera/checker/modules.py); the 45 module tests are unaffected.