Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
80 changes: 80 additions & 0 deletions domains/UNSHADOW.log.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,86 @@

Append-only history sister of `UNSHADOW.md`. Each entry starts with `## <ISO timestamp> โ€” <header>` (newest on top); body = `- [x]` (done) / `- [ ]` (pending) checkbox tasks.

## 2026-05-29T12:59Z โ€” #4 atlas-guided const-fold pilot โ€” ๐Ÿ”ต๐ŸŸข g5 IDENTICAL ยท ~65% faster

UNSHADOW.easy.md ยงA ("๋ฃจํ”„/ํ˜ธ์ถœ์„ ์•ˆ ๋Œ๊ธฐ"): codegen ์ด PUREยทatlas-๊ฒ€์ฆ
fn ์„ ๋ชจ๋“  ์ธ์ž ๋ฆฌํ„ฐ๋Ÿด๋กœ ํ˜ธ์ถœํ•˜๋Š” ๊ฒƒ์„ ๋ณด๋ฉด, ๋Ÿฐํƒ€์ž„ call ๋Œ€์‹  atlas ๊ฐ€
๋ณด์ฆํ•œ ๋ฆฌํ„ฐ๋Ÿด ๊ฒฐ๊ณผ๋ฅผ **์ง์ ‘ emit** ํ•œ๋‹ค. LLVM ์€ theorem/verdict DB ๊ฐ€
์—†์–ด ๊ตฌ์กฐ์ ์œผ๋กœ ๋ถˆ๊ฐ€๋Šฅํ•œ ์ตœ์ ํ™”. ์ข๊ฒŒ **๋”ฑ 1๊ฑด**๋งŒ ์‹ค์ฆ (general fold
framework ์•„๋‹˜).

**Pilot fn**: `beenet_grid_bins(ฯ‰_max, ฮ”ฯ‰) = floor(ฯ‰_max/ฮ”ฯ‰)+1`
(RTSC d7 ฮฑยฒF grid bin ์ˆ˜ ยท verify_cli.hexa:1500 `_beenet_grid_bins`).

**Atlas verdict (g5 ยท @D h_verify_auto_absorb ยท VERBATIM)**:
```
verify --expr beenet_grid_bins(100.0,10.0)=11.0
calc = 11.0 โ‰ˆ expected 11.0 (|ฮ”|=0.0 โ‰ค ฮต=1e-9)
tier = ๐ŸŸข SUPPORTED-NUMERICAL (hexa-native libm-class recompute, TECS-L n6-rep Tier2)
absorb = ยท already in atlas โ€” idempotent skip (default ยท @D g69)
```
(`hexa verify --expr beenet_grid_bins 100.0 10.0 11` ยท ๋กœ์ปฌ prebuilt
`bin/hexa-verify` 2026-05-29.)

**Codegen fold (self/codegen.hexa, gen2_expr Call โ†’ Ident ๋ถ„๊ธฐ ์ตœ์ƒ๋‹จ)**:
```
if name == "beenet_grid_bins" && _is_known_fn_global(name)
&& !_gen2_has_decl(name) && len(node.args) == 2 {
let _fa0 = node.args[0]; let _fa1 = node.args[1]
if _fa0.kind == "FloatLit" && _fa1.kind == "FloatLit"
&& _fa0.value == "100.0" && _fa1.value == "10.0" {
return "hexa_int(11)" // atlas-verified literal โ€” skip the call
}
}
```
GUARD ๊ฐ€ EXACT (comptime-fold-shadow family ํšŒํ”ผ): (a) ์ด๋ฆ„ ์ •ํ™•ํžˆ
์ผ์น˜, (b) top-level fn ์œผ๋กœ ํ•ด์„ (`_is_known_fn_global` โ€” fold-off=์‹ค์ œ
user call โ†’ byte ๋น„๊ต ๊ฐ€๋Šฅ), (c) ์ธ์ž ์ •ํ™•ํžˆ 2๊ฐœ, (d) ๋‘˜ ๋‹ค FloatLit ์ด๊ณ 
์†Œ์Šค ํ† ํฐ์ด ๊ฒ€์ฆ์Œ `"100.0"`/`"10.0"` ์™€ ์ •ํ™•ํžˆ ์ผ์น˜. ๊ทธ ์™ธ ๋ชจ๋“  ํ˜ธ์ถœ
(๋‹ค๋ฅธ ์ธ์žยท๋น„๋ฆฌํ„ฐ๋Ÿด ์ธ์žยทlocal-let shadow) ์€ ๋ณ€๊ฒฝ ์—†์ด ํ†ต๊ณผ =
general-case zero behavior change. DOUBLE-EVAL SAFE: ๋ฆฌํ„ฐ๋Ÿด ์ธ์ž๋Š”
ํ‰๊ฐ€๋˜์ง€ ์•Š๊ณ  ํ˜ธ์ถœ ์ „์ฒด๊ฐ€ ์ƒ์ˆ˜๋กœ ์น˜ํ™˜ โ†’ double-eval surface ์ž์ฒด๊ฐ€ ์—†์Œ.

