Land PRs #14-#16: opaque_ coverage, ELet decode fix, println fix, 334-file harness

.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,18 +101,26 @@ 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
           ref: ${{ steps.setup-march.outputs.march-version }}
           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

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

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