Both pre-push lint-gate checks certified in #10 are structurally inert

[andreij6]

Summary

This issue has two parts.

Part one is a correction to issue #10, item 7. That item reviews scripts/lint-ratchet.sh and certifies it: it calls the M0155_BASELINE=0 ratchet "a genuine hard-zero", it vouches for the moc --check errors leg, and it concludes that the gate's "limitations are self-documented and it does not overclaim". Issue #10's audit of the surrounding checks is sound and its framing — that this is the repo's mechanical defence against regressions — is right, which is why the gap matters. But the two legs it specifically certifies do not function:

• Finding 65 — the type-check leg's error pattern (grep -qE ': error') cannot match moc's diagnostic format (: type error [M0057],), and moc's exit code is discarded. Check 1 prints type-check: ok on a tree that does not compile.
• Finding 66 — the M0155 ratchet invokes moc without --implicit-package=core, so the compile aborts on 144 unbound-variable errors before the warning pass. It counts 0 M0155 sites in src/backend/main.mo — a 14,977-line file that holds most of the backend arithmetic — and reports "at baseline". The real count under the build flags is 2.

Correction of an earlier claim, stated up front: an earlier draft of finding 65 asserted that a broken tree is pushed. That is wrong and we are correcting it here rather than repeating it. A genuine compile error is still blocked, by check 4. What actually follows from finding 65 is a misleading status line, degraded diagnostics, and an unintended load-bearing dependency on check 4. Details and proof below.

Part two is three latent correctness defects in the vendored OQL (findings 23, 47, 49). None of them fires in the deployed canister today. They are library bugs that would activate the moment the served-entity or secondary-index path is adopted.

Severity. Part one is developer tooling only; it has no effect on the deployed canister and does not let a broken push through. Its value is narrower and specific: two defences that issue #10 certified as working do not work, so the repo's stated guarantees about them are not currently backed by anything. Part two is latent. Neither part is an emergency.

Found and verified with Claude Opus 5. All line numbers re-checked against the current tree. Both proofs are runnable from the repo root and modify nothing outside a mktemp -d directory.

---

Part one — the pre-push lint gate

Finding 65 — the type-check gate's error pattern can never match moc's output

Where. scripts/lint-ratchet.sh lines 61-72; the predicate is line 64.

# 1) Type-check (main.mo transitively checks the whole backend). moc --check exits
# nonzero on warnings too, so gate on ERRORS only; surface other warnings as info.
TYPE_OUT=$("$MOC" $SRCS --check src/backend/main.mo 2>&1)
if printf '%s\n' "$TYPE_OUT" | grep -qE ': error'; then
  echo "✗ type-check failed (moc --check):" >&2
  printf '%s\n' "$TYPE_OUT" | grep -E ': error' | head -20 >&2
  fail=1
else
  WARN_N=$(printf '%s\n' "$TYPE_OUT" | grep -E ': warning \[M' | grep -v 'M0155' \
           | grep -oE 'src/backend/[^:]+:[0-9]+' | grep -v '/oql/' | sort -u | wc -l | tr -d ' ')
  echo "✓ type-check: ok (${WARN_N} non-M0155 moc warning(s) — run 'mops check' to see them)"
fi

What is wrong. moc emits a hard error as:

<file>:<line>.<col>-<line>.<col>: type error [M0050], literal of type