**g5 correctness (host=mini macOS arm64; hexat.base vs hexat.new 2๊ฐœ
ํŠธ๋žœ์ŠคํŒŒ์ผ๋Ÿฌ ๋นŒ๋“œ ยท ๋™์ผ runtime.o ๋งํฌ)**:
- HIT corpus (`beenet_grid_bins(100.0,10.0)`): base=`11` ยท new=`11` โ†’
**BYTE-IDENTICAL** (md5 `166d77ac1b46a1ec38aa35ab7e628ab5` ์–‘์ชฝ).
- NO-HIT corpus (`(50.0,5.0)` ยท `(200.0,10.0)` ยท `(var,10.0)`):
base=`11/21/11` ยท new=`11/21/11` โ†’ **BYTE-IDENTICAL**. emit C ๋„ ๋‘
arm ์ด **์™„์ „ ๋™์ผ** = fold ๊ฐ€ ๋น„๋งค์นญ site ์—์„œ inert (general-case ์ฆ๊ฑฐ).
- isolation (emit C): HIT `u_main` ์—์„œ base ๋Š”
`beenet_grid_bins(hexa_float(100.0), hexa_float(10.0))` (์‹ค์ œ call),
new ๋Š” `hexa_int(11)` (folded). ์ •ํ™•ํžˆ ์˜๋„ํ•œ ์น˜ํ™˜ 1๊ณณ๋งŒ.

**perf (mini ยท 30M-iter ํ•ซ๋ฃจํ”„ ยท clang -O2 ยท 5 interleaved trials)**:

| arm | wall (s, 5 trials) | best |
|------------------|-----------------------------|-------|
| base (real call) | 0.26 0.26 0.26 0.26 0.26 | 0.26 |
| new (folded) | 0.09 0.09 0.09 0.09 0.09 | 0.09 |

ฮ” โ‰ˆ 65% faster. asm: `u_main` ์˜ `bl` ํ˜ธ์ถœ 13 (base) โ†’ 11 (new) โ€”
ํ•ซ๋ฃจํ”„์—์„œ `beenet_grid_bins` call + arena/box call 2๊ฐœ ์†Œ๊ฑฐ.
sum ์ถœ๋ ฅ `330000000` (=11ร—30M) ์–‘ arm ๋™์ผ.

Honesty (roofline ยท g5): REAL win. fold-on ์€ ํ˜ธ์ถœ์„ ์•„์˜ˆ ์•ˆ ํ•จ โ†’ clang
์ด ์ƒ์ˆ˜ `11` ์„ ๋ฃจํ”„ ๋ฐ–์œผ๋กœ hoist. ์ด๊ฒƒ์ด UNSHADOW ยงA ๊ฐ€ ์˜ˆ์ธกํ•œ
"๋ฃจํ”„๋ฅผ ๋นจ๋ฆฌ ๋Œ๊ธฐ(๐ŸŸก)" ๊ฐ€ ์•„๋‹ˆ๋ผ "๋ฃจํ”„๋ฅผ ์•ˆ ๋Œ๊ธฐ(๐Ÿ”ต)" โ€” ๊ฒ€์ฆ๋œ
closed-form/๋ฆฌํ„ฐ๋Ÿด ์น˜ํ™˜. LLVM ๋น„๊ต๋Œ€์ƒ ์—†์Œ (theorem DB ๋ถ€์žฌ).

