From 314d9fd75b347d6f909546605eba3c0bc3db6bf0 Mon Sep 17 00:00:00 2001 From: jasisz Date: Sat, 8 Aug 2026 02:40:54 +0200 Subject: [PATCH 1/2] Type a smart-constructor call over an all-literal in-range list as total MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A call to a recognized `List` refinement's smart constructor whose single argument is a syntactic list of integer literals, each inside the interval the refinement itself proves, cannot reach the constructor's error branch, so it types as the refined type and lowers to the carrier construction on every backend: `Bytes.fromList([0, 10, 255]) : Bytes`, no `?` and no `match`. Any other argument shape keeps `Result` unchanged — an identifier, a computed list, a computed element, an out-of-range or negative literal, or a magnitude beyond `i64`. The gate is derived, never named. A new analysis module builds it from two existing recognizers: the shape tier's `RefinementSmartConstructor` pattern supplies the carrier field and the validating predicate, and the packed layout's element-interval derivation (factored out for reuse) supplies the bound. Sharing the second step is what makes the rule safe on wasm-gc, where a packed carrier writes elements into a raw `i8` array with no range check: "the discharge admits it" and "the packed layout can store it" are now literally the same function. The table lives on the `SymbolTable`, the one place entry items and dependency modules are jointly in hand, so the typechecker and the HIR resolver read one table and cannot fork. Every callee spelling that denotes the constructor decides alike, because the wasm-gc backend flattens a dependency's constructor and all of its call sites — qualified and in-module — into one prefixed bare name before re-resolving. Lean re-establishes the gate's own claim as a `Subtype` obligation; since the predicate is compiled by well-founded recursion the tactic ladder gains a `simp []` rung named from the refinement's invariant. Dafny discharges the same fact as a subset-type constraint. A `Result` or `Option` constructor pattern whose subject is neither is now a type error, so the migration is loud rather than a match that silently walks off the end. Migrates the in-repo call sites, adds the diagnostic slugs and repair hints, and refuses discharged programs at the self-host boundary with an error naming the call sites, since the Aver-in-Aver resolver carries no refinement recognizer. Also migrates one literal-divisor leftover in the workflow-engine corpus that was failing thirteen units. Co-Authored-By: Claude Fable 5 --- docs/diagnostics-slugs.md | 2 + docs/language.md | 1 + docs/services.md | 15 +- projects/workflow_engine/domain/time.av | 24 +- src/analysis/literal_refinement.rs | 591 ++++++++++++++++++ src/analysis/mod.rs | 1 + src/ast/mod.rs | 44 ++ src/codegen/lean/expr.rs | 49 +- src/codegen/proof_lower/mod.rs | 2 +- src/codegen/proof_lower/packed_sequence.rs | 37 +- src/diagnostics/classify.rs | 24 + src/ir/hir/resolve.rs | 50 ++ src/ir/symbol_table.rs | 32 + src/main/commands.rs | 85 +++ src/main/replay_cmd/backends.rs | 11 + src/stdlib.rs | 8 +- src/types/checker/infer/expr.rs | 48 ++ src/types/checker/infer/patterns.rs | 21 + stdlib/bytes.av | 7 +- stdlib/crypto/digest32.av | 8 +- tests/cross_backend_stress.rs | 109 ++++ tests/fixtures/discharged_bytes_law.av | 43 ++ .../fixtures/discharged_bytes_long_literal.av | 24 + tests/proof_spec/builds.rs | 58 ++ tests/rust_codegen_differential.rs | 58 +- tests/typechecker_spec.rs | 192 +++++- tests/verify_tcp_bytes_given_stub.rs | 4 +- tests/wasip2_codegen_regression.rs | 2 +- tests/wasip2_tcp.rs | 12 +- tests/wasm_gc_codegen_regression.rs | 4 +- .../wasm_gc_effect_arg_overflow_regression.rs | 22 +- tests/wasm_gc_packed_sequence.rs | 180 +++++- tests/wasm_gc_spec.rs | 2 +- 33 files changed, 1694 insertions(+), 76 deletions(-) create mode 100644 src/analysis/literal_refinement.rs create mode 100644 tests/fixtures/discharged_bytes_law.av create mode 100644 tests/fixtures/discharged_bytes_long_literal.av diff --git a/docs/diagnostics-slugs.md b/docs/diagnostics-slugs.md index 2879a893c..d79b43aa4 100644 --- a/docs/diagnostics-slugs.md +++ b/docs/diagnostics-slugs.md @@ -22,6 +22,8 @@ Source of truth: `src/diagnostics/classify.rs` (classifier) and `src/checker/*.r | `arity-mismatch` | error | Function or constructor called with the wrong number of args. | Adjust the number of arguments. | | `effect-violation` | error | A function calls an effect it doesn't declare in `! [...]`. | Add the missing effect to the function's `! [...]`. | | `int-div` | error | The `/` operator was used on two `Int`s. Integer division is partial (the divisor may be zero → `Result.Err`), so it is a function, not an operator. | Use `Int.div(a, b) : Result`; handle with `match` or `Result.withDefault`. With a nonzero literal divisor, `Int.div(a, k)` is total and returns plain `Int`. | +| `error-prop-non-result` | error | `?` was applied to an expression that is not a `Result`. | Drop the `?`. A smart-constructor call over an all-literal list inside the refinement's proven element interval (`Bytes.fromList([0, 10, 255])`) is total and already returns the refined type. | +| `pattern-subject-mismatch` | error | A `Result` / `Option` constructor pattern was matched against a subject of some other type — no value can ever take the arm. | Match the value's own shape; a discharged literal smart-constructor call returns the refined type, not a `Result`. | ## Intent / verify hygiene diff --git a/docs/language.md b/docs/language.md index c5669778c..f4e6a6980 100644 --- a/docs/language.md +++ b/docs/language.md @@ -50,6 +50,7 @@ Duplicate binding of the same name in the same scope is a type error. Arithmetic: `+`, `-`, `*` — operands must match (`Int+Int`, `Float+Float`, `String+String`). No implicit promotion; use `Float.fromInt` / `Int.fromFloat` to convert. The `/` operator is **Float-only**; integer `/` is a type error. For integers use `Int.div(a, b) : Result` (Euclidean; `b == 0` → `Result.Err`) and `Int.mod(a, b) : Result` — there is no integer `%`. `Int` is arbitrary-precision (ℤ): no overflow, no wraparound. Literal-divisor discharge: when the divisor of `Int.div` / `Int.mod` is a syntactic nonzero integer literal — `Int.div(x, 2)`, `Int.mod(x, -3)` — the call cannot fail, so it types as plain `Int` and every backend emits the division directly (no `Result`, no unwrapping). The boundary is exactly "a syntactic integer literal other than `0`, optionally under one unary minus": a `0` literal, an identifier, a named constant, or a constant expression like `8 + 8` all keep the `Result` type unchanged. Parentheses are transparent here, because the parser erases them around a single expression: `(16)`, `(-16)` and `-(16)` are the same syntax tree as `16` and `-16`, so all three discharge — while `(0)` is still zero and `(k)` is still an identifier, and both keep the `Result` type. This is a typing rule for these two functions only, not a general constant-propagation or refinement mechanism. +Literal smart-constructor discharge: the same idea extends to a validating smart constructor over a `List` carrier — the shape `stdlib/bytes.av` uses. When the argument is a syntactic list of integer literals and every element is inside the interval the refinement itself proves, the call cannot reach its `Result.Err` branch, so it types as the refined type and constructs the value directly: `Bytes.fromList([0, 10, 255]) : Bytes`, no `?` and no `match`. The empty list `Bytes.fromList([])` discharges too. The boundary is narrow and entirely syntactic on the argument side: there must be exactly one argument, it must be a list literal written out at the call site, and every element must be a plain integer literal with at most one unary minus. Every spelling that denotes the constructor decides the same way — `Bytes.fromList(...)` from outside and a bare `fromList(...)` inside the defining module alike. Everything else keeps `Result` unchanged — an identifier (`Bytes.fromList(values)`), a computed list (`Bytes.fromList(List.concat(a, b))`), a computed element (`Bytes.fromList([n * 2])`), an out-of-range literal (`Bytes.fromList([65, 256])`), a negative one (`Bytes.fromList([-1])`), or a literal beyond `i64`. The bound is never hardcoded: it is read off the refinement's own validating predicate, so a user-defined refinement with a different range discharges against that range, and a record with no smart constructor never discharges at all. Programs run under `--self-host` are refused with an explicit error when they contain a discharged call, because the self-hosted resolver does not yet carry the rule. Unary minus negates a numeric expression: `-n` (equivalent to `0 - n`), and numeric literals may be written negative (`-3`, `-1.5`). Comparison: `==`, `!=`, `<`, `>`, `<=`, `>=`. Error propagation: `expr?` — unwraps `Result.Ok`, propagates `Result.Err` as a `RuntimeError`. diff --git a/docs/services.md b/docs/services.md index c70a26d64..76cdf8728 100644 --- a/docs/services.md +++ b/docs/services.md @@ -24,9 +24,22 @@ requiring exactly 32 bytes. Both remain ordinary Aver types and retain their invariants in Lean and Dafny proof export. +`Bytes.fromList` written against a list literal whose every element is an +integer literal in `0..=255` cannot fail, so it types as plain `Bytes` — no +`?`, no `match`: + +```aver +payload = Bytes.fromList([249, 190, 180, 217]) -- : Bytes +Tcp.sendBytes("127.0.0.1", 9, payload) +``` + +Anything else keeps `Result`: a variable, a computed list, a +computed element, or a literal outside `0..=255`. See +[language.md](language.md#operators) for the exact boundary. + | Function | Signature | Notes | |---|---|---| -| `Bytes.fromList` | `List -> Result` | Validates every octet; `Result.Err` names the offending value and its index | +| `Bytes.fromList` | `List -> Result` | Validates every octet; `Result.Err` names the offending value and its index. An all-literal in-range list argument discharges to plain `Bytes` — see below | | `Bytes.toList` | `Bytes -> List` | Exposes validated values | | `Bytes.fromHex` | `String -> Result` | Even length, case-insensitive, no `0x` prefix | | `Bytes.toHex` | `Bytes -> String` | Total, lowercase output | diff --git a/projects/workflow_engine/domain/time.av b/projects/workflow_engine/domain/time.av index a5bc99825..86aa08527 100644 --- a/projects/workflow_engine/domain/time.av +++ b/projects/workflow_engine/domain/time.av @@ -58,23 +58,11 @@ verify parseSlice fn isLeapYear(year: Int) -> Bool ? "Gregorian leap year rule." - match Int.mod(year, 400) - Result.Ok(rem400) -> match rem400 == 0 - true -> true - false -> match Int.mod(year, 100) - Result.Ok(rem100) -> match rem100 == 0 - true -> false - false -> match Int.mod(year, 4) - Result.Ok(rem4) -> rem4 == 0 - _ -> false - _ -> false - _ -> match Int.mod(year, 100) - Result.Ok(rem100) -> match rem100 == 0 - true -> false - false -> match Int.mod(year, 4) - Result.Ok(rem4) -> rem4 == 0 - _ -> false - _ -> false + match Int.mod(year, 400) == 0 + true -> true + false -> match Int.mod(year, 100) == 0 + true -> false + false -> Int.mod(year, 4) == 0 verify isLeapYear isLeapYear(2024) => true @@ -190,7 +178,7 @@ verify parseIsoKnownShape fn leapYearsBefore(year: Int) -> Int ? "Number of leap years before January 1 of the given year." prev = year - 1 - Result.withDefault(Int.div(prev, 4), 0) - Result.withDefault(Int.div(prev, 100), 0) + Result.withDefault(Int.div(prev, 400), 0) + Int.div(prev, 4) - Int.div(prev, 100) + Int.div(prev, 400) verify leapYearsBefore leapYearsBefore(1) => 0 diff --git a/src/analysis/literal_refinement.rs b/src/analysis/literal_refinement.rs new file mode 100644 index 000000000..b343e22b3 --- /dev/null +++ b/src/analysis/literal_refinement.rs @@ -0,0 +1,591 @@ +//! Derived gate for the literal smart-constructor discharge. +//! +//! A call to a recognized `List` refinement's smart constructor whose +//! single argument is a syntactic list of integer literals, every one of +//! them inside the refinement's OWN proven element interval, cannot fail: +//! the constructor's validating predicate is decided at compile time. Such +//! a call therefore types as the refined type itself instead of +//! `Result`, and lowers straight to the carrier construction. +//! +//! ```text +//! Bytes.fromList([1, 2, 3]) : Bytes (discharged) +//! Bytes.fromList([1, 256]) : Result (out of interval) +//! Bytes.fromList(values) : Result (not a literal list) +//! ``` +//! +//! # The gate is derived, never named +//! +//! Nothing here mentions `Bytes`, `fromList`, or `0..=255`. The table is +//! built from two existing recognizers: +//! +//! * [`crate::analysis::shape::detect_module_patterns`] finds every +//! `RefinementSmartConstructor` — the single-field record plus its +//! validating `match pred(x) { true -> Ok(T(f = x)); false -> Err(…) }` +//! constructor — and hands back the carrier field and the predicate AST. +//! * `packed_sequence::element_interval_from_predicate` turns that +//! predicate into the per-element interval, via the same recursive-`all` +//! recognizer and the same [`crate::ir::interval::interval_of_invariant`] +//! engine the wasm-gc packed layout is derived from. +//! +//! Sharing the second step is what makes the discharge safe on wasm-gc: a +//! packed carrier stores its elements in a raw `i8`/`i16` array with no +//! range check, so "the discharge admits it" and "the packed layout can +//! store it" MUST be the same predicate. They are — literally the same +//! function. +//! +//! # Boundary +//! +//! * Every callee spelling that DENOTES the recognized constructor decides +//! the same way — qualified (`Bytes.fromList(…)`) and bare in-module +//! (`fromList(…)` inside `stdlib/bytes.av` itself) alike. Spelling +//! insensitivity is not a convenience: the wasm-gc backend re-resolves a +//! FLATTENED compile unit in which `flatten_multimodule` has renamed a +//! dependency's `fromList` to the entry-scope `Dep_fromList` and +//! rewritten BOTH the qualified and the in-module call sites to that one +//! bare name. After the flatten the two spellings are indistinguishable, +//! so a spelling-sensitive rule would discharge before it and not after +//! — the checked/unchecked fork this rule must not create. A bare +//! spelling shared by two recognized constructors is fail-closed: it +//! denotes neither. +//! * Exactly one argument, and it must be a syntactic list literal whose +//! every element is a plain integer literal with at most one unary minus +//! (`crate::ast::literal_int_list_elements`). An identifier, a call, a +//! `BigInt` literal, or any computed list declines. +//! * Every element must be inside the derived interval. `[65, 256]` +//! declines against `[0, 255]`. +//! * An EMPTY list literal discharges: every element is in range +//! vacuously, and the constructor's predicate is `true` on `[]` by the +//! recognized shape's own base case. + +use std::collections::HashSet; + +use crate::analysis::shape::{ModulePattern, detect_module_patterns}; +use crate::ast::{Expr, FnDef, Spanned, TopLevel}; +use crate::codegen::ModuleInfo; +use crate::ir::SymbolTable; +use crate::ir::interval::Interval; + +/// One recognized smart constructor over a `List` carrier whose +/// element interval the refinement itself proves. +#[derive(Debug, Clone, PartialEq)] +pub struct ListRefinementCtor { + /// Dependency-module prefix that owns the refinement (`"Bytes"`), or + /// `None` when the refinement is declared in the entry file. + pub scope: Option, + /// Bare source name of the refined record (`"Bytes"`). + pub type_name: String, + /// The record's single carrier field (`"values"`). + pub carrier_field: String, + /// Bare source name of the smart constructor (`"fromList"`). + pub constructor_fn: String, + /// Interval proven for EVERY element of the carrier list. + pub element_interval: Interval, +} + +/// Every literal-dischargeable smart constructor in one compilation, +/// addressed by the qualified callee spelling a call site writes. +#[derive(Debug, Clone, Default)] +pub struct LiteralRefinementTable { + ctors: Vec, + /// Prefix an entry-scope refinement is addressable under, taken from + /// the entry file's own `module X` declaration. Aver lets a module + /// spell its own members qualified, so `X.fromList([…])` in an entry + /// file that declares `module X` reaches the same constructor. + entry_prefix: Option, +} + +impl LiteralRefinementTable { + /// Recognize every dischargeable constructor across the entry file and + /// its dependency modules. Unrecognized predicate shapes, non-`List` + /// carriers, and open or non-`i64` intervals are all omitted — the table + /// is fail-closed, and an absent entry simply keeps the `Result` path. + pub fn build( + entry_items: &[TopLevel], + dep_modules: &[ModuleInfo], + symbols: &SymbolTable, + ) -> Self { + // Cheap pre-filter: the rule can only ever fire for a + // single-field product whose carrier is `List`. Programs + // without one — the overwhelming majority — skip the pattern + // detection entirely. + let has_candidate_carrier = entry_items + .iter() + .filter_map(|item| match item { + TopLevel::TypeDef(td) => Some(td), + _ => None, + }) + .chain(dep_modules.iter().flat_map(|m| m.type_defs.iter())) + .any(is_int_list_carrier_product); + if !has_candidate_carrier { + return Self::default(); + } + + let entry_fns: Vec<&FnDef> = entry_items + .iter() + .filter_map(|item| match item { + TopLevel::FnDef(fd) => Some(fd), + _ => None, + }) + .filter(|fd| crate::codegen::common::is_pure_fn(fd)) + .collect(); + + // A bare record name declared in more than one scope would make the + // per-scope lookup ambiguous downstream; the packed-layout table + // declines those, so decline them here too. + let mut seen: HashSet<(Option, String)> = HashSet::new(); + let mut ctors = Vec::new(); + for pattern in detect_module_patterns(entry_items, dep_modules) { + let ModulePattern::RefinementSmartConstructor { + scope, + type_name, + carrier_field, + carrier_type, + constructor_fn, + param_name, + predicate, + } = pattern + else { + continue; + }; + if !is_int_list(&carrier_type) { + continue; + } + let scope_fns: Vec<&FnDef> = match scope.as_deref() { + None => entry_fns.clone(), + Some(prefix) => dep_modules + .iter() + .filter(|m| m.prefix == prefix) + .flat_map(|m| m.fn_defs.iter()) + .filter(|fd| crate::codegen::common::is_pure_fn(fd)) + .collect(), + }; + let resolve = |expr: &Spanned| { + let mut rctx = crate::ir::hir::ResolveCtx::new(symbols); + rctx.current_module = scope.clone(); + let stmt = crate::ast::Stmt::Expr(expr.clone()); + match crate::ir::hir::resolve::resolve_stmt_external(&rctx, &stmt) { + crate::ir::hir::ResolvedStmt::Expr(s) => s, + crate::ir::hir::ResolvedStmt::Binding { value, .. } => value, + } + }; + let Some(element_interval) = + crate::codegen::proof_lower::packed_sequence::element_interval_from_predicate( + &predicate, + ¶m_name, + &scope_fns, + &resolve, + ) + else { + continue; + }; + if !seen.insert((scope.clone(), type_name.clone())) { + continue; + } + ctors.push(ListRefinementCtor { + scope, + type_name, + carrier_field, + constructor_fn, + element_interval, + }); + } + + let entry_prefix = entry_items.iter().find_map(|item| match item { + TopLevel::Module(m) => Some(m.name.clone()), + _ => None, + }); + + Self { + ctors, + entry_prefix, + } + } + + /// `true` when nothing in this program is dischargeable — lets callers + /// skip the per-call-site work entirely. + pub fn is_empty(&self) -> bool { + self.ctors.is_empty() + } + + /// Decide the discharge for one call site. + /// + /// `callee` is the dotted spelling the source wrote — qualified + /// (`"Bytes.fromList"`) or bare (`"fromList"` from inside the owning + /// module). Returns the constructor whose refined type the call now + /// produces, or `None` to keep the declared `Result` signature. + /// + /// Every spelling that DENOTES the recognized constructor decides the + /// same way, deliberately: the wasm-gc backend flattens a dependency's + /// `fromList` and every one of its call sites — qualified and + /// in-module alike — into a single bare `Dep_fromList` before + /// re-resolving, so a spelling-sensitive rule would discharge before + /// the flatten and not after. + pub fn discharge(&self, callee: &str, args: &[Spanned]) -> Option<&ListRefinementCtor> { + if args.len() != 1 { + return None; + } + let ctor = self.resolve_ctor(callee)?; + let elements = crate::ast::literal_int_list_elements(&args[0])?; + elements + .iter() + .all(|k| ctor.element_interval.contains_point(*k)) + .then_some(ctor) + } + + /// Which recognized constructor a callee spelling denotes, if any. + /// Fail-closed on ambiguity: when two refinements in the program share + /// a bare constructor name, a bare call site denotes neither. + fn resolve_ctor(&self, callee: &str) -> Option<&ListRefinementCtor> { + // Qualified spelling: `.`, or `.` for a refinement declared in the entry file. + if let Some((prefix, fn_name)) = callee.rsplit_once('.') + && let Some(ctor) = self.ctors.iter().find(|c| { + c.constructor_fn == fn_name + && match c.scope.as_deref() { + Some(scope) => scope == prefix, + None => self.entry_prefix.as_deref() == Some(prefix), + } + }) + { + return Some(ctor); + } + // Bare spelling: an in-module call, or a post-flatten call to the + // prefixed name flatten gave the dependency's function. + let mut matches = self.ctors.iter().filter(|c| c.constructor_fn == callee); + let first = matches.next()?; + matches.next().is_none().then_some(first) + } +} + +/// Every call site in `items` the discharge rewrites, as +/// `(line, qualified callee)`, in source order. +/// +/// Exists for the self-host boundary: the Aver-in-Aver resolver has no +/// refinement recognizer, so a discharged program would build a guest +/// `Result` where the host typechecker produced the refined type. That +/// divergence is SILENT (the guest fails much later, or not at all), so +/// the self-host driver refuses such a program up front and points at +/// the exact call sites. +pub fn discharge_sites(table: &LiteralRefinementTable, items: &[TopLevel]) -> Vec<(usize, String)> { + let mut out = Vec::new(); + if table.is_empty() { + return out; + } + for item in items { + match item { + TopLevel::FnDef(fd) => { + for stmt in fd.body.stmts() { + let (crate::ast::Stmt::Binding(_, _, e) | crate::ast::Stmt::Expr(e)) = stmt; + walk(table, e, &mut out); + } + } + TopLevel::Stmt(crate::ast::Stmt::Binding(_, _, e)) + | TopLevel::Stmt(crate::ast::Stmt::Expr(e)) => walk(table, e, &mut out), + TopLevel::Verify(block) => { + for (left, right) in &block.cases { + walk(table, left, &mut out); + walk(table, right, &mut out); + } + } + TopLevel::Module(_) | TopLevel::Decision(_) | TopLevel::TypeDef(_) => {} + } + } + out.sort_by_key(|(line, _)| *line); + out +} + +/// Exhaustive `Expr` walk. Deliberately has NO catch-all arm: a new +/// expression form must be classified here explicitly, or the self-host +/// rejection could silently miss a discharged call nested inside it. +fn walk(table: &LiteralRefinementTable, expr: &Spanned, out: &mut Vec<(usize, String)>) { + match &expr.node { + Expr::FnCall(callee, args) => { + if let Some(dotted) = crate::codegen::common::expr_to_dotted_name(&callee.node) + && table.discharge(&dotted, args).is_some() + { + out.push((expr.line, dotted)); + } + walk(table, callee, out); + for a in args { + walk(table, a, out); + } + } + Expr::Attr(obj, _) => walk(table, obj, out), + Expr::BinOp(_, l, r) => { + walk(table, l, out); + walk(table, r, out); + } + Expr::Neg(inner) | Expr::ErrorProp(inner) | Expr::Constructor(_, Some(inner)) => { + walk(table, inner, out) + } + Expr::Match { subject, arms } => { + walk(table, subject, out); + for arm in arms { + walk(table, &arm.body, out); + } + } + Expr::InterpolatedStr(parts) => { + for part in parts { + if let crate::ast::StrPart::Parsed(inner) = part { + walk(table, inner, out); + } + } + } + Expr::List(items) | Expr::Tuple(items) | Expr::IndependentProduct(items, _) => { + for item in items { + walk(table, item, out); + } + } + Expr::MapLiteral(pairs) => { + for (k, v) in pairs { + walk(table, k, out); + walk(table, v, out); + } + } + Expr::RecordCreate { fields, .. } => { + for (_, value) in fields { + walk(table, value, out); + } + } + Expr::RecordUpdate { base, updates, .. } => { + walk(table, base, out); + for (_, value) in updates { + walk(table, value, out); + } + } + Expr::TailCall(data) => { + for a in &data.args { + walk(table, a, out); + } + } + Expr::Literal(_) | Expr::Ident(_) | Expr::Constructor(_, None) | Expr::Resolved { .. } => {} + } +} + +fn is_int_list(annotation: &str) -> bool { + matches!( + crate::types::parse_type_str(annotation), + crate::ast::Type::List(inner) if *inner == crate::ast::Type::Int + ) +} + +fn is_int_list_carrier_product(td: &crate::ast::TypeDef) -> bool { + matches!( + td, + crate::ast::TypeDef::Product { fields, .. } + if fields.len() == 1 && is_int_list(&fields[0].1) + ) +} + +#[cfg(test)] +mod tests { + use super::*; + + fn table_for(entry: &str, dep: Option<(&str, &str)>) -> LiteralRefinementTable { + let parse = |src: &str| { + let mut lexer = crate::lexer::Lexer::new(src); + let tokens = lexer.tokenize().expect("lex"); + crate::parser::Parser::new(tokens).parse().expect("parse") + }; + let entry_items = parse(entry); + let dep_modules: Vec = dep + .map(|(prefix, src)| { + let items = parse(src); + vec![ModuleInfo { + prefix: prefix.to_string(), + depends: Vec::new(), + type_defs: items + .iter() + .filter_map(|i| match i { + TopLevel::TypeDef(td) => Some(td.clone()), + _ => None, + }) + .collect(), + fn_defs: items + .iter() + .filter_map(|i| match i { + TopLevel::FnDef(fd) => Some(fd.clone()), + _ => None, + }) + .collect(), + verify_laws: Vec::new(), + analysis: None, + }] + }) + .unwrap_or_default(); + let symbols = SymbolTable::build(&entry_items, &dep_modules); + LiteralRefinementTable::build(&entry_items, &dep_modules, &symbols) + } + + const OCTETS: &str = r#" +module Octets + intent = "structural refinement with no standard-library name in sight" + exposes [fromList] + exposes opaque [Octets] + effects [] + +record Octets + values: List + +fn allInRange(xs: List) -> Bool + match xs + [] -> true + [head, ..tail] -> match Bool.and(head >= 0, head <= 255) + true -> allInRange(tail) + false -> false + +fn fromList(xs: List) -> Result + match allInRange(xs) + true -> Result.Ok(Octets(values = xs)) + false -> Result.Err("oob") +"#; + + const CONSUMER: &str = r#" +module Consumer + intent = "calls the refinement's smart constructor" + depends [Octets] + exposes [go] + effects [] + +fn go() -> Int + 1 +"#; + + fn list(src: &str) -> Spanned { + let mut lexer = crate::lexer::Lexer::new(src); + let tokens = lexer.tokenize().expect("lex"); + let items = crate::parser::Parser::new(tokens).parse().expect("parse"); + match items.into_iter().next() { + Some(TopLevel::Stmt(crate::ast::Stmt::Expr(e))) => e, + other => panic!("expected an expression, got {other:?}"), + } + } + + #[test] + fn derives_the_element_interval_without_naming_the_refinement() { + let table = table_for(CONSUMER, Some(("Octets", OCTETS))); + assert_eq!( + table.ctors, + vec![ListRefinementCtor { + scope: Some("Octets".to_string()), + type_name: "Octets".to_string(), + carrier_field: "values".to_string(), + constructor_fn: "fromList".to_string(), + element_interval: Interval::between(0, 255), + }] + ); + } + + #[test] + fn derives_the_element_interval_for_the_real_standard_library_bytes_module() { + let table = table_for( + CONSUMER, + Some(("Bytes", include_str!("../../stdlib/bytes.av"))), + ); + assert_eq!( + table + .ctors + .iter() + .find(|c| c.type_name == "Bytes") + .map(|c| c.element_interval), + Some(Interval::between(0, 255)) + ); + } + + #[test] + fn discharges_only_all_literal_in_interval_lists() { + let table = table_for(CONSUMER, Some(("Octets", OCTETS))); + let discharges = |src: &str| table.discharge("Octets.fromList", &[list(src)]).is_some(); + + assert!(discharges("[1, 2, 3]")); + assert!(discharges("[]")); + assert!(discharges("[0, 255]")); + // Out of the DERIVED interval, not a hardcoded range. + assert!(!discharges("[65, 256]")); + assert!(!discharges("[-1]")); + // Beyond i64 — the syntactic predicate declines BigInt outright. + assert!(!discharges("[65, 1208925819614629174706176]")); + // Not a syntactic list of literals. + assert!(!discharges("values")); + assert!(!discharges("[double(0)]")); + assert!(!discharges("List.concat([1], [2])")); + } + + #[test] + fn accepts_every_spelling_that_denotes_the_constructor() { + let table = table_for(CONSUMER, Some(("Octets", OCTETS))); + // Qualified, and the bare in-module / post-flatten spelling. + assert!( + table + .discharge("Octets.fromList", &[list("[1, 2]")]) + .is_some() + ); + assert!(table.discharge("fromList", &[list("[1, 2]")]).is_some()); + // A different module's same-named function denotes nothing here. + assert!( + table + .discharge("Tree.fromList", &[list("[1, 2]")]) + .is_none() + ); + assert!(table.discharge("toList", &[list("[1, 2]")]).is_none()); + } + + #[test] + fn a_bare_spelling_shared_by_two_refinements_is_fail_closed() { + // Two recognized constructors with the same bare name: the + // qualified spellings still decide, the bare one denotes neither. + let second = r#" +record Nibbles + values: List + +fn inNibbleRange(xs: List) -> Bool + match xs + [] -> true + [head, ..tail] -> match Bool.and(head >= 0, head <= 15) + true -> inNibbleRange(tail) + false -> false + +fn fromList(xs: List) -> Result + match inNibbleRange(xs) + true -> Result.Ok(Nibbles(values = xs)) + false -> Result.Err("oob") +"#; + let dep = format!("{OCTETS}{second}"); + let table = table_for(CONSUMER, Some(("Octets", &dep))); + assert_eq!(table.ctors.len(), 2, "expected two recognized constructors"); + assert!(table.discharge("fromList", &[list("[1, 2]")]).is_none()); + assert!( + table + .discharge("Octets.fromList", &[list("[1, 2]")]) + .is_some() + ); + } + + #[test] + fn declines_a_record_with_no_smart_constructor() { + let src = r#" +module Local + intent = "a bare record that never validates anything" + effects [] + +record Octets + values: List + +fn go() -> Int + 1 +"#; + let table = table_for(src, None); + assert!(table.is_empty()); + } + + #[test] + fn addresses_an_entry_scope_refinement_through_the_entry_module_prefix() { + let table = table_for(OCTETS, None); + assert!(table.discharge("Octets.fromList", &[list("[7]")]).is_some()); + assert!( + table + .discharge("Octets.fromList", &[list("[700]")]) + .is_none() + ); + } +} diff --git a/src/analysis/mod.rs b/src/analysis/mod.rs index 7b989e34a..63563a78e 100644 --- a/src/analysis/mod.rs +++ b/src/analysis/mod.rs @@ -13,4 +13,5 @@ //! See issue #232 (0.23 "Shape") for the architectural plan and the //! peer-review notes that produced this split. +pub mod literal_refinement; pub mod shape; diff --git a/src/ast/mod.rs b/src/ast/mod.rs index df3df4dfa..2966072e0 100644 --- a/src/ast/mod.rs +++ b/src/ast/mod.rs @@ -135,6 +135,50 @@ pub fn is_literal_nonzero_int_divisor(expr: &Spanned) -> bool { } } +/// Syntactic value of an integer literal, allowing at most ONE unary minus: +/// `7` → `Some(7)`, `-7` → `Some(-7)`, `--7` / `x` / `3 + 4` → `None`. +/// A `BigInt` literal (magnitude beyond `i64`) declines by construction — +/// every interval a refinement can prove fits `i64`, so a magnitude that +/// overflows it can never be inside one, and declining keeps the predicate +/// fail-closed rather than making it depend on bignum parsing. +pub fn single_negation_int_literal(expr: &Spanned) -> Option { + fn plain(node: &Expr) -> Option { + match node { + Expr::Literal(Literal::Int(k)) => Some(*k as i128), + _ => None, + } + } + match &expr.node { + Expr::Neg(inner) => plain(&inner.node).map(|k| -k), + node => plain(node), + } +} + +/// Literal-list discharge predicate, shared by the typechecker and the HIR +/// resolver: the SYNTACTIC half of the "all-literal list argument" rule. +/// Returns the element values exactly when `expr` is a syntactic list +/// literal (`[…]`) whose every element is a plain integer literal with at +/// most one unary minus. An empty list literal returns an empty vector — it +/// satisfies any element-wise bound vacuously. +/// +/// Declines for every other argument shape: an identifier, a call, a +/// `List.concat` / spread, an interpolated element, a `BigInt` literal, a +/// double negation. The boundary is deliberately syntactic and this +/// function is deliberately blind to WHICH refinement is being constructed +/// — the element bound comes from the derived refinement interval +/// (`crate::analysis::literal_refinement`), never from a hardcoded range. +/// +/// Both consumers MUST share this one predicate. Real pipelines resolve +/// without typechecking (`tests/eval_spec.rs` compiles straight from the +/// resolver), so the HIR rewrite cannot key on type stamps — a stamp-keyed +/// rewrite would fork semantics between checked and unchecked pipelines. +pub fn literal_int_list_elements(expr: &Spanned) -> Option> { + let Expr::List(items) = &expr.node else { + return None; + }; + items.iter().map(single_negation_int_literal).collect() +} + #[derive(Debug, Clone, Copy, PartialEq)] pub enum BinOp { Add, diff --git a/src/codegen/lean/expr.rs b/src/codegen/lean/expr.rs index 910d4a898..61834bc77 100644 --- a/src/codegen/lean/expr.rs +++ b/src/codegen/lean/expr.rs @@ -185,14 +185,31 @@ pub fn emit_expr(expr: &Spanned, ctx: &CodegenContext) -> String { // structure shape and a plain `{ value := … }` record // literal, so this fast-path is gated on the carrier // matching. - if crate::codegen::common::find_refined_type(ctx, type_name).is_some() + // * for a structural carrier the predicate is a + // recursive helper compiled by well-founded + // recursion, which `decide` cannot evaluate through + // the elaborator (see `crypto_model.lean`). Those + // goals need the helper's equation lemmas, so a + // final `simp []` rung is appended when + // the invariant's head is a nameable function — the + // name is read off the refinement's own invariant, + // never hardcoded. This is the rung that closes the + // literal smart-constructor discharge + // (`Bytes.fromList([0, 10, 255])` → `⟨[0, 10, 255], + // by … simp [Bytes.allInRange]⟩`): the emitted proof + // re-establishes, in Lean, exactly the fact the + // discharge gate claimed. + if let Some(decl) = crate::codegen::common::find_refined_type(ctx, type_name) && fields.len() == 1 { let (_, value_expr) = &fields[0]; let value_str = emit_expr(value_expr, ctx); - return format!( - "⟨{value_str}, by first | omega | decide | (simp_all; omega) | assumption⟩" - ); + let mut ladder = + "first | omega | decide | (simp_all; omega) | assumption".to_string(); + if let Some(predicate) = invariant_head_name(&decl.invariant.expr, ctx) { + ladder.push_str(&format!(" | simp [{predicate}]")); + } + return format!("⟨{value_str}, by {ladder}⟩"); } let parts: Vec = fields .iter() @@ -289,6 +306,30 @@ fn escape_lean_string(s: &str) -> String { crate::codegen::common::escape_string_literal(s) } +/// Lean name of the function a refinement's invariant applies, when the +/// invariant is a single call (`allInRange xs`). Used to give the +/// Subtype-construction tactic ladder an unfolding rung for predicates +/// the elaborator cannot evaluate — structural helpers compiled by +/// well-founded recursion. A non-call invariant (a bare comparison such +/// as `n >= 0`) has no name to unfold and returns `None`; those goals +/// are already closed by `omega` / `decide`. +fn invariant_head_name(invariant: &Spanned, ctx: &CodegenContext) -> Option { + // Only a USER function has equation lemmas worth unfolding; a builtin + // head (`Bool.and`, a comparison) is already in `simp`'s reach and + // rendering one here would need its arguments anyway. + let ResolvedExpr::Call(ResolvedCallee::Fn(fn_id), _) = &invariant.node else { + return None; + }; + let entry = ctx.symbol_table.fn_entry(*fn_id); + let bare = aver_name_to_lean(entry.key.name.as_str()); + Some(match entry.key.scope_str() { + Some(prefix) if !ctx.modules.is_empty() => { + format!("{}.{}", super::syntax::aver_path_to_lean(prefix), bare) + } + _ => bare, + }) +} + fn emit_fn_call( callee: &ResolvedCallee, args: &[Spanned], diff --git a/src/codegen/proof_lower/mod.rs b/src/codegen/proof_lower/mod.rs index 099575a7d..54fab64d8 100644 --- a/src/codegen/proof_lower/mod.rs +++ b/src/codegen/proof_lower/mod.rs @@ -2868,7 +2868,7 @@ mod induction; mod inequality; mod int_decimal_roundtrip; mod map_laws; -mod packed_sequence; +pub(crate) mod packed_sequence; mod refinement; mod ring; mod simp; diff --git a/src/codegen/proof_lower/packed_sequence.rs b/src/codegen/proof_lower/packed_sequence.rs index e659ca414..b631a0a02 100644 --- a/src/codegen/proof_lower/packed_sequence.rs +++ b/src/codegen/proof_lower/packed_sequence.rs @@ -147,18 +147,43 @@ fn element_interval_from_refinement( inputs: &ProofLowerInputs<'_>, scope: Option<&str>, ) -> Option { - let (predicate_fn, predicate_args) = call_target_and_args(&info.predicate.node)?; - if predicate_args.len() != 1 || !expr_is_ident(&predicate_args[0], info.param_name) { + element_interval_from_predicate( + info.predicate, + info.param_name, + &inputs.pure_fns_in_scope(scope), + &|expr| inputs.resolve_expr(expr, scope), + ) +} + +/// Derive the per-element interval of a canonical `List` refinement +/// from the smart constructor's predicate call, the same-scope function +/// pool, and a resolver for the per-element predicate expression. +/// +/// Split out of [`element_interval_from_refinement`] so the analysis tier +/// (`crate::analysis::literal_refinement`, which drives the literal +/// discharge in the typechecker and the HIR resolver) derives the element +/// bound through the SAME recognizer the packed layout uses, instead of +/// re-deriving — or worse, hardcoding — a range. Both callers therefore +/// agree by construction: a value the discharge admits is a value the +/// packed layout can store. +pub(crate) fn element_interval_from_predicate( + predicate: &Spanned, + param_name: &str, + scope_fns: &[&FnDef], + resolve: &dyn Fn(&Spanned) -> Spanned, +) -> Option { + let (predicate_fn, predicate_args) = call_target_and_args(&predicate.node)?; + if predicate_args.len() != 1 || !expr_is_ident(&predicate_args[0], param_name) { return None; } - let helper = inputs - .pure_fns_in_scope(scope) - .into_iter() + let helper = scope_fns + .iter() + .copied() .find(|fd| same_callee_name(&fd.name, &predicate_fn))?; recursive_list_element_predicate(helper).and_then(|(element_name, element_predicate)| { let predicate = Predicate { free_vars: vec![(element_name, QuantifierType::Plain("Int".to_string()))], - expr: inputs.resolve_expr(element_predicate, scope), + expr: resolve(element_predicate), }; let (interval, known) = crate::ir::interval::interval_of_invariant(&predicate); known.then_some(interval) diff --git a/src/diagnostics/classify.rs b/src/diagnostics/classify.rs index 84eaa2674..31a68729f 100644 --- a/src/diagnostics/classify.rs +++ b/src/diagnostics/classify.rs @@ -258,6 +258,30 @@ pub(crate) fn classify_type_error(msg: &str) -> TypeErrorClassification { ); } + if msg.contains("Operator '?' can only be applied to Result") { + return ( + "error-prop-non-result", + None, + Vec::new(), + Some( + "`?` unwraps a Result; this expression already has its payload type. A smart-constructor call over an all-literal list inside the refinement's proven element interval — Bytes.fromList([0, 10, 255]) — is total and returns the refined type directly, so drop the `?`" + .to_string(), + ), + ); + } + + if msg.contains("but the match subject is") { + return ( + "pattern-subject-mismatch", + None, + Vec::new(), + Some( + "Match the value's own shape. A Result arm cannot apply to a value that is not a Result — a smart-constructor call over an all-literal in-range list returns the refined type directly, so match on it (or bind it) instead of on Result.Ok / Result.Err" + .to_string(), + ), + ); + } + ("type-error", None, Vec::new(), None) } diff --git a/src/ir/hir/resolve.rs b/src/ir/hir/resolve.rs index f2c1638ce..66de16ae5 100644 --- a/src/ir/hir/resolve.rs +++ b/src/ir/hir/resolve.rs @@ -374,6 +374,56 @@ fn resolve_expr(ctx: &ResolveCtx<'_>, expr: &Spanned) -> ResolvedExpr { return ResolvedExpr::Call(ResolvedCallee::Intrinsic(intrinsic), resolved_args); } } + // Literal smart-constructor discharge: a call to a recognized + // `List` refinement's smart constructor over an + // all-literal, all-in-interval list literal cannot take the + // `Err` branch, so it lowers to the carrier construction the + // `Ok` branch would have produced — no `Result` wrap to unwrap + // on any backend. The gate is the SAME derived table the + // typechecker's discharge rule reads + // (`SymbolTable::literal_refinements`), and it keys on the + // refinement's own proven element interval, never on a name. + // Every spelling that denotes the constructor decides alike: + // this resolver also runs over a FLATTENED wasm-gc compile + // unit, where the qualified and in-module spellings have + // already collapsed into one prefixed bare name. + // + // Why a construct site rather than a call to the constructor: + // `RecordCreate` is total on every backend and needs no new IR + // node, the packed carrier bridge treats it identically to the + // constructor's own `Ok` branch, and the precedent already + // exists — `proof_lower::multi_field_record_demotions` treats a + // construct site whose every field is a literal inside the + // proven interval as exactly as gated as the smart constructor. + // The rewrite runs on resolved HIR, so the AST-walking demotion + // scans still see only the smart-constructor call. + let mut resolved_args = resolved_args; + if let Some(dotted) = expr_to_dotted_name(&callee.node) + && let Some(ctor) = ctx.symbols.literal_refinements().discharge(&dotted, args) + && resolved_args.len() == 1 + { + let key = match ctor.scope.as_deref() { + Some(prefix) => TypeKey::in_module(prefix, &ctor.type_name), + None => TypeKey::entry(&ctor.type_name), + }; + // Spell the construct site exactly as source in this scope + // would: bare inside the owning module, qualified from + // outside it. Backends resolve a record's layout from this + // spelling through the flatten-derived alias map, and a + // cross-module construct written bare resolves a different + // struct type than the surrounding expression expects. + let type_name = match ctor.scope.as_deref() { + Some(prefix) if ctx.current_module.as_deref() != Some(prefix) => { + format!("{prefix}.{}", ctor.type_name) + } + _ => ctor.type_name.clone(), + }; + return ResolvedExpr::RecordCreate { + type_id: ctx.symbols.type_id_of(&key), + type_name, + fields: vec![(ctor.carrier_field.clone(), resolved_args.remove(0))], + }; + } ResolvedExpr::Call(resolved_callee, resolved_args) } Expr::BinOp(op, l, r) => ResolvedExpr::BinOp( diff --git a/src/ir/symbol_table.rs b/src/ir/symbol_table.rs index 8cee7baa7..89a7819d9 100644 --- a/src/ir/symbol_table.rs +++ b/src/ir/symbol_table.rs @@ -120,6 +120,9 @@ pub struct SymbolTable { ctor_index: HashMap<(TypeId, String), CtorId>, /// Builtin canonical name → `BuiltinId` (Phase 6 wave 11). builtin_index: HashMap, + /// Recognized literal-dischargeable smart constructors — see + /// [`SymbolTable::literal_refinements`]. + literal_refinements: crate::analysis::literal_refinement::LiteralRefinementTable, } /// Phase 6 wave 11 — interned record for a built-in fn name. @@ -237,9 +240,38 @@ impl SymbolTable { } } + // Derived last: the recognizer resolves each refinement's + // per-element predicate against the table that is being built, + // so it needs every fn/type already indexed. It reads the table + // through the ordinary resolver, whose own discharge rewrite + // consults `literal_refinements` — still empty at this point, so + // the derivation can never recurse into itself. + table.literal_refinements = + crate::analysis::literal_refinement::LiteralRefinementTable::build( + entry_items, + dep_modules, + &table, + ); + table } + /// Derived gate for the literal smart-constructor discharge. + /// + /// Lives on the symbol table because that is the single place where + /// entry items and dependency modules are jointly in hand, and + /// because the coupling is exactly right: a qualified + /// `Dep.fromList(…)` can only RESOLVE against a table that knows + /// `Dep`, so every consumer able to resolve the call is also able to + /// see whether it discharges. Both the typechecker and the HIR + /// resolver read this one table, which is what keeps the checked and + /// unchecked pipelines from forking. + pub fn literal_refinements( + &self, + ) -> &crate::analysis::literal_refinement::LiteralRefinementTable { + &self.literal_refinements + } + /// Resolve a `FnKey` to its `FnId`. `None` when the key /// doesn't name any function in the program. pub fn fn_id_of(&self, key: &FnKey) -> Option { diff --git a/src/main/commands.rs b/src/main/commands.rs index 58a26c904..917698206 100644 --- a/src/main/commands.rs +++ b/src/main/commands.rs @@ -1274,6 +1274,87 @@ pub(super) fn cmd_run_vm( } } +/// Refuse a program the self-host pipeline would run with different +/// semantics than the host. +/// +/// The literal smart-constructor discharge is a HOST rule: the host +/// typechecker types `Dep.fromList([1, 2, 3])` as the refined type and +/// the host resolver lowers it to the carrier construction. The +/// Aver-in-Aver resolver (`self_hosted/domain/resolver/calls.av`) has no +/// refinement recognizer — it has no type defs, no dependency-module +/// ASTs and no interval derivation — so it keeps building a guest +/// `Result`. Mirroring the rule there is not the three syntactic +/// predicates the literal-divisor rule needed; it is the whole +/// recognizer. Until that lands, the boundary is a LOUD error: staying +/// silent means the guest returns `Result.Ok(v)` where the host-checked +/// source expects `v`, and the program dies far from the cause (or, in +/// the worst case, does not). +pub(super) fn reject_literal_refinement_discharge( + items: &[TopLevel], + module_root: Option<&str>, +) -> Result<(), String> { + use aver::analysis::literal_refinement::{LiteralRefinementTable, discharge_sites}; + + let loaded = module_root + .and_then(|base| { + items + .iter() + .find_map(|item| match item { + TopLevel::Module(m) => Some(m.depends.clone()), + _ => None, + }) + .and_then(|depends| aver::source::load_module_tree(&depends, base).ok()) + }) + .unwrap_or_default(); + let dep_modules: Vec = loaded + .iter() + .map(|m| aver::codegen::ModuleInfo { + prefix: m.dep_name.clone(), + depends: Vec::new(), + type_defs: m + .items + .iter() + .filter_map(|i| match i { + TopLevel::TypeDef(td) => Some(td.clone()), + _ => None, + }) + .collect(), + fn_defs: m + .items + .iter() + .filter_map(|i| match i { + TopLevel::FnDef(fd) => Some(fd.clone()), + _ => None, + }) + .collect(), + verify_laws: Vec::new(), + analysis: None, + }) + .collect(); + let symbols = aver::ir::SymbolTable::build(items, &dep_modules); + let table = LiteralRefinementTable::build(items, &dep_modules, &symbols); + + let mut sites = discharge_sites(&table, items); + for module in &loaded { + sites.extend(discharge_sites(&table, &module.items)); + } + if sites.is_empty() { + return Ok(()); + } + let listed: Vec = sites + .iter() + .map(|(line, callee)| format!(" line {line}: {callee}(…)")) + .collect(); + Err(format!( + "The self-host pipeline does not support the literal smart-constructor discharge.\n\ + These calls type as the refined type on the host but would build a Result in the \ + self-hosted interpreter:\n{}\n\ + Pass the list through a binding or a non-literal expression to keep the Result path, \ + or run without --self-host.", + listed.join("\n") + )) +} + pub(super) fn cmd_run_self_hosted( file: &str, module_root_override: Option<&str>, @@ -1317,6 +1398,10 @@ pub(super) fn cmd_run_self_hosted( eprintln!("{}", format_type_errors(&tc.errors).red()); process::exit(1); } + if let Err(e) = reject_literal_refinement_discharge(&items, Some(&mr)) { + eprintln!("{}", e.red()); + process::exit(1); + } } let module_root = resolve_module_root(module_root_override); diff --git a/src/main/replay_cmd/backends.rs b/src/main/replay_cmd/backends.rs index 59aa5dd54..89cbc29b8 100644 --- a/src/main/replay_cmd/backends.rs +++ b/src/main/replay_cmd/backends.rs @@ -298,6 +298,17 @@ pub(super) fn run_self_host_replay( check_args: bool, ) -> Result { let replay_program_file = resolve_replay_program_file(recording, replay_module_root); + // Same host/guest divergence gate as `aver run --self-host`: a + // discharged literal smart-constructor call means the guest resolver + // would build a `Result` the host-checked source no longer expects. + if let Ok(source) = super::super::shared::read_file(&replay_program_file) + && let Ok(items) = super::super::shared::parse_file(&source) + { + super::super::commands::reject_literal_refinement_discharge( + &items, + Some(replay_module_root), + )?; + } let binary_path = find_self_host_binary()?; let guest_args = decode_self_host_guest_args(&recording.input)?; diff --git a/src/stdlib.rs b/src/stdlib.rs index 864d445d1..436f42cf6 100644 --- a/src/stdlib.rs +++ b/src/stdlib.rs @@ -123,8 +123,14 @@ mod tests { // Rust codegen emits verify cases into a #[cfg(test)] module, so a // sha256 call that appears ONLY inside a verify block still needs // the Bytes/Digest32 modules in the generated project. + // + // The two sides of the case sit on opposite sides of the literal + // discharge boundary on purpose: `[double(0)]` has a computed + // element so it keeps `Result` (hence the `?`), while `[0]` is an + // all-literal in-range list and types as `Bytes` directly. The + // implicit-dependency scan must reach both spellings. let items = parse( - "module VerifyOnly\n intent = \"sha256 only in a verify case\"\n depends [Bytes]\n effects []\n\nfn double(n: Int) -> Int\n ? \"Double a number.\"\n n * 2\n\nverify double\n Crypto.sha256(Bytes.fromList([double(0)])?) => Crypto.sha256(Bytes.fromList([0])?)\n", + "module VerifyOnly\n intent = \"sha256 only in a verify case\"\n depends [Bytes]\n effects []\n\nfn double(n: Int) -> Int\n ? \"Double a number.\"\n n * 2\n\nverify double\n Crypto.sha256(Bytes.fromList([double(0)])?) => Crypto.sha256(Bytes.fromList([0]))\n", ); assert_eq!( implicit_stdlib_deps(&items), diff --git a/src/types/checker/infer/expr.rs b/src/types/checker/infer/expr.rs index c4e055dff..e79a48c88 100644 --- a/src/types/checker/infer/expr.rs +++ b/src/types/checker/infer/expr.rs @@ -654,8 +654,24 @@ impl TypeChecker { if let Expr::Ident(name) = &fn_expr.node { if let Some(sig) = self.find_fn_sig(name).cloned() { + // Literal smart-constructor discharge, bare-callee + // seam — see the qualified seam below for the rule. + // A module's own unqualified call to its recognized + // constructor must decide exactly as the qualified + // spelling does: the wasm-gc backend flattens both + // to one prefixed bare name before re-resolving, so + // a seam that discharged only one of them would fork + // the checked and unchecked pipelines. + let discharged = self + .symbol_table + .literal_refinements() + .discharge(name, args) + .is_some(); let ret = check_call(self, name, sig); validate_special_call(self, name, args); + if discharged && let Type::Result(payload, _) = ret { + return *payload; + } return ret; } if let Some(binding_ty) = self.binding_type(name) { @@ -773,6 +789,38 @@ impl TypeChecker { } _ => {} } + + // Literal smart-constructor discharge: a QUALIFIED call + // to a recognized `List` refinement's smart + // constructor whose single argument is a syntactic list + // of integer literals, every one inside the interval + // that refinement itself proves, cannot reach the `Err` + // branch — so it types as the refined type instead of + // `Result`. The gate is derived, never named: + // `LiteralRefinementTable` reads the same recognizer the + // wasm-gc packed layout is derived from, so "discharged" + // and "storable in the packed carrier" are the same + // predicate. The HIR resolver applies the identical rule + // to the identical shape. + if self + .symbol_table + .literal_refinements() + .discharge(&display_name, args) + .is_some() + && let Some(sig) = self.find_fn_sig(&display_name).cloned() + { + // Keep the standard arity/arg-type checks; only the + // return type is discharged, and it is taken from + // the constructor's own `Result` signature so + // the refined type is the exact canonical identity + // the checker already resolved — never a re-derived + // name. + let ret = check_call(self, &display_name, sig); + if let Type::Result(payload, _) = ret { + return *payload; + } + return ret; + } if let Some(sig) = self.find_fn_sig(&display_name).cloned() { let ret = check_call(self, &display_name, sig); validate_special_call(self, &display_name, args); diff --git a/src/types/checker/infer/patterns.rs b/src/types/checker/infer/patterns.rs index 661433711..a0dd5d65a 100644 --- a/src/types/checker/infer/patterns.rs +++ b/src/types/checker/infer/patterns.rs @@ -126,6 +126,27 @@ impl TypeChecker { } return; } + // A `Result` / `Option` constructor pattern against a + // subject that is neither is always a bug: no value of the + // subject's type can ever take the arm, so the match walks + // off the end at runtime with no diagnostic. The literal + // smart-constructor discharge makes this reachable by + // ordinary edits — `match Bytes.fromList([1, 2])` used to + // scrutinise a `Result` and now scrutinises a `Bytes` — so + // the migration has to be loud instead of silent. + if matches!(type_prefix, "Result" | "Option") + && !matches!( + subject_ty, + Type::Result(_, _) | Type::Option(_) | Type::Invalid | Type::Var(_) + ) + { + self.error(format!( + "Pattern '{}' matches a {} value, but the match subject is {}", + name, + type_prefix, + subject_ty.display() + )); + } let binding_tys = self.pattern_constructor_binding_types(name, subject_ty, bindings.len()); for (bind_name, bind_ty) in bindings.iter().zip(binding_tys) { diff --git a/stdlib/bytes.av b/stdlib/bytes.av index 8bae0b092..2991bff22 100644 --- a/stdlib/bytes.av +++ b/stdlib/bytes.av @@ -170,7 +170,8 @@ verify firstOutOfRangeIndex firstOutOfRangeIndex([255, -7]) => 1 verify fromList - fromList([0, 127, 255]) => Result.Ok(Bytes(values = [0, 127, 255])) + fromList([0, 127, 255]) => Bytes(values = [0, 127, 255]) + fromList(List.concat([0, 127], [255])) => Result.Ok(Bytes(values = [0, 127, 255])) fromList([256]) => Result.Err("byte 256 at index 0 is outside 0..=255") fromList([0, 256]) => Result.Err("byte 256 at index 1 is outside 0..=255") @@ -216,5 +217,5 @@ verify fromHex fromHex("0g") => Result.Err("Bytes.fromHex: invalid hexadecimal character 'g'") verify toHex - toHex(fromList([])?) => "" - toHex(fromList([0, 10, 255])?) => "000aff" + toHex(fromList([])) => "" + toHex(fromList([0, 10, 255])) => "000aff" diff --git a/stdlib/crypto/digest32.av b/stdlib/crypto/digest32.av index 9ccaa3718..a901700dc 100644 --- a/stdlib/crypto/digest32.av +++ b/stdlib/crypto/digest32.av @@ -33,12 +33,12 @@ fn toHex(digest: Digest32) -> String Bytes.toHex(toBytes(digest)) verify hasLength32 - hasLength32(Bytes.fromList([])?) => false - hasLength32(Bytes.fromList([0, 0])?) => false - hasLength32(Bytes.fromList([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])?) => true + hasLength32(Bytes.fromList([])) => false + hasLength32(Bytes.fromList([0, 0])) => false + hasLength32(Bytes.fromList([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])) => true verify fromBytes - fromBytes(Bytes.fromList([0, 0])?) => Result.Err("digest must contain exactly 32 bytes") + fromBytes(Bytes.fromList([0, 0])) => Result.Err("digest must contain exactly 32 bytes") verify fromHex fromHex("0000") => Result.Err("digest must contain exactly 32 bytes") diff --git a/tests/cross_backend_stress.rs b/tests/cross_backend_stress.rs index 38532533a..908256dc3 100644 --- a/tests/cross_backend_stress.rs +++ b/tests/cross_backend_stress.rs @@ -528,6 +528,115 @@ fn cross_literal_divisor_discharge_self_host() { LITERAL_DIVISOR_OUT, ); } + +/// Literal smart-constructor discharge, executed end to end. +/// `Local.fromList([1, 2, 3])` types as the refined type — the elements are +/// literals inside the interval the refinement's own predicate proves — so +/// every backend must produce the carrier directly, with no `Result` to +/// unwrap. `dynamic` keeps the fallible path in the same program, so a +/// backend that discharged too much or too little diverges here. +const LITERAL_REFINEMENT_SRC: &str = r#"module Local + +record Octets + values: List + +fn allInRange(xs: List) -> Bool + match xs + [] -> true + [head, ..tail] -> match Bool.and(head >= 0, head <= 255) + true -> allInRange(tail) + false -> false + +fn fromList(xs: List) -> Result + match allInRange(xs) + true -> Result.Ok(Octets(values = xs)) + false -> Result.Err("oob") + +fn count(o: Octets) -> Int + List.len(o.values) + +fn first(o: Octets) -> Int + match o.values + [head, .._] -> head + [] -> 0 - 1 + +fn dynamic(xs: List) -> Int + match fromList(xs) + Result.Ok(o) -> count(o) + Result.Err(_) -> 0 - 2 + +fn main() + ! [Console.print] + Console.print(String.fromInt(count(Local.fromList([1, 2, 3])))) + Console.print(String.fromInt(first(Local.fromList([200, 0])))) + Console.print(String.fromInt(count(Local.fromList([])))) + Console.print(String.fromInt(dynamic([1, 2]))) + Console.print(String.fromInt(dynamic([256]))) +"#; +const LITERAL_REFINEMENT_OUT: &str = "3\n200\n0\n2\n-2"; + +#[test] +fn cross_literal_refinement_discharge_vm() { + assert_eq_with_label( + "VM", + &run_vm("aver-cross-litref-vm", LITERAL_REFINEMENT_SRC), + LITERAL_REFINEMENT_OUT, + ); +} + +#[test] +fn cross_literal_refinement_discharge_wasm_gc() { + assert_eq_with_label( + "wasm-gc", + &run_wasm_gc("aver-cross-litref-wasmgc", LITERAL_REFINEMENT_SRC), + LITERAL_REFINEMENT_OUT, + ); +} + +#[test] +fn cross_literal_refinement_discharge_rejected_by_self_host() { + // The self-hosted resolver has no refinement recognizer — no type + // defs, no dependency-module ASTs, no interval derivation — so it + // cannot mirror this rule the way it mirrors the purely syntactic + // literal-divisor one. Doing nothing would NOT be neutral: the guest + // would keep building a `Result` where the host-checked source expects + // the refined type, and the program would fail far from the cause (the + // pre-gate symptom was a bare `field access on non-record`). The + // boundary is therefore a loud, specific refusal that names the call + // sites, and this test is what keeps it loud. + let repo_root = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + let aver_bin = env!("CARGO_BIN_EXE_aver"); + let path = temp_module("aver-cross-litref-sh", LITERAL_REFINEMENT_SRC); + let module_root = path.parent().expect("temp module has parent"); + let out = Command::new(aver_bin) + .current_dir(&repo_root) + .arg("run") + .arg(&path) + .arg("--module-root") + .arg(module_root) + .arg("--self-host") + .output() + .expect("expected `aver run --self-host` to execute"); + cleanup(&path); + let combined = format!( + "{}{}", + String::from_utf8_lossy(&out.stdout), + String::from_utf8_lossy(&out.stderr) + ); + assert!( + !out.status.success(), + "self-host must REFUSE a discharged program, not run it:\n{combined}" + ); + assert!( + combined.contains("does not support the literal smart-constructor discharge"), + "self-host refusal must name the rule:\n{combined}" + ); + assert!( + combined.contains("Local.fromList"), + "self-host refusal must name the offending call sites:\n{combined}" + ); +} + // ─── Verify cross-target ──────────────────────────────────────────────── // // `aver verify` and `aver verify --wasm-gc` evaluate the same verify diff --git a/tests/fixtures/discharged_bytes_law.av b/tests/fixtures/discharged_bytes_law.av new file mode 100644 index 000000000..4f5eaa3bc --- /dev/null +++ b/tests/fixtures/discharged_bytes_law.av @@ -0,0 +1,43 @@ +module DischargedBytesLaw + intent = + "Laws and examples over literal smart-constructor discharge, on both proof backends. `Bytes.fromList([0, 10, 255])` types as plain `Bytes` because every element is an integer literal inside the interval the `Bytes` refinement itself proves, so the call constructs the carrier directly instead of returning `Result`. In Lean that lands as a `Subtype` construction whose obligation is `Bytes.allInRange [0, 10, 255] = true` — the discharge gate's own claim, re-established by the kernel rather than assumed; `allInRange` is compiled by well-founded recursion, which `decide` cannot evaluate through the elaborator, so the obligation is closed by the emitted `simp [Bytes.allInRange]` rung. In Dafny the construction collapses to the bare carrier and the subset-type constraint is discharged at the use site by unfolding the same recursive predicate over a literal sequence. Coverage: a three-element frame, the vacuous empty frame, and `dynamicOctetCount`, which keeps the `Result` path because its argument is computed — the emission-correctness pin, since the file only builds if the discharged calls became direct constructions WHILE the computed one stayed a fallible call in the same program. The long-literal stress case lives in `discharged_bytes_long_literal.av`, which is Lean-only: Dafny's default function fuel does not unfold a 32-element sequence through the recursive predicate." + depends [Bytes] + exposes [octetCount, literalFrame, emptyFrame, dynamicOctetCount, framesAgree] + effects [] + +fn literalFrame() -> Bytes + ? "A three-octet frame built from an all-literal in-range list." + Bytes.fromList([0, 10, 255]) + +fn emptyFrame() -> Bytes + ? "The empty frame; the element bound holds vacuously." + Bytes.fromList([]) + +fn octetCount(bytes: Bytes) -> Int + ? "How many octets a validated frame carries." + List.len(Bytes.toList(bytes)) + +fn dynamicOctetCount(values: List) -> Result + ? "Count octets through the fallible constructor; the argument is not a literal list." + bytes = Bytes.fromList(values)? + Result.Ok(octetCount(bytes)) + +fn framesAgree(bytes: Bytes) -> Bool + ? "Whether a frame carries the same octets as the literal three-octet frame." + Bytes.toList(bytes) == Bytes.toList(literalFrame()) + +verify literalFrame + Bytes.toHex(literalFrame()) => "000aff" + octetCount(literalFrame()) => 3 + +verify emptyFrame + Bytes.toHex(emptyFrame()) => "" + octetCount(emptyFrame()) => 0 + +verify dynamicOctetCount + dynamicOctetCount([0, 10, 255]) => Result.Ok(3) + dynamicOctetCount([0, 256]) => Result.Err("byte 256 at index 1 is outside 0..=255") + +verify framesAgree law literalFrameIsItsOwnOctets + given n: Int = 0..2 + framesAgree(literalFrame()) => true diff --git a/tests/fixtures/discharged_bytes_long_literal.av b/tests/fixtures/discharged_bytes_long_literal.av new file mode 100644 index 000000000..40a1dc070 --- /dev/null +++ b/tests/fixtures/discharged_bytes_long_literal.av @@ -0,0 +1,24 @@ +module DischargedBytesLongLiteral + intent = + "Long-literal stress case for the literal smart-constructor discharge, Lean only. A 32-element all-literal in-range list types as plain `Bytes`, and Lean must close `Bytes.allInRange [0, 0, …] = true` through 32 unfoldings of a well-founded recursive predicate — the depth at which `decide` and the pre-existing tactic ladder both fail and the emitted `simp [Bytes.allInRange]` rung is doing the work. Dafny is deliberately NOT gated on this file: a refinement construction collapses to the bare carrier there and the subset-type constraint is discharged at the use site, which Dafny's default function fuel does not unfold that far. The three-element and empty frames, which BOTH backends discharge, live in `discharged_bytes_law.av`." + depends [Bytes] + exposes [digestSizedFrame, octetCount] + effects [] + +fn digestSizedFrame() -> Bytes + ? "A 32-octet frame built from an all-literal in-range list." + Bytes.fromList([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]) + +fn mixedLongFrame() -> Bytes + ? "A 32-octet frame spanning the whole proven element interval." + Bytes.fromList([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255]) + +fn octetCount(bytes: Bytes) -> Int + ? "How many octets a validated frame carries." + List.len(Bytes.toList(bytes)) + +verify digestSizedFrame + octetCount(digestSizedFrame()) => 32 + +verify mixedLongFrame + octetCount(mixedLongFrame()) => 32 diff --git a/tests/proof_spec/builds.rs b/tests/proof_spec/builds.rs index 49c1a795f..6be932824 100644 --- a/tests/proof_spec/builds.rs +++ b/tests/proof_spec/builds.rs @@ -840,6 +840,64 @@ fn proof_export_verifies_discharged_div_law_when_lake_is_available() { ); } +#[test] +fn proof_export_builds_discharged_bytes_law_when_lake_is_available() { + // Literal smart-constructor discharge, Lean side + // (tests/fixtures/discharged_bytes_law.av). `Bytes.fromList([0, 10, + // 255])` types as plain `Bytes`, so the Lean backend emits a `Subtype` + // construction `⟨[0, 10, 255], by …⟩` whose obligation is + // `Bytes.allInRange [0, 10, 255] = true` — the discharge gate's own + // claim, re-established by the kernel instead of assumed. + // + // That obligation is why the emitted tactic ladder grew a + // `simp []` rung. `allInRange` is compiled by well-founded + // recursion, which `decide` cannot evaluate through the elaborator + // (see the note in `src/codegen/lean/crypto_model.lean`), so + // `first | omega | decide | (simp_all; omega) | assumption` closes + // none of these goals. The rung names the predicate the refinement's + // own invariant applies, so it is derived, not hardcoded. + // + // The empty frame is the vacuous case, and `dynamicOctetCount` keeps + // the `Result` path: the file only builds if the discharged calls + // became direct constructions WHILE the computed-argument call stayed + // fallible. + assert_proof_builds( + "tests/fixtures/discharged_bytes_law.av", + "aver-proof-discharged-bytes-law", + ); +} + +#[test] +fn proof_export_builds_discharged_bytes_long_literal_when_lake_is_available() { + // Recursion-depth stress case for the same rung: 32-element literal + // frames, one all-zero and one spanning the whole proven interval. + // Closing `Bytes.allInRange [0, 0, …] = true` needs 32 unfoldings of a + // well-founded recursive predicate, which is exactly the depth at + // which `decide` and the pre-existing ladder both fail. + // + // Lean only, deliberately: Dafny discharges the same fact as a + // subset-type constraint at the use site, and its default function + // fuel does not unfold a 32-element sequence. The shapes BOTH backends + // discharge live in `discharged_bytes_law.av` above. + assert_proof_builds( + "tests/fixtures/discharged_bytes_long_literal.av", + "aver-proof-discharged-bytes-long-literal", + ); +} + +#[test] +fn proof_dafny_verifies_discharged_bytes_law_when_dafny_is_available() { + // Dafny side of the discharge. A refinement construction collapses to + // the bare carrier there, so `Bytes.fromList([0, 10, 255])` becomes the + // literal sequence and Dafny must discharge the subset-type constraint + // `allInRange(xs)` at the use site by unfolding the same recursive + // predicate the Lean obligation names. + assert_dafny_verifies( + "tests/fixtures/discharged_bytes_law.av", + "aver-dafny-discharged-bytes-law", + ); +} + #[test] fn proof_export_builds_result_default_cone_when_lake_is_available() { // A law whose unfold cone contains the `Result.withDefault` builtin diff --git a/tests/rust_codegen_differential.rs b/tests/rust_codegen_differential.rs index 07c135ad9..3db3ff731 100644 --- a/tests/rust_codegen_differential.rs +++ b/tests/rust_codegen_differential.rs @@ -386,6 +386,49 @@ fn run_vm_inline(name: &str, source: &str) -> Result { out } +/// Literal smart-constructor discharge on the Rust backend. A call whose +/// argument is an all-literal list inside the interval the refinement itself +/// proves types as the refined type and lowers to a direct carrier +/// construction; a computed argument keeps the fallible constructor. Both +/// shapes sit in one program, so a backend that discharged too much or too +/// little diverges from the VM here. +#[test] +fn rust_literal_refinement_discharge_matches_vm() { + let src = r#"module LiteralRefinement + intent = "Discharged and fallible smart-constructor calls in one program" + depends [Bytes] + effects [Console.print] + +fn describe(bytes: Bytes) -> String + ? "Render a validated frame as hex plus its length." + "{Bytes.toHex(bytes)}/{List.len(Bytes.toList(bytes))}" + +fn dynamic(values: List) -> String + ? "Validate a computed list through the fallible constructor." + match Bytes.fromList(values) + Result.Ok(bytes) -> describe(bytes) + Result.Err(e) -> e + +fn main() -> Unit + ? "Print the discharged and fallible results side by side." + ! [Console.print] + Console.print(describe(Bytes.fromList([249, 190, 180, 217]))) + Console.print(describe(Bytes.fromList([]))) + Console.print(dynamic(List.concat([249, 190], [180, 217]))) + Console.print(dynamic([65, 256])) +"#; + let expected = "f9beb4d9/4\n/0\nf9beb4d9/4\nbyte 256 at index 1 is outside 0..=255"; + + let vm = run_vm_inline("literal_refinement_discharge", src).expect("vm run"); + let rust = build_run_rust_inline("literal_refinement_discharge", src) + .expect("rust compile + cargo build + run"); + assert_eq!(vm, expected, "VM literal-discharge contract changed"); + assert_eq!( + rust, expected, + "Rust literal-discharge contract diverged from VM" + ); +} + /// `aver compile` can succeed while leaving a MIR-walker `compile_error!` in /// the emitted project, so this regression must drive `Tcp.sendBytes` through /// a real `cargo build`. Invalid raw lists fail at `Bytes.fromList` before any @@ -522,11 +565,13 @@ fn main() -> Unit /// `cargo test` with E0433. Driving `cargo test` (not just the build) also /// proves the digest-equality cases hold in the generated code. /// -/// The verify cases use `Bytes.fromList(…)?` directly, which doubles as -/// the regression for `?` inside a verify case: the generated test fn +/// The last verify case uses `Bytes.fromHex(…)?` directly, which doubles +/// as the regression for `?` inside a verify case: the generated test fn /// returns `Result<(), String>` while generated stdlib fns error with /// `AverStr`, so the emitter must convert at the `?` boundary (bare `?` -/// used to fail `cargo test` with E0277). +/// used to fail `cargo test` with E0277). It also pins that a discharged +/// literal `Bytes.fromList([1, 2])` and the equivalent value built +/// through the fallible `fromHex` path hash to the same digest. #[test] fn rust_sha256_verify_only_generates_testable_project() { let src = r#"module Sha256VerifyOnly @@ -546,8 +591,9 @@ fn main() -> Unit Console.print(describe(true)) verify describe - describe(Crypto.sha256(Bytes.fromList([1, 2])?) == Crypto.sha256(Bytes.fromList([1, 2])?)) => "same" - describe(Crypto.sha256(Bytes.fromList([1, 2])?) == Crypto.sha256(Bytes.fromList([2, 1])?)) => "different" + describe(Crypto.sha256(Bytes.fromList([1, 2])) == Crypto.sha256(Bytes.fromList([1, 2]))) => "same" + describe(Crypto.sha256(Bytes.fromList([1, 2])) == Crypto.sha256(Bytes.fromList([2, 1]))) => "different" + describe(Crypto.sha256(Bytes.fromHex("0102")?) == Crypto.sha256(Bytes.fromList([1, 2]))) => "same" "#; let name = "sha256_verify_only"; @@ -2457,7 +2503,7 @@ fn rust_tcp_send_bytes_round_trips_non_utf8() { fn exchange() -> Result ? "Send one binary payload to a loopback echo server." ! [Tcp.sendBytes] - payload = Bytes.fromList([249, 190, 180, 217])? + payload = Bytes.fromList([249, 190, 180, 217]) Tcp.sendBytes("127.0.0.1", {port}, payload) fn main() -> Unit diff --git a/tests/typechecker_spec.rs b/tests/typechecker_spec.rs index cae9ab21e..ce3ef6a06 100644 --- a/tests/typechecker_spec.rs +++ b/tests/typechecker_spec.rs @@ -1382,7 +1382,7 @@ fn valid_verify_trace_given_stub_for_tcp_read_bytes() { "\n", "fn readStub(path: BranchPath, n: Int, conn: Tcp.Connection, count: Int) -> Result\n", " ? \"Honest stub returning a fixed frame.\"\n", - " Bytes.fromList([1, 2, 3, 4])\n", + " Result.Ok(Bytes.fromList([1, 2, 3, 4]))\n", "\n", "fn readFrame(conn: Tcp.Connection) -> Result\n", " ? \"Read one 4-byte frame.\"\n", @@ -1392,7 +1392,7 @@ fn valid_verify_trace_given_stub_for_tcp_read_bytes() { "verify readFrame trace\n", " given conn: Tcp.Connection = [Tcp.Connection(id = \"fake\", host = \"h\", port = 1)]\n", " given reader: Tcp.readBytes = [readStub]\n", - " readFrame(conn) => Bytes.fromList([1, 2, 3, 4])\n", + " readFrame(conn) => Result.Ok(Bytes.fromList([1, 2, 3, 4]))\n", ); let errs = errors_with_base(src, env!("CARGO_MANIFEST_DIR")); assert!(errs.is_empty(), "expected no errors, got: {errs:?}"); @@ -1420,7 +1420,7 @@ fn valid_verify_trace_given_stub_for_tcp_write_bytes() { "verify sendFrame trace\n", " given conn: Tcp.Connection = [Tcp.Connection(id = \"fake\", host = \"h\", port = 1)]\n", " given writer: Tcp.writeBytes = [writeStub]\n", - " sendFrame(conn, Bytes.fromList([1, 2])?) => Result.Ok(Unit)\n", + " sendFrame(conn, Bytes.fromList([1, 2])) => Result.Ok(Unit)\n", ); let errs = errors_with_base(src, env!("CARGO_MANIFEST_DIR")); assert!(errs.is_empty(), "expected no errors, got: {errs:?}"); @@ -1687,6 +1687,192 @@ fn literal_divisor_discharge_parentheses_are_transparent() { assert_no_errors("fn f(a: Int) -> Result\n Int.mod(a, (0))\n"); } +// ─── Literal smart-constructor discharge ──────────────────────────────── +// +// `Bytes.fromList([])` types as plain `Bytes`. Every other +// argument shape keeps `Result`. The tests below are named +// after the boundary they pin; the element bound is DERIVED from +// `stdlib/bytes.av`'s own `allInRange` predicate, never hardcoded, so a +// program with a different refinement discharges against a different +// range (see `src/analysis/literal_refinement.rs`). + +/// Program skeleton for the discharge tests: one fn body, `depends [Bytes]`. +fn bytes_program(signature: &str, body: &str) -> String { + format!( + "module Prog\n intent = \"literal Bytes discharge\"\n depends [Bytes]\n effects []\n\n{signature}\n ? \"probe\"\n{body}\n" + ) +} + +fn assert_bytes_program_clean(signature: &str, body: &str) { + let src = bytes_program(signature, body); + let errs = errors_with_base(&src, env!("CARGO_MANIFEST_DIR")); + assert!( + errs.is_empty(), + "expected no type errors for:\n{src}\ngot:\n {}", + errs.join("\n ") + ); +} + +fn assert_bytes_program_error(signature: &str, body: &str, snippet: &str) { + let src = bytes_program(signature, body); + let errs = errors_with_base(&src, env!("CARGO_MANIFEST_DIR")); + assert!( + errs.iter().any(|e| e.contains(snippet)), + "expected error containing {snippet:?} for:\n{src}\ngot:\n {}", + if errs.is_empty() { + "".to_string() + } else { + errs.join("\n ") + } + ); +} + +#[test] +fn literal_bytes_discharge_types_as_the_refined_type() { + assert_bytes_program_clean("fn f() -> Bytes", " Bytes.fromList([0, 10, 255])"); + // The empty list satisfies the element bound vacuously. + assert_bytes_program_clean("fn f() -> Bytes", " Bytes.fromList([])"); + // Interval endpoints are inclusive. + assert_bytes_program_clean("fn f() -> Bytes", " Bytes.fromList([0])"); + assert_bytes_program_clean("fn f() -> Bytes", " Bytes.fromList([255])"); + // The discharged value flows straight into a `Bytes` consumer. + assert_bytes_program_clean( + "fn f() -> String", + " Bytes.toHex(Bytes.fromList([0, 10, 255]))", + ); + // …and no longer satisfies a `Result` return or the `?` operator. + assert_bytes_program_error( + "fn f() -> Result", + " Bytes.fromList([1, 2])", + "body returns Bytes but declared return type is Result", + ); + assert_bytes_program_error( + "fn f() -> Bytes", + " Bytes.fromList([1, 2])?", + "can only be applied to Result", + ); +} + +#[test] +fn literal_bytes_discharge_boundary_out_of_interval_literal_stays_result() { + // THE BOUNDARY, element side: a literal outside the interval the + // refinement proves keeps the fallible signature, because the + // constructor really can take its `Err` branch. + assert_bytes_program_clean( + "fn f() -> Result", + " Bytes.fromList([65, 256])", + ); + assert_bytes_program_clean( + "fn f() -> Result", + " Bytes.fromList([-1])", + ); + // A magnitude beyond `i64` is declined outright by the syntactic half + // of the predicate — no bignum comparison, fail-closed. + assert_bytes_program_clean( + "fn f() -> Result", + " Bytes.fromList([65, 1208925819614629174706176])", + ); +} + +#[test] +fn literal_bytes_discharge_boundary_is_syntactic_literal_lists_only() { + // THE BOUNDARY, argument-shape side: the discharge is keyed on a + // syntactic list of syntactic literals, nothing wider. Widening it + // (constant folding, flow facts, a proved-in-range variable) is a + // deliberate design decision — if you are here to relax this test, + // that decision needs its own review. + // + // An identifier stays `Result`, even when it is bound to a literal + // list in plain sight. + assert_bytes_program_clean( + "fn f() -> Result", + " xs = [1, 2]\n Bytes.fromList(xs)", + ); + // A parameter stays `Result`. + assert_bytes_program_clean( + "fn f(xs: List) -> Result", + " Bytes.fromList(xs)", + ); + // A computed list stays `Result` (no folding). + assert_bytes_program_clean( + "fn f() -> Result", + " Bytes.fromList(List.concat([1], [2]))", + ); + // A computed ELEMENT stays `Result`, even though its value is in range. + assert_bytes_program_clean( + "fn f() -> Result", + " Bytes.fromList([1 + 1])", + ); + // A doubly-negated literal is not a syntactic literal. + assert_bytes_program_clean( + "fn f() -> Result", + " Bytes.fromList([--5])", + ); + // One in-range element does not carry an out-of-range sibling. + assert_bytes_program_clean( + "fn f() -> Result", + " Bytes.fromList([1, 2, 300])", + ); + // A non-list argument does not discharge; the ordinary argument check + // rejects it instead of a discharge skipping past it. + assert_bytes_program_error( + "fn f() -> Bytes", + " Bytes.fromList(\"0102\")", + "Argument 1 of 'Bytes.fromList': expected List, got String", + ); +} + +#[test] +fn literal_bytes_discharge_decides_the_same_for_every_callee_spelling() { + // THE BOUNDARY, callee side: qualified and bare in-module spellings + // must decide IDENTICALLY. This is not a convenience — the wasm-gc + // backend flattens a dependency's constructor and all of its call + // sites, qualified and in-module alike, into one prefixed bare name + // before re-resolving, so after the flatten the two spellings are + // indistinguishable. A spelling-sensitive rule would discharge before + // the flatten and not after, forking the checked and unchecked + // pipelines. Both fns below therefore return the refined type. + let src = "module Local\n intent = \"an entry-scope refinement\"\n effects []\n\nrecord Octets\n values: List\n\nfn allInRange(xs: List) -> Bool\n ? \"probe\"\n match xs\n [] -> true\n [head, ..tail] -> match Bool.and(head >= 0, head <= 255)\n true -> allInRange(tail)\n false -> false\n\nfn fromList(xs: List) -> Result\n ? \"probe\"\n match allInRange(xs)\n true -> Result.Ok(Octets(values = xs))\n false -> Result.Err(\"oob\")\n\nfn unqualified() -> Octets\n ? \"probe\"\n fromList([1, 2])\n\nfn qualified() -> Octets\n ? \"probe\"\n Local.fromList([1, 2])\n\nfn stillFallible(xs: List) -> Result\n ? \"probe\"\n fromList(xs)\n"; + assert_no_errors(src); +} + +#[test] +fn a_result_pattern_against_a_discharged_value_is_an_error() { + // The migration must be LOUD. Before the discharge, + // `match Bytes.fromList([1, 2])` scrutinised a `Result`; now it + // scrutinises a `Bytes`, and the `Result.Ok` / `Result.Err` arms can + // never be taken. Left unchecked the match just walks off the end at + // runtime with no diagnostic, so the pattern checker rejects a + // `Result` / `Option` constructor pattern whose subject is neither. + assert_bytes_program_error( + "fn f() -> String", + " match Bytes.fromList([1, 2])\n Result.Ok(b) -> Bytes.toHex(b)\n Result.Err(e) -> e", + "Pattern 'Result.Ok' matches a Result value, but the match subject is Bytes", + ); + // The same guard on a plainly wrong match, discharge or not. + assert_error_containing( + "fn f(n: Int) -> Int\n match n\n Result.Ok(v) -> v\n Result.Err(_) -> 0\n", + "but the match subject is Int", + ); + // A genuine Result subject is untouched. + assert_bytes_program_clean( + "fn f(values: List) -> String", + " match Bytes.fromList(values)\n Result.Ok(b) -> Bytes.toHex(b)\n Result.Err(e) -> e", + ); +} + +#[test] +fn literal_bytes_discharge_boundary_needs_a_recognized_smart_constructor() { + // THE BOUNDARY, refinement side: the gate is derived from the + // refinement SHAPE, not from a constructor name. A bare record with a + // `fromList` of its own — no validating predicate, so nothing proves + // an element interval — never discharges, and its declared + // `Result` signature stands. + let src = "module Local\n intent = \"a fromList that validates nothing\"\n effects []\n\nrecord Octets\n values: List\n\nfn fromList(xs: List) -> Result\n ? \"probe\"\n Result.Ok(Octets(values = xs))\n\nfn use() -> Result\n ? \"probe\"\n Local.fromList([1, 2])\n"; + assert_no_errors(src); +} + #[test] fn integer_slash_operator_is_a_type_error() { // The bare `/` operator on two Ints is partial (a zero divisor; over ℤ diff --git a/tests/verify_tcp_bytes_given_stub.rs b/tests/verify_tcp_bytes_given_stub.rs index 957c0b9d8..e378e595b 100644 --- a/tests/verify_tcp_bytes_given_stub.rs +++ b/tests/verify_tcp_bytes_given_stub.rs @@ -25,7 +25,7 @@ fn user_given_stub_for_tcp_read_bytes_typechecks_and_runs_on_vm() { fn readStub(path: BranchPath, n: Int, conn: Tcp.Connection, count: Int) -> Result ? "Honest stub returning a fixed frame." - Bytes.fromList([1, 2, 3, 4]) + Result.Ok(Bytes.fromList([1, 2, 3, 4])) fn readFrame(conn: Tcp.Connection) -> Result ? "Read one 4-byte frame." @@ -35,7 +35,7 @@ fn readFrame(conn: Tcp.Connection) -> Result verify readFrame trace given conn: Tcp.Connection = [Tcp.Connection(id = "fake", host = "127.0.0.1", port = 1)] given reader: Tcp.readBytes = [readStub] - readFrame(conn) => Bytes.fromList([1, 2, 3, 4]) + readFrame(conn) => Result.Ok(Bytes.fromList([1, 2, 3, 4])) "#; let items = parse_source(src).unwrap_or_else(|e| panic!("parse failed: {e:?}")); let results = run_verify_for_items_vm( diff --git a/tests/wasip2_codegen_regression.rs b/tests/wasip2_codegen_regression.rs index ea14fe6d5..da2f32881 100644 --- a/tests/wasip2_codegen_regression.rs +++ b/tests/wasip2_codegen_regression.rs @@ -163,7 +163,7 @@ fn tcp_send_bytes_compiles_and_validates_as_component() { fn main() -> Result ? "Send and receive bytes without UTF-8 conversion." ! [Tcp.sendBytes] - payload = Bytes.fromList([249, 190, 180, 217])? + payload = Bytes.fromList([249, 190, 180, 217]) Tcp.sendBytes("127.0.0.1", 9, payload) "#; let (items, type_aliases) = diff --git a/tests/wasip2_tcp.rs b/tests/wasip2_tcp.rs index fd9fd58cc..470853fc9 100644 --- a/tests/wasip2_tcp.rs +++ b/tests/wasip2_tcp.rs @@ -382,11 +382,9 @@ fn writeFrame(c: Tcp.Connection, payload: Bytes) -> Unit Result.Ok(_) -> awaitAck(c) Result.Err(e) -> Console.print("write err: {{e}}") -fn usePayload(c: Tcp.Connection, payload: Result) -> Unit +fn usePayload(c: Tcp.Connection, payload: Bytes) -> Unit ! [Tcp.writeBytes, Tcp.readLine, Tcp.close, Console.print] - match payload - Result.Ok(bytes) -> writeFrame(c, bytes) - Result.Err(e) -> Console.print("bytes err: {{e}}") + writeFrame(c, payload) fn main() -> Unit ! [Tcp.connect, Tcp.writeBytes, Tcp.readLine, Tcp.close, Console.print] @@ -618,11 +616,9 @@ fn renderBytes(bytes: List) -> String fn main() -> Unit ! [Tcp.sendBytes, Console.print] - match Bytes.fromList([249, 190, 180, 217]) + match Tcp.sendBytes("127.0.0.1", {port}, Bytes.fromList([249, 190, 180, 217])) + Result.Ok(r) -> Console.print("got: {{renderBytes(Bytes.toList(r))}}") Result.Err(e) -> Console.print("err: {{e}}") - Result.Ok(payload) -> match Tcp.sendBytes("127.0.0.1", {port}, payload) - Result.Ok(r) -> Console.print("got: {{renderBytes(Bytes.toList(r))}}") - Result.Err(e) -> Console.print("err: {{e}}") "# ); let fixture = write_fixture(&dir, "send_bytes.av", &src); diff --git a/tests/wasm_gc_codegen_regression.rs b/tests/wasm_gc_codegen_regression.rs index 7f949f85f..870d1acfe 100644 --- a/tests/wasm_gc_codegen_regression.rs +++ b/tests/wasm_gc_codegen_regression.rs @@ -164,7 +164,7 @@ fn tcp_send_bytes_imports_host_function_and_validates() { fn main() -> Result ? "Send and receive bytes without UTF-8 conversion." ! [Tcp.sendBytes] - payload = Bytes.fromList([249, 190, 180, 217])? + payload = Bytes.fromList([249, 190, 180, 217]) Tcp.sendBytes("127.0.0.1", 9, payload) "#; let (items, type_aliases) = @@ -289,7 +289,7 @@ fn sha256_compiles_without_digest32_in_depends() { fn main() -> Result ? "Hash a payload and report that a digest was produced." ! [Console.print] - payload = Bytes.fromList([1, 2, 3])? + payload = Bytes.fromList([1, 2, 3]) digest = Crypto.sha256(payload) Console.print("hashed") Result.Ok("hashed") diff --git a/tests/wasm_gc_effect_arg_overflow_regression.rs b/tests/wasm_gc_effect_arg_overflow_regression.rs index b86e76566..41f2aad57 100644 --- a/tests/wasm_gc_effect_arg_overflow_regression.rs +++ b/tests/wasm_gc_effect_arg_overflow_regression.rs @@ -233,11 +233,9 @@ fn tcp_send_bytes_round_trips_nominal_bytes_on_wasm_gc() { fn main() -> Unit ! [Tcp.sendBytes, Console.print] - match Bytes.fromList([249, 190, 180, 217]) + match Tcp.sendBytes("127.0.0.1", {port}, Bytes.fromList([249, 190, 180, 217])) Result.Err(e) -> Console.print("err: {{e}}") - Result.Ok(payload) -> match Tcp.sendBytes("127.0.0.1", {port}, payload) - Result.Err(e) -> Console.print("err: {{e}}") - Result.Ok(response) -> Console.print("{{Bytes.toList(response) == [249, 190, 180, 217]}}") + Result.Ok(response) -> Console.print("{{Bytes.toList(response) == [249, 190, 180, 217]}}") "# ); let (out, recorded) = run_wasm_gc_with_mode(&src, aver::runtime::wasm_gc::EffectMode::Record) @@ -364,15 +362,13 @@ fn writeFrame(conn: Tcp.Connection, payload: Bytes) -> Result fn main() -> Unit ! [Tcp.connect, Tcp.writeBytes, Tcp.close, Console.print] - match Bytes.fromList([249, 190, 180, 217]) - Result.Err(e) -> Console.print("bytes err: {{e}}") - Result.Ok(payload) -> match Tcp.connect("127.0.0.1", {port}) - Result.Err(e) -> Console.print("connect err: {{e}}") - Result.Ok(conn) -> match writeFrame(conn, payload) - Result.Err(e) -> Console.print("write err: {{e}}") - Result.Ok(_) -> match Tcp.close(conn) - Result.Err(e) -> Console.print("close err: {{e}}") - Result.Ok(_) -> Console.print("written") + match Tcp.connect("127.0.0.1", {port}) + Result.Err(e) -> Console.print("connect err: {{e}}") + Result.Ok(conn) -> match writeFrame(conn, Bytes.fromList([249, 190, 180, 217])) + Result.Err(e) -> Console.print("write err: {{e}}") + Result.Ok(_) -> match Tcp.close(conn) + Result.Err(e) -> Console.print("close err: {{e}}") + Result.Ok(_) -> Console.print("written") "# ); let (out, recorded) = run_wasm_gc_with_mode(&src, aver::runtime::wasm_gc::EffectMode::Record) diff --git a/tests/wasm_gc_packed_sequence.rs b/tests/wasm_gc_packed_sequence.rs index c57c46547..03fefac5c 100644 --- a/tests/wasm_gc_packed_sequence.rs +++ b/tests/wasm_gc_packed_sequence.rs @@ -110,6 +110,45 @@ fn compile(source: &str, packed: bool) -> Vec { wasm } +/// Multi-module variant of `compile`: emits the wasm-gc module for an +/// entry that depends on one module file, so type-section assertions can +/// be made about a refinement declared in a dependency. +fn compile_multi(entry_src: &str, dep_file: &str, dep_src: &str, packed: bool) -> Vec { + let id = NEXT_TEMP_ID.fetch_add(1, Ordering::Relaxed); + let dir = std::env::temp_dir().join(format!( + "aver-packed-sequence-compile-multi-{}-{id}", + std::process::id() + )); + std::fs::create_dir_all(&dir).expect("temp dir"); + let path = dir.join("main.av"); + let out_dir = dir.join("out"); + std::fs::write(&path, entry_src).expect("entry source"); + std::fs::write(dir.join(dep_file), dep_src).expect("dep source"); + let mut command = Command::new(env!("CARGO_BIN_EXE_aver")); + command + .arg("compile") + .arg(&path) + .arg("--module-root") + .arg(&dir) + .arg("--target") + .arg("wasm-gc") + .arg("-o") + .arg(&out_dir); + if !packed { + command.env("AVER_NO_PACKED_SEQUENCES", "1"); + } + let output = command.output().expect("compile aver"); + assert!( + output.status.success(), + "compile failed: {}{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr) + ); + let wasm = std::fs::read(out_dir.join("main.wasm")).expect("compiled wasm"); + let _ = std::fs::remove_dir_all(dir); + wasm +} + fn i8_array_count(wasm: &[u8]) -> usize { use wasmparser::{CompositeInnerType, Parser, Payload, StorageType}; @@ -159,7 +198,7 @@ fn same(left: Octets, right: Octets) -> Bool fn main() -> Unit ! [Console.print] - match fromList([0, 1, 127, 128, 255]) + match fromList(List.concat([0, 1, 127], [128, 255])) Result.Ok(value) -> match Vector.get(Vector.fromList([value]), 0) Option.Some(first) -> match Map.get(Map.set({}, "value", first), "value") Option.Some(stored) -> match Map.get(Map.set({}, stored, "present"), value) @@ -240,7 +279,7 @@ fn firstValue(o: Dep.Octets) -> Int [] -> 0 - 1 fn run() -> Result - o: Dep.Octets = Dep.fromList([200])? + o: Dep.Octets = Dep.fromList([200]) Result.Ok(firstValue(o)) fn main() -> Unit @@ -412,3 +451,140 @@ fn ungated_constructor_demotes_instead_of_truncating() { assert_eq!(wasm, vm); assert_eq!(vm, "256"); } + +// ─── Literal smart-constructor discharge ──────────────────────────────── +// +// `Dep.fromList([])` types as +// `Dep.Octets` and lowers to the carrier construction instead of a +// `Result`. The packed layout must survive that, and it does by +// construction: the discharge gate reads the SAME derived element +// interval the packed layout is chosen from, so an admitted value is +// always storable in the packed `i8` array. The two tests below pin both +// halves — the representation (type-section shape) and the value +// (VM / packed wasm-gc / boxed wasm-gc all agree). + +const DISCHARGED_ENTRY: &str = r#"module Main + intent = "a discharged literal smart-constructor call over a packed dep carrier" + depends [Dep] + effects [Console] + +fn firstValue(o: Dep.Octets) -> Int + match o.values + [head, .._] -> head + [] -> 0 - 1 + +fn describe(discharged: Dep.Octets, gated: Dep.Octets) -> String + match discharged == gated + true -> "{firstValue(discharged)} {List.len(Dep.toList(discharged))} same" + false -> "different" + +fn run() -> Result + discharged = Dep.fromList([200, 0, 255]) + gated = Dep.fromList(List.concat([200], [0, 255]))? + Result.Ok(describe(discharged, gated)) + +fn main() -> Unit + ! [Console.print] + match run() + Result.Ok(text) -> Console.print(text) + Result.Err(error) -> Console.print(error) +"#; + +// Same program with an out-of-interval element. The discharge declines, +// the smart constructor runs, and every backend reports its error — +// nothing reaches the packed store, whose element write is a raw +// `array.set` with no range check. +const DISCHARGE_DECLINED_ENTRY: &str = r#"module Main + intent = "an out-of-interval literal keeps the fallible constructor" + depends [Dep] + effects [Console] + +fn main() -> Unit + ! [Console.print] + match Dep.fromList([65, 256]) + Result.Ok(value) -> Console.print("unexpected {List.len(Dep.toList(value))}") + Result.Err(error) -> Console.print(error) +"#; + +const DISCHARGE_DEP: &str = r#"module Dep + intent = "sole-declarer gated Octets refinement with a reader" + exposes [Octets, fromList, toList] + depends [] + +record Octets + values: List + +fn allInRange(xs: List) -> Bool + match xs + [] -> true + [head, ..tail] -> match Bool.and(head >= 0, head <= 255) + true -> allInRange(tail) + false -> false + +fn fromList(xs: List) -> Result + match allInRange(xs) + true -> Result.Ok(Octets(values = xs)) + false -> Result.Err("oob") + +fn toList(o: Octets) -> List + o.values +"#; + +#[test] +fn discharged_literal_construction_keeps_the_packed_layout_and_matches_vm() { + let (vm_ok, vm) = run_multi(DISCHARGED_ENTRY, "dep.av", DISCHARGE_DEP, false, true); + let (packed_ok, packed) = run_multi(DISCHARGED_ENTRY, "dep.av", DISCHARGE_DEP, true, true); + let (boxed_ok, boxed) = run_multi(DISCHARGED_ENTRY, "dep.av", DISCHARGE_DEP, true, false); + assert!(vm_ok, "VM failed: {vm}"); + assert!(packed_ok, "packed wasm failed: {packed}"); + assert!(boxed_ok, "boxed wasm failed: {boxed}"); + // The discharged value is indistinguishable from the one the smart + // constructor builds, on every backend. + assert_eq!(vm, "200 3 same"); + assert_eq!(packed, vm, "packed wasm-gc diverged from the VM"); + assert_eq!(boxed, vm, "boxed wasm-gc diverged from the VM"); + + // Representation: the discharged construct site is NOT an ungated + // construction. The proof-derived packed layout is still installed, so + // the packed module carries exactly one more `i8` array than the boxed + // one — the same delta a gated-only program produces. + let packed_wasm = compile_multi(DISCHARGED_ENTRY, "dep.av", DISCHARGE_DEP, true); + let boxed_wasm = compile_multi(DISCHARGED_ENTRY, "dep.av", DISCHARGE_DEP, false); + assert_eq!( + i8_array_count(&packed_wasm), + i8_array_count(&boxed_wasm) + 1, + "a discharged literal construct site must keep the proof-derived \ + packed layout" + ); +} + +#[test] +fn out_of_interval_literal_declines_the_discharge_on_every_backend() { + let (vm_ok, vm) = run_multi( + DISCHARGE_DECLINED_ENTRY, + "dep.av", + DISCHARGE_DEP, + false, + true, + ); + let (packed_ok, packed) = run_multi( + DISCHARGE_DECLINED_ENTRY, + "dep.av", + DISCHARGE_DEP, + true, + true, + ); + let (boxed_ok, boxed) = run_multi( + DISCHARGE_DECLINED_ENTRY, + "dep.av", + DISCHARGE_DEP, + true, + false, + ); + assert!(vm_ok, "VM failed: {vm}"); + assert!(packed_ok, "packed wasm failed: {packed}"); + assert!(boxed_ok, "boxed wasm failed: {boxed}"); + assert_eq!(vm, "oob"); + assert_eq!(packed, vm, "packed wasm-gc must not silently truncate 256"); + assert_eq!(boxed, vm); +} diff --git a/tests/wasm_gc_spec.rs b/tests/wasm_gc_spec.rs index 666d3029d..c4657cf5d 100644 --- a/tests/wasm_gc_spec.rs +++ b/tests/wasm_gc_spec.rs @@ -522,7 +522,7 @@ fn firstValue(o: Dep.Octets) -> Int [] -> 0 - 1 fn run() -> Result - o: Dep.Octets = Dep.fromList([200])? + o: Dep.Octets = Dep.fromList([200]) Result.Ok(firstValue(o)) fn main() -> Int From 4da4f665d46219753f41d345ccbdbaa5d1c083bb Mon Sep 17 00:00:00 2001 From: jasisz Date: Sat, 8 Aug 2026 03:53:29 +0200 Subject: [PATCH 2/2] Key the literal smart-constructor discharge on the resolved callee MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The discharge matched a call site by the callee's spelling, so a module that declares its own `fromList` over an imported refinement's smart constructor got two answers at once: the type checker obeyed Aver's shadowing rule and typed `fromList([1, 2, 3])` as the local function's return type, while the resolver rewrote the very same call into the refinement's carrier construction. The VM then printed a record where the program asked for a length. The two backends disagreed as well — after the wasm-gc flatten the local and the imported name are no longer spelled alike, so that backend declined the rewrite the VM performed. Both consult sites now key on the function identity ordinary name resolution assigned the call. The checker takes the identity out of the same lookup that produced the signature it checks the call against, and the resolver uses the callee it just classified: the discharge and the normal resolution must agree, or the discharge declines. Two recognized constructors that collapse onto one identity are fail-closed. The self-host rejection scan asks the resolver's own callee classifier, so it reports exactly the calls the rewrite fires on and no others. Keying on identity exposed an older divergence underneath. The wasm-gc resolver context carried no current module, so a program that spelled its own members qualified (`Local.fromList(xs)`) failed to resolve there and lowered to a trap, while every other backend called it. It now carries the declared module name like every other resolution site. Also: say in the resolver what actually makes the synthesised construction safe — the element interval shared with the packed layout, not the AST demotion scans, which never see the generated node; add a law over one body that holds a discharged construction and a fallible call at once; cover the self-host refusal on the replay path; and drop a recomputation of the refinement table the symbol table already carries. Co-Authored-By: Claude Fable 5 --- docs/language.md | 2 +- src/analysis/literal_refinement.rs | 421 +++++++++++++++++-------- src/codegen/wasm_gc/view.rs | 14 +- src/ir/hir/resolve.rs | 39 ++- src/main/commands.rs | 21 +- src/types/checker/infer/expr.rs | 53 ++-- src/types/checker/mod.rs | 22 +- tests/cross_backend_stress.rs | 110 +++++++ tests/fixtures/discharged_bytes_law.av | 16 +- tests/proof_spec/builds.rs | 14 +- tests/typechecker_spec.rs | 137 ++++++++ 11 files changed, 672 insertions(+), 177 deletions(-) diff --git a/docs/language.md b/docs/language.md index f4e6a6980..3303158e5 100644 --- a/docs/language.md +++ b/docs/language.md @@ -50,7 +50,7 @@ Duplicate binding of the same name in the same scope is a type error. Arithmetic: `+`, `-`, `*` — operands must match (`Int+Int`, `Float+Float`, `String+String`). No implicit promotion; use `Float.fromInt` / `Int.fromFloat` to convert. The `/` operator is **Float-only**; integer `/` is a type error. For integers use `Int.div(a, b) : Result` (Euclidean; `b == 0` → `Result.Err`) and `Int.mod(a, b) : Result` — there is no integer `%`. `Int` is arbitrary-precision (ℤ): no overflow, no wraparound. Literal-divisor discharge: when the divisor of `Int.div` / `Int.mod` is a syntactic nonzero integer literal — `Int.div(x, 2)`, `Int.mod(x, -3)` — the call cannot fail, so it types as plain `Int` and every backend emits the division directly (no `Result`, no unwrapping). The boundary is exactly "a syntactic integer literal other than `0`, optionally under one unary minus": a `0` literal, an identifier, a named constant, or a constant expression like `8 + 8` all keep the `Result` type unchanged. Parentheses are transparent here, because the parser erases them around a single expression: `(16)`, `(-16)` and `-(16)` are the same syntax tree as `16` and `-16`, so all three discharge — while `(0)` is still zero and `(k)` is still an identifier, and both keep the `Result` type. This is a typing rule for these two functions only, not a general constant-propagation or refinement mechanism. -Literal smart-constructor discharge: the same idea extends to a validating smart constructor over a `List` carrier — the shape `stdlib/bytes.av` uses. When the argument is a syntactic list of integer literals and every element is inside the interval the refinement itself proves, the call cannot reach its `Result.Err` branch, so it types as the refined type and constructs the value directly: `Bytes.fromList([0, 10, 255]) : Bytes`, no `?` and no `match`. The empty list `Bytes.fromList([])` discharges too. The boundary is narrow and entirely syntactic on the argument side: there must be exactly one argument, it must be a list literal written out at the call site, and every element must be a plain integer literal with at most one unary minus. Every spelling that denotes the constructor decides the same way — `Bytes.fromList(...)` from outside and a bare `fromList(...)` inside the defining module alike. Everything else keeps `Result` unchanged — an identifier (`Bytes.fromList(values)`), a computed list (`Bytes.fromList(List.concat(a, b))`), a computed element (`Bytes.fromList([n * 2])`), an out-of-range literal (`Bytes.fromList([65, 256])`), a negative one (`Bytes.fromList([-1])`), or a literal beyond `i64`. The bound is never hardcoded: it is read off the refinement's own validating predicate, so a user-defined refinement with a different range discharges against that range, and a record with no smart constructor never discharges at all. Programs run under `--self-host` are refused with an explicit error when they contain a discharged call, because the self-hosted resolver does not yet carry the rule. +Literal smart-constructor discharge: the same idea extends to a validating smart constructor over a `List` carrier — the shape `stdlib/bytes.av` uses. When the argument is a syntactic list of integer literals and every element is inside the interval the refinement itself proves, the call cannot reach its `Result.Err` branch, so it types as the refined type and constructs the value directly: `Bytes.fromList([0, 10, 255]) : Bytes`, no `?` and no `match`. The empty list `Bytes.fromList([])` discharges too. The boundary is narrow and entirely syntactic on the argument side: there must be exactly one argument, it must be a list literal written out at the call site, and every element must be a plain integer literal with at most one unary minus. What decides is the function the call resolves to, never how it is spelled: `Bytes.fromList(...)` from outside and a bare `fromList(...)` inside the defining module both reach the constructor and both discharge, while a module that declares its own `fromList` shadows the imported one as usual — that call means the local function and is not discharged at all. Everything else keeps `Result` unchanged — an identifier (`Bytes.fromList(values)`), a computed list (`Bytes.fromList(List.concat(a, b))`), a computed element (`Bytes.fromList([n * 2])`), an out-of-range literal (`Bytes.fromList([65, 256])`), a negative one (`Bytes.fromList([-1])`), or a literal beyond `i64`. The bound is never hardcoded: it is read off the refinement's own validating predicate, so a user-defined refinement with a different range discharges against that range, and a record with no smart constructor never discharges at all. Programs run under `--self-host` are refused with an explicit error when they contain a discharged call, because the self-hosted resolver does not yet carry the rule. Unary minus negates a numeric expression: `-n` (equivalent to `0 - n`), and numeric literals may be written negative (`-3`, `-1.5`). Comparison: `==`, `!=`, `<`, `>`, `<=`, `>=`. Error propagation: `expr?` — unwraps `Result.Ok`, propagates `Result.Err` as a `RuntimeError`. diff --git a/src/analysis/literal_refinement.rs b/src/analysis/literal_refinement.rs index b343e22b3..7c4709129 100644 --- a/src/analysis/literal_refinement.rs +++ b/src/analysis/literal_refinement.rs @@ -33,20 +33,38 @@ //! store it" MUST be the same predicate. They are — literally the same //! function. //! +//! # The discharge is keyed on RESOLVED IDENTITY, never on spelling +//! +//! **Invariant.** The discharge fires only when ordinary name resolution — +//! the checker's own resolved signature, the HIR resolver's own +//! [`crate::ir::hir::ResolvedCallee::Fn`] — lands on the recognized smart +//! constructor's [`FnId`]. If the two disagree about which function the +//! call site denotes, the discharge DECLINES. That is what makes the +//! checked type and the lowered IR the same decision rather than two +//! opinions about a name. +//! +//! Spelling would be the wrong key in both directions: +//! +//! * It under-fires. The wasm-gc backend re-resolves a FLATTENED compile +//! unit in which `flatten_multimodule` has renamed a dependency's +//! `fromList` to the entry-scope `Dep_fromList` and rewritten BOTH the +//! qualified and the in-module call sites to that one bare name. Keyed on +//! identity, the flatten is invisible: the rebuilt symbol table resolves +//! the renamed call sites to the renamed constructor's `FnId`. +//! * It OVER-fires, which is a miscompilation. An entry module that +//! declares its own `fn fromList(xs: List) -> Int` shadows the +//! stdlib constructor — Aver's pinned shadowing rule, so the checker +//! types `fromList([1, 2, 3])` as `Int`. A name-keyed discharge would +//! still have rewritten that body to a `Bytes` carrier construction, and +//! the checked type and the emitted code would disagree. +//! +//! Two recognized constructors that collapse onto one `FnId` (one scope +//! declaring the same constructor name twice, where the symbol table keys +//! one `FnKey` to one `FnId`) are fail-closed: neither discharges, because +//! no call site can name one without naming the other. +//! //! # Boundary //! -//! * Every callee spelling that DENOTES the recognized constructor decides -//! the same way — qualified (`Bytes.fromList(…)`) and bare in-module -//! (`fromList(…)` inside `stdlib/bytes.av` itself) alike. Spelling -//! insensitivity is not a convenience: the wasm-gc backend re-resolves a -//! FLATTENED compile unit in which `flatten_multimodule` has renamed a -//! dependency's `fromList` to the entry-scope `Dep_fromList` and -//! rewritten BOTH the qualified and the in-module call sites to that one -//! bare name. After the flatten the two spellings are indistinguishable, -//! so a spelling-sensitive rule would discharge before it and not after -//! — the checked/unchecked fork this rule must not create. A bare -//! spelling shared by two recognized constructors is fail-closed: it -//! denotes neither. //! * Exactly one argument, and it must be a syntactic list literal whose //! every element is a plain integer literal with at most one unary minus //! (`crate::ast::literal_int_list_elements`). An identifier, a call, a @@ -57,18 +75,23 @@ //! vacuously, and the constructor's predicate is `true` on `[]` by the //! recognized shape's own base case. -use std::collections::HashSet; +use std::collections::{HashMap, HashSet}; use crate::analysis::shape::{ModulePattern, detect_module_patterns}; use crate::ast::{Expr, FnDef, Spanned, TopLevel}; use crate::codegen::ModuleInfo; use crate::ir::SymbolTable; +use crate::ir::hir::{ResolveCtx, ResolvedCallee}; +use crate::ir::identity::{FnId, FnKey}; use crate::ir::interval::Interval; /// One recognized smart constructor over a `List` carrier whose /// element interval the refinement itself proves. #[derive(Debug, Clone, PartialEq)] pub struct ListRefinementCtor { + /// Resolved identity of the smart constructor — the ONLY key a call + /// site is matched against. See the module-level invariant. + pub fn_id: FnId, /// Dependency-module prefix that owns the refinement (`"Bytes"`), or /// `None` when the refinement is declared in the entry file. pub scope: Option, @@ -76,22 +99,18 @@ pub struct ListRefinementCtor { pub type_name: String, /// The record's single carrier field (`"values"`). pub carrier_field: String, - /// Bare source name of the smart constructor (`"fromList"`). + /// Bare source name of the smart constructor (`"fromList"`). Carried + /// for diagnostics only; it is never a lookup key. pub constructor_fn: String, /// Interval proven for EVERY element of the carrier list. pub element_interval: Interval, } /// Every literal-dischargeable smart constructor in one compilation, -/// addressed by the qualified callee spelling a call site writes. +/// addressed by the [`FnId`] name resolution assigns the callee. #[derive(Debug, Clone, Default)] pub struct LiteralRefinementTable { ctors: Vec, - /// Prefix an entry-scope refinement is addressable under, taken from - /// the entry file's own `module X` declaration. Aver lets a module - /// spell its own members qualified, so `X.fromList([…])` in an entry - /// file that declares `module X` reaches the same constructor. - entry_prefix: Option, } impl LiteralRefinementTable { @@ -181,7 +200,19 @@ impl LiteralRefinementTable { if !seen.insert((scope.clone(), type_name.clone())) { continue; } + // The one key a call site is ever matched against. A + // constructor the symbol table doesn't index cannot be named + // by any resolved callee, so it is dropped rather than kept + // under a spelling. + let key = match scope.as_deref() { + Some(prefix) => FnKey::in_module(prefix, &constructor_fn), + None => FnKey::entry(&constructor_fn), + }; + let Some(fn_id) = symbols.fn_id_of(&key) else { + continue; + }; ctors.push(ListRefinementCtor { + fn_id, scope, type_name, carrier_field, @@ -190,15 +221,17 @@ impl LiteralRefinementTable { }); } - let entry_prefix = entry_items.iter().find_map(|item| match item { - TopLevel::Module(m) => Some(m.name.clone()), - _ => None, - }); - - Self { - ctors, - entry_prefix, + // Fail-closed on a shared identity: one scope declaring the same + // constructor name twice collapses both refinements onto a single + // `FnId`, and no call site can then denote one without denoting + // the other. Neither discharges. + let mut per_identity: HashMap = HashMap::new(); + for ctor in &ctors { + *per_identity.entry(ctor.fn_id).or_default() += 1; } + ctors.retain(|ctor| per_identity[&ctor.fn_id] == 1); + + Self { ctors } } /// `true` when nothing in this program is dischargeable — lets callers @@ -209,56 +242,35 @@ impl LiteralRefinementTable { /// Decide the discharge for one call site. /// - /// `callee` is the dotted spelling the source wrote — qualified - /// (`"Bytes.fromList"`) or bare (`"fromList"` from inside the owning - /// module). Returns the constructor whose refined type the call now - /// produces, or `None` to keep the declared `Result` signature. - /// - /// Every spelling that DENOTES the recognized constructor decides the - /// same way, deliberately: the wasm-gc backend flattens a dependency's - /// `fromList` and every one of its call sites — qualified and - /// in-module alike — into a single bare `Dep_fromList` before - /// re-resolving, so a spelling-sensitive rule would discharge before - /// the flatten and not after. - pub fn discharge(&self, callee: &str, args: &[Spanned]) -> Option<&ListRefinementCtor> { + /// `callee` is the [`FnId`] ORDINARY NAME RESOLUTION assigned this + /// call — the checker's own resolved signature, or the HIR resolver's + /// own [`ResolvedCallee::Fn`]. Never a spelling: a caller that passes + /// an identity it did not itself resolve breaks the invariant this + /// whole module exists to hold. Returns the constructor whose refined + /// type the call now produces, or `None` to keep the declared + /// `Result` signature. + pub fn discharge(&self, callee: FnId, args: &[Spanned]) -> Option<&ListRefinementCtor> { if args.len() != 1 { return None; } - let ctor = self.resolve_ctor(callee)?; + let ctor = self.ctors.iter().find(|c| c.fn_id == callee)?; let elements = crate::ast::literal_int_list_elements(&args[0])?; elements .iter() .all(|k| ctor.element_interval.contains_point(*k)) .then_some(ctor) } - - /// Which recognized constructor a callee spelling denotes, if any. - /// Fail-closed on ambiguity: when two refinements in the program share - /// a bare constructor name, a bare call site denotes neither. - fn resolve_ctor(&self, callee: &str) -> Option<&ListRefinementCtor> { - // Qualified spelling: `.`, or `.` for a refinement declared in the entry file. - if let Some((prefix, fn_name)) = callee.rsplit_once('.') - && let Some(ctor) = self.ctors.iter().find(|c| { - c.constructor_fn == fn_name - && match c.scope.as_deref() { - Some(scope) => scope == prefix, - None => self.entry_prefix.as_deref() == Some(prefix), - } - }) - { - return Some(ctor); - } - // Bare spelling: an in-module call, or a post-flatten call to the - // prefixed name flatten gave the dependency's function. - let mut matches = self.ctors.iter().filter(|c| c.constructor_fn == callee); - let first = matches.next()?; - matches.next().is_none().then_some(first) - } } /// Every call site in `items` the discharge rewrites, as -/// `(line, qualified callee)`, in source order. +/// `(line, callee spelling)`, in source order. +/// +/// `scope` is the module prefix `items` belong to (`None` for the entry +/// file), because the callee identity is resolved exactly the way the HIR +/// resolver resolves it — through +/// [`crate::ir::hir::resolve::classify_callee`] against the same symbol +/// table and the same current-module context. Same resolver, same answer: +/// a call the rewrite will not fire on is not reported here either. /// /// Exists for the self-host boundary: the Aver-in-Aver resolver has no /// refinement recognizer, so a discharged program would build a guest @@ -266,25 +278,31 @@ impl LiteralRefinementTable { /// divergence is SILENT (the guest fails much later, or not at all), so /// the self-host driver refuses such a program up front and points at /// the exact call sites. -pub fn discharge_sites(table: &LiteralRefinementTable, items: &[TopLevel]) -> Vec<(usize, String)> { +pub fn discharge_sites( + symbols: &SymbolTable, + scope: Option<&str>, + items: &[TopLevel], +) -> Vec<(usize, String)> { let mut out = Vec::new(); - if table.is_empty() { + if symbols.literal_refinements().is_empty() { return out; } + let mut ctx = ResolveCtx::new(symbols); + ctx.current_module = scope.map(str::to_string); for item in items { match item { TopLevel::FnDef(fd) => { for stmt in fd.body.stmts() { let (crate::ast::Stmt::Binding(_, _, e) | crate::ast::Stmt::Expr(e)) = stmt; - walk(table, e, &mut out); + walk(&ctx, e, &mut out); } } TopLevel::Stmt(crate::ast::Stmt::Binding(_, _, e)) - | TopLevel::Stmt(crate::ast::Stmt::Expr(e)) => walk(table, e, &mut out), + | TopLevel::Stmt(crate::ast::Stmt::Expr(e)) => walk(&ctx, e, &mut out), TopLevel::Verify(block) => { for (left, right) in &block.cases { - walk(table, left, &mut out); - walk(table, right, &mut out); + walk(&ctx, left, &mut out); + walk(&ctx, right, &mut out); } } TopLevel::Module(_) | TopLevel::Decision(_) | TopLevel::TypeDef(_) => {} @@ -297,65 +315,71 @@ pub fn discharge_sites(table: &LiteralRefinementTable, items: &[TopLevel]) -> Ve /// Exhaustive `Expr` walk. Deliberately has NO catch-all arm: a new /// expression form must be classified here explicitly, or the self-host /// rejection could silently miss a discharged call nested inside it. -fn walk(table: &LiteralRefinementTable, expr: &Spanned, out: &mut Vec<(usize, String)>) { +fn walk(ctx: &ResolveCtx<'_>, expr: &Spanned, out: &mut Vec<(usize, String)>) { match &expr.node { Expr::FnCall(callee, args) => { - if let Some(dotted) = crate::codegen::common::expr_to_dotted_name(&callee.node) - && table.discharge(&dotted, args).is_some() + if let ResolvedCallee::Fn(fn_id) = crate::ir::hir::resolve::classify_callee(ctx, callee) + && ctx + .symbols + .literal_refinements() + .discharge(fn_id, args) + .is_some() { - out.push((expr.line, dotted)); + let spelling = crate::codegen::common::expr_to_dotted_name(&callee.node) + .unwrap_or_else(|| ctx.symbols.fn_entry(fn_id).key.name.clone()); + out.push((expr.line, spelling)); } - walk(table, callee, out); + walk(ctx, callee, out); for a in args { - walk(table, a, out); + walk(ctx, a, out); } } - Expr::Attr(obj, _) => walk(table, obj, out), + Expr::Attr(obj, _) => walk(ctx, obj, out), Expr::BinOp(_, l, r) => { - walk(table, l, out); - walk(table, r, out); + walk(ctx, l, out); + walk(ctx, r, out); } Expr::Neg(inner) | Expr::ErrorProp(inner) | Expr::Constructor(_, Some(inner)) => { - walk(table, inner, out) + walk(ctx, inner, out) } Expr::Match { subject, arms } => { - walk(table, subject, out); + walk(ctx, subject, out); for arm in arms { - walk(table, &arm.body, out); + walk(ctx, &arm.body, out); } } Expr::InterpolatedStr(parts) => { for part in parts { if let crate::ast::StrPart::Parsed(inner) = part { - walk(table, inner, out); + walk(ctx, inner, out); } } } Expr::List(items) | Expr::Tuple(items) | Expr::IndependentProduct(items, _) => { for item in items { - walk(table, item, out); + walk(ctx, item, out); } } Expr::MapLiteral(pairs) => { for (k, v) in pairs { - walk(table, k, out); - walk(table, v, out); + walk(ctx, k, out); + walk(ctx, v, out); } } Expr::RecordCreate { fields, .. } => { for (_, value) in fields { - walk(table, value, out); + walk(ctx, value, out); } } Expr::RecordUpdate { base, updates, .. } => { - walk(table, base, out); + walk(ctx, base, out); for (_, value) in updates { - walk(table, value, out); + walk(ctx, value, out); } } Expr::TailCall(data) => { for a in &data.args { - walk(table, a, out); + walk(ctx, a, out); } } Expr::Literal(_) | Expr::Ident(_) | Expr::Constructor(_, None) | Expr::Resolved { .. } => {} @@ -381,17 +405,22 @@ fn is_int_list_carrier_product(td: &crate::ast::TypeDef) -> bool { mod tests { use super::*; - fn table_for(entry: &str, dep: Option<(&str, &str)>) -> LiteralRefinementTable { + /// Build the program's `SymbolTable` — the discharge table hangs off + /// it, and so does the name resolution every lookup below goes + /// through. Tests never address a constructor by spelling alone; + /// they resolve the spelling first, exactly as the compiler does. + fn symbols_for(entry: &str, deps: &[(&str, &str)]) -> SymbolTable { let parse = |src: &str| { let mut lexer = crate::lexer::Lexer::new(src); let tokens = lexer.tokenize().expect("lex"); crate::parser::Parser::new(tokens).parse().expect("parse") }; let entry_items = parse(entry); - let dep_modules: Vec = dep + let dep_modules: Vec = deps + .iter() .map(|(prefix, src)| { let items = parse(src); - vec![ModuleInfo { + ModuleInfo { prefix: prefix.to_string(), depends: Vec::new(), type_defs: items @@ -410,11 +439,30 @@ mod tests { .collect(), verify_laws: Vec::new(), analysis: None, - }] + } }) - .unwrap_or_default(); - let symbols = SymbolTable::build(&entry_items, &dep_modules); - LiteralRefinementTable::build(&entry_items, &dep_modules, &symbols) + .collect(); + SymbolTable::build(&entry_items, &dep_modules) + } + + /// Decide one call site the way a compiler pass does: resolve the + /// callee spelling against `symbols` from `scope`, then discharge on + /// the identity that came back. An unresolvable spelling declines. + fn discharges_from(symbols: &SymbolTable, scope: Option<&str>, call: &str) -> bool { + let mut ctx = ResolveCtx::new(symbols); + ctx.current_module = scope.map(str::to_string); + let expr = expr_of(call); + let Expr::FnCall(callee, args) = &expr.node else { + panic!("expected a call expression, got {expr:?}"); + }; + let ResolvedCallee::Fn(fn_id) = crate::ir::hir::resolve::classify_callee(&ctx, callee) + else { + return false; + }; + symbols + .literal_refinements() + .discharge(fn_id, args) + .is_some() } const OCTETS: &str = r#" @@ -451,7 +499,7 @@ fn go() -> Int 1 "#; - fn list(src: &str) -> Spanned { + fn expr_of(src: &str) -> Spanned { let mut lexer = crate::lexer::Lexer::new(src); let tokens = lexer.tokenize().expect("lex"); let items = crate::parser::Parser::new(tokens).parse().expect("parse"); @@ -463,10 +511,14 @@ fn go() -> Int #[test] fn derives_the_element_interval_without_naming_the_refinement() { - let table = table_for(CONSUMER, Some(("Octets", OCTETS))); + let symbols = symbols_for(CONSUMER, &[("Octets", OCTETS)]); + let fn_id = symbols + .fn_id_of(&FnKey::in_module("Octets", "fromList")) + .expect("Octets.fromList must be indexed"); assert_eq!( - table.ctors, + symbols.literal_refinements().ctors, vec![ListRefinementCtor { + fn_id, scope: Some("Octets".to_string()), type_name: "Octets".to_string(), carrier_field: "values".to_string(), @@ -478,12 +530,13 @@ fn go() -> Int #[test] fn derives_the_element_interval_for_the_real_standard_library_bytes_module() { - let table = table_for( + let symbols = symbols_for( CONSUMER, - Some(("Bytes", include_str!("../../stdlib/bytes.av"))), + &[("Bytes", include_str!("../../stdlib/bytes.av"))], ); assert_eq!( - table + symbols + .literal_refinements() .ctors .iter() .find(|c| c.type_name == "Bytes") @@ -494,8 +547,9 @@ fn go() -> Int #[test] fn discharges_only_all_literal_in_interval_lists() { - let table = table_for(CONSUMER, Some(("Octets", OCTETS))); - let discharges = |src: &str| table.discharge("Octets.fromList", &[list(src)]).is_some(); + let symbols = symbols_for(CONSUMER, &[("Octets", OCTETS)]); + let discharges = + |arg: &str| discharges_from(&symbols, None, &format!("Octets.fromList({arg})")); assert!(discharges("[1, 2, 3]")); assert!(discharges("[]")); @@ -512,28 +566,108 @@ fn go() -> Int } #[test] - fn accepts_every_spelling_that_denotes_the_constructor() { - let table = table_for(CONSUMER, Some(("Octets", OCTETS))); - // Qualified, and the bare in-module / post-flatten spelling. + fn accepts_every_spelling_that_resolves_to_the_constructor() { + let symbols = symbols_for(CONSUMER, &[("Octets", OCTETS)]); + // Qualified from the consumer. + assert!(discharges_from(&symbols, None, "Octets.fromList([1, 2])")); + // Bare from inside the owning module — the in-module spelling and + // the post-flatten spelling both resolve to the same `FnId`. + assert!(discharges_from( + &symbols, + Some("Octets"), + "fromList([1, 2])" + )); + // Bare from the consumer resolves to nothing at all here. + assert!(!discharges_from(&symbols, None, "fromList([1, 2])")); + // A different module's same-named function is a different identity. + assert!(!discharges_from(&symbols, None, "Tree.fromList([1, 2])")); + assert!(!discharges_from(&symbols, None, "Octets.toList([1, 2])")); + } + + #[test] + fn a_local_fn_shadowing_the_constructor_keeps_its_own_identity() { + // THE MISCOMPILATION GUARD. An entry module declaring its own + // `fromList` shadows the dependency's constructor (Aver's pinned + // shadowing rule), so `fromList([1, 2])` in that entry denotes the + // LOCAL fn. A spelling-keyed discharge fired here and rewrote the + // body to a carrier construction while the checker typed the call + // as the local fn's return type. + let shadowing_entry = r#" +module Consumer + intent = "declares its own fromList over the dependency's" + depends [Octets] + exposes [go] + effects [] + +fn fromList(xs: List) -> Int + List.len(xs) + +fn go() -> Int + fromList([1, 2]) +"#; + let symbols = symbols_for(shadowing_entry, &[("Octets", OCTETS)]); assert!( - table - .discharge("Octets.fromList", &[list("[1, 2]")]) - .is_some() + !symbols.literal_refinements().is_empty(), + "the dependency's constructor is still recognized" ); - assert!(table.discharge("fromList", &[list("[1, 2]")]).is_some()); - // A different module's same-named function denotes nothing here. - assert!( - table - .discharge("Tree.fromList", &[list("[1, 2]")]) - .is_none() + assert!(!discharges_from(&symbols, None, "fromList([1, 2])")); + // The dependency's own constructor is untouched: still reachable + // qualified, and still discharging. + assert!(discharges_from(&symbols, None, "Octets.fromList([1, 2])")); + } + + #[test] + fn same_bare_name_in_two_modules_resolves_per_scope() { + // Two recognized constructors, one per module, sharing a bare + // name. Identity keying makes each in-module call discharge + // against its OWN interval — the derived bound follows the + // resolved callee, not the spelling. + let nibbles = r#" +module Nibbles + intent = "a second refinement whose constructor shares the bare name" + exposes [fromList] + exposes opaque [Nibbles] + effects [] + +record Nibbles + values: List + +fn inNibbleRange(xs: List) -> Bool + match xs + [] -> true + [head, ..tail] -> match Bool.and(head >= 0, head <= 15) + true -> inNibbleRange(tail) + false -> false + +fn fromList(xs: List) -> Result + match inNibbleRange(xs) + true -> Result.Ok(Nibbles(values = xs)) + false -> Result.Err("oob") +"#; + let symbols = symbols_for(CONSUMER, &[("Octets", OCTETS), ("Nibbles", nibbles)]); + assert_eq!( + symbols.literal_refinements().ctors.len(), + 2, + "expected two recognized constructors" ); - assert!(table.discharge("toList", &[list("[1, 2]")]).is_none()); + // 200 is inside Octets' interval and outside Nibbles'. + assert!(discharges_from(&symbols, Some("Octets"), "fromList([200])")); + assert!(!discharges_from( + &symbols, + Some("Nibbles"), + "fromList([200])" + )); + assert!(discharges_from(&symbols, Some("Nibbles"), "fromList([15])")); + // Qualified spellings decide the same way from any scope. + assert!(discharges_from(&symbols, None, "Octets.fromList([200])")); + assert!(!discharges_from(&symbols, None, "Nibbles.fromList([200])")); } #[test] - fn a_bare_spelling_shared_by_two_refinements_is_fail_closed() { - // Two recognized constructors with the same bare name: the - // qualified spellings still decide, the bare one denotes neither. + fn two_constructors_collapsed_onto_one_identity_are_fail_closed() { + // One module declaring `fromList` twice: the symbol table keys one + // `FnKey` to one `FnId`, so no call site can denote one refinement + // without denoting the other. Neither discharges. let second = r#" record Nibbles values: List @@ -551,14 +685,18 @@ fn fromList(xs: List) -> Result false -> Result.Err("oob") "#; let dep = format!("{OCTETS}{second}"); - let table = table_for(CONSUMER, Some(("Octets", &dep))); - assert_eq!(table.ctors.len(), 2, "expected two recognized constructors"); - assert!(table.discharge("fromList", &[list("[1, 2]")]).is_none()); + let symbols = symbols_for(CONSUMER, &[("Octets", &dep)]); assert!( - table - .discharge("Octets.fromList", &[list("[1, 2]")]) - .is_some() + symbols.literal_refinements().is_empty(), + "a shared identity must retire both constructors, got: {:?}", + symbols.literal_refinements().ctors ); + assert!(!discharges_from(&symbols, None, "Octets.fromList([1, 2])")); + assert!(!discharges_from( + &symbols, + Some("Octets"), + "fromList([1, 2])" + )); } #[test] @@ -574,18 +712,25 @@ record Octets fn go() -> Int 1 "#; - let table = table_for(src, None); - assert!(table.is_empty()); + let symbols = symbols_for(src, &[]); + assert!(symbols.literal_refinements().is_empty()); } #[test] fn addresses_an_entry_scope_refinement_through_the_entry_module_prefix() { - let table = table_for(OCTETS, None); - assert!(table.discharge("Octets.fromList", &[list("[7]")]).is_some()); - assert!( - table - .discharge("Octets.fromList", &[list("[700]")]) - .is_none() - ); + let symbols = symbols_for(OCTETS, &[]); + // The entry file declares `module Octets`, so both the bare and + // the self-qualified spelling resolve to the same entry-scope fn. + assert!(discharges_from( + &symbols, + Some("Octets"), + "Octets.fromList([7])" + )); + assert!(discharges_from(&symbols, Some("Octets"), "fromList([7])")); + assert!(!discharges_from( + &symbols, + Some("Octets"), + "Octets.fromList([700])" + )); } } diff --git a/src/codegen/wasm_gc/view.rs b/src/codegen/wasm_gc/view.rs index 5a31dc3dd..380df0384 100644 --- a/src/codegen/wasm_gc/view.rs +++ b/src/codegen/wasm_gc/view.rs @@ -87,7 +87,19 @@ impl WasmGcLinkedView { /// flattened items carry every dep fn under prefixed names. pub(super) fn build(items: &[TopLevel], fn_defs: &[&FnDef]) -> Result { let symbol_table = SymbolTable::build(items, &[]); - let resolve_ctx = crate::ir::hir::ResolveCtx::new(&symbol_table); + let mut resolve_ctx = crate::ir::hir::ResolveCtx::new(&symbol_table); + // Same current-module context every other resolution site uses + // (`resolve_program`, the Rust and Dafny lifters, `CodegenContext`): + // a program that declares `module Local` may spell its own members + // qualified, and `ResolveCtx::resolve_fn_id` only probes the entry + // scope for `Local.f` when it knows `Local` IS the current module. + // Without this, a self-qualified call resolved to `Unresolved` here + // and lowered to `unreachable` — while every other backend called + // it fine. + resolve_ctx.current_module = items.iter().find_map(|i| match i { + TopLevel::Module(m) => Some(m.name.clone()), + _ => None, + }); let resolved_fn_defs: Vec = fn_defs .iter() .filter_map(|fd| resolve_fn_def_external(&resolve_ctx, fd)) diff --git a/src/ir/hir/resolve.rs b/src/ir/hir/resolve.rs index 66de16ae5..c5a621295 100644 --- a/src/ir/hir/resolve.rs +++ b/src/ir/hir/resolve.rs @@ -383,10 +383,17 @@ fn resolve_expr(ctx: &ResolveCtx<'_>, expr: &Spanned) -> ResolvedExpr { // typechecker's discharge rule reads // (`SymbolTable::literal_refinements`), and it keys on the // refinement's own proven element interval, never on a name. - // Every spelling that denotes the constructor decides alike: - // this resolver also runs over a FLATTENED wasm-gc compile - // unit, where the qualified and in-module spellings have - // already collapsed into one prefixed bare name. + // + // INVARIANT: the discharge and ordinary name resolution must + // agree on the callee, or the discharge declines. That is why + // the key is `resolved_callee` — the identity THIS resolver + // just picked — and not the callee's spelling. A spelling key + // would rewrite an entry module's own `fn fromList(…) -> Int` + // into a carrier construction while the checker, obeying + // Aver's shadowing rule, types the same call as `Int`. It also + // survives the wasm-gc flatten for free: the flattened compile + // unit is re-resolved against a rebuilt symbol table, so the + // renamed call sites resolve to the renamed constructor. // // Why a construct site rather than a call to the constructor: // `RecordCreate` is total on every backend and needs no new IR @@ -395,11 +402,20 @@ fn resolve_expr(ctx: &ResolveCtx<'_>, expr: &Spanned) -> ResolvedExpr { // exists — `proof_lower::multi_field_record_demotions` treats a // construct site whose every field is a literal inside the // proven interval as exactly as gated as the smart constructor. - // The rewrite runs on resolved HIR, so the AST-walking demotion - // scans still see only the smart-constructor call. + // + // What makes that safe is NOT that the demotion scans vet this + // node: they walk the AST, and this `RecordCreate` is HIR the + // resolver synthesises afterwards, so they never see it at all. + // Safety rests on the SHARED DERIVED INTERVAL. The discharge + // admits an element only if + // `packed_sequence::element_interval_from_predicate` — the very + // function the packed layout's own bound is derived from — + // proves it in range. "This literal discharges" and "the packed + // carrier can store this literal" are therefore one predicate, + // not two that happen to agree today. let mut resolved_args = resolved_args; - if let Some(dotted) = expr_to_dotted_name(&callee.node) - && let Some(ctor) = ctx.symbols.literal_refinements().discharge(&dotted, args) + if let ResolvedCallee::Fn(fn_id) = &resolved_callee + && let Some(ctor) = ctx.symbols.literal_refinements().discharge(*fn_id, args) && resolved_args.len() == 1 { let key = match ctor.scope.as_deref() { @@ -557,7 +573,12 @@ fn resolve_pattern(ctx: &ResolveCtx<'_>, pat: &Pattern) -> ResolvedPattern { /// `buffer_build`; `LocalSlot` for first-class fn values; the /// `Unresolved` passthrough for anything else (typechecker already /// reported it). -fn classify_callee(ctx: &ResolveCtx<'_>, callee: &Spanned) -> ResolvedCallee { +/// +/// `pub(crate)` so the self-host discharge scan +/// ([`crate::analysis::literal_refinement::discharge_sites`]) can ask +/// this exact function which fn a callee denotes, rather than +/// re-deriving it and risking a different answer than the rewrite below. +pub(crate) fn classify_callee(ctx: &ResolveCtx<'_>, callee: &Spanned) -> ResolvedCallee { match &callee.node { Expr::Resolved { slot, diff --git a/src/main/commands.rs b/src/main/commands.rs index 917698206..589b265a6 100644 --- a/src/main/commands.rs +++ b/src/main/commands.rs @@ -1293,7 +1293,7 @@ pub(super) fn reject_literal_refinement_discharge( items: &[TopLevel], module_root: Option<&str>, ) -> Result<(), String> { - use aver::analysis::literal_refinement::{LiteralRefinementTable, discharge_sites}; + use aver::analysis::literal_refinement::discharge_sites; let loaded = module_root .and_then(|base| { @@ -1331,12 +1331,25 @@ pub(super) fn reject_literal_refinement_discharge( analysis: None, }) .collect(); + // `SymbolTable::build` already derives the refinement table (and the + // scan resolves callee identities against this same table anyway), so + // there is nothing left to recompute here. let symbols = aver::ir::SymbolTable::build(items, &dep_modules); - let table = LiteralRefinementTable::build(items, &dep_modules, &symbols); - let mut sites = discharge_sites(&table, items); + // Entry items resolve under their DECLARED module name (that is what + // `resolve_program` sets), dep items under the prefix the symbol table + // indexed them by. Same context as the rewrite, same answers. + let entry_scope = items.iter().find_map(|item| match item { + TopLevel::Module(m) => Some(m.name.clone()), + _ => None, + }); + let mut sites = discharge_sites(&symbols, entry_scope.as_deref(), items); for module in &loaded { - sites.extend(discharge_sites(&table, &module.items)); + sites.extend(discharge_sites( + &symbols, + Some(&module.dep_name), + &module.items, + )); } if sites.is_empty() { return Ok(()); diff --git a/src/types/checker/infer/expr.rs b/src/types/checker/infer/expr.rs index e79a48c88..0d165477a 100644 --- a/src/types/checker/infer/expr.rs +++ b/src/types/checker/infer/expr.rs @@ -653,20 +653,28 @@ impl TypeChecker { }; if let Expr::Ident(name) = &fn_expr.node { - if let Some(sig) = self.find_fn_sig(name).cloned() { + if let Some((resolved_id, sig)) = self + .find_fn_sig_resolved(name) + .map(|(id, sig)| (id, sig.clone())) + { // Literal smart-constructor discharge, bare-callee // seam — see the qualified seam below for the rule. - // A module's own unqualified call to its recognized - // constructor must decide exactly as the qualified - // spelling does: the wasm-gc backend flattens both - // to one prefixed bare name before re-resolving, so - // a seam that discharged only one of them would fork - // the checked and unchecked pipelines. - let discharged = self - .symbol_table - .literal_refinements() - .discharge(name, args) - .is_some(); + // + // INVARIANT: the discharge and the normal resolution + // must agree on the callee, or the discharge + // declines. `resolved_id` is the identity the very + // lookup that produced `sig` settled on, so an entry + // module's own `fn fromList(…)` — which shadows the + // stdlib constructor under Aver's pinned shadowing + // rule — keeps its own signature here AND is left + // alone by the HIR rewrite, which keys on the same + // identity. + let discharged = resolved_id.is_some_and(|id| { + self.symbol_table + .literal_refinements() + .discharge(id, args) + .is_some() + }); let ret = check_call(self, name, sig); validate_special_call(self, name, args); if discharged && let Type::Result(payload, _) = ret { @@ -802,12 +810,21 @@ impl TypeChecker { // and "storable in the packed carrier" are the same // predicate. The HIR resolver applies the identical rule // to the identical shape. - if self - .symbol_table - .literal_refinements() - .discharge(&display_name, args) - .is_some() - && let Some(sig) = self.find_fn_sig(&display_name).cloned() + // + // INVARIANT: the discharge and the normal resolution + // must agree on the callee, or the discharge declines. + // The identity comes out of the same lookup as the + // signature the call is then checked against, so a + // qualified name that resolves to some other function + // cannot be discharged as this one. + if let Some((Some(resolved_id), sig)) = self + .find_fn_sig_resolved(&display_name) + .map(|(id, sig)| (id, sig.clone())) + && self + .symbol_table + .literal_refinements() + .discharge(resolved_id, args) + .is_some() { // Keep the standard arity/arg-type checks; only the // return type is discharged, and it is taken from diff --git a/src/types/checker/mod.rs b/src/types/checker/mod.rs index e57045fc5..8b76115d4 100644 --- a/src/types/checker/mod.rs +++ b/src/types/checker/mod.rs @@ -981,6 +981,22 @@ impl TypeChecker { // -- Unified lookups --------------------------------------------------- fn find_fn_sig(&self, key: &str) -> Option<&FnSig> { + self.find_fn_sig_resolved(key).map(|(_, sig)| sig) + } + + /// [`Self::find_fn_sig`] plus the resolved user-fn identity the + /// signature came from. + /// + /// The `FnId` is `Some` EXACTLY when the returned signature is the one + /// `fn_sigs[id]` holds — i.e. when the reference resolved to a + /// program-declared function. Builtin and constructor signatures come + /// out of `extra_sigs`, which has no identity, so they answer `None`. + /// + /// Callers that key a rewrite on "which function is this really" must + /// use this and not re-resolve the name themselves: the whole point is + /// that the identity and the signature the call is checked against are + /// produced by one lookup and therefore cannot disagree. + pub(crate) fn find_fn_sig_resolved(&self, key: &str) -> Option<(Option, &FnSig)> { // Phase B: user fns live in `fn_sigs` keyed by `FnId`; everything // else (builtins + sum-type variant constructors) stays in // `extra_sigs`. Direct hit on `extra_sigs` covers references that @@ -989,16 +1005,16 @@ impl TypeChecker { if let Some(id) = self.resolve_fn_id(key) && let Some(sig) = self.fn_sigs.get(&id) { - return Some(sig); + return Some((Some(id), sig)); } if let Some(sig) = self.extra_sigs.get(key) { - return Some(sig); + return Some((None, sig)); } // Try canonicalised form for type-derived keys // (`"Module.Type.Variant"`). let canonical = self.canonical_extra_key(key); if canonical != key { - return self.extra_sigs.get(&canonical); + return self.extra_sigs.get(&canonical).map(|sig| (None, sig)); } None } diff --git a/tests/cross_backend_stress.rs b/tests/cross_backend_stress.rs index 908256dc3..791d4864f 100644 --- a/tests/cross_backend_stress.rs +++ b/tests/cross_backend_stress.rs @@ -637,6 +637,116 @@ fn cross_literal_refinement_discharge_rejected_by_self_host() { ); } +#[test] +fn cross_literal_refinement_discharge_rejected_by_self_host_replay() { + // Same refusal, second entrance. `aver replay --self-host` reaches the + // guest through `run_self_host_replay`, not through `cmd_run_self_hosted` + // — a separate call site of `reject_literal_refinement_discharge` that + // the `aver run --self-host` test above cannot cover. Replay is where a + // silent divergence would be worst: the recording pins the HOST's effect + // trace, so a guest that rebuilt a `Result` would either mismatch far + // from the cause or, if the discharged value never reaches an effect, + // report a clean replay of a program it executed differently. + // + // The gate runs before the cached self-host binary is even looked up, + // so this test does not depend on that binary existing. + let repo_root = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + let aver_bin = env!("CARGO_BIN_EXE_aver"); + let path = temp_module("aver-cross-litref-replay", LITERAL_REFINEMENT_SRC); + let module_root = path.parent().expect("temp module has parent"); + let rec_dir = module_root.join("recordings"); + + // Record on the VM, which runs the discharged program happily. + let record = Command::new(aver_bin) + .current_dir(&repo_root) + .arg("run") + .arg(&path) + .arg("--module-root") + .arg(module_root) + .arg("--record") + .arg(&rec_dir) + .output() + .expect("expected `aver run --record` to execute"); + assert!( + record.status.success(), + "VM record run of a discharged program must succeed:\n{}", + format_output(&record) + ); + + let out = Command::new(aver_bin) + .current_dir(&repo_root) + .arg("replay") + .arg(&rec_dir) + .arg("--self-host") + .arg("--test") + .output() + .expect("expected `aver replay --self-host` to execute"); + cleanup(&path); + let combined = format!( + "{}{}", + String::from_utf8_lossy(&out.stdout), + String::from_utf8_lossy(&out.stderr) + ); + assert!( + !out.status.success(), + "self-host replay must REFUSE a discharged program, not replay it:\n{combined}" + ); + assert!( + combined.contains("does not support the literal smart-constructor discharge"), + "self-host replay refusal must name the rule:\n{combined}" + ); + assert!( + combined.contains("Local.fromList"), + "self-host replay refusal must name the offending call sites:\n{combined}" + ); +} + +// ─── Local shadowing of a recognized smart constructor ────────────────── +// +// A module declaring its own `fromList` shadows the dependency's +// recognized constructor. The checker types the call as the LOCAL fn's +// return type (pinned in `tests/typechecker_spec.rs`), so every backend +// must EXECUTE the local fn too. Keying the discharge on a callee +// spelling broke exactly this: the checker said `Int`, the HIR resolver +// rewrote the body to a `Bytes` carrier construction, and the VM printed +// `Bytes(values: [1, 2, 3])` where the program asked for a length. +// +// The last line keeps the dependency's constructor discharging in the +// SAME program, so a fix that simply switched the whole rule off would +// not pass either. + +const SHADOWED_CTOR_SRC: &str = r#"module Local + depends [Bytes] + +fn fromList(xs: List) -> Int + List.len(xs) + +fn main() + ! [Console.print] + Console.print(String.fromInt(fromList([1, 2, 3]))) + Console.print(String.fromInt(fromList([]))) + Console.print(Bytes.toHex(Bytes.fromList([0, 10, 255]))) +"#; +const SHADOWED_CTOR_OUT: &str = "3\n0\n000aff"; + +#[test] +fn cross_shadowed_smart_constructor_runs_the_local_fn_vm() { + assert_eq_with_label( + "VM", + &run_vm("aver-cross-shadowctor-vm", SHADOWED_CTOR_SRC), + SHADOWED_CTOR_OUT, + ); +} + +#[test] +fn cross_shadowed_smart_constructor_runs_the_local_fn_wasm_gc() { + assert_eq_with_label( + "wasm-gc", + &run_wasm_gc("aver-cross-shadowctor-wasmgc", SHADOWED_CTOR_SRC), + SHADOWED_CTOR_OUT, + ); +} + // ─── Verify cross-target ──────────────────────────────────────────────── // // `aver verify` and `aver verify --wasm-gc` evaluate the same verify diff --git a/tests/fixtures/discharged_bytes_law.av b/tests/fixtures/discharged_bytes_law.av index 4f5eaa3bc..e31755250 100644 --- a/tests/fixtures/discharged_bytes_law.av +++ b/tests/fixtures/discharged_bytes_law.av @@ -1,8 +1,8 @@ module DischargedBytesLaw intent = - "Laws and examples over literal smart-constructor discharge, on both proof backends. `Bytes.fromList([0, 10, 255])` types as plain `Bytes` because every element is an integer literal inside the interval the `Bytes` refinement itself proves, so the call constructs the carrier directly instead of returning `Result`. In Lean that lands as a `Subtype` construction whose obligation is `Bytes.allInRange [0, 10, 255] = true` — the discharge gate's own claim, re-established by the kernel rather than assumed; `allInRange` is compiled by well-founded recursion, which `decide` cannot evaluate through the elaborator, so the obligation is closed by the emitted `simp [Bytes.allInRange]` rung. In Dafny the construction collapses to the bare carrier and the subset-type constraint is discharged at the use site by unfolding the same recursive predicate over a literal sequence. Coverage: a three-element frame, the vacuous empty frame, and `dynamicOctetCount`, which keeps the `Result` path because its argument is computed — the emission-correctness pin, since the file only builds if the discharged calls became direct constructions WHILE the computed one stayed a fallible call in the same program. The long-literal stress case lives in `discharged_bytes_long_literal.av`, which is Lean-only: Dafny's default function fuel does not unfold a 32-element sequence through the recursive predicate." + "Laws and examples over literal smart-constructor discharge, on both proof backends. `Bytes.fromList([0, 10, 255])` types as plain `Bytes` because every element is an integer literal inside the interval the `Bytes` refinement itself proves, so the call constructs the carrier directly instead of returning `Result`. In Lean that lands as a `Subtype` construction whose obligation is `Bytes.allInRange [0, 10, 255] = true` — the discharge gate's own claim, re-established by the kernel rather than assumed; `allInRange` is compiled by well-founded recursion, which `decide` cannot evaluate through the elaborator, so the obligation is closed by the emitted `simp [Bytes.allInRange]` rung. In Dafny the construction collapses to the bare carrier and the subset-type constraint is discharged at the use site by unfolding the same recursive predicate over a literal sequence. Coverage: a three-element frame, the vacuous empty frame, and `dynamicOctetCount`, which keeps the `Result` path because its argument is computed — the emission-correctness pin, since the file only builds if the discharged calls became direct constructions WHILE the computed one stayed a fallible call in the same program. `frameOctets` tightens that pin to a SINGLE body: one branch constructs the carrier from an all-literal list, the other matches on the fallible constructor over a computed one-element list, and the file does not even typecheck unless the two calls got different types. Its law is the theorem obligation over that body — proving the literal branch reduces to the frame's own octets, universally in the computed value, on both backends. The long-literal stress case lives in `discharged_bytes_long_literal.av`, which is Lean-only: Dafny's default function fuel does not unfold a 32-element sequence through the recursive predicate." depends [Bytes] - exposes [octetCount, literalFrame, emptyFrame, dynamicOctetCount, framesAgree] + exposes [octetCount, literalFrame, emptyFrame, dynamicOctetCount, framesAgree, frameOctets] effects [] fn literalFrame() -> Bytes @@ -26,6 +26,14 @@ fn framesAgree(bytes: Bytes) -> Bool ? "Whether a frame carries the same octets as the literal three-octet frame." Bytes.toList(bytes) == Bytes.toList(literalFrame()) +fn frameOctets(mode: Int, value: Int) -> Result, String> + ? "The literal frame's octets, or a one-octet frame built from a computed value." + match mode == 0 + true -> Result.Ok(Bytes.toList(Bytes.fromList([0, 10, 255]))) + false -> match Bytes.fromList([value]) + Result.Ok(other) -> Result.Ok(Bytes.toList(other)) + Result.Err(message) -> Result.Err(message) + verify literalFrame Bytes.toHex(literalFrame()) => "000aff" octetCount(literalFrame()) => 3 @@ -41,3 +49,7 @@ verify dynamicOctetCount verify framesAgree law literalFrameIsItsOwnOctets given n: Int = 0..2 framesAgree(literalFrame()) => true + +verify frameOctets law literalFrameIsIndependentOfTheComputedFrame + given n: Int = 0..2 + frameOctets(0, n) => Result.Ok([0, 10, 255]) diff --git a/tests/proof_spec/builds.rs b/tests/proof_spec/builds.rs index 6be932824..24d5ae30c 100644 --- a/tests/proof_spec/builds.rs +++ b/tests/proof_spec/builds.rs @@ -861,6 +861,15 @@ fn proof_export_builds_discharged_bytes_law_when_lake_is_available() { // the `Result` path: the file only builds if the discharged calls // became direct constructions WHILE the computed-argument call stayed // fallible. + // + // `frameOctets` puts both in ONE body and carries the law + // `literalFrameIsIndependentOfTheComputedFrame` — a single theorem + // obligation, universal in the computed value, over a body whose + // literal branch is a direct construction and whose other branch + // matches on the fallible constructor. Both must be true of the same + // body at once for it to close (and, upstream of the prover, for the + // file to typecheck at all: a `Result` pattern over a non-`Result` + // subject is an error). assert_proof_builds( "tests/fixtures/discharged_bytes_law.av", "aver-proof-discharged-bytes-law", @@ -891,7 +900,10 @@ fn proof_dafny_verifies_discharged_bytes_law_when_dafny_is_available() { // the bare carrier there, so `Bytes.fromList([0, 10, 255])` becomes the // literal sequence and Dafny must discharge the subset-type constraint // `allInRange(xs)` at the use site by unfolding the same recursive - // predicate the Lean obligation names. + // predicate the Lean obligation names. Includes the mixed-body law + // `frameOctets.literalFrameIsIndependentOfTheComputedFrame`, which + // Dafny closes as a lemma over the same one body that holds a + // discharged construction and a fallible call side by side. assert_dafny_verifies( "tests/fixtures/discharged_bytes_law.av", "aver-dafny-discharged-bytes-law", diff --git a/tests/typechecker_spec.rs b/tests/typechecker_spec.rs index ce3ef6a06..4dfd08e19 100644 --- a/tests/typechecker_spec.rs +++ b/tests/typechecker_spec.rs @@ -1873,6 +1873,143 @@ fn literal_bytes_discharge_boundary_needs_a_recognized_smart_constructor() { assert_no_errors(src); } +// ─── The discharge is keyed on RESOLVED IDENTITY, not on the spelling ─── +// +// Aver's shadowing rule is pinned above by +// `entry_local_fn_shadows_dep_module_bare_alias`: a bare call inside an +// entry module that declares its own `doit` means the entry's own `doit`, +// not the dependency's. The discharge must obey the SAME resolution — it +// may fire only when the callee the checker resolved IS the recognized +// smart constructor. Otherwise the checked type and the lowered IR +// disagree about which function ran, which is a miscompilation, not a +// missed optimisation. See `src/analysis/literal_refinement.rs`. + +/// Entry program with `depends [Bytes]` that declares its own `fromList` +/// with the given signature and body, plus one caller fn. +fn shadowing_from_list_program( + local_signature: &str, + local_body: &str, + caller_signature: &str, + caller_body: &str, +) -> String { + format!( + "module Prog\n intent = \"a local fromList shadowing the recognized constructor\"\n depends [Bytes]\n effects []\n\n{local_signature}\n ? \"probe\"\n{local_body}\n\n{caller_signature}\n ? \"probe\"\n{caller_body}\n" + ) +} + +#[test] +fn a_local_from_list_returning_int_shadows_the_recognized_constructor() { + // The local fn wins, so the call has type `Int`. A discharge keyed on + // the spelling `fromList` fired here too — the checker kept `Int` only + // because `Int` is not a `Result` to unwrap, while the HIR resolver + // went ahead and rewrote the body to a `Bytes` carrier construction. + // The runtime half of this pin lives in `tests/cross_backend_stress.rs` + // (`cross_shadowed_smart_constructor_runs_the_local_fn_*`), which is + // where that divergence was actually observable. + let clean = shadowing_from_list_program( + "fn fromList(xs: List) -> Int", + " List.len(xs)", + "fn caller() -> Int", + " fromList([0, 10, 255])", + ); + let errs = errors_with_base(&clean, env!("CARGO_MANIFEST_DIR")); + assert!( + errs.is_empty(), + "the local `fromList` must type the call as its own `Int`:\n{clean}\ngot:\n {}", + errs.join("\n ") + ); + + // …and it is NOT the refined type: the call cannot satisfy a `Bytes` + // return, which is what a discharge would have made it do. + let wrong = shadowing_from_list_program( + "fn fromList(xs: List) -> Int", + " List.len(xs)", + "fn caller() -> Bytes", + " fromList([0, 10, 255])", + ); + let errs = errors_with_base(&wrong, env!("CARGO_MANIFEST_DIR")); + assert!( + errs.iter() + .any(|e| e.contains("body returns Int but declared return type is Bytes")), + "expected the local fn's `Int` to clash with a `Bytes` return:\n{wrong}\ngot:\n {}", + if errs.is_empty() { + "".to_string() + } else { + errs.join("\n ") + } + ); + + // The dependency's constructor is untouched: still recognized, still + // discharging under its qualified spelling in the very same program. + let qualified = shadowing_from_list_program( + "fn fromList(xs: List) -> Int", + " List.len(xs)", + "fn caller() -> Bytes", + " Bytes.fromList([0, 10, 255])", + ); + let errs = errors_with_base(&qualified, env!("CARGO_MANIFEST_DIR")); + assert!( + errs.is_empty(), + "the shadowed dependency constructor must still discharge when named:\n{qualified}\ngot:\n {}", + errs.join("\n ") + ); +} + +#[test] +fn a_local_from_list_returning_a_result_keeps_its_own_result() { + // The sharp case. The local fn returns `Result`, so the + // spelling-keyed discharge really did strip the wrapper: the call typed + // as plain `Int` and the `Result` return below was reported as an + // error. The local fn is not a recognized refinement smart constructor + // — it has no refined carrier and no proven interval — so nothing about + // it may be discharged. + let clean = shadowing_from_list_program( + "fn fromList(xs: List) -> Result", + " Result.Ok(List.len(xs))", + "fn caller() -> Result", + " fromList([0, 10, 255])", + ); + let errs = errors_with_base(&clean, env!("CARGO_MANIFEST_DIR")); + assert!( + errs.is_empty(), + "the local `fromList` must keep its own `Result`:\n{clean}\ngot:\n {}", + errs.join("\n ") + ); + + // The `?` operator still applies, which it could not if the call had + // been discharged to the bare payload. + let propagated = shadowing_from_list_program( + "fn fromList(xs: List) -> Result", + " Result.Ok(List.len(xs))", + "fn caller() -> Result", + " n = fromList([0, 10, 255])?\n Result.Ok(n)", + ); + let errs = errors_with_base(&propagated, env!("CARGO_MANIFEST_DIR")); + assert!( + errs.is_empty(), + "`?` must still apply to the local fn's `Result`:\n{propagated}\ngot:\n {}", + errs.join("\n ") + ); + + // And the payload is the local fn's `Int`, not the dependency's `Bytes`. + let wrong = shadowing_from_list_program( + "fn fromList(xs: List) -> Result", + " Result.Ok(List.len(xs))", + "fn caller() -> Result", + " fromList([0, 10, 255])", + ); + let errs = errors_with_base(&wrong, env!("CARGO_MANIFEST_DIR")); + assert!( + errs.iter().any(|e| e.contains("Result")), + "expected the local fn's payload to clash with `Result`:\n{wrong}\ngot:\n {}", + if errs.is_empty() { + "".to_string() + } else { + errs.join("\n ") + } + ); +} + #[test] fn integer_slash_operator_is_a_type_error() { // The bare `/` operator on two Ints is partial (a zero divisor; over ℤ