The literal text is : type error [. The extended regex ': error' requires a space immediately after the colon, so it matches no moc error line — not M0050, not M0057, not any code. The pattern is not merely narrow; it matches nothing moc produces.

Line 63 captures moc's stdout+stderr into TYPE_OUT and discards $?; line 64 tests only the grep. So the exit status — which is the reliable signal here, and which the comment on line 61-62 explicitly reasons about — is never consulted. Check 1 therefore always takes the else branch and always prints type-check: ok.

The same broken pattern is reused on line 66 for the display, so even if the predicate somehow matched, the printed diagnostics would be empty.

Note also that line 69's warning counter (': warning \[M') does match moc's format, so WARN_N is computed correctly — from the output of a compile that aborted early (see finding 66). It under-reports for the same root cause.

Why it matters — and precisely what does not follow.

A broken push is not allowed through. Check 4 (scripts/lint-ratchet.sh lines 103-141) recompiles main.mo with --idl using the correct flags:

if "$MOC" $SRCS --default-persistent-actors --implicit-package=core --idl \
     -o "$DID_TMP/new.wasm" src/backend/main.mo >/dev/null 2>&1 && [ -f "$DID_TMP/new.did" ]; then

That compile fails on a genuine type error, the else branch sets fail=1, and the push is blocked with ✗ candid: could not regenerate the interface (moc --idl failed). We verified this by injecting a type error into a temp copy of src/ — see the proof below.

What does follow is three things:

1. A false status line. The gate prints ✓ type-check: ok on a tree that does not compile. A developer reading the output believes the type-check passed when it did not run to a verdict.
2. Degraded diagnostics. Because the failure surfaces at check 4 instead of check 1, the developer is told could not regenerate the interface (moc --idl failed) — a Candid-freshness message — instead of the actual type error [M0050] ... text moc produced. The --idl compile's own output is sent to /dev/null (line 110), so the real diagnostic is discarded entirely. Diagnosing a compile break from that message requires knowing to re-run moc by hand.
3. Check 4 is load-bearing in a way the design did not intend. It runs only under if [ "$fail" -eq 0 ] (line 106), and its own comment (lines 104-105) states the opposite intent: "The full compile (--idl needs codegen, ~40s) only runs when checks 1-3 passed, so a broken tree fails fast above." Checks 1-3 are what is supposed to catch a broken tree; check 4 is meant to be reached only on a healthy one. Today it is the sole compile-error gate, and it sits behind a condition designed on the assumption that it is not. If a future change causes check 2, 3 or 5 to set fail=1 before it — or reorders the checks, or short-circuits the expensive --idl step — compile errors stop being caught at all. That is the real risk here, and it is a latent one, not a present one.

Proof. Two lines of Motoko in a temp directory, compiled with the repo's pinned moc (1.9.0), then the gate's predicate applied verbatim to that output.

MOC=$(mops toolchain bin moc | tail -1)
TMP=$(mktemp -d)
printf 'module {\n  public func f() : Nat { "not a nat" };\n}\n' > "$TMP/Broken.mo"
RAW=$("$MOC" --check "$TMP/Broken.mo" 2>&1); RC=$?
printf '%s\n' "$RAW"; echo "moc exit code: $RC"
printf '%s\n' "$RAW" | grep -qE ': error' \
  && echo "MATCH -> fail=1" \
  || echo "NO MATCH -> gate prints 'type-check: ok', fail stays 0"
rm -rf "$TMP"

Verbatim output:

MOC=/Users/andrejones/Library/Caches/mops/moc/1.9.0/moc
--- source ---
module {
  public func f() : Nat { "not a nat" };
}
--- moc --check ---
/var/folders/q7/k4g0hx7j4_dbwshfz_t9y6qh0000gn/T/tmp.bXFLhduJX7/Broken.mo:2.27-2.38: type error [M0050], literal of type
  Text
does not have expected type
  Nat
moc exit code: 1
--- gate predicate from lint-ratchet.sh:64, applied verbatim ---
NO MATCH -> gate prints 'type-check: ok', fail stays 0
matching lines: 0

moc exits 1 and says type error [M0050]. The gate's predicate matches zero lines.

Proof that check 4 still blocks (the correction). Same method, but on a full temp copy of src/ with a type error injected into src/backend/lib/SafeMath.mo (imported by main.mo at line 13). Nothing in the repo was touched.

--- tail of the modified SafeMath.mo copy (temp dir only) ---
  };
  public func __injected() : Nat { "not a nat" };
};

--- lint-ratchet.sh check 1 (lines 63-64) on this tree ---
  -> prints 'type-check: ok' (fail stays 0)
--- lint-ratchet.sh check 4 (lines 109-110) on this tree ---
/var/folders/q7/k4g0hx7j4_dbwshfz_t9y6qh0000gn/T/tmp.MA3v6RU5VE/src/backend/lib/SafeMath.mo:25.36-25.47: type error [M0050], literal of type
  moc --idl exit=1  new.did produced: no

