Feat/jeg complete - #105
Merged
Merged
Conversation
`weave` performed no usage checking at all. It built the strand context,
checked the body, computed `Tangle[A,B]` — and discarded it, returning gamma
unchanged. Three unsound programs were accepted in silence:
weave strands a, b into (a > a) yield strands a, b # contraction
weave strands a, b into (a > b) yield strands a, b, a # contraction
weave strands a, b into (a > b) yield strands a # weakening
The spec already forbade the first (`i != j` on [T-Cross-Over]) and the third
("yield declarations match B"). Both side conditions were written down and
never enforced.
## Why a semiring and not "make the language linear"
The requirement is genuinely mixed, so a single discipline is the wrong answer
in both directions:
* braid WORDS are unrestricted (omega) — `x . x` is sigma_1^2, a legitimate
braid. Blanket linearity would reject valid programs.
* STRANDS are linear (1) — a strand is a physical thread. A braid on n
strands is a permutation of those n strands, so strand count is a
conservation law. AFFINE is specifically wrong here: affine permits
discarding, and a strand cannot vanish. That case is what decides it.
* the CLAIM in `Epi[k, rho, tau]` is erased (0) — A-TG-11.1's recorded gap.
`compiler/lib/quantity.ml` provides {0, 1, omega} with add/mul/permits.
Independent uses combine with semiring addition, so two uses of one strand give
1 + 1 = omega, which is not permitted where 1 was declared.
## Applied in BOTH weave forms
Wiring the check into the weave STATEMENT rule alone left `def x = weave ...`
— the idiomatic spelling — entirely unchecked, because it reaches the weave
EXPRESSION rule and never touches the statement rule. The new conformance tier
caught this on its first run.
## Gating
New `conformance/ill-typed/` tier with a DOUBLE assertion: the file must PARSE
and then FAIL to typecheck. Asserting only "the compiler rejects it" is the
failure this suite already had once, when three invalid/ cases scored points
because the command was wrong and failed on every input. Requiring the parse
first proves the rejection came from the typechecker, not from a typo in the
fixture.
Wired into `scripts/check-corpus.sh` (what CI runs) as well as
`run_conformance.sh`, and verified with a negative control: making one
ill-typed fixture well-typed turns the gate red, restoring it turns it green.
`valid/` is now also required to TYPECHECK, not merely parse. All 16 already do.
## Verification
* semiring laws checked EXHAUSTIVELY over all 27 triples — a "semiring"
whose operations don't satisfy the laws is two arbitrary tables, and every
soundness claim resting on it is worth nothing
* 677 compiler tests pass (`dune runtest --force`)
* conformance 23/23; 8/8 examples evaluate; stdlib typechecks
* corpus + RSR gates green
Spec: new section 3.10.1 with the [T-Weave-Linear] rule and the quantity table.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Seventeen rules matched a `-> ()` arm in `check`. That is not a partial
check — it is an ACCEPT. A forged node naming T-Close, T-App or T-Weave could
conclude any type at all and the graph still checked green. Since the JEG's
whole claim is "evidence, not a log", those arms were the part that made the
claim false.
## What made them underivable, and the fix
Three of them (T-App, T-Crossing, T-Weave) genuinely could not be re-derived
from the recorded data, because the judgement did not carry what the rule
reads. So the judgement was widened:
* `j_ctx` now holds `env_entry`, not `ty` — a T-App node cannot be checked
without the callee's SIGNATURE.
* `j_sigma` (new) holds the strand context — T-Crossing and T-Weave read
Sigma rather than premise types. They were previously bare LEAVES:
nodes asserting a type with nothing licensing it at all.
The rest were derivable all along and simply had not been written.
## Shared rule functions, so the JEG cannot drift
`infer_binop` was already a type-in/type-out function. The remaining rules
were inline in `infer_expr`, so the JEG would have had to RE-IMPLEMENT them —
and a JEG that re-implements the rules can drift from the typechecker, at
which point it certifies a rule the compiler does not apply and the evidence
is worthless.
Extracted 16 of them (`infer_close`, `infer_mirror`, `infer_echo_eq`,
`join_arm_ty`, ...) into one definition each, called by BOTH. Drift is now
impossible by construction rather than by discipline. The extraction is
behaviour-preserving: all pre-existing tests pass unchanged.
## Two rules with real substance
* T-Let checks the conclusion is the BODY's type AND that the body was
checked under the binding the let actually makes. Checking only the type
would accept a derivation whose body silently assumed `x` had some more
convenient type — there is a test for exactly that forgery.
* T-Weave re-runs the strand LINEARITY check, so a graph cannot launder a
weave that duplicates or drops a strand.
## The remaining hole is reported, not hidden
T-Add-Block's island has its own judgement (|-_hd). Rather than a silent
accept, it is recorded: new `unchecked : derivation -> (string * judgement)
list`. "check succeeded" and "check succeeded and re-derived every node" are
now distinguishable, and `--derive` prints which it was:
== c == (3 nodes, depth 3, every node re-derived)
## Verification
* JEG suite 19 -> 51 tests; an honest/forged PAIR for each rule closed, so
each test's forged half is a case that would have PASSED before
* 709 compiler tests pass (`dune runtest --force`)
* conformance 23/23, corpus + RSR gates green
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Closes #
Type of change
How has this been verified?
Checklist
git commit -S).SPDX-License-Identifier(code/configMPL-2.0,prose
CC-BY-SA-4.0); I did not relicense existing files.Notes for reviewers