Repository navigation

Typed layer with ci - #1

Merged

yiyunliu merged 24 commits into

mainfrom

typed-layer-with-ci

Jul 20, 2026

Commits on Jul 15, 2026
- M1: theorem topology map, claim hygiene, axiom gates (zero proof-term changes)
  
  yiyunliu
  and
  claude
  committed
  507f63a
- M2: comment sweep — timeless invariants replace audit archaeology (comment-only)
  
  yiyunliu
  and
  claude
  committed
  0c4850d
Commits on Jul 16, 2026
Commits on Jul 17, 2026
- M4 (typed-layer): statement immediates in Coq; nft_lower.ml retired to structural injection (M-C grep-zero)
  
  yiyunliu
  and
  claude
  committed
  03c1cdb
- M6 (typed-layer): typed Gen files (zero raw-byte immediates), boundary gate, TCB ledger
  
  yiyunliu
  and
  claude
  committed
  cb43a6e
- typed-layer repair: IPv6 literal expansion moves from the lexer into verified Coq
  
  yiyunliu
  and
  claude
  committed
  61b2460
- Retire IR/Elab.v: the four M0 shapes become first-class txmatch constructors
  
  yiyunliu
  and
  claude
  committed
  636f5ae
- T1: single-fold rule semantics — one kernel-faithful walk per rule, mut_wf eliminated
  
  yiyunliu
  and
  claude
  committed
  1bdb862
- T2A: corpus wire-level bug fixes B/C/D/E/F/N + ratchet gate + upstream ct-id
  
  yiyunliu
  and
  claude
  committed
  396e415
- T2A-corpus-bugs repair: class G in-frame ethertype guard + crash-fix gate + ratchet raise
  
  yiyunliu
  and
  claude
  committed
  e0b1c5e
- T2B-intra-rule-optimizer: two unconditional intra-rule passes + composable -O CLI
  
  yiyunliu
  and
  claude
  committed
  f1bc8a8
- T3-parser-and-objects: full frontend coverage, zero silent drops
  
  yiyunliu
  and
  claude
  committed
  f1e5ed8
- T3 repair: bidirectional corpus ok/fail ratchet + argument-range rejects
  
  yiyunliu
  and
  claude
  committed
  97c8272
- T3 repair (R1-R4): sound corpus-okfail gate + honest residual
  
  yiyunliu
  and
  claude
  committed
  6d65029
Commits on Jul 20, 2026
- add CI
  yiyunliu
  committed
  c9fcaa7

Navigation Menu

Repository navigation

Typed layer with ci - #1

Typed layer with ci#1
yiyunliu merged 24 commits into
mainfrom
typed-layer-with-ci

Commits on Jul 15, 2026

M1: theorem topology map, claim hygiene, axiom gates (zero proof-term changes)

M2: comment sweep — timeless invariants replace audit archaeology (comment-only)

Commits on Jul 16, 2026

M3: honest state flow — explicit world (env split), one step function per side, derived _mut stratum, source-side mut_wf

M4: typed, readable source AST with verified elaboration onto the byte IR

M5: module topology + naming — role directories, invariant-named gates, one optimizer convention

M1 (proof-eng): gates that match the claims — axiom gate covers the README, gen-check, make gates, mut_wf + nat-overflow discharged at the tool boundary

M2 (proof-eng): known-infidelity ledger + theorem-scope honesty

M3 (proof-eng): TCB + external-validation honesty — oracle direction, evidence ledger, elab boundary, pkt_flow rationale, fuzz-gate rationale, byteorder/jhash

M4: config-proof soundness — fuel adequacy proved, gen_env pins de-vacuized

M1 (typed-layer/T1): Coq surface AST + datatype/coercion lattice + typechecker gate

M2 (typed-layer/T2 seed): verified scalar-match lowering — OCaml stops constructing byte-level scalar matchconds

M3 (typed-layer/T2): verified composite immediates — set/map/vmap elements, CIDR intervals, concat slot padding, interning

Commits on Jul 17, 2026

M4 (typed-layer): statement immediates in Coq; nft_lower.ml retired to structural injection (M-C grep-zero)

M6 (typed-layer): typed Gen files (zero raw-byte immediates), boundary gate, TCB ledger

typed-layer repair: IPv6 literal expansion moves from the lexer into verified Coq

Retire IR/Elab.v: the four M0 shapes become first-class txmatch constructors

T1: single-fold rule semantics — one kernel-faithful walk per rule, mut_wf eliminated

T2A: corpus wire-level bug fixes B/C/D/E/F/N + ratchet gate + upstream ct-id

T2A-corpus-bugs repair: class G in-frame ethertype guard + crash-fix gate + ratchet raise

T2B-intra-rule-optimizer: two unconditional intra-rule passes + composable -O CLI

T3-parser-and-objects: full frontend coverage, zero silent drops

T3 repair: bidirectional corpus ok/fail ratchet + argument-range rejects

T3 repair (R1-R4): sound corpus-okfail gate + honest residual

Commits on Jul 20, 2026

add CI