Check 1 says ok; check 4 fails and sets fail=1. The push is blocked, with the wrong message.

How to confirm on the current, healthy tree. Run check 1's own command and its predicate against the unmodified repo:

moc diagnostics containing 'type error [M': 146
lines matched by the gate predicate ': error' : 0
GATE -> ✓ type-check: ok (1 non-M0155 moc warning(s) — run 'mops check' to see them)

Both defects are visible in that one line. The gate's own moc invocation produced 146 type errors (finding 66 explains why they are spurious), the predicate matched none of them, and the gate reported ok with a warning count of 1.

Related. proofs/h65-typecheck-gate-never-fails.sh exists in the repo and reproduces the pattern mismatch correctly, but its concluding text ("push ALLOWED", "the gate can never block a push") states the overclaim corrected above. Its final assertion should be narrowed to what it actually demonstrates: that check 1 cannot set fail=1.

---

Finding 66 — the M0155 Nat-subtraction ratchet counts zero for main.mo

Where. scripts/lint-ratchet.sh lines 89-101 (the ratchet), line 90 (the moc invocation), line 44 (M0155_BASELINE=0). Same flagless invocation as line 63.

# 3) M0155 ratchet — count unique sites across our code.
M0155_N=$(for f in $OUR_FILES; do "$MOC" $SRCS --check "$f" 2>&1 | grep 'M0155'; done \
          | grep -oE 'src/backend/[^:]+\.mo:[0-9]+' | grep -v '/oql/' | sort -u | wc -l | tr -d ' ')

What is wrong. mops.toml line 26 declares the flags the backend is actually built with:

[canisters.backend]
main = "src/backend/main.mo"
args = [ "--default-persistent-actors", "--implicit-package=core", "--public-metadata", "candid:service", "--max-stable-pages", "131072" ]

--implicit-package=core is what binds the unqualified module name Fixed. src/backend/main.mo uses Fixed. 187 times and has no import Fixed line — it relies entirely on that flag. Without it, moc aborts on 144 type error [M0057], unbound variable Fixed diagnostics before the warning pass runs, and emits zero M0155 lines for the file.

So the ratchet counts 0 for main.mo, compares against M0155_BASELINE=0, and prints ✓ M0155: 0 (at baseline). The real count under the build flags is 2 — src/backend/main.mo:3696 and src/backend/main.mo:10926:

// main.mo:3696
let otherColl = if (h.collateralUsd > baseLegUsd) { h.collateralUsd - baseLegUsd } else { 0 };

// main.mo:10926
let dev = if (avg > ref) { avg - ref } else { ref - avg };

Both are benign — each subtraction is immediately guarded by the comparison in the surrounding if. That is not the point. The point is that the repo's headline Nat-subtraction defence is structurally blind to the file, and would be equally blind to an unguarded one.

Why it matters. The gate's own header (lines 10-18 and the baseline history at lines 32-40) documents this ratchet as the repo's primary protection against unguarded Nat subtraction, and describes a dedicated 45-site cleanup on 2026-07-09 to reach the hard zero:

#   45 (2026-07-09) — the OQL re-vendor (16c5200) unmasked 24 PRE-EXISTING
#      main.mo sites (blame: 2026-04→06, none new); audited safe.
#    0 (2026-07-09) — all 45 sites resolved (subOrZero for the longhand clamps,
#      explicit `: Nat` for the invariant-backed ones) so the IDE shows no
#      warnings and any new M0155 stands out. Now a hard zero gate.

That cleanup was real and its result is real — the 2 remaining sites are both guarded, and the file is in good shape. But main.mo is 14,977 lines and holds most of the backend's arithmetic, and the ratchet does not read it. A future unguarded a - b added anywhere in that file passes the gate silently. The other src/backend files are counted correctly; it is specifically the file that most needs the check that is excluded, and it is excluded by accident rather than by a documented decision.

The history comment's own note that moc was once "SUPPRESSING all warnings for main.mo" is the same class of failure recurring through a different mechanism.

Proof. From the repo root:

