`implies` appears 9 times in live source and 0 times in the compiler: the consequent is discarded and typecheck reports OK

[gHashTag]

implies is a word this compiler has never heard, and 82 assertions are silently truncated at the antecedent

$ grep -c 'implies\|==>' bootstrap/src/compiler.rs
0
$ grep -rn --include='*.t27' 'implies' specs/ | wc -l
82          (in 19 specs)

The corpus writes implication 82 times. The compiler contains no token, no
parse arm and no lowering for it, in any spelling.

What happens instead

Minimal probe, four lines, written from scratch:

invariant a_implies_b
    given x = a()
    assert x == true implies b() == false

$ t27c gen-c /tmp/imp.t27
void invariant_a_implies_b(void) {
    __auto_type x = a();
    assert((x == true));          <-- the consequent is gone
}
$ t27c check /tmp/imp.t27
Typecheck OK (0 errors, 0 warnings)

Real corpus site, specs/fpga/top_level.t27:201:

assert busy == false implies ready == true

/* gen-c */            assert((busy == false));

/* gen */              const ready = system_ready();
                       _ = ready; // dead after const-inlining
                       if (!(busy == false)) __t27_assert_fail(...);
                       // invariant: ... NOT CHECKED -- body was not lowered (T43)

Why this is worse than dropping the assertion

P implies Q is vacuously true whenever P is false. What is emitted is
assert P -- a different and strictly stronger proposition. The invariant
above says nothing when the system is busy; the generated code demands it
not be busy. An assertion that says nothing is a gap; an assertion that says
something else can fail on correct behaviour, or pass while the property it was
written for is violated.

Zig's output is the honest half of the same confusion: it emits the wrong check
AND, two lines later, NOT CHECKED -- body was not lowered. Two contradictory
statements about one invariant, in adjacent lines.

Not Verilog-only

