Type Bytes.fromList with an all-literal in-range list as total

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<Int, String>`; 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
 

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<Int, String>` (Euclidean; `b == 0` → `Result.Err`) and `Int.mod(a, b) : Result<Int, String>` — 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<Int, String>` 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<Int>` 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<Bytes, String>` 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`.

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<Bytes, String>`: 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<Int> -> Result<Bytes, String>` | Validates every octet; `Result.Err` names the offending value and its index |
+| `Bytes.fromList` | `List<Int> -> Result<Bytes, String>` | 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<Int>` | Exposes validated values |
 | `Bytes.fromHex` | `String -> Result<Bytes, String>` | Even length, case-insensitive, no `0x` prefix |
 | `Bytes.toHex` | `Bytes -> String` | Total, lowercase output |

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