bash proofs/h66-ratchet-missing-moc-flags.sh

Verbatim output:

gate command (flagless, lint-ratchet.sh:63/:90):
  moc $(mops sources) --check src/backend/main.mo
    exit=1  'unbound variable Fixed' errors=144  M0155 sites in main.mo=0
with the build flag (mops.toml [canisters.backend] args):
  moc $(mops sources) --implicit-package=core --check src/backend/main.mo
    exit=0  M0155 sites in main.mo=2
      src/backend/main.mo:3696.57-3696.85: warning [M0155], operator may trap for inferred type
      src/backend/main.mo:10926.36-10926.45: warning [M0155], operator may trap for inferred type
      src/backend/main.mo:10926.55-10926.64: warning [M0155], operator may trap for inferred type
OBSERVED: ratchet's M0155 count for main.mo = 0 (compare M0155_BASELINE=0 -> reports 'at baseline')
CORRECT : M0155 count for main.mo = 2
BUG REPRODUCED: the flagless gate command dies with 144 unbound-variable errors before
  warning analysis, so the M0155 ratchet sees 0 sites in main.mo while 2 real sites exist.

(Three warning lines, two unique source lines — the ratchet dedupes by file:line, hence 2.)

Honest limitation of this proof: the script hand-copies the moc command from lines 63 and 90 rather than invoking lint-ratchet.sh itself, so it demonstrates the compiler behaviour under the two flag sets, not the script's end-to-end output. The ratchet's arithmetic on top of that count is trivial and visible at line 90-101; the (at baseline) conclusion follows directly from a count of 0.

Secondary consequence — mops check fails on a clean checkout. The same missing flag breaks mops check, which line 71's success message tells the developer to run:

echo "✓ type-check: ok (${WARN_N} non-M0155 moc warning(s) — run 'mops check' to see them)"

On an unmodified checkout of main, mops check exits 1 with 146 errors — 144 M0057 (unbound variable Fixed) plus 2 M0234 — all phantom, all from the same root cause. A developer following the gate's own advice is handed 146 errors on a tree that compiles and deploys correctly. If mops check is ever wired into CI as-is, it fails permanently.

---

Part two — three latent correctness defects in the vendored OQL

Read this framing first, so nobody chases a live bug.

All nine entities registered in src/backend/main.mo (lines 14504-14923) are built with OQL.Entity.manual. No entity in the repo calls Entity.withServed, and no IndexedMap is instantiated outside src/backend/oql/ — we grepped the whole of src/backend for IndexedMap, servedOf and .served and found no hits outside the vendored library.

Consequently:

• Findings 23 and 49 cannot fire today. Both require an entity with a served capability (finding 23) or a maintained secondary index (finding 49). Neither exists.
• Finding 47's code path does run today — groupKey is on the shared scan path — but its trigger requires a U+001F byte inside a text column. We did not find a caller-writable text field that reaches any registered entity: usernames are generated internally from the actor's entropy pool (Profiles.usernameFromDraws, src/backend/lib/Profiles.mo:81), not supplied by the caller. So it is not injectable through the current API surface.

These are library-correctness bugs. They would bite the moment the served-entity or secondary-index path is adopted — which the library is clearly built to support — and they fail silently, returning a wrong answer rather than trapping. That is why they are worth recording now.

Cross-reference to issue #8. Issue #8's OQL findings are all data-leakage defects, and they are located upstream of the executor — in the registry, the entity builder, and the access/scoping layer. Its preamble affirmatively describes the executor as well-defended and its aggregates as sound. Nothing below contradicts that. These three are correctness defects with no privacy dimension: none of them causes a caller to see a row they are not entitled to. Finding 23 returns a #null_ where a value belongs; finding 47 merges two groups that should be distinct; finding 49 returns zero rows where rows exist. In every case the affected data was already readable by that caller. Issue #8's security assessment of the executor stands.

---

Finding 23 — the index-served aggregate path skips path validation

