feat: decoder-coverage gate + model Check 6 (a live false accept); MATCH 86→87

.github/workflows/conformance.yml

@@ -27,6 +27,16 @@ name: Conformance
 #     accept-side bug.
 # See those files' headers and the harness's own comments for the full
 # rationale.
+#
+# A third ledger gates a DIFFERENT question, ahead of the harness:
+#   - scripts/decoder-degraded-kinds.txt, enforced by
+#     scripts/decoder-coverage.sh, pins every march AST node "kind" that
+#     MarchLean/Elab.lean does not decode into a real modelled constructor,
+#     and exactly how it degrades. The harness cannot see this: a kind with
+#     no decoder arm just makes the file SKIP, which the harness and the
+#     skip ledger both read as expected. Two of the worst defects here
+#     (ELet, EAnnot) were precisely that, and were found by hand-probing
+#     rather than by CI.
 on:
   push:
     branches: [main]
@@ -134,6 +144,42 @@ jobs:
       - name: Install z3
         run: sudo apt-get install -y z3
 
+      # Decoder-coverage gate. Runs BEFORE the conformance harness on
+      # purpose: it re-checks nothing in Lean (it only runs --emit-core-ast
+      # and compares two sets), so it finishes in a couple of minutes where
+      # the harness takes 15-20, and a decoder gap should surface in that
+      # first couple of minutes rather than at the end of a long run.
+      #
+      # It catches a failure mode the harness structurally CANNOT. When
+      # MarchLean/Elab.lean has no arm for a "kind" march emits, the node
+      # decodes to `Term.unsupported`, `hasUnsupported` goes true, and
+      # march-lean-check honestly exits 2 — a SKIP, which the harness treats
+      # as expected (see its A1/A2 note). The skip ledger then observes only
+      # that the file's skip status is unchanged. Nothing anywhere reports
+      # that the REASON for the skip is a hole in the decoder. That is
+      # exactly how ELet and EAnnot survived: both silently discarded a
+      # child expression and blinded the CapCheck capability walks, and both
+      # were eventually found by hand-probing rather than by CI.
+      #
+      # Same four corpora and the same flag names the harness gets, so the
+      # two can never drift onto different inputs. --histogram prints kind
+      # -> occurrence counts into the log for auditing; it is worth the few
+      # lines, because rarity is the signal here (EAnnot occurs exactly ONCE
+      # across all 334 files, so a corpus sweep is the only thing likely to
+      # witness it). --jobs 4 matches the runner's core count:
+      # --emit-core-ast costs about a second of fixed startup per file
+      # regardless of file size, so the sweep is entirely process-bound and
+      # parallelises linearly.
+      - name: Check decoder coverage
+        run: |
+          scripts/decoder-coverage.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" \
+            --jobs 4 \
+            --histogram
+
       - name: Run conformance harness
         run: |
           scripts/conformance-harness.sh \

MarchLean.lean

@@ -7,3 +7,4 @@ import MarchLean.Infer
 import MarchLean.Compare
 import MarchLean.CapLattice
 import MarchLean.CapCheck
+import MarchLean.KindCoverage

MarchLean/Compare.lean

@@ -234,7 +234,7 @@ terms). A decl's own top-level body is never itself a callee. -/
 def declSpanTys (env : TyEnv) : Decl → List (Span × Ty)
   | .dtype .. => []
   | .dlet _ body => termSpanTys env false body
-  | .dfn _ _ _ body => termSpanTys env false body
+  | .dfn _ _ _ _ body => termSpanTys env false body
   -- A3 Task 2/3 decode-only constructors: no term of their own, so no
   -- `(span, ty)` pairs to contribute. `dmod` is inert-but-unreachable here:
   -- `inferModule` flattens nested `dmod`s via `flattenDecls` before this is

MarchLean/Elab.lean

@@ -617,7 +617,7 @@ carry no name into the value/type namespace); `dmod`'s own decls are walked
 separately by `flattenedBindingNames`, one scope level at a time, so `dmod`
 itself contributes nothing here. -/
 def declBindingName : Decl → Option String
-  | .dfn n _ _ _ => some n
+  | .dfn _ n _ _ _ => some n
   | .dlet n _ => some n
   | .dtype n _ _ => some n
   | .dmod _ _ | .dneeds _ | .duse _ | .dextern _ _ | .dproofcap _ | .dopts _ | .unsupported => none
@@ -652,6 +652,18 @@ partial def decodeDecl (j : Json) : Except String Decl := do
   | "DFn" => do
       let fn ← field j "fn"
       let (name, _) ← decodeName (← field fn "name")