This is C, Zig and Rust. The Verilog backend emits every invariant as a comment
(#2869), so it is the one backend where the truncation cannot mislead anybody --
the peer-backend oracle this project relies on has all three surviving arms
agreeing on the same wrong proposition, which is exactly the case #2847 named as
where cross-checking is blind.

The decision in it

Adding ==> as !a || b was already declined once, in #2774, for a stated
reason: a false antecedent then makes the invariant a pass, and what a quantified
implication means at codegen commits four backends. That reason still holds and
this issue does not reopen it.

What is not a decision: the silence. Whatever implies should mean, the
compiler should not accept the word, discard half the assertion, and print
Typecheck OK. The narrow repair is to reject it by name until it has a
meaning -- the third state this repository already has a word for.

Refs #2774, #2869

[gHashTag]

Correction: the compiler DOES record the discard — it just never says so where it matters

I wrote that the truncation is invisible. That is wrong in one important
direction, and the corrected statement is sharper.

The AST, first — the consequent is gone before typechecking

$ t27c ast-dump /tmp/imp2.t27
InvariantBlock name='a_implies_b'
  StmtLocal name='x'
    ExprCall name='a'
  StmtExpr
    ExprCall name='assert'
      ExprBinary            <- x == true
        ExprIdentifier x
        ExprLiteral

Source: assert x == true implies b() == false. There is no node for
b() == false anywhere. So this is a parse-time loss, not a lowering loss,
and every AST-based check downstream is blind to it by construction — the same
mechanism #2850 records for parse_invariant_clause.

But parse-complete counts it

Planting one implies clause into the corpus and re-running the repository's own
completeness scan:

	without the probe	with it
specs scanned	650	651
parse and consume all	505	505
parse but TRUNCATE	0	0
parse but DISCARD	76 (23 831 tokens)	77 (23 843 tokens)
do not parse	69	69

+1 file, +12 tokens, and the probe is named in the listing. The compiler
knows it threw the consequent away and records it in the discard channel.

So the corrected claim is not "nothing sees it". It is:

The one instrument that records the loss is a corpus-completeness scan nobody
runs on the assert path, while t27c check — the command a contributor
actually types — prints Typecheck OK (0 errors, 0 warnings) and all three
backends emit assert P and compile clean.

Same shape as #2831: the resolver already wrote every refusal down, and every
backend strips comments before emitting. The information exists; it reaches
nobody at the point where a wrong answer is produced.

Why that makes the narrow repair narrower

Nothing has to decide what implies means to stop the silence. The discard is
already recorded at the site that makes it — so the assert path can say so,
at the severity this repository uses for exactly this situation: a warning,
which moves no ratchet (the precedent is #2897, where a soundness comparison was
added at the argument's severity for that reason).

That is not the same as rejecting the word, which would turn 82 currently-clean
sites into errors across 19 specs and is a decision. #2774's reason for declining
==> still stands and this does not reopen it.

What I did not establish

• How many of the 23 831 discarded tokens corpus-wide are implies consequents.
  One probe clause cost 12 tokens; clauses differ in length and extrapolating
  from one would be a guess, not a measurement.
• Whether the discard channel labels them distinguishably —
  tri discard classify groups by recovery site, and I did not check which
  channel this lands in.

[gHashTag]

Closing the second gap: the channel is top-level-resync, and the head token is given

tri discard classify groups the discard by which recovery threw it away and
what it stopped on. Planting one implies clause and diffing the whole table:

< 282  17  11  top-level-resync    given
> 294  18  12  top-level-resync    given

That is the only row that moves: tokens 282 → 294 (+12), runs 17 → 18,
specs 11 → 12. Total 23 831 → 23 843, runs 1670 → 1671, and the number of
distinct head tokens is unchanged at 87.

So the loss is recorded, and it is recorded under given — the head of the
clause the resync swallowed — never under implies. grep -i implies over the
classification table returns nothing.

Which means a reader looking for this construct in the instrument that records
it finds zero, and reads that as this does not happen here. Exactly the shape
already on the record for the other spelling:

==> never appears in a drop trace — the lexer splits it, and a matcher for
the source spelling finds zero of the 38.

Same defect class, second spelling, one layer over. The construct is invisible in
the classification for a structural reason and not because it is rare: 82
occurrences in 19 specs, and the table cannot name one of them.

Both stated gaps are now closed, and one remains open on purpose

• which channel → top-level-resync, head token given.
• how many corpus tokens → still not measured, and deliberately not
  extrapolated: one probe clause cost 12 tokens, clauses differ in length, and
  the run boundary is a LINE GAP, so a clause spanning two lines is counted as
  one run while two clauses on one line read as one. The table says so itself.
  The honest number needs a per-spec counterfactual, not a multiplication.

[gHashTag]

WITHDRAWN: the number in this issue's title. It is 9, not 82 — inflated nine times, by me

I opened this with "82 times in the corpus, 19 specs". That came from
grep -rn 'implies' specs/ --include='*.t27' | wc -l — a substring count with no
word boundary and no comment handling. Both errors inflate.

The three readings

loose  (what I published)   82 lines   19 specs
word-boundary               39 lines   14 specs
minus text after // or #     9 lines    4 specs      <- the operator, live, in source

The gap between the first two is identifiers containing the letters:

  39  implies                    <- the operator
  15  k3_implies
   1  trit_lt_implies_le
   1  trit_gt_implies_ge
   1  tf3_lt_implies_le
   1  tf3_gt_implies_ge
   1  tf3_eq_implies_le_and_ge
   1  ternary_word_is_all_same_zero_implies_is_zero

— and my own probe was named a_implies_b, so I wrote one of them myself. The
gap between the second and third is comments, including five trailing ones in
numeric/goldenfloat_family.t27 of the form
then report.all_valid == true // implies format_count == 9, which my first
comment filter missed because it only tested whether a line starts with a
marker.

The nine, all of them

specs/fpga/top_level.t27:201   assert busy == false implies ready == true
specs/fpga/top_level.t27:206   assert error == true implies busy == false
specs/fpga/top_level.t27:210   assert ready == true implies system_state.mac_ready == true
specs/base/ternary_add.t27:367 assert carry_sign(s) == .pos  implies s > 1
specs/base/ternary_add.t27:368 assert carry_sign(s) == .neg  implies s < -1
specs/base/ternary_add.t27:369 assert carry_sign(s) == .zero implies -1 <= s <= 1
specs/fpga/spi.t27:355         assert spi.busy implies spi.cs_asserted or spi.state == SPI_CS_ASSERT
specs/fpga/spi.t27:358         assert spi.busy implies spi.state == SPI_CS_ASSERT or …
specs/igla/evaluation/multi_lang_harness.t27:88  assert !r.syntax_ok implies !r.compile_ok

Four specs. Not nineteen.

What does NOT change

Every one of the nine is still truncated at the antecedent, the consequent is
still absent from the AST, t27c check still prints
Typecheck OK (0 errors, 0 warnings), and C, Zig and Rust still emit assert P
— a different and stronger proposition than P implies Q. The mechanism, the
probe, the discard-channel measurement and the correction about top-level-resync / given all stand. Only the size was wrong, and it was wrong in the direction
that makes a defect look bigger than it is.

This is section 421 of my own notes — an address is not a count; the loose
matcher fires inside identifiers, and this repository is made of them — applied
to me, in the same pass I wrote it down. The cheap check I skipped is the one
that page names: feed the strict and the loose matcher the same corpus and
subtract.

One overlap I checked rather than left hanging

Two of the four specs — fpga/top_level and fpga/spi — are also in the nine
that report failures under tri vsim funnel. That is a coincidence: the failing
tests are set_uart_data_boundary and spi_prescaler_div_16, unrelated to the
invariants, and the Verilog backend emits every invariant as a comment (#2869)
so an invariant cannot produce a runtime verdict at all.

Title corrected.