Where. src/backend/oql/Executor.mo lines 76-88, inside runWith. The early return is line 81; collectHops runs at line 88.

    // Index-served aggregate: answer count / min / max / group-count straight
    // off the index stats, with no scan. Same gate as the planner (unrestricted
    // + served); exact cases only, so the result equals a scan of the query.
    switch (startSubject, entity.served) {
      case (null, ?s) {
        switch (aggPlan(s, q)) {
          case (?(rows, cols)) { return finishRows(rows, ?cols, false, q, entity.fields) };
          case null {};
        };
      };
      case _ {};
    };

    let hops = collectHops(r, entity, q, access);

What is wrong. collectHops is the only thing that (a) validates every dotted path in select/orderBy/groupBy against the schema — trapping on an invalid hop — and (b) builds the hops structure that wrapRow uses to make a dotted path resolvable on a row. On the scan path both happen (Executor.mo:128 and :143):

    let kept = filter(
      if (hasEdges) { baseRows.map(func (row : Row) : Row = wrapRow(row, entity.name, hops)) }
      else          { baseRows },
      q.where_,
      scanCap,
    );

The index-served aggregate path returns at line 81, before line 88. Its rows are never wrapped, so a dotted path such as "dept.name" has nothing to traverse. finishRows calls projectionPaths and project (lines 165-170) on unwrapped rows, and the row's get returns null for the unresolvable path, which projects as #null_.

Why it matters. The comment on lines 76-78 states the design contract explicitly: "exact cases only, so the result equals a scan of the query." That contract is violated for any query whose select or orderBy contains a dotted edge path. The same query returns joined values when it happens to scan and #null_ when it happens to be served from the index — with no error, no trap, and no signal to the caller. Whether an index serves a given query depends on which indexes are declared and whether their backfill has completed, so the answer can change over the lifetime of a canister without the query changing.

The second half is equally bad: path validation is skipped, so a query naming a nonexistent edge — which the scan path traps on — is answered with #null_ instead. A malformed query gets a plausible-looking result.

How to confirm. Declare an entity via IndexedMap.entity with an .edge to a second entity, and issue an aggregate query whose select includes a dotted path across that edge (e.g. groupBy: ["dept"], aggregate: [count], select: ["dept.name"]) with aggPlan satisfiable from index stats. Compare against the same query on an equivalent Entity.manual entity: the served answer has #null_ in the dept.name column, the scanned answer has the joined value. Then repeat with a bogus edge name — the manual entity traps, the served entity returns #null_.

---

Finding 47 — unescaped group-key separator merges distinct groups