Build note (codegen-change landing recipe ยท B9):
- `hexa_cc.c` ๋Š” B9 generated boot image (`.hexanoport` ยท gitignored
`.new`) โ†’ commit ๋Œ€์ƒ ์•„๋‹˜. SSOT = `self/codegen.hexa` ํ•œ ํŒŒ์ผ๋งŒ.
- regen ์€ `$HEXA_LANG/self/native/hexa_cc.c` ๊ฐ€ ์กด์žฌํ•ด์•ผ `resolve_hxroot`
๊ฐ€ build tree ๋ฅผ ๊ณ ๋ฆ„ (์„ค์น˜ ํŒจํ‚ค์ง€์—์„œ seed ํ›„ `hexa cc --regen`).
- merged-amalgam smoke ์˜ link ์‹คํŒจ๋Š” PRE-EXISTING merge-MVP ํ•œ๊ณ„
(concat + main-strip). ๊ฒ€์ฆ์€ DIRECT ๊ฒฝ๋กœ: `hexa cc --regen` ์˜ `.new`
๋ฅผ `clang -c` โ†’ ์„ค์น˜ `runtime.o` ์™€ ๋งํฌ โ†’ standalone hexat โ†’ corpus
์ง์ ‘ ํŠธ๋žœ์ŠคํŒŒ์ผ. base/mine ๋‘ hexat ์œผ๋กœ A/B byte-diff.
- mini ์˜ `hexa verify` (verify_cli ๋นŒ๋“œ) ๋Š” `bessel_j0`/`bessel_j1` ๊ฐ€
math-builtin ์œผ๋กœ codegen Call ๋ถ„๊ธฐ์— ๋ฏธ๋ฐฐ์„  โ†’ dup-symbol/undeclared
๋กœ clang ์‹คํŒจ (๋ณ„๊ฐœ pre-existing codegen gap). verdict ๋Š” ๋กœ์ปฌ
prebuilt `bin/hexa-verify` ๋กœ ํš๋“ (๊ฐ’์€ atlas ์— ์ด๋ฏธ ์กด์žฌ ยท idempotent).
## 2026-05-29T02:00Z โ€” #3 arena-reclaim ์ธก์ • (UNSHADOW item #3) โ€” ๐ŸŸข MEASURED ฮ” (RSS โˆ’40% ยท wall โˆ’26%)

์›Œํฌ๋กœ๋“œ = `self/bench/arena_reclaim_bench.hexa` (+ `bench_str` ์ˆœ์ˆ˜ string churn ๋ณ€ํ˜•).
Expand Down
2 changes: 1 addition & 1 deletion domains/UNSHADOW.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@

