Skip to content

Move derived loop facts into structured checking - #205

Merged
hiroki23 merged 5 commits into
mainfrom
feat/derived-mir-fact-ownership
Sep 2, 2026
Merged

Move derived loop facts into structured checking#205
hiroki23 merged 5 commits into
mainfrom
feat/derived-mir-fact-ownership

Conversation

@hiroki23

@hiroki23 hiroki23 commented Sep 2, 2026

Copy link
Copy Markdown
Contributor

Summary

  • derive the accepted literal-zero and active base + small nonnegative literal
    loop facts while the structured checker consumes declarations, control flow,
    and assignments
  • retain only the verified result or an enclosing verified-fact dependency in
    mir_loop_facts before QBE emission
  • delete the lexical whole-loop proof scan, emitter-only local state 3, and
    the now-unused emitter function_end field
  • extend negative controls for dynamic, negative, non-adjacent, and invalidated
    outer-loop derived facts

The QBE adapter now receives both accepted induction shapes through the same
checked-program fact boundary. Nested facts follow an already-derived enclosing
fact instead of rescanning token ranges, and the adapter never reconstructs a
derived initializer from source tokens.

Scope

This is the bounded ownership migration registered in #204. It does not add
general range propagation, dominance, interprocedural analysis, a serialized
MIR field, a backend option, or language/runtime behavior. The active-loop
emitted-value carrier and direct base-plus-literal expression propagation remain
temporary until the next general Native MIR control/value slice replaces them.

Verification

  • trb fmt --check compiler/gate4/src/compiler.trb compiler/gate4/src/compiler_test.trb
  • trb check --config compiler/gate4/trbconfig.jsonc
  • TYPE_RB_NATIVE_ROOT="$PWD" trb test: 80/80
  • trb test --config compiler/gate4/trbconfig.jsonc: 62/62
  • eight positive/control application fixtures have byte-identical baseline and
    candidate QBE: literal-zero, derived, reassigned, non-unit, dynamic,
    negative, non-adjacent, and conditional
  • an outer loop invalidated after checking a nested derived loop invalidates
    that dependency; the generated path retains negative-index normalization and
    an executable negative-index probe prints 40
  • three local Darwin arm64 Native generations are 299,648 bytes each and emit
    byte-identical compiler QBE; the local linker varied only the Mach-O UUID and
    signature, so hosted exact executable identity remains authoritative
  • the local fixed compiler QBE is 956,214 bytes with SHA-256
    f90ecf48bfb7a95a03b645130a6891de5b75b7af8ebfc0240996530821481bbd
  • static target run
    passes at 299,656 Darwin bytes, 271,928 Linux bytes, and 571,584 bytes
    combined; target-neutral QBE is 956,214 bytes with the same SHA-256 recorded
    locally
  • persistent-worker run
    passes at 299,696 and 271,920 stripped compiler bytes, 571,616 combined,
    while preserving the lifecycle and memory evidence
  • Gate 6N run
    passes the current amd64 and arm64 regressions and cross-target contract
  • complete Native gate
    passes every repository, runtime, benchmark, closure, and Go-free bootstrap
    check on exact head 0fdc4b6ebfe71f7135cbaa2a5caab6626dc90bdc

Closes #204

@hiroki23
hiroki23 merged commit cfcb587 into main Sep 2, 2026
10 checks passed
@hiroki23
hiroki23 deleted the feat/derived-mir-fact-ownership branch September 2, 2026 12:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Move derived induction fact ownership above QBE

1 participant