diff --git a/.github/workflows/conformance.yml b/.github/workflows/conformance.yml index 211f9b8..cdaf0f1 100644 --- a/.github/workflows/conformance.yml +++ b/.github/workflows/conformance.yml @@ -15,7 +15,11 @@ name: Conformance # independently checks a modeled fragment. Two ledgers keep that honest, # and both are enforced in BOTH directions (a new skip and a stale entry # each fail the run): -# - scripts/expected-skips.txt: the accept- AND reject-side skip sets. +# - scripts/expected-skips.txt: the accept- AND reject-side skip sets, +# across all FOUR swept corpora — specs/lang/types/{accept,reject} +# (--corpus-dir) plus specs/lang/grammar/{parse,reject} and +# specs/lang/golden (--lang-dir). The latter three are directory- +# qualified in the ledger; see that file's PATH FORMAT note. # - scripts/known-limitations.txt: the handful of march=reject files # whose rejection reason is erased before --emit-core-ast (so it is # structurally invisible to a Core-AST checker) and which A2 therefore @@ -97,11 +101,17 @@ jobs: with: march-version: 7c1d701cf561c13ad094845f52175f449e1c1892 - # Only the static-semantics corpus is needed from march's own repo - # (the binary itself came from setup-march above); pinned to the - # exact commit setup-march resolved and built so corpus and binary - # never drift apart. - - name: Checkout march corpus (specs/lang/types) + # Only the conformance corpora are needed from march's own repo (the + # binary itself came from setup-march above); pinned to the exact + # commit setup-march resolved and built so corpus and binary never + # drift apart. + # + # FOUR corpora are swept now, so all four must be fetched: + # specs/lang/types/{accept,reject} (via --corpus-dir) plus + # specs/lang/grammar/{parse,reject} and specs/lang/golden (via + # --lang-dir). If a --lang-dir subdirectory were missing the harness + # exits 1 with an explicit error rather than silently scanning less. + - name: Checkout march corpora (specs/lang) uses: actions/checkout@v4 with: repository: march-language/march @@ -109,6 +119,8 @@ jobs: path: march-checkout sparse-checkout: | specs/lang/types + specs/lang/grammar + specs/lang/golden sparse-checkout-cone-mode: false # z3: the refinement-type conformance corpus (@types-check, i.e. @@ -127,6 +139,7 @@ jobs: scripts/conformance-harness.sh \ --march-bin "$(command -v march)" \ --corpus-dir "$GITHUB_WORKSPACE/march-checkout/specs/lang/types" \ + --lang-dir "$GITHUB_WORKSPACE/march-checkout/specs/lang" \ --march-lean-check-bin "$GITHUB_WORKSPACE/.lake/build/bin/march-lean-check" # Best-effort: publish the built checker as a release asset on tag diff --git a/MarchLean/CapCheck.lean b/MarchLean/CapCheck.lean index d9884a0..22b54ba 100644 --- a/MarchLean/CapCheck.lean +++ b/MarchLean/CapCheck.lean @@ -392,6 +392,18 @@ partial def bodyCalls (banned : List String) : Term → Bool | .match_ scrut arms _ => bodyCalls banned scrut || arms.any (fun (_, g, e) => (g.map (bodyCalls banned)).getD false || bodyCalls banned e) + -- `.opaque_` (`ECond`/`ERecordUpdate`/`EAtom`/`EAssert`/`EDbg`/`ELetFn`/ + -- `ELetQ`/`ESend`/`ESpawn`) RECURSES. Its own shape is unmodelled, but it + -- carries the exact child-expression list march's `calls_in_expr` descends + -- into for those kinds (`typecheck.ml:7734-7750`), and `calls_in_expr` is + -- the shared body-walk behind `check_pure_module`, + -- `check_deterministic_module`, `check_no_panic_module` and Check 8. A + -- banned call inside `match do c -> println("leak") end` or + -- `send(p, unix_time_ms())` must therefore be found HERE — before the skip + -- gate — or the file exits 2 while march exits 1. Recursing costs nothing + -- in false-reject exposure: it can only ever ADD a `true`, i.e. only ever + -- turn a skip into a reject that march also renders. + | .opaque_ children _ => children.any (bodyCalls banned) -- LOAD-BEARING: this arm is safe returning `false` (rather than `true`, -- which would be the conservative choice) ONLY because -- `MarchLeanCheck.lean`'s `run` invokes `CapCheck.checkCaps` BEFORE the @@ -403,6 +415,20 @@ partial def bodyCalls (banned : List String) : Term → Bool -- arm itself reports "no IO here". If the driver is ever reordered so the -- skip gate runs before (or independently of) `checkCaps`, this arm -- becomes a false accept and must be revisited. + -- + -- **That ordering dependency is now DEEPER, not merely inherited.** + -- `Term.opaque_` exists solely to exploit it: the constructor hard-codes + -- `Term.hasUnsupported = true` (so the file still skips, so `Infer` and + -- `Linearity` never judge a construct they have no rules for — the exact + -- mechanism that produced the previous slice's false rejects) WHILE its + -- children stay visible to this walk and its siblings (`bodyAllocates`, + -- `divisionVerdict`, `matchesIn`, `termMentionsAny`). The whole value of + -- the constructor is the window between `checkCaps` and the skip gate. If + -- anyone reorders `MarchLeanCheck.run` so the skip gate precedes (or + -- short-circuits) `checkCaps`, `Term.opaque_` stops detecting ANYTHING — + -- it does not degrade to "conservative", it degrades to silent — and this + -- arm becomes a false accept besides. Reorder the driver only by first + -- deleting `Term.opaque_`. | .unsupported _ => false /-- `bodyCallsIO`, kept as a thin specialisation of `bodyCalls` over @@ -444,6 +470,16 @@ partial def bodyAllocates : Term → Bool | .match_ scrut arms _ => bodyAllocates scrut || arms.any (fun (_, g, e) => (g.map bodyAllocates).getD false || bodyAllocates e) + -- `.opaque_` RECURSES, and contributes NO allocation of its own. Verified + -- against march's `no_alloc.ml` directly: its four allocating arms are + -- `ETuple (_::_)`, `ERecord`, `ECon (_, _::_)` and `ELam` — none of the + -- nine `opaque_` kinds is among them, and `check_expr` has an explicit + -- recurse-only arm for every one (`ELetFn`, `ELetQ`, `ECond`, `ESpawn`, + -- `EAssert`, `EDbg`, `ESend`, `ERecordUpdate`, `EAtom`; + -- `no_alloc.ml:41-63`). Note in particular that march does NOT treat + -- `ERecordUpdate` as an allocation even though it treats `ERecord` as one, + -- so this arm must not answer `true` the way `.record` does. + | .opaque_ children _ => children.any bodyAllocates | .unsupported _ => false /-- Division operators march's own division-safety pass flags @@ -544,6 +580,15 @@ partial def termMentionsAny (names : List String) : Term → Bool | .match_ scrut arms _ => termMentionsAny names scrut || arms.any (fun (_, g, e) => (g.map (termMentionsAny names)).getD false || termMentionsAny names e) + -- `.opaque_` RECURSES. This walk is the DELIBERATELY over-approximate + -- `expr_mentions`, whose only use is to DISCARD a path fact when a name it + -- talks about is rebound; over-approximating loses information (a division + -- goes unproven → skip) instead of inventing a proof. Recursing therefore + -- moves strictly in the safe direction, and matches march, whose + -- `expr_mentions` is itself total over `Ast.expr`. Leaving it at `false` + -- would let a stale guard about an outer `d` survive a rebinding hidden in + -- an `ELetQ`/`ELetFn` child and license a WRONG non-zero proof. + | .opaque_ children _ => children.any (termMentionsAny names) | .unsupported _ => false /-- Drop every path entry whose condition mentions a name in `names` — march's @@ -769,6 +814,17 @@ def divisorVerdict (facts : DivFacts) (path : DivPath) (divisor : Term) : DivVer | .lit _ _ | .app _ _ _ | .lam _ _ _ | .let_ _ _ _ _ _ _ | .letfn _ _ _ _ _ _ _ | .ite _ _ _ _ | .con _ _ _ | .tuple _ _ | .record _ _ | .field _ _ _ _ | .match_ _ _ _ => .divZero + -- `.opaque_` as the DIVISOR ITSELF (`10 / dbg(x)`, `10 / :tag(x)`, ...) + -- stays at "cannot judge", deliberately NOT joined into the `.divZero` + -- row above. All nine kinds really do land in march's arm-4 catch-all + -- today, so rejecting would be right — but this is a JUDGEMENT site, not + -- a collector, and the whole point of this slice is that `opaque_` + -- carries children WITHOUT modelling the node. Answering `unknown` keeps + -- the file's verdict exactly what it was before `opaque_` existed (the + -- enclosing decl's `hasUnsupported` sends it to exit 2 regardless), so + -- the slice adds detection only where it can also justify it. Tightening + -- this to `.divZero` is a separate, separately-verified change. + | .opaque_ _ _ => .unknown -- `.unsupported` is `decodeTerm`'s open catch-all for march `kind`s this -- fragment does not decode — including ones that do not exist yet. Every -- kind it currently covers IS in march's arm 4, but a future one need not @@ -925,6 +981,24 @@ partial def divisionVerdict (facts : DivFacts) (path : DivPath) : Term → DivVe | none => path' ((g.map (divisionVerdict facts' path')).getD .safe).join (divisionVerdict facts' bodyPath e)))) + -- `.opaque_` RECURSES — but with BOTH channels EMPTIED, and that is the + -- load-bearing part of this arm. march's `iter_div_sites` + -- (`division_safety.ml:204-269`) walks all nine kinds too, but it walks + -- them KNOWING their shape: `ELetFn`/`ELetQ` retire the names they bind + -- (`under (n :: lam_param_names ps) body`, `under (pat_binders p) body`) + -- and `ECond` pushes each arm's condition onto `path`. `Term.opaque_` + -- records neither binders nor arm structure, so we cannot reproduce either. + -- Carrying the OUTER facts/path in unchanged would be unsound in the + -- false-REJECT direction: a stale `d = 0` fact surviving into an `ELetFn` + -- body that rebinds `d` would manufacture a `divZero` march never renders. + -- Emptying both channels is conservative on both sides — with no facts a + -- `var` divisor answers `unknown` (skip, never a fabricated reject), and + -- with no path nothing is fabricated as PROVEN non-zero either. What + -- survives is exactly the two judgements march makes unconditionally, with + -- no solver, no refinement escape and no path escape: a literal-zero + -- divisor (arm 1) and a complex divisor (arm 4). So `10 / 0` hidden in a + -- `cond` arm is now the reject march says it is, and nothing else moves. + | .opaque_ children _ => DivVerdict.joinAll (children.map (divisionVerdict [] [])) | .unsupported _ => .safe /-- `no_panic`'s SECOND half (A3 slice (c) Task 3): a non-exhaustive `match` @@ -1268,6 +1342,16 @@ partial def matchesIn : Term → List (Ty × List (Pattern × Option Term × Ter | .match_ scrut arms _ => (scrut.ty, arms) :: (matchesIn scrut ++ arms.flatMap (fun (_, g, e) => (g.map matchesIn).getD [] ++ matchesIn e)) + -- `.opaque_` RECURSES: a pure collector, and a non-exhaustive `match` + -- nested inside a `cond` arm or a `let?` continuation is exactly as much a + -- runtime-panic surface as a top-level one. march agrees — its + -- exhaustiveness diagnostic is recorded by the typechecker's own total + -- expression walk, which visits these nodes, and `check_no_panic_module` + -- then promotes the recorded span to an error. `matchExhaustive` remains + -- the judgement site and remains conservative (unsure ⇒ "exhaustive"), so + -- adding nodes here cannot manufacture a reject on a match this checker + -- cannot actually classify. + | .opaque_ children _ => children.flatMap matchesIn | .unsupported _ => [] /-- Does `t` (a function body) contain any non-exhaustive `match_` at all, @@ -3689,4 +3773,396 @@ def npOrPatternUnderCapStillNonExhaustive : Module := { #eval checkCaps npOrPatternUnderCapStillNonExhaustive -- expect: violation naming no_panic (non-exhaustive) example : (checkCaps npOrPatternUnderCapStillNonExhaustive).isViolation = true := by native_decide +-- --------------------------------------------------------------------- +-- `Term.opaque_`: the nine unmodelled-but-child-carrying march kinds. +-- +-- The 242-file conformance corpus CANNOT regression-test any of this: a +-- census found NO file combining a `cap` directive with a capability +-- violation inside any of these constructors. A green harness run is +-- therefore no evidence at all here, and these hand-built pins are the only +-- coverage. Each fixture reproduces the exact CHILD-LIST ARRANGEMENT +-- `Elab.decodeTerm` produces for that `kind` (see its docstring's table), +-- since that arrangement — not the node's shape, which is not modelled — is +-- the whole contract between the decoder and the cap layer. +-- +-- Every violating shape below was verified end to end against the real +-- march binary: march rejects it naming the capability, and +-- `march --emit-core-ast | march-lean-check` now exits 1 (it exited 2 +-- before `Term.opaque_`). Every non-violating counterpart was verified to be +-- ACCEPTED by march, and must NOT produce a violation here — a `violation` +-- on one of those would be a false reject, the worst error class this +-- oracle has. + +def opqSp : Span := ⟨"o", 0, 0, 0, 0⟩ +def opqUnitTy : Ty := Ty.con "Unit" [] +def opqIntTy : Ty := Ty.con "Int" [] + +/-- `println("x")` — an `IO.Console` builtin, banned under `cap pure`. This is +the violation every `*Violating` fixture below hides inside an `opaque_`. -/ +def opqBanned : Term := + Term.app (Term.var "println" opqSp opqUnitTy) + [Term.lit (Lit.str "x") (Ty.con "String" [])] opqUnitTy + +/-- An inert child: no call, no allocation, no division. -/ +def opqInert : Term := Term.lit (Lit.int 1) opqIntTy + +/-- `mod P do cap pure ... fn f() do end end`. -/ +def opqPureMod (body : Term) : Module := { + decls := [Decl.dmod "P" [Decl.dopts ["pure"], Decl.dfn "f" [] none body]], + schemes := [], insts := [], moduleCaps := [] } + +/-- The invariant the whole design rests on: an `opaque_` node is out of +fragment REGARDLESS of its children, so `Compare.inferModule`'s whole-file +skip gate still fires and `Infer`/`Linearity` never judge it. If this ever +becomes `false`, every one of the nine fixtures below turns into a +false-reject risk. -/ +example : (Term.opaque_ [] opqIntTy).hasUnsupported = true := by native_decide +example : (Term.opaque_ [opqInert] opqIntTy).hasUnsupported = true := by native_decide + +/-- `ECond` — `match do c1 -> println("x") ... end`. Children are the arms +flattened as `cond, body, cond, body, ...`; BOTH halves are expressions and +march's `calls_in_expr` folds both. -/ +def opqCondViolating : Module := opqPureMod + (Term.opaque_ [Term.var "c1" opqSp (Ty.con "Bool" []), opqBanned, + Term.var "c2" opqSp (Ty.con "Bool" []), opqInert] opqIntTy) +#eval checkCaps opqCondViolating -- expect: violation naming `pure` +example : (checkCaps opqCondViolating).isViolation = true := by native_decide + +/-- `ECond` near-miss: same shape, no banned call anywhere. march ACCEPTS. -/ +def opqCondClean : Module := opqPureMod + (Term.opaque_ [Term.var "c1" opqSp (Ty.con "Bool" []), opqInert, + Term.var "c2" opqSp (Ty.con "Bool" []), opqInert] opqIntTy) +#eval checkCaps opqCondClean -- expect: ok +example : (checkCaps opqCondClean).isViolation = false := by native_decide + +/-- `ERecordUpdate` — `{ r with a: println("x") }`. Children are `base` +followed by each field's `value`; the field NAMES carry no expression. -/ +def opqRecordUpdateViolating : Module := opqPureMod + (Term.opaque_ [Term.var "r" opqSp opqIntTy, opqBanned] opqIntTy) +#eval checkCaps opqRecordUpdateViolating -- expect: violation naming `pure` +example : (checkCaps opqRecordUpdateViolating).isViolation = true := by native_decide + +def opqRecordUpdateClean : Module := opqPureMod + (Term.opaque_ [Term.var "r" opqSp opqIntTy, opqInert] opqIntTy) +#eval checkCaps opqRecordUpdateClean -- expect: ok +example : (checkCaps opqRecordUpdateClean).isViolation = false := by native_decide + +/-- `EAtom` — `:tag(println("x"))`. Children are `args`; the atom itself is a +bare string in the envelope, not an expression. -/ +def opqAtomViolating : Module := opqPureMod (Term.opaque_ [opqBanned] opqIntTy) +#eval checkCaps opqAtomViolating -- expect: violation naming `pure` +example : (checkCaps opqAtomViolating).isViolation = true := by native_decide + +def opqAtomClean : Module := opqPureMod (Term.opaque_ [opqInert] opqIntTy) +#eval checkCaps opqAtomClean -- expect: ok +example : (checkCaps opqAtomClean).isViolation = false := by native_decide + +/-- `EAssert` — `assert println("x") > 0`. One child, `expr`. -/ +def opqAssertViolating : Module := opqPureMod + (Term.opaque_ [Term.app (Term.var ">" opqSp (Ty.con "Bool" [])) + [opqBanned, opqInert] (Ty.con "Bool" [])] opqUnitTy) +#eval checkCaps opqAssertViolating -- expect: violation naming `pure` +example : (checkCaps opqAssertViolating).isViolation = true := by native_decide + +def opqAssertClean : Module := opqPureMod + (Term.opaque_ [Term.app (Term.var ">" opqSp (Ty.con "Bool" [])) + [opqInert, opqInert] (Ty.con "Bool" [])] opqUnitTy) +#eval checkCaps opqAssertClean -- expect: ok +example : (checkCaps opqAssertClean).isViolation = false := by native_decide + +/-- `EDbg` — `dbg(println("x"))`. One child when `expr` is present. -/ +def opqDbgViolating : Module := opqPureMod (Term.opaque_ [opqBanned] opqUnitTy) +#eval checkCaps opqDbgViolating -- expect: violation naming `pure` +example : (checkCaps opqDbgViolating).isViolation = true := by native_decide + +/-- `EDbg` with NO expression — bare `dbg()` emits `"expr": null`, which +decodes to an EMPTY child list (march's own `EDbg (None, _)` arm contributes +nothing). Nothing to find, and no decode error either. -/ +def opqDbgNullaryClean : Module := opqPureMod (Term.opaque_ [] opqUnitTy) +#eval checkCaps opqDbgNullaryClean -- expect: ok +example : (checkCaps opqDbgNullaryClean).isViolation = false := by native_decide + +/-- `ELetFn` — a nested `fn g() do println("x") end` inside a block. The child +is `body` ONLY: `params` are `param_to_json` records (name/ty/lin) carrying no +expression, and march's `ELetFn` arm of `calls_in_expr` walks only `body`. -/ +def opqLetFnViolating : Module := opqPureMod (Term.opaque_ [opqBanned] opqIntTy) +#eval checkCaps opqLetFnViolating -- expect: violation naming `pure` +example : (checkCaps opqLetFnViolating).isViolation = true := by native_decide + +def opqLetFnClean : Module := opqPureMod (Term.opaque_ [opqInert] opqIntTy) +#eval checkCaps opqLetFnClean -- expect: ok +example : (checkCaps opqLetFnClean).isViolation = false := by native_decide + +/-- `ELetQ` — `let? v = r` with the banned call in the CONTINUATION. Children +are `value` then `cont`; the pattern binds names but carries no expression. +The `cont` position is the one that matters: parser folding turns the rest of +the enclosing block into it, so most real code puts its work there. -/ +def opqLetQViolating : Module := opqPureMod + (Term.opaque_ [Term.var "r" opqSp opqIntTy, opqBanned] opqIntTy) +#eval checkCaps opqLetQViolating -- expect: violation naming `pure` +example : (checkCaps opqLetQViolating).isViolation = true := by native_decide + +def opqLetQClean : Module := opqPureMod + (Term.opaque_ [Term.var "r" opqSp opqIntTy, opqInert] opqIntTy) +#eval checkCaps opqLetQClean -- expect: ok +example : (checkCaps opqLetQClean).isViolation = false := by native_decide + +/-- `ESend` — `send(p, println("x"))`. Children are `cap` then `msg`. -/ +def opqSendViolating : Module := opqPureMod + (Term.opaque_ [Term.var "p" opqSp opqIntTy, opqBanned] opqUnitTy) +#eval checkCaps opqSendViolating -- expect: violation naming `pure` +example : (checkCaps opqSendViolating).isViolation = true := by native_decide + +def opqSendClean : Module := opqPureMod + (Term.opaque_ [Term.var "p" opqSp opqIntTy, opqInert] opqUnitTy) +#eval checkCaps opqSendClean -- expect: ok +example : (checkCaps opqSendClean).isViolation = false := by native_decide + +/-- `ESpawn` — `spawn()`. One child, `actor`. march additionally +requires that child to be a bare actor name, so in WELL-TYPED code nothing can +hide there; the arm exists because `calls_in_expr` walks it anyway and because +`--emit-core-ast` still emits an AST for a program march rejects. -/ +def opqSpawnViolating : Module := opqPureMod (Term.opaque_ [opqBanned] opqUnitTy) +#eval checkCaps opqSpawnViolating -- expect: violation naming `pure` +example : (checkCaps opqSpawnViolating).isViolation = true := by native_decide + +def opqSpawnClean : Module := opqPureMod + (Term.opaque_ [Term.var "Counter" opqSp opqIntTy] opqUnitTy) +#eval checkCaps opqSpawnClean -- expect: ok +example : (checkCaps opqSpawnClean).isViolation = false := by native_decide + +/-- The other three cap-layer walks reach through `opaque_` too. + +`no_panic` / `divisionVerdict`: a LITERAL-ZERO divisor hidden in an +`opaque_` child is a violation — march's arm 1 errors on it unconditionally, +with no solver, no refinement escape and no path escape, so the emptied +facts/path this arm recurses with cannot cost us the answer. -/ +def opqNoPanicDivZeroInChild : Module := { + decls := [Decl.dmod "NP" [ + Decl.dopts ["no_panic"], + Decl.dfn "f" [] none + (Term.opaque_ [divTerm (Term.lit (Lit.int 10) divIntTy) + (Term.lit (Lit.int 0) divIntTy)] divIntTy)]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps opqNoPanicDivZeroInChild -- expect: violation naming no_panic +example : (checkCaps opqNoPanicDivZeroInChild).isViolation = true := by native_decide + +/-- ...and a NON-zero literal divisor in the same position stays ok. -/ +def opqNoPanicDivNonZeroInChild : Module := { + decls := [Decl.dmod "NP" [ + Decl.dopts ["no_panic"], + Decl.dfn "f" [] none + (Term.opaque_ [divTerm (Term.lit (Lit.int 10) divIntTy) + (Term.lit (Lit.int 2) divIntTy)] divIntTy)]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps opqNoPanicDivNonZeroInChild -- expect: ok +example : (checkCaps opqNoPanicDivNonZeroInChild).isViolation = false := by native_decide + +/-- The emptied-channels choice, pinned. A `let d = 0` fact in scope OUTSIDE +an `opaque_` must NOT be carried into its children: `opaque_` records no +binders, so an `ELetFn`/`ELetQ` child that REBINDS `d` would be judged against +a stale fact and false-reject a program march accepts. `divisionVerdict` +recurses with empty facts AND empty path, so `10 / d` inside the child is an +undischarged variable — `DivVerdict.unknown`, i.e. a SKIP, never a reject. -/ +def opqNoPanicStaleFactNotCarried : Module := { + decls := [Decl.dmod "NP" [ + Decl.dopts ["no_panic"], + Decl.dfn "f" [] none + (Term.let_ "d" Lin.unrestricted none (Term.lit (Lit.int 0) divIntTy) + (Term.opaque_ [divTerm (Term.lit (Lit.int 10) divIntTy) + (Term.var "d" divSp divIntTy)] divIntTy) + divIntTy)]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps opqNoPanicStaleFactNotCarried -- expect: skip, NOT violation +example : (checkCaps opqNoPanicStaleFactNotCarried).isViolation = false := by native_decide +example : (checkCaps opqNoPanicStaleFactNotCarried).isSkip = true := by native_decide + +/-- `no_alloc` / `bodyAllocates`: an allocation NESTED in an `opaque_` child is +found (march's `no_alloc.ml` recurses into all nine kinds)... -/ +def opqNoAllocTupleInChild : Module := { + decls := [Decl.dmod "NA" [ + Decl.dopts ["no_alloc"], + Decl.dfn "f" [] none + (Term.opaque_ [Term.tuple [opqInert, opqInert] (Ty.tuple [opqIntTy, opqIntTy])] + opqIntTy)]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps opqNoAllocTupleInChild -- expect: violation naming no_alloc +example : (checkCaps opqNoAllocTupleInChild).isViolation = true := by native_decide + +/-- ...but the `opaque_` node itself allocates NOTHING. This matters most for +`ERecordUpdate`: march flags `ERecord` as an allocation and does NOT flag +`ERecordUpdate` (`no_alloc.ml:23` vs `:62`), so this arm must not copy +`.record`'s unconditional `true`. -/ +def opqNoAllocNodeItselfIsNotAnAllocation : Module := { + decls := [Decl.dmod "NA" [ + Decl.dopts ["no_alloc"], + Decl.dfn "f" [] none + (Term.opaque_ [Term.var "r" opqSp opqIntTy, opqInert] opqIntTy)]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps opqNoAllocNodeItselfIsNotAnAllocation -- expect: ok +example : (checkCaps opqNoAllocNodeItselfIsNotAnAllocation).isViolation = false := by native_decide + +/-- `no_panic` / `matchesIn`: a non-exhaustive `match` nested inside an +`opaque_` child (e.g. inside a `cond` arm) is as much a runtime-panic surface +as a top-level one, and is reached. -/ +def opqNoPanicNonExhaustiveMatchInChild : Module := { + decls := [ + colorDType, + Decl.dmod "G" [ + Decl.dopts ["no_panic"], + Decl.dfn "describe" [("c", Lin.unrestricted, none)] none + (Term.opaque_ + [Term.match_ (Term.var "c" npSpan colorTy) + [(Pattern.con "Red" [], none, Term.lit (Lit.int 0) opqIntTy)] + opqIntTy] + opqIntTy)]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps opqNoPanicNonExhaustiveMatchInChild -- expect: violation naming no_panic +example : (checkCaps opqNoPanicNonExhaustiveMatchInChild).isViolation = true := by native_decide + +-- --------------------------------------------------------------------- +-- TRAILING `ELet` (a `do` block's last/only statement). +-- +-- ROOT CAUSE these pin: `Elab.decodeTerm` had NO `"ELet"` arm. march's +-- emitter does not wrap a single-statement block in an `EBlock`, and +-- `decodeBlockStmts` hands an `EBlock`'s FINAL element straight back to +-- `decodeTerm` — so a trailing `let` hit the `| _ => Term.unsupported` +-- fallback and its right-hand side was DISCARDED before any walk below ever +-- saw it. Every cap walk went blind at once: `bodyCalls`, `bodyAllocates`, +-- `divisionVerdict` and `matchesIn`. march rejected +-- `fn f() : Unit do let q = println("leak") end`; we exited 2. +-- +-- This was NOT an `opaque_` bug and NOT specific to the app-fn position that +-- surfaced it (`{ p with x: println("leak") }` applied to `()`): `bodyCalls`'s +-- generic `.app fn args` arm was always correct, it just never received a +-- term. The shapes below are what the FIXED decoder now emits, so they pin +-- the contract between decoder and cap layer, not the decoder's own dispatch +-- (that is pinned by the `#eval`s in `Elab`'s `Test` namespace). +-- +-- Every violating fixture was verified end to end against the real march +-- binary (march exit 1 naming the cap; `--emit-core-ast | march-lean-check` +-- exited 2 before this fix and exits 1 after). Every clean counterpart was +-- verified ACCEPTED by march and must NOT produce a violation here. + +/-- A trailing `let` has no continuation, so `decodeTerm`'s `ELet` arm makes +`Term.unsupported` the `let_`'s BODY. That is what keeps `hasUnsupported` +true (the file still skips, `Infer`/`Linearity` still never judge it) while +leaving the RHS on a real `let_` — so `divisionVerdict`'s fact/path +retirement still applies to the bound name, which `opaque_` could not offer. +If this ever becomes `false`, the trailing-let shape stops skipping and every +fixture below turns into a false-reject risk. -/ +def trailingLet (rhs : Term) (ty : Ty) : Term := + Term.let_ "q" Lin.unrestricted none rhs (Term.unsupported ty) ty + +example : (trailingLet opqInert opqIntTy).hasUnsupported = true := by native_decide + +/-- The reported reproducer, exactly: `let q = { p with x: println("leak") }` +as a fn body, where march parses the record-update as the FN of a zero-arg +`EApp`. Two previously-fatal layers at once — the trailing `let` (which used +to drop everything) and the `opaque_` in app-fn position. -/ +def letAppFnOpaqueViolating : Module := opqPureMod + (trailingLet + (Term.app + (Term.opaque_ [Term.var "p" opqSp opqIntTy, opqBanned] opqIntTy) [] opqIntTy) + opqIntTy) +#eval checkCaps letAppFnOpaqueViolating -- expect: violation naming `pure` +example : (checkCaps letAppFnOpaqueViolating).isViolation = true := by native_decide + +/-- Near-miss: same two layers, no banned call. march ACCEPTS — a violation +here would be a false reject. -/ +def letAppFnOpaqueClean : Module := opqPureMod + (trailingLet + (Term.app + (Term.opaque_ [Term.var "p" opqSp opqIntTy, opqInert] opqIntTy) [] opqIntTy) + opqIntTy) +#eval checkCaps letAppFnOpaqueClean -- expect: ok +example : (checkCaps letAppFnOpaqueClean).isViolation = false := by native_decide + +/-- The general case, with no `opaque_` involved at all: a banned call sitting +DIRECTLY in a trailing let's RHS. This is the fixture that shows the bug was +never about the app-fn position. -/ +def letTrailingBannedCall : Module := opqPureMod (trailingLet opqBanned opqUnitTy) +#eval checkCaps letTrailingBannedCall -- expect: violation naming `pure` +example : (checkCaps letTrailingBannedCall).isViolation = true := by native_decide + +/-- Sibling walk `bodyAllocates`: a non-empty tuple in a trailing let's RHS. -/ +def letTrailingAllocates : Module := { + decls := [Decl.dmod "NA" [ + Decl.dopts ["no_alloc"], + Decl.dfn "f" [] none + (trailingLet (Term.tuple [opqInert, opqInert] opqIntTy) opqIntTy)]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps letTrailingAllocates -- expect: violation naming no_alloc +example : (checkCaps letTrailingAllocates).isViolation = true := by native_decide + +/-- Sibling walk `divisionVerdict`: `let q = 10 / 0` as the whole body. -/ +def letTrailingDivZero : Module := { + decls := [Decl.dmod "NP" [ + Decl.dopts ["no_panic"], + Decl.dfn "f" [] none + (trailingLet + (Term.app (Term.var "/" opqSp opqIntTy) + [Term.lit (Lit.int 10) opqIntTy, Term.lit (Lit.int 0) opqIntTy] opqIntTy) + opqIntTy)]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps letTrailingDivZero -- expect: violation naming no_panic +example : (checkCaps letTrailingDivZero).isViolation = true := by native_decide + +/-- Near-miss for the above: `let q = 10 / 2`. march ACCEPTS. -/ +def letTrailingDivNonZero : Module := { + decls := [Decl.dmod "NP" [ + Decl.dopts ["no_panic"], + Decl.dfn "f" [] none + (trailingLet + (Term.app (Term.var "/" opqSp opqIntTy) + [Term.lit (Lit.int 10) opqIntTy, Term.lit (Lit.int 2) opqIntTy] opqIntTy) + opqIntTy)]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps letTrailingDivNonZero -- expect: ok +example : (checkCaps letTrailingDivNonZero).isViolation = false := by native_decide + +/-- Sibling walk `matchesIn`: a non-exhaustive `match` in a trailing let's +RHS. (An `Int` scrutinee would NOT pin this — `matchExhaustive` is +deliberately conservative there and answers "exhaustive"; only a user ADT +whose constructors it can enumerate exercises the walk.) -/ +def letTrailingNonExhaustiveMatch : Module := { + decls := [ + colorDType, + Decl.dmod "G" [ + Decl.dopts ["no_panic"], + Decl.dfn "describe" [("c", Lin.unrestricted, none)] none + (trailingLet + (Term.match_ (Term.var "c" npSpan colorTy) + [(Pattern.con "Red" [], none, Term.lit (Lit.int 0) opqIntTy)] + opqIntTy) + opqIntTy)]], + schemes := [], insts := [], moduleCaps := [] } +#eval checkCaps letTrailingNonExhaustiveMatch -- expect: violation naming no_panic +example : (checkCaps letTrailingNonExhaustiveMatch).isViolation = true := by native_decide + +/-- SEPARATE SIBLING, same class: a NON-`PatVar`/`PatWild` `ELet` binder in +NON-tail position. `decodeBlockStmts` used to answer `Term.unsupported` for +the whole element, throwing away both the RHS and the entire remainder of the +block; it now answers `Term.opaque_ [rhs, rest]`. Verified against march: +`let (a, b) = (println("leak"), 1)` followed by `a` is a reject we skipped. +`opaque_` (not a synthetic `let_ "_"`) is the right carrier here because it +empties `divisionVerdict`'s channels, so a stale fact about a name the +destructuring pattern rebinds cannot manufacture a false reject. -/ +def letDestructuringBinderViolating : Module := opqPureMod + (Term.opaque_ + [Term.tuple [opqBanned, opqInert] opqIntTy, Term.var "a" opqSp opqIntTy] + opqIntTy) +#eval checkCaps letDestructuringBinderViolating -- expect: violation naming `pure` +example : (checkCaps letDestructuringBinderViolating).isViolation = true := by native_decide + +/-- Near-miss for the above: `let (a, b) = (1, 2)` then `a`, under `cap pure`. +march ACCEPTS. (This fixture is `cap pure`, not `no_alloc` — the tuple IS an +allocation, so it would legitimately violate `no_alloc`.) -/ +def letDestructuringBinderClean : Module := opqPureMod + (Term.opaque_ + [Term.tuple [opqInert, opqInert] opqIntTy, Term.var "a" opqSp opqIntTy] + opqIntTy) +#eval checkCaps letDestructuringBinderClean -- expect: ok +example : (checkCaps letDestructuringBinderClean).isViolation = false := by native_decide + end MarchLean.CapCheck diff --git a/MarchLean/Compare.lean b/MarchLean/Compare.lean index 4a0b8b8..e45093e 100644 --- a/MarchLean/Compare.lean +++ b/MarchLean/Compare.lean @@ -218,6 +218,15 @@ partial def termSpanTys (env : TyEnv) (isCallee : Bool) : Term → List (Span × | .match_ scrut arms _ => termSpanTys env false scrut ++ (arms.map (fun (_, _, body) => termSpanTys env false body)).foldl (· ++ ·) [] + -- `.opaque_` is grouped with `.unsupported` and yields NO cross-check + -- targets. This walk runs only inside `inferModule` step (3), i.e. AFTER + -- the step-(1) whole-file skip gate — and `Term.hasUnsupported` hard-codes + -- `true` for `opaque_`, so any module containing one has already returned + -- `.skip`. The arm is unreachable; mirroring `.unsupported` is the choice + -- that provably changes nothing. (Recursing would also be harmless, but it + -- would suggest these spans participate in the resolved_ty cross-check, + -- and they never can: their children are never inferred.) + | .opaque_ _ _ => [] | .unsupported _ => [] /-- `termSpanTys`, dispatched over one declaration (`dtype` carries no diff --git a/MarchLean/Elab.lean b/MarchLean/Elab.lean index 95a7677..fb739df 100644 --- a/MarchLean/Elab.lean +++ b/MarchLean/Elab.lean @@ -278,15 +278,69 @@ mutual /-- Decode an expr node into a `Term`. Every arm reads the node's own `resolved_ty` first (via `decodeResolvedTy`) so it's threaded as `ty` on whichever constructor is produced, including the `unsupported` fallback for -any `kind` not handled below (`ECond`/`EPipe`/`EAnnot`/`EHole`/`EAtom`/ -`ESend`/`ESpawn`/`EResultRef`/`EDbg`/`ELetFn`/`ELetQ`/`EAssert`/`ESigil` — -none of these appear in the 8 real samples; `Term` has a dedicated `letfn` -constructor for a future `ELetFn` decoder, but since no sample exercises it -this task leaves it on the unsupported fallback rather than guessing at an -undertested currying/sequencing shape). `ELet` is handled only via -`decodeBlockStmts` (inside `EBlock`) — it never reaches this dispatch -directly, since march's grammar only produces `ELet` as one element of an -`EBlock`'s expr list. -/ +any `kind` not handled below (`EPipe`/`EAnnot`/`EHole`/`EResultRef`/`ESigil` +— plus, by design, every march `kind` that does not exist yet). `Term` has a +dedicated `letfn` constructor for a future `ELetFn` decoder, but since no +sample exercises it this file does not guess at an undertested +currying/sequencing shape: `ELetFn` decodes to `opaque_` (below) instead. +**`ELet` reaches this dispatch directly, and MUST have an arm here.** An +earlier revision of this docstring asserted the opposite ("march's grammar +only produces `ELet` as one element of an `EBlock`'s expr list"), and that +assertion was FALSE — it cost a whole class of false skips. march's emitter +does not wrap a single-statement `do` block in an `EBlock` at all: a fn body +that is one `ELet` is emitted as a bare `ELet` node, and `decodeBlockStmts` +funnels an `EBlock`'s FINAL element straight back here too (`[last] => +decodeTerm last`). With no `ELet` arm, both shapes fell to the +`| _ => Term.unsupported` fallback at the bottom of this match, DISCARDING the +binding's right-hand side — and with it any `println` / allocation / +`10 / 0` / non-exhaustive `match` hiding in it. march rejected +`fn f() do let q = println("leak") end`; we exited 2. (The narrow symptom +that surfaced this was an `EApp` whose `fn` is an `ERecordUpdate` — but the +app-fn position was a red herring: `bodyCalls`'s generic `.app fn args` arm +was always correct, it simply never got a term to walk.) + +A trailing `ELet` has no continuation to be the `Term.let_` body, so this arm +supplies `Term.unsupported` as the body. That keeps the RHS structurally +where every `CapCheck` walk already expects it (a real `let_`, so +`divisionVerdict`'s fact/path retirement still applies to the bound name — +unlike `opaque_`, which must empty both channels) while `hasUnsupported` +stays `true` through the unsupported body, so `Compare.inferModule`'s step-(1) +skip gate still fires and `Infer`/`Linearity` never judge the node. A +non-`PatVar`/`PatWild` pattern cannot be curried into `Term.let_`'s +plain-`String` binder, so it decodes to `Term.opaque_ [rhs]` instead: still +cap-transparent, still out of fragment, and — because `opaque_` empties +`divisionVerdict`'s channels — it cannot let a stale fact about a name the +pattern rebinds manufacture a false reject. + +**The `opaque_` arms.** Nine `kind`s — `ECond`, `ERecordUpdate`, `EAtom`, +`EAssert`, `EDbg`, `ELetFn`, `ELetQ`, `ESend`, `ESpawn` — are still not +modelled, but each can NEST arbitrary sub-expressions, and march's +`calls_in_expr` (`typecheck.ml:7704-7752`) walks into all of them. They +therefore decode to `Term.opaque_ children ty`, carrying exactly the +sub-expression list march's own walk descends into and in march's order, so +`CapCheck`'s cap-layer walks can find a `cap pure`/`deterministic`/ +`no_alloc`/`no_panic` violation hiding inside one. `Term.opaque_` still +reports `hasUnsupported = true`, so nothing else about these files changes — +they still hit the whole-file skip gate. Child fields were read off the +emitter (`lib/dump/ast_json.ml:379-503`), NOT guessed: + +| `kind` | emitter fields | children (march order) | +|-----------------|-----------------------------------|------------------------| +| `ECond` | `arms : [{cond, body}]` | `cond`,`body` per arm, in order (`calls_in_expr`: `calls_in_expr (calls_in_expr a ce) be`) | +| `ERecordUpdate` | `base`, `fields : [{name,value}]` | `base` then each `value` | +| `EAtom` | `atom`, `args` | `args` (`atom` is a bare string) | +| `EAssert` | `expr` | `expr` | +| `EDbg` | `expr` (NULLABLE — `dbg()`) | `[]` when null, else `expr` | +| `ELetFn` | `name`,`params`,`ret_ty`,`body` | `body` only — `params` are `param_to_json` records (`name`/`ty`/`lin`), no exprs, and march's `ELetFn` arm walks only `body` | +| `ELetQ` | `pattern`,`value`,`cont` | `value` then `cont` | +| `ESend` | `cap`, `msg` | `cap` then `msg` | +| `ESpawn` | `actor` | `actor` | + +`EPipe`/`ESigil` are deliberately NOT here: `Desugar` eliminates both before +emission (`lib/desugar/desugar.ml:543-586`, `:733-744`), so arms for them +would be dead code. `EAnnot`/`EHole`/`EResultRef` are also excluded — no +parser production reaches them here, and `EHole`/`EResultRef` are leaves with +no sub-expression a capability could hide in. -/ partial def decodeTerm (j : Json) : Except String Term := do let ty ← decodeResolvedTy j match ← kindOf j with @@ -352,13 +406,86 @@ partial def decodeTerm (j : Json) : Except String Term := do let t ← decodeTerm (← field j "then_") let e ← decodeTerm (← field j "else_") .ok (Term.ite c t e ty) + -- ── The nine `opaque_` kinds (see this function's docstring for the + -- field-by-field emitter correspondence). Shape is NOT modelled; only the + -- child EXPRESSIONS march's `calls_in_expr` walks are carried. + | "ECond" => + -- `arms : [{cond, body}]` — BOTH halves are expressions, and march's + -- `ECond` arm folds `cond` then `body` for each arm in order. + let armsJ ← (← field j "arms").getArr?.mapError (fun _ => "arms") + let kids ← armsJ.toList.mapM (fun a => do + let c ← decodeTerm (← field a "cond") + let b ← decodeTerm (← field a "body") + pure [c, b]) + .ok (Term.opaque_ kids.flatten ty) + | "ERecordUpdate" => + let base ← decodeTerm (← field j "base") + let fsJ ← (← field j "fields").getArr?.mapError (fun _ => "fields") + let vals ← fsJ.toList.mapM (fun f => do decodeTerm (← field f "value")) + .ok (Term.opaque_ (base :: vals) ty) + | "EAtom" => + let argsJ ← (← field j "args").getArr?.mapError (fun _ => "args") + let args ← argsJ.toList.mapM decodeTerm + .ok (Term.opaque_ args ty) + | "EAssert" => + let e ← decodeTerm (← field j "expr") + .ok (Term.opaque_ [e] ty) + | "EDbg" => + -- `dbg()` emits `"expr": null` (`json_opt expr_to_json`); march's own + -- `EDbg (None, _)` arm contributes nothing, so an absent child is an + -- EMPTY child list, not a decode error. + let eJ ← field j "expr" + if eJ.isNull then .ok (Term.opaque_ [] ty) + else do .ok (Term.opaque_ [← decodeTerm eJ] ty) + | "ELetFn" => + -- `params` carry no expressions (`param_to_json` = name/ty/lin) and + -- march's `ELetFn` arm walks only `body`. + let body ← decodeTerm (← field j "body") + .ok (Term.opaque_ [body] ty) + | "ELetQ" => + let value ← decodeTerm (← field j "value") + let cont ← decodeTerm (← field j "cont") + .ok (Term.opaque_ [value, cont] ty) + | "ESend" => + let cap ← decodeTerm (← field j "cap") + let msg ← decodeTerm (← field j "msg") + .ok (Term.opaque_ [cap, msg] ty) + | "ESpawn" => + let actor ← decodeTerm (← field j "actor") + .ok (Term.opaque_ [actor] ty) + -- A TRAILING `ELet` — a `do` block's last (or only) statement. See this + -- function's docstring: this arm's absence silently discarded the binding's + -- RHS, hiding `cap` violations from every `CapCheck` walk at once. + | "ELet" => + let binding ← field j "binding" + let patJ ← field binding "pattern" + let rhs ← decodeTerm (← field binding "expr") + match ← kindOf patJ with + | "PatVar" => + let (n, _) ← decodeName (← field patJ "name") + let lin ← decodeLin (← field binding "lin") + let annot ← decodeOptAnnot binding + .ok (Term.let_ n lin annot rhs (Term.unsupported ty) ty) + | "PatWild" => + let lin ← decodeLin (← field binding "lin") + let annot ← decodeOptAnnot binding + .ok (Term.let_ "_" lin annot rhs (Term.unsupported ty) ty) + | _ => .ok (Term.opaque_ [rhs] ty) | _ => .ok (Term.unsupported ty) /-- Desugar an `EBlock`'s flat expr list into `Term`'s nested-`let_` shape. -An `ELet` element binds its pattern (must be `PatVar`/`PatWild` — anything -else can't be curried into `Term.let_`'s plain-`String` binder, so the whole -block decodes to `Term.unsupported` rather than misrepresenting the -binding) around the recursively-decoded rest of the block. A non-`ELet` +An `ELet` element binds its pattern around the recursively-decoded rest of +the block. The pattern must be `PatVar`/`PatWild` — anything else can't be +curried into `Term.let_`'s plain-`String` binder, so rather than +misrepresenting the binding the element decodes to +`Term.opaque_ [rhs, rest]`. (It used to decode to a bare +`Term.unsupported blockTy`, which threw away BOTH the binding's RHS and the +entire remainder of the block: `let (a, b) = (println("leak"), 1); a` is a +march reject that we skipped. `opaque_` keeps both children visible to the +`CapCheck` walks while still reporting `hasUnsupported = true`, and — unlike +a synthetic `let_ "_"` — it empties `divisionVerdict`'s fact/path channels, +so a stale fact about a name the destructuring pattern rebinds cannot +manufacture a false reject.) A non-`ELet` statement in non-tail position (e.g. a `print(..)` call whose result is discarded) is sequenced the same way, under a synthetic `"_"` binder — this is the standard let-sequencing encoding of `e; rest`, and is exactly the @@ -384,7 +511,12 @@ partial def decodeBlockStmts (exprs : List Json) (blockTy : Ty) : Except String | "PatWild" => pure (some "_") | _ => pure none : Except String (Option String)) match nameOpt with - | none => .ok (Term.unsupported blockTy) + | none => + -- Out-of-fragment BINDER, not an out-of-fragment block: keep both + -- the RHS and the rest of the block walkable (docstring above). + let rhs ← decodeTerm (← field binding "expr") + let body ← decodeBlockStmts rest blockTy + .ok (Term.opaque_ [rhs, body] blockTy) | some name => let lin ← decodeLin (← field binding "lin") let annot ← decodeOptAnnot binding @@ -963,4 +1095,36 @@ private def collisionEnvelope (nestedName : String) : String := | .ok (some t) => IO.println s!"decoded={repr t}, hasUnsupported={t.hasUnsupported}" -- expect: decoded=Ty.con "Tagged" [Ty.con "Int" [], Ty.con "Realtime" []], hasUnsupported=false +-- A TRAILING `ELet` reaches `decodeTerm` directly (march emits a +-- single-statement `do` block as a bare node, with no `EBlock` wrapper, and +-- `decodeBlockStmts` routes an `EBlock`'s FINAL element back here too) and +-- MUST keep its RHS. Before the `"ELet"` arm existed this fell to +-- `| _ => Term.unsupported`, silently discarding the right-hand side and +-- blinding `bodyCalls`/`bodyAllocates`/`divisionVerdict`/`matchesIn` at once. +-- The `let_`'s BODY is `Term.unsupported` (there is no continuation), which +-- is what keeps `hasUnsupported = true` and the file skipping. +#eval show IO Unit from do + let j := Json.parse r#"{"kind":"ELet","resolved_ty":{"kind":"TCon","name":"Unit","args":[]},"binding":{"pattern":{"kind":"PatVar","name":{"txt":"q","span":{"file":"f","start_line":1,"start_col":1,"end_line":1,"end_col":2}}},"lin":{"kind":"Unrestricted"},"expr":{"kind":"EVar","resolved_ty":{"kind":"TCon","name":"Unit","args":[]},"name":{"txt":"println","span":{"file":"f","start_line":1,"start_col":1,"end_line":1,"end_col":2}}}}}"# + match j with + | .error e => IO.println s!"parse failed: {e}" + | .ok j => + match decodeTerm j with + | .error e => IO.println s!"decode failed: {e}" + | .ok t => IO.println s!"decoded={repr t}, hasUnsupported={t.hasUnsupported}" + -- expect: Term.let_ "q" .. (rhs = Term.var "println" ..) (body = Term.unsupported); + -- hasUnsupported=true + +-- A trailing `ELet` whose pattern is NOT `PatVar`/`PatWild` cannot be curried +-- into `Term.let_`'s plain-`String` binder, so it decodes to +-- `Term.opaque_ [rhs]` — still cap-transparent, still out of fragment. +#eval show IO Unit from do + let j := Json.parse r#"{"kind":"ELet","resolved_ty":{"kind":"TCon","name":"Unit","args":[]},"binding":{"pattern":{"kind":"PatTuple","elements":[]},"lin":{"kind":"Unrestricted"},"expr":{"kind":"EVar","resolved_ty":{"kind":"TCon","name":"Unit","args":[]},"name":{"txt":"println","span":{"file":"f","start_line":1,"start_col":1,"end_line":1,"end_col":2}}}}}"# + match j with + | .error e => IO.println s!"parse failed: {e}" + | .ok j => + match decodeTerm j with + | .error e => IO.println s!"decode failed: {e}" + | .ok t => IO.println s!"decoded={repr t}, hasUnsupported={t.hasUnsupported}" + -- expect: Term.opaque_ [Term.var "println" ..] (Ty.con "Unit" []); hasUnsupported=true + end MarchLean.Elab.Test diff --git a/MarchLean/Infer.lean b/MarchLean/Infer.lean index 122ee37..05ecf3c 100644 --- a/MarchLean/Infer.lean +++ b/MarchLean/Infer.lean @@ -867,6 +867,13 @@ partial def infer (s : Supply) (ctx : Ctx) : Term → InferM MTy let bt ← infer s ctx' body unify s resTy bt pure resTy + -- Both out-of-fragment escapes throw identically. `Term.opaque_` carries its + -- children only so `CapCheck` (which runs BEFORE the skip gate) can walk + -- them; it models NO typing rule of its own, so reaching here would mean the + -- gate at `Compare.inferModule` had failed, and a throw is exactly the loud + -- failure that wants. `Term.hasUnsupported` hard-codes `true` for `opaque_` + -- precisely so this is unreachable. + | .opaque_ _ _ => throw "infer: opaque node (should have been skip-gated)" | .unsupported _ => throw "infer: unsupported node (should have been skip-gated)" /-- Build one poly-1 scheme `∀a[:cls]. build a` by minting a fresh @@ -902,6 +909,11 @@ def builtins (s : Supply) : InferM (List (String × EnvEntry)) := do let cap := fun (t : MTy) => MTy.con "Cap" [t] let capIO := cap (MTy.con "IO" []) out := ("cap_narrow", .scheme (← mkPoly1 s [] (fun a => arr capIO (cap a)))) :: out + -- `println : ∀a. a → ()` — UNCONSTRAINED, and deliberately NOT the + -- `Mono (String → ())` that march's builtin table registers at + -- `typecheck.ml:1951`. See the `println` note below for why march's own + -- effective signature is this one. + out := ("println", .scheme (← mkPoly1 s [] (fun a => arr a u))) :: out pure <| out ++ [ -- The IO capability root, threaded from the entry point. (typecheck.ml:1971) mono "root_cap" capIO, @@ -913,7 +925,13 @@ def builtins (s : Supply) : InferM (List (String × EnvEntry)) := do mono "not" (arr b b), mono "++" (arr str (arr str str)), mono "string_concat" (arr str (arr str str)), mono "string_length" (arr str i), - mono "print" (arr str u), mono "println" (arr str u), + -- `print` is NOT prelude-shadowed (stdlib/prelude.march defines no + -- `fn print`), so it keeps march's builtin `Mono (String → ())` + -- (`typecheck.ml:1950`) — verified directly: `print(1)` is rejected by + -- march with "expected `String` but got `Int`". Ditto `print_int` / + -- `print_float`. `println` is the sole exception and is registered + -- polymorphically above. + mono "print" (arr str u), mono "print_int" (arr i u), mono "print_float" (arr f u), mono "int_to_string" (arr i str), mono "float_to_string" (arr f str), mono "bool_to_string" (arr b str) @@ -937,6 +955,46 @@ def builtins (s : Supply) : InferM (List (String × EnvEntry)) := do -- A real fix needs `println`/`print`/etc. modeled as polymorphic-over-`Show` -- (or some other coverage-gap-safe treatment of builtin-ADT term/pattern -- resolution), which is out of this task's scope. +-- +-- UPDATE (println fix): the `println : String → ()` half of that blocker is +-- GONE — `println` is now `∀a. a → ()` (see the note below), so a bare `None` +-- reaching `println` no longer fails to unify. The `builtinCtorSigs` decision +-- itself is UNCHANGED and still reverted: it was never re-attempted here, and +-- any future attempt must re-verify `accept/t59` and `accept/t86` from scratch +-- rather than assume this note cleared the way. +-- +-- ── Why `println` is `∀a. a → ()` and not `String → ()` ── +-- +-- march's builtin env DOES register `("println", Mono (TArrow (t_string, +-- t_unit)))` (`typecheck.ml:1951`), but that entry is DEAD for any real +-- program: march's stdlib prelude defines a user-level +-- +-- fn println(x) do print(show(x)) ; print("\n") end +-- +-- at `stdlib/prelude.march:243`, and `bin/main.ml:214-217` UNWRAPS +-- prelude.march's `mod` body into the entry module's own top-level scope +-- (prelude.march is the head of `stdlib_file_list`, `bin/main.ml:236`), so +-- this ordinary declaration SHADOWS the builtin binding at every call site. +-- +-- That shadowing binding is `∀a. a → ()` with NO class constraint, not +-- `∀a. Show(a) => a → ()`. march only attaches DECLARED constraints to a +-- function scheme — `bound_constraints` from `fn_bounds` +-- (`typecheck.ml:6926`) and `class_constraints` from a `when` clause +-- (`typecheck.ml:7051`), spliced onto the generalized type at +-- `typecheck.ml:7139-7165`. The `CInterface ("Show", _)` that the body's +-- `show(x)` raises is never captured into the scheme; it goes to +-- `env.pending_constraints` and is discharged at the declaration boundary, +-- where its type is still an unresolved `TVar` and `discharge` takes the +-- `| TVar _ -> () (* Still polymorphic — cannot check yet *)` branch +-- (`typecheck.ml:7530-7531`) and drops it. +-- +-- Verified directly against march (`--check`, exit 0 = accept): `println(1)`, +-- `println(true)`, `println((1, "a"))`, `println({ x: 1, y: 2 })`, +-- `println(Red)` for a `type Color = Red | Green` with NO `impl Show`, and +-- `println(some_fn_name)` ALL accept. A `Show`-constrained scheme modeled here +-- would therefore be a FALSE REJECT source (this checker models no `impl` +-- declarations at all, so every user ADT would look Show-less) — strictly +-- worse than the unconstrained scheme, which can only over-accept. /-- Infer every declaration of a module, returning the `(span, MTy)` record for each `var`/`field` node (Task 6 diffs these against march's computed @@ -1375,5 +1433,93 @@ march rejects the same program for the same reason (typecheck.ml:4684). -/ | .ok _ => IO.println "value-restriction-ok: FALSE (net wrongly polymorphic)" -- expected: value-restriction-ok: true +/-! ### `println` is `∀a. a → ()` (println-of-non-String fixtures) + +Pins the shapes that the `String → ()` signature used to FALSE-REJECT. +march's real `println` comes from `stdlib/prelude.march:243`, shadows the +builtin table's `Mono (String → ())` (`typecheck.ml:1951`), and carries NO +`Show` constraint (see the long note above `inferModule'`). Each fixture below +throws — failing the build — when the shape it pins regresses, so these are +assertions rather than printed observations. + +`native_decide` is not usable for these: `InferM = ExceptT String IO`, so +every `Infer`/`Compare` entry point is `IO`-bound and there is no pure +`Decidable` proposition to discharge. The `native_decide` fixtures in this +repo all live in `Syntax`/`CapCheck`, whose functions are pure. Throwing +`#eval`s are the strongest machine-checked form available here. -/ + +/-- Run `infer` on `println(arg)` and report whether it succeeded. -/ +private def printlnAccepts (arg : Term) : IO Bool := do + let s ← Supply.new + let ctx ← freshCtx s + let call := Term.app (Term.var "println" dSpan dTy) [arg] dTy + match ← (infer s ctx call).run with + | .ok _ => pure true + | .error _ => pure false + +/-- Same, for the non-shadowed `print` (must stay `String → ()`). -/ +private def printAccepts (arg : Term) : IO Bool := do + let s ← Supply.new + let ctx ← freshCtx s + let call := Term.app (Term.var "print" dSpan dTy) [arg] dTy + match ← (infer s ctx call).run with + | .ok _ => pure true + | .error _ => pure false + +private def pin (label : String) (actual expected : Bool) : IO Unit := do + IO.println s!"{label}: {actual}" + if actual != expected then + throw (IO.userError s!"{label}: expected {expected}, got {actual}") + +/- `println(1)`, `println(true)`, `println(1.5)`, `println((1, true))` and +`println("hi")` all accept — exactly march's behaviour (all five verified +directly against `march --check`, exit 0). The first four were the live false +rejects: they produced "cannot unify String with Int|Bool" under the old +monomorphic signature, which is what made all 8 +`specs/lang/grammar/parse/*.march` files reject. -/ +#eval show IO Unit from do + pin "println-int" (← printlnAccepts (Term.lit (Lit.int 1) dTy)) true + pin "println-bool" (← printlnAccepts (Term.lit (Lit.bool true) dTy)) true + pin "println-float" (← printlnAccepts (Term.lit (Lit.float "1.5") dTy)) true + pin "println-string" (← printlnAccepts (Term.lit (Lit.str "hi") dTy)) true + pin "println-tuple" + (← printlnAccepts (Term.tuple [Term.lit (Lit.int 1) dTy, + Term.lit (Lit.bool true) dTy] dTy)) true +-- expected: println-int/bool/float/string/tuple all true + +/- The `println` result is `()` regardless of the argument type — the return +is fixed by the scheme, only the domain is quantified. -/ +#eval show IO Unit from do + let s ← Supply.new + let ctx ← freshCtx s + let call := Term.app (Term.var "println" dSpan dTy) [Term.lit (Lit.int 1) dTy] dTy + match ← (do let t ← infer s ctx call; zonk s t).run with + | .ok t => pin "println-returns-unit" (t matches MTy.tuple []) true + | .error e => throw (IO.userError s!"println-returns-unit-ERROR: {e}") +-- expected: println-returns-unit: true + +/- Two calls at DIFFERENT argument types in one context both succeed — i.e. +`println` really is a scheme that re-instantiates per call site, not a +monomorphic binding that the first call site pins down. -/ +#eval show IO Unit from do + let s ← Supply.new + let ctx ← freshCtx s + let p := fun (a : Term) => Term.app (Term.var "println" dSpan dTy) [a] dTy + let both := Term.tuple [p (Term.lit (Lit.int 1) dTy), + p (Term.lit (Lit.str "hi") dTy)] dTy + match ← (infer s ctx both).run with + | .ok _ => pin "println-two-instantiations" true true + | .error e => throw (IO.userError s!"println-two-instantiations-FAIL: {e}") +-- expected: println-two-instantiations: true + +/- SIBLING BUILTINS — `print` is NOT prelude-shadowed and must stay +`String → ()`. `print(1)` is rejected by march ("expected `String` but got +`Int`", verified directly), so this checker must keep rejecting it too: +widening `print` alongside `println` would be a false ACCEPT. -/ +#eval show IO Unit from do + pin "print-string-accepts" (← printAccepts (Term.lit (Lit.str "hi") dTy)) true + pin "print-int-rejects" (← printAccepts (Term.lit (Lit.int 1) dTy)) false +-- expected: print-string-accepts: true / print-int-rejects: false + end Test end MarchLean.Infer diff --git a/MarchLean/Linearity.lean b/MarchLean/Linearity.lean index 081b02b..20a65d5 100644 --- a/MarchLean/Linearity.lean +++ b/MarchLean/Linearity.lean @@ -87,7 +87,19 @@ partial def uses (name : String) : Term → Nat uses name s + (arms.map (fun (p, g, e) => if (Pattern.boundNames p).contains name then 0 else uses name e + (g.map (uses name)).getD 0)).foldl Nat.max 0 - | .lit _ _ | .unsupported _ => 0 + -- `.opaque_` is grouped with `.unsupported`, NOT recursed into, and the + -- reason is the same for all three linearity walks below: a `Term.opaque_` + -- reports `hasUnsupported = true`, so `Compare.inferModule`'s skip gate + -- returns `.skip` and `MarchLeanCheck.run` exits 2 BEFORE `checkLinearity` + -- is ever called. This walk is unreachable on any module containing one, so + -- the only correct choice is the one that changes nothing — and counting 0 + -- is additionally the SAFE half of the unreachable pair: `opaque_`'s + -- children are an unordered bag with no modelled binder or + -- mutual-exclusivity structure (an `ECond`'s arms are mutually exclusive + -- like a `match_`'s, but nothing here records that), so summing their uses + -- would over-count a linear binder used once per arm into a bogus "used N + -- times" reject. + | .lit _ _ | .opaque_ _ _ | .unsupported _ => 0 /-- The outermost linearity qualifier a type carries (`Ty.lin l _`), else `unrestricted`. march writes a value's linearity either as a binder keyword @@ -142,7 +154,11 @@ partial def capturedInLam (name : String) : Term → Bool capturedInLam name s || arms.any (fun (p, g, e) => if (Pattern.boundNames p).contains name then false else capturedInLam name e || (g.map (capturedInLam name)).getD false) - | .lit _ _ | .var _ _ _ | .unsupported _ => false + -- `.opaque_` with `.unsupported`: unreachable behind the skip gate (see + -- `uses`), and `false` keeps this predicate consistent with `uses`'s 0 — + -- reporting a capture whose use count is not being tracked would flip an + -- unreachable file from its old answer to a `.skip` for no gain. + | .lit _ _ | .var _ _ _ | .opaque_ _ _ | .unsupported _ => false /-- Enforce a binder's linearity given its use count. -/ def enforce (name : String) (l : Lin) (n : Nat) : CheckResult := @@ -199,7 +215,10 @@ partial def checkTerm : Term → CheckResult | none => checkTerm e) | o => o) .ok | o => o - | .lit _ _ | .var _ _ _ | .unsupported _ => .ok + -- `.opaque_` with `.unsupported`: unreachable behind the skip gate (see + -- `uses`). `.ok` is the behavior-preserving answer and cannot mask + -- anything — the file exits 2 before this pass runs either way. + | .lit _ _ | .var _ _ _ | .opaque_ _ _ | .unsupported _ => .ok def checkDecl : Decl → CheckResult | .dfn _ ps _ body => diff --git a/MarchLean/Syntax.lean b/MarchLean/Syntax.lean index beaea3f..422c330 100644 --- a/MarchLean/Syntax.lean +++ b/MarchLean/Syntax.lean @@ -143,6 +143,33 @@ inductive Term where -- march's `check_exhaustiveness` (`typecheck.ml:4546`), which computes -- coverage over the GUARDLESS branches only. | match_ (scrut : Term) (arms : List (Pattern × Option Term × Term)) (ty : Ty) + /-- **Out-of-fragment node that nonetheless CARRIES its child expressions.** + + Decoded (`Elab.decodeTerm`) from the nine march `kind`s whose own shape this + fragment does not model but which can nest ARBITRARY sub-expressions: + `ECond`, `ERecordUpdate`, `EAtom`, `EAssert`, `EDbg`, `ELetFn`, `ELetQ`, + `ESend`, `ESpawn`. march's `calls_in_expr` (`typecheck.ml:7704`) is TOTAL + over `Ast.expr` and descends into every one of them, so a `cap pure` / + `cap deterministic` / `cap no_alloc` / `cap no_panic` violation can hide + inside one. Decoding them to `unsupported` DISCARDED those children, so the + capability layer could not see the violation and the file silently skipped + (exit 2) where march rejected (exit 1). + + `children` is exactly the sub-expression list march's own walk descends + into, in march's order — see each new arm of `Elab.decodeTerm`, keyed field + by field to the emitter (`lib/dump/ast_json.ml`). NOTHING about the node's + own semantics is modelled: not its shape, not its binders, not its + evaluation order, not its arm structure. It is a bag of subterms. + + **`Term.hasUnsupported` is hard-coded `true` for this constructor** (see + below), so a file containing one still trips `Compare.inferModule`'s + whole-file skip gate exactly as `unsupported` does. `Infer` and `Linearity` + therefore NEVER see an `opaque_` node, and this constructor carries ZERO + false-reject exposure: the only pass that can act on it is + `CapCheck.checkCaps`, which `MarchLeanCheck.run` invokes BEFORE that gate. + Named `opaque_` (not `opaque`) because `opaque` is a Lean keyword — same + trailing-underscore convention as `let_`/`match_`/`or_`. -/ + | opaque_ (children : List Term) (ty : Ty) | unsupported (ty : Ty) deriving Repr, Inhabited @@ -150,7 +177,8 @@ inductive Term where def Term.ty : Term → Ty | .lit _ t | .var _ _ t | .app _ _ t | .lam _ _ t | .let_ _ _ _ _ _ t | .letfn _ _ _ _ _ _ t | .ite _ _ _ t | .con _ _ t | .tuple _ t - | .record _ t | .field _ _ _ t | .match_ _ _ t | .unsupported t => t + | .record _ t | .field _ _ _ t | .match_ _ _ t | .opaque_ _ t + | .unsupported t => t /-- Does an optional surface annotation carry an out-of-fragment type? An absent annotation is always in-fragment; a present one is out of fragment iff @@ -163,6 +191,15 @@ def optTyHasUnsupported : Option Ty → Bool /-- Is this term (or any subterm/type) out of fragment? -/ partial def Term.hasUnsupported : Term → Bool | .unsupported _ => true + -- LOAD-BEARING, and deliberately NOT a recursion into `children`: an + -- `opaque_` node is out of fragment BY CONSTRUCTION (its own shape is + -- unmodelled), independent of whether its children happen to be modelled. + -- Hard-coding `true` is what keeps `Compare.inferModule`'s whole-file skip + -- gate firing on exactly the files it fired on before this constructor + -- existed, which is the entire reason carrying the children costs nothing + -- in false-reject exposure. Do not "improve" this to + -- `children.any hasUnsupported`. + | .opaque_ _ _ => true | t => t.ty.hasUnsupported || (match t with diff --git a/scripts/conformance-harness.sh b/scripts/conformance-harness.sh index 60bf5ee..fc2f915 100755 --- a/scripts/conformance-harness.sh +++ b/scripts/conformance-harness.sh @@ -78,6 +78,31 @@ # .lake/build/bin/march-lean-check — NOT `lake exe march-lean-check`, # which re-triggers a build check on every invocation and is far too # slow over a whole corpus). Required. +# --lang-dir PATH (env LANG_DIR) +# Path to march's specs/lang root, enabling the THREE additional +# corpora below on top of --corpus-dir's accept/ + reject/. OPTIONAL: +# omit it and this script scans exactly what it always has (the +# --corpus-dir sweep is untouched either way — the extra corpora are +# purely additive), but the summary then prints +# "EXTRA CORPORA: NOT SCANNED" so the missing coverage is loud rather +# than silent. CI passes it. +# +# specs/lang/grammar/parse accept-side (parse/ ⇒ expect accept) +# specs/lang/grammar/reject reject-side (reject/ ⇒ expect reject) +# specs/lang/golden accept-side (golden/ ⇒ expect accept) +# +# Expected verdict is still derived SOLELY from the file's parent +# directory name (the corpus-violation mechanism — see step 5 above); +# `parse` and `golden` simply join `accept` in the accept-side arm of +# that same case statement, and grammar/reject's own `reject` basename +# already lands in the reject-side arm. Non-*.march files (e.g. +# specs/lang/golden/INDEX.md) are not matched by the glob and so are +# skipped automatically. +# +# Ledger paths for these corpora are directory-qualified +# ("grammar/parse/pNN_….march", "grammar/reject/rNN_….march", +# "golden/gNN_….march") so they never collide with the --corpus-dir +# entries ("accept/…", "reject/…") in scripts/expected-skips.txt. # -h, --help # Print this help and exit 0. # @@ -107,6 +132,7 @@ print_help() { march_bin="${MARCH_BIN:-}" corpus_dir="${CORPUS_DIR:-}" lean_check_bin="${MARCH_LEAN_CHECK_BIN:-}" +lang_dir="${LANG_DIR:-}" while [ $# -gt 0 ]; do case "$1" in @@ -122,6 +148,10 @@ while [ $# -gt 0 ]; do lean_check_bin="$2"; shift 2 ;; --march-lean-check-bin=*) lean_check_bin="${1#--march-lean-check-bin=}"; shift ;; + --lang-dir) + lang_dir="$2"; shift 2 ;; + --lang-dir=*) + lang_dir="${1#--lang-dir=}"; shift ;; -h|--help) print_help; exit 0 ;; *) @@ -151,6 +181,28 @@ if [ ! -d "$corpus_dir/accept" ] || [ ! -d "$corpus_dir/reject" ]; then echo "error: CORPUS_DIR must contain accept/ and reject/ subdirectories: $corpus_dir" >&2 exit 1 fi +# The set of directories to sweep, one "DIR|REL_PREFIX" pair per line. +# REL_PREFIX is what the file's ledger path is built from; the file's own +# parent-directory NAME (not this prefix) is what the expected verdict is +# derived from, exactly as before. +scan_specs="$corpus_dir/accept|accept +$corpus_dir/reject|reject" + +if [ -n "$lang_dir" ]; then + if [ ! -d "$lang_dir" ]; then + echo "error: --lang-dir is not a directory: $lang_dir" >&2 + exit 1 + fi + for extra in grammar/parse grammar/reject golden; do + if [ ! -d "$lang_dir/$extra" ]; then + echo "error: --lang-dir is missing the expected subdirectory $extra: $lang_dir" >&2 + exit 1 + fi + scan_specs="$scan_specs +$lang_dir/$extra|$extra" + done +fi + if ! command -v jq >/dev/null 2>&1; then echo "error: jq is required (used to read the \"verdict\" field out of --emit-core-ast JSON)" >&2 exit 1 @@ -185,20 +237,25 @@ fi json_tmp="$(mktemp)" trap 'rm -f "$json_tmp"' EXIT -for f in "$corpus_dir"/accept/*.march "$corpus_dir"/reject/*.march; do +while IFS='|' read -r scan_dir rel_prefix; do + [ -n "$scan_dir" ] || continue + for f in "$scan_dir"/*.march; do [ -e "$f" ] || continue total=$((total + 1)) # expected_verdict comes solely from the file's parent directory name — - # the corpus's own naming convention (accept/ vs reject/) — independent - # of anything march or Lean report. + # the corpus's own naming convention (accept/ vs reject/, plus grammar's + # parse/ and the golden/ corpus, which are accept-side by the same + # convention) — independent of anything march or Lean report. parent_dir="$(basename "$(dirname "$f")")" case "$parent_dir" in - accept) expected_verdict="accept" ;; + accept|parse|golden) expected_verdict="accept" ;; reject) expected_verdict="reject" ;; *) expected_verdict="unknown" ;; esac - rel_path="$parent_dir/$(basename "$f")" + # Ledger path: directory-qualified by the scan spec's REL_PREFIX so + # grammar/reject/rNN never collides with the types corpus's reject/tNN. + rel_path="$rel_prefix/$(basename "$f")" if "$march_bin" --check "$f" >/dev/null 2>&1; then march_verdict="accept" @@ -258,7 +315,10 @@ for f in "$corpus_dir"/accept/*.march "$corpus_dir"/reject/*.march; do # ledger-tracked (see the ledger-enforcement block after the loop). skip_files="$skip_files$f (lean_verdict=skip, march_verdict=$march_verdict)"$'\n' observed_skip_paths="$observed_skip_paths$rel_path"$'\n' - if [ "$parent_dir" = "accept" ]; then + # Accept-side vs reject-side is the file's EXPECTED verdict (i.e. its + # directory placement), which now covers grammar/parse and golden on + # the accept side and grammar/reject on the reject side. + if [ "$expected_verdict" = "accept" ]; then accept_skip_paths="$accept_skip_paths$rel_path"$'\n' else reject_skip_n=$((reject_skip_n + 1)) @@ -288,7 +348,10 @@ for f in "$corpus_dir"/accept/*.march "$corpus_dir"/reject/*.march; do # above); either way this is intentionally excluded from # match_count. fi -done + done +done < acc` catch-all entirely, so a future constructor fails to +compile here rather than silently falling through the scan again. + +Confirmed converged: `(println("hi"), 1)` under `cap pure` is now rejected by +march AND by `march-lean-check`. The deliberate `bodyCalls` over-detection that +this finding documented is no longer a divergence. + +Note the fix INVERTED the coverage relationship for a while — march's total +walk reached constructs our decoder mapped to `Term.unsupported`, so we skipped +where march rejected. Closed separately by `Term.opaque_` (nine AST kinds) and +by the `ELet` decode fix. + +--- + +## Behavior we DEPEND ON (not a bug): march drops inferred `CInterface` constraints + +**What.** `MarchLean/Infer.lean` registers `println : ∀a. a → ()` — fully +unconstrained. That is deliberately *more permissive* than it looks, and it is +correct only because of a specific march behavior. + +march's builtin `("println", Mono (TArrow (t_string, t_unit)))` +(`typecheck.ml:1951`) is **dead code**. `stdlib/prelude.march:243` defines an +ordinary `fn println(x) do print(show(x)); print("\n") end`, and +`bin/main.ml:214-217` unwraps prelude.march's `mod` body into the entry +module's own top-level scope — it is the head of `stdlib_file_list` +(`bin/main.ml:236`) and the only stdlib file so unwrapped. The prelude binding +therefore shadows the builtin at every call site. + +That prelude scheme is unconstrained. march attaches only *declared* +constraints — `bound_constraints` (`typecheck.ml:6926`) and `when`-clause +`class_constraints` (`typecheck.ml:7051`), spliced at `:7139-7165`. The +`CInterface("Show", _)` raised by the body's `show(x)` lands in +`env.pending_constraints` and is discharged at the declaration boundary while +still a `TVar`, hitting `| TVar _ -> () (* Still polymorphic — cannot check +yet *)` at `typecheck.ml:7530-7531`, and is dropped. + +**Verified** (`march --check`, all exit 0): `println(1)`, `println(true)`, +`println((1,"a"))`, `println({x:1,y:2})`, `println(some_fn_name)`, and +`println(Red)` for a `type Color = Red | Green` with **no `impl Show`**. + +**Why we match it rather than model `Show`.** A `Show`-constrained scheme would +be a NEW false-reject source here: this checker models no `impl` declarations +at all, so no `Show` constraint could ever discharge. Modelling march's actual +(constraint-dropping) behavior is the faithful choice. + +**The fragility.** This is a bug-for-bug match against an *implementation +accident*, not a specified rule. If march ever propagates inferred +`CInterface` constraints into schemes, `println` becomes genuinely +`Show`-constrained and our unconstrained version starts **false-accepting** — +and no corpus file would catch the flip, because every corpus use of `println` +is on a Show-able type. Re-check this at every CI re-pin: if +`typecheck.ml:7530-7531` stops dropping `TVar` constraints, revisit +`Infer.lean`'s `println` registration. + +**Contrast.** `print` is NOT prelude-shadowed (prelude defines no `fn print`), +so it keeps `Mono (String → ())` and march rejects `print(1)`. We match. The +`print`/`println` split is the discriminating pair — pinned by fixture. + +**Status.** not a march bug; no upstream report. Recorded because our +correctness depends on it and the dependency is invisible from our source alone.