- [x] hexa-native primitive vs clang -O2 baseline micro-bench harness (์žฌ์‚ฌ์šฉ ์ธก์ •๋Œ€ ยท M1)
- [x] ๐ŸŸข cross-layer ์ธ๋ผ์ธ ์ธก์ • โ€” ๋Ÿฐํƒ€์ž„/์œ ์ € C-ABI ๋ฒฝ ์ œ๊ฑฐ ์‹œ ฮ” โ€” `hexa_int` ์ •์ˆ˜๋ฆฌํ„ฐ๋Ÿด ๋ฐ•์Šค ์ธ๋ผ์ธ(`((HexaVal){.tag=TAG_INT,.i=(N)})`) โ†’ mini macOS arm64 hot-loop ~28% faster (1.83โ†’1.31s), -O2 `bl _hexa_int` 13โ†’5; g5 byte-identical (md5 5dd08ae3). ์ƒ์„ธ = UNSHADOW.log.md
- [ ] ๐Ÿ”ต A ๋ฃจํ”„โ†’closed-form ์ œ๊ฑฐ 1๊ฑด (atlas Faulhaber๋ฅ˜ โ€” "์•ˆ ๋Œ๊ธฐ" ์‹ค์ฆ)
- [x] ๐Ÿ”ต A atlas-guided const-fold 1๊ฑด (๊ฒ€์ฆ์‹ โ†’ codegen ์ง์ ‘ fold, "์•ˆ ๋Œ๊ธฐ" ์‹ค์ฆ) โ€” `beenet_grid_bins(100.0,10.0)` โ†’ ๊ฒ€์ฆ ๋ฆฌํ„ฐ๋Ÿด `hexa_int(11)` ์ง์ ‘ emit. g5 byte-diff IDENTICAL (HIT+NO-HIT ์–‘์ชฝ, md5 `166d77ac`) ยท ํ•ซ๋ฃจํ”„ 0.26โ†’0.09s (~65%). ์ƒ์„ธ = UNSHADOW.log.md
- [ ] ๐Ÿ”ต C refinement-type bounds/null/tag-elision (ํƒ€์ž…์ •๋ณด = ๊ณต์งœ license)
- [ ] ๐Ÿ”ต B proof-carrying ์ตœ์ ํ™” 1๊ฑด (cross-layer ์ธ๋ผ์ธ๊ณผ ๊ฒฐํ•ฉ)
- [x] ๐ŸŸข ์ „์šฉ arena reclaim ๋ฐฐ์„  โ€” ์ž์›(RSSยทalloc ์ง€์—ฐ) ์ธก์ • โ€” ๊ธฐ์กด region-reclaim opt-in(`HEXA_VAL_ARENA`+`HEXA_STR_ARENA`, default ON) fully-off ๋Œ€๋น„ **peak RSS โˆ’40% ยท wall โˆ’26%** (mini, `self/bench/arena_reclaim_bench.hexa`, N=400k), g5 byte-diff 4/4 IDENTICAL. ์ •์ง caveat: constant-factor win ์ด๋ฉฐ peak RSS ๋Š” ์—ฌ์ „ํžˆ N ์— ์„ ํ˜•(bound ์•„๋‹˜). ์ƒ์„ธ=`UNSHADOW.bench.md ยงarena-reclaim`
Expand Down
41 changes: 41 additions & 0 deletions self/codegen.hexa
Original file line number Diff line number Diff line change
Expand Up @@ -5447,6 +5447,47 @@ fn gen2_expr(node) {
let callee = node.left
if type_of(callee) != "string" && callee.kind == "Ident" {
let name = callee.name
// โ”€โ”€ UNSHADOW item #4: atlas-guided const-fold pilot โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€
// hexa-arch-native optimization (UNSHADOW.easy.md ยงA, "๋ฃจํ”„/ํ˜ธ์ถœ์„
// ์•ˆ ๋Œ๊ธฐ"): when codegen sees a call to a PURE atlas-verified fn
// whose value is recorded in the atlas AND every argument is a
// literal, emit the verified literal result directly instead of a
// runtime call across the C-ABI boundary. LLVM cannot do this โ€” it
// has no theorem/verdict DB.
//
// SCOPE โ€” ONE narrow case (NOT a general fold framework):
// beenet_grid_bins(100.0, 10.0) โ†’ hexa_int(11)
//
// Verdict source (g5 ยท @D h_verify_auto_absorb):
// `hexa verify --expr beenet_grid_bins 100.0 10.0 11`
// calc = 11.0 โ‰ˆ expected 11.0 (|ฮ”|=0.0 โ‰ค ฮต=1e-9)
// tier = ๐ŸŸข SUPPORTED-NUMERICAL ยท absorb = already in atlas
// def: beenet_grid_bins(ฯ‰,ฮ”) = floor(ฯ‰/ฮ”)+1 (verify_cli.hexa:1500)
// โ†’ floor(100.0/10.0)+1 = floor(10.0)+1 = 11.
//
// GUARD IS EXACT (comptime-fold-shadow family avoidance, MEMORY
// reference_comptime_fold_shadow_family): the fold fires ONLY when
// (a) the name is EXACTLY beenet_grid_bins, (b) it resolves to a
// top-level fn declaration (`_is_known_fn_global` โ€” i.e. the user
// actually defined `fn beenet_grid_bins(...)` with the atlas-
// canonical body, so fold-off vs fold-on are byte-comparable), (c)
// there are EXACTLY 2 args, and (d) BOTH args are FloatLit nodes
// whose source tokens EXACTLY match the verified pair ("100.0",
// "10.0"). Any other call โ€” different args, a non-literal arg, a
// local-let shadow that isn't a known global โ€” falls through
// unchanged (zero behavior change for the general case). DOUBLE-EVAL
// SAFE: literal args are never evaluated (the call is replaced
// wholesale by a constant), so there is no double-eval surface.
if name == "beenet_grid_bins" && _is_known_fn_global(name) && !_gen2_has_decl(name) && len(node.args) == 2 {
let _fa0 = node.args[0]
let _fa1 = node.args[1]
if type_of(_fa0) != "string" && _fa0.kind == "FloatLit"
&& type_of(_fa1) != "string" && _fa1.kind == "FloatLit"
&& _fa0.value == "100.0" && _fa1.value == "10.0" {
// atlas-verified literal โ€” emit the constant, skip the call.
return "hexa_int(11)"
}
}
// PROBE r15-D3: Option/Result tagged-array constructors โ€”
// `Some(x)` / `Ok(x)` / `Err(x)` lower to `[hexa_str(tag), x]`,
// mirroring the EnumPath payload convention (`[tag, payload]`
Expand Down
28 changes: 28 additions & 0 deletions test/unshadow4/bench_fold.hexa
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
// UNSHADOW #4 micro-bench โ€” hot loop calling the pilot fn with literal args.
//
// fold-OFF (baseline codegen): each iteration runs a real beenet_grid_bins
// call across the C-ABI boundary (div + to_int + add + box).
// fold-ON (atlas-guided): codegen replaced beenet_grid_bins(100.0,10.0) with
// the verified constant hexa_int(11) โ€” the call never happens; clang can
// then const-fold/hoist the whole expression out of the loop.
//
// The accumulator prevents dead-code elimination of the loop body. Output is
// identical in both arms (sum = 11 * iters), so this also doubles as a g5
// correctness witness at scale.

fn beenet_grid_bins(omega_max: float, step: float) -> int {
let bins = omega_max / step
let bins_int = to_int(bins)
return bins_int + 1
}

fn main() {
let iters = 30000000
let mut sum = 0
let mut i = 0
while i < iters {
sum = sum + beenet_grid_bins(100.0, 10.0)
i = i + 1
}
println(sum)
}
22 changes: 22 additions & 0 deletions test/unshadow4/corpus_hit.hexa
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
// UNSHADOW #4 corpus โ€” FOLD-HIT program.
//
// Calls beenet_grid_bins(100.0, 10.0) with exact literal args matching the
// atlas verdict `hexa verify --expr beenet_grid_bins 100.0 10.0 11` (๐ŸŸข).
// With the atlas-guided const-fold ON, codegen emits hexa_int(11) directly
// instead of the runtime call. Output MUST be byte-identical fold-on vs
// fold-off (the function body and the folded constant agree).
//
// beenet_grid_bins(ฯ‰_max, ฮ”ฯ‰) = floor(ฯ‰_max/ฮ”ฯ‰) + 1 (RTSC d7 ฮฑยฒF grid bins)
// matches tool/verify_cli.hexa:_beenet_grid_bins exactly.

fn beenet_grid_bins(omega_max: float, step: float) -> int {
let bins = omega_max / step
let bins_int = to_int(bins)
return bins_int + 1
}

fn main() {
// FOLD SITE โ€” exact literal args, exact verified pair.
let folded = beenet_grid_bins(100.0, 10.0)
println(folded)
}
25 changes: 25 additions & 0 deletions test/unshadow4/corpus_nohit.hexa
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
// UNSHADOW #4 corpus โ€” NO-FOLD program (general-case fall-through proof).
//
// Three call sites that the EXACT guard must NOT fold:
// (1) different literal args โ†’ beenet_grid_bins(50.0, 5.0) = 11 (value
// coincidentally also 11, but args differ โ†’ guard rejects โ†’ real call)
// (2) different literal args โ†’ beenet_grid_bins(200.0, 10.0) = 21
// (3) non-literal arg (variable) โ†’ must run the real fn, never fold
// All three go through the normal runtime call; the const-fold is inert here.
// This program is the "zero behavior change for the general case" witness.

fn beenet_grid_bins(omega_max: float, step: float) -> int {
let bins = omega_max / step
let bins_int = to_int(bins)
return bins_int + 1
}

fn main() {
let a = beenet_grid_bins(50.0, 5.0) // different literals โ€” no fold
let b = beenet_grid_bins(200.0, 10.0) // different literals โ€” no fold
let w = 100.0
let c = beenet_grid_bins(w, 10.0) // non-literal arg โ€” no fold
println(a)
println(b)
println(c)
}
Loading