+      -- `fn.vis` — the `fn`/`pfn` marker, emitted as `{"kind":"Public"}` /
+      -- `{"kind":"Private"}` (`ast_json.ml`'s `visibility_to_json`, threaded
+      -- from `fn_def_to_json`). Read ONLY by `CapCheck`'s Check 6, whose
+      -- same-module branch fires exclusively on a PRIVATE fn. Anything other
+      -- than a literal `"Private"` — a missing field, a non-object payload, an
+      -- unrecognised kind string — is treated as PUBLIC, the verdict-free
+      -- value: an unread `vis` can then only cost a Check 6 reject we would
+      -- otherwise have made, never manufacture one.
+      let vis : Vis :=
+        match fn.getObjVal? "vis" >>= (·.getObjVal? "kind") >>= (·.getStr?) with
+        | .ok "Private" => Vis.priv
+        | _ => Vis.pub
       -- The declared return-type annotation (`ret_ty`), decoded as `Option Ty`
       -- (`none` for an unannotated `fn` or a `null` `ret_ty`). A refinement
       -- (`{Int | _ >= 0}` → `TyRefine`), a session channel, or any other
@@ -741,12 +753,12 @@ partial def decodeDecl (j : Json) : Except String Decl := do
                 -- `{"kind":"DLet",...}`) is unaffected — it still decodes via
                 -- the separate `"DLet"` arm below to `Decl.dlet`.
                 let body ← decodeTerm bodyJ
-                .ok (Decl.dfn name [] retTy body)
+                .ok (Decl.dfn vis name [] retTy body)
             | some params =>
                 -- N-ary: carry the whole param list directly (no currying),
                 -- plus the (in-fragment) return annotation for Check 1.
                 let body ← decodeTerm bodyJ
-                .ok (Decl.dfn name params retTy body)
+                .ok (Decl.dfn vis name params retTy body)
       | _ => .ok Decl.unsupported   -- 0 or 2+ clauses: multi-clause fns unsupported
   | "DLet" => do
       let binding ← field j "binding"

MarchLean/Infer.lean

@@ -1028,7 +1028,7 @@ def inferModule' (s : Supply) (m : Module) : InferM (List (Span × MTy)) := do
         let t ← infer s { ctx with level := ctx.level + 1 } rhs
         let sch ← generalize s ctx.level t
         ctx := ctx.addScheme name sch
-    | .dfn name params retAnnot body => do
+    | .dfn _ name params retAnnot body => do
         let lvl := ctx.level + 1
         let recTy ← freshMVar s lvl
         let paramMTys ← params.mapM (fun _ => freshMVar s lvl)
@@ -1388,7 +1388,7 @@ with no unbound-variable throw for `cap_narrow`/`root_cap`. Modeled as a
   let s ← Supply.new
   let capIO : Ty := Ty.con "Cap" [Ty.con "IO" []]
   let capNet : Ty := Ty.con "Cap" [Ty.con "IO.Network" []]
-  let boot : Decl := .dfn "boot" [("root", .unrestricted, some capIO)] (some capNet)
+  let boot : Decl := .dfn .pub "boot" [("root", .unrestricted, some capIO)] (some capNet)
     (Term.app (Term.var "cap_narrow" dSpan dTy) [Term.var "root" dSpan dTy] dTy)
   let m : Module := { decls := [boot], schemes := [], insts := [] }
   match ← (inferModule' s m).run with
@@ -1433,7 +1433,7 @@ treat transparently). This `#eval` has teeth: deleting the `retAnnot` unify
 makes it print `retannot-mismatch-FAIL: accepted`. -/
 #eval show IO Unit from do
   let s ← Supply.new
-  let bad : Decl := .dfn "f" [("n", .unrestricted, some (Ty.con "Int" []))]
+  let bad : Decl := .dfn .pub "f" [("n", .unrestricted, some (Ty.con "Int" []))]
     (some (Ty.con "String" [])) (Term.var "n" dSpan dTy)
   match ← (inferModule' s { decls := [bad], schemes := [], insts := [] }).run with
   | .ok _ => IO.println "retannot-mismatch-FAIL: accepted"
@@ -1444,7 +1444,7 @@ makes it print `retannot-mismatch-FAIL: accepted`. -/
 AGREES with the body still infers cleanly. `fn f(n : Int) : Int do n end`. -/
 #eval show IO Unit from do
   let s ← Supply.new
-  let ok : Decl := .dfn "f" [("n", .unrestricted, some (Ty.con "Int" []))]
+  let ok : Decl := .dfn .pub "f" [("n", .unrestricted, some (Ty.con "Int" []))]
     (some (Ty.con "Int" [])) (Term.var "n" dSpan dTy)
   match ← (inferModule' s { decls := [ok], schemes := [], insts := [] }).run with
   | .ok _ => IO.println "retannot-match-accepted: true"
@@ -1455,7 +1455,7 @@ AGREES with the body still infers cleanly. `fn f(n : Int) : Int do n end`. -/
 so a body of any type still infers. `fn f(n : Int) do n end`. -/
 #eval show IO Unit from do
   let s ← Supply.new
-  let un : Decl := .dfn "f" [("n", .unrestricted, some (Ty.con "Int" []))]
+  let un : Decl := .dfn .pub "f" [("n", .unrestricted, some (Ty.con "Int" []))]
     none (Term.var "n" dSpan dTy)
   match ← (inferModule' s { decls := [un], schemes := [], insts := [] }).run with
   | .ok _ => IO.println "retannot-absent-accepted: true"