Where. src/backend/oql/Executor.mo lines 952-967. groupKey is called from aggregateRows at line 831.

  /// Type-tagged serialisation of the group-key tuple, so distinct values
  /// (and distinct types) never collide into the same bucket.
  func groupKey(vals : [Value]) : Text {
    var s = "";
    for (v in vals.values()) s := s # valueKey(v) # "\u{1f}";
    s
  };

  func valueKey(v : Value) : Text = switch v {
    case (#null_)   { "0:" };
    case (#bool b)  { "1:" # Bool.toText(b) };
    case (#nat n)   { "2:" # Nat.toText(n) };
    case (#int i)   { "3:" # Int.toText(i) };
    case (#float f) { "4:" # Float.toText(f) };
    case (#text t)  { "5:" # t };
  };

What is wrong. groupKey concatenates per-column keys separated by U+001F (unit separator). valueKey for #text emits "5:" # t with no escaping — t is spliced verbatim. The type tag defends against cross-type collisions, which is what the doc comment claims and delivers. It does nothing about a separator byte occurring inside a text value.

So for a multi-column groupBy over text columns, the tuples

(#text "a\u{1f}b", #text "c")   ->  "5:a\u{1f}b\u{1f}5:c\u{1f}"
(#text "a",        #text "b\u{1f}5:c")  ->  "5:a\u{1f}5:b\u{1f}5:c\u{1f}"

are distinct, but the general construction admits collisions: any text value containing U+001F can be split across the separator boundary so that two distinct tuples serialise to the same string. Those rows land in one bucket, and every aggregate computed over that bucket — count, sum, min, max — is wrong for both of the groups that were merged. The result row carries one of the two key tuples; the other simply disappears from the output.

Why it matters. It is a silent wrong answer in an aggregate — the failure mode with the least chance of being noticed. There is no trap, no warning, and the row count still looks plausible.

The exposure today is limited, as noted in the framing above: groupKey runs on the scan path and so is reachable, but we found no caller-writable text field that reaches a registered entity, so the byte cannot currently be injected through the API. The defect is in the library, and the library is vendored for reuse; any future entity exposing a user-supplied text column as a groupable field activates it.

The fix shape is a length-prefix or an escape of the separator inside valueKey's #text case, so that the serialisation is injective. Not proposing a patch here.

How to confirm. Call aggregateRows (or issue a groupBy query) over two rows whose text cells differ only in where a U+001F falls relative to the column boundary, and observe one output group where two are expected.

---

Finding 49 — an index on a .payload/.flatten column keys every row null

Where. src/backend/oql/IndexedMap.mo lines 110-135 (put/delete), src/backend/oql/SecondaryIndex.mo lines 219-224 (keyOf), src/backend/oql/IndexedMap.mo lines 164-181 (entity), src/backend/oql/Entity.mo lines 440-454 (fullRow).

  public func put<K, V>(
    self    : IndexedMap<K, V>,
    k       : K,
    v       : V,
    compare : (implicit : (K, K) -> Order.Order),
    _toRow  : (implicit : V -> Row),
  ) {
    let old = self.inner.get(compare, k);
    self.inner.add(compare, k, v);
    SecondaryIndex.onChange<K>(self.ix, compare, k, Option.map<V, Row>(old, _toRow), ?(_toRow(v)));
  };

What is wrong. There are two different notions of "the row for v", and the index and the query layer use different ones.

The index is maintained from _toRow — the compiler's structural __record combiner over V. It contains exactly the record's own fields. IndexedMap's module header (lines 27-28) states the assumption directly: "The index keys come from the same _toRow an OQL entity uses, so index keys and query columns agree by construction."

The query layer uses toPredRow, resolved in Entity.build from fullRow (Entity.mo:454), which is toRow plus every .payload / .flatten extra:

    func rawCellList(v : T) : List.List<(Text, Value)> {
      let cells = List.empty<(Text, Value)>();
      for (cell in self.toRow(v).values()) cells.add(cell);
      for (extra in extras.values()) {
        for (cell in extra(v).values()) cells.add(cell);
      };
      cells
    };
    func fullRow(v : T) : Row = dedupeNames(rawCellList(v));

Extras attach at the Entity.Builder layer (Entity.payload at Entity.mo:250, Entity.flatten at :273), after IndexedMap.entity has handed _toRow to Entity.new (IndexedMap.mo:172). The index never sees them. The header's "agree by construction" claim holds only for entities with no extras.

The failure is then silent because of SecondaryIndex.keyOf:

  // A row's value for `col`: the cell if present, else `#null_` (missing fields
  // index under null, so a query for null still finds them).
  func keyOf(row : Row, col : Text) : Value {
    for ((k, v) in row.values()) { if (k == col) return v };
    #null_
  };

A column that does not exist in the structural row defaults to #null_. That default is correct for a genuinely missing field, but here it means an index declared on a payload-extra column keys every row under #null_.

Meanwhile kindOf (SecondaryIndex.mo:158-162) reports the column as indexed — it consults only the decl list and the pending set, and has no knowledge of whether the column appears in any row:

  public func kindOf<Ref>(ix : Index<Ref>, col : Text) : ?Kind {
    if (ix.pending.contains(Text.compare, col)) return null;
    for ((c, k) in ix.decls.values()) { if (c == col) return ?k };
    null
  };

So the planner's sargability checks (Executor.mo:401, :467, :475, :485) see kindOf(col) != null, route the query to point, and get back the posting for the queried value — which is empty, because every row is filed under #null_.

Why it matters. A planned #eq query on such a column returns zero rows where a scan over the same data would match. Again: no trap, no warning, an empty result set that is indistinguishable from "nothing matched". Because the planner only engages for unrestricted reads, the same query can return rows for a scoped caller (scan) and nothing for an unrestricted one (index) — the opposite of the expected relationship, which makes it hard to attribute.

The declaration itself is the only place this could be caught. addIndex (IndexedMap.mo:85) traps on a duplicate column but does not check that the column exists in the row shape, and it cannot: at addIndex time the entity builder has not run yet, so the extras are not known. That ordering is the structural cause.

How to confirm. Build an IndexedMap<K, V> with an index on a column name that is not a field of V, declare that column on the entity with .payload, and issue an unrestricted #eq query on it. The entity's schema() lists the column, kindOf reports it indexed, and the query returns zero rows. Remove the index declaration and the same query — now scanned — returns the matching rows.

---

Verification notes

• All line numbers were re-checked against the current tree: scripts/lint-ratchet.sh (157 lines), mops.toml (42 lines), src/backend/main.mo (14,977 lines), src/backend/oql/Executor.mo, src/backend/oql/IndexedMap.mo, src/backend/oql/SecondaryIndex.mo, src/backend/oql/Entity.mo.
• Toolchain used: moc 1.9.0, lintoko 0.5.1 (pinned in mops.toml).
• Both proofs for part one were executed. proofs/h66-ratchet-missing-moc-flags.sh runs from the repo root and reads only; the finding-65 proofs use mktemp -d and remove it on exit. git status was unchanged by every run.
• Part two was verified by reading; no proof script is included, since no code path in the deployed canister reaches these defects and constructing one requires adding a served entity.
• No patches are proposed in this issue.

---

Getting the proof scripts. The proofs/ paths referenced above are not in this repository — they ship separately, so nothing is added to your tree. All of them are here:

https://gist.github.com/andreij6/ed9f244e47a71a786405bc7959550d4b

To run them, clone the gist into a proofs/ directory at the root of a public-multidex checkout:

git clone https://gist.github.com/ed9f244e47a71a786405bc7959550d4b.git proofs
bash proofs/run_all_proofs.sh

Verified end to end from a clean checkout. The scripts are read-only: they compile and read the product source, modify nothing, and contain no fixes. Each prints the observed value alongside the correct one, exits 0 with BUG REPRODUCED: while the defect is present, and flips to exit 1 once it is fixed. The gist README maps every proof to its issue and also includes the proofs for candidates that were investigated and not filed.

[dominicwilliams]

Part one is confirmed and closed. Part two is confirmed and correctly labelled latent.

Part one — both pre-push lint-gate checks are structurally inert. Confirmed, and the compounding failure underneath was worse than the surface claim.

The type-check gate could not fail: step 1 omitted the project's real build flags, so its output filled with spurious M0057 noise, and its detector was grep -qE ': error' — but Motoko always emits ": type error [Mxxxx]", never a bare ": error". It matched neither the real errors nor the noise, and printed ✓ type-check: ok unconditionally. Confirmed directly: the ratchet exited PASS in the same tree where mops test reported 14/15 files passing, 1 failing.

The same missing flags had silently disabled the second gate. The M0155 "hard zero" ratchet reported 0 because moc aborted on M0057 before the analysis ran. With the flags restored it immediately found two real unguarded subtractions that had been in the tree the whole time — on the liquidation-price and slippage-impact paths, both now SafeMath.subOrZero. The repaired gate paid for itself on its first run, which is the strongest possible argument for your report.

Both legs are repaired and the M0155 count is now genuinely 0 rather than blind. Today's build still reports it as zero — that number now means something.

One note on a related remedy. The fix proposed for the same area in the earlier wave — widen the glob — was incomplete: tests/ is never fed to the idl step, and the M0155 grep would ignore an M0151 anyway. The gate needed a real per-file type-check with a working pattern, not a wider input set. Your framing of the problem as structural inertness rather than insufficient coverage is what made that clear.

Part two — three latent defects in the vendored OQL. Confirmed, not fixed, and your own labelling is right: they do not fire in the deployed canister and activate only if the served-entity or secondary-index path is adopted. They are recorded as a note on that future change rather than as live bugs. Reporting them with that bound stated, instead of inflating them, is the reason the rest of the report is easy to trust.

The code is in #30, the first push to this mirror since the July snapshot; your line numbers against 0241cba still resolve.