Repository navigation
Expand file tree
/
Copy pathindex.html
More file actions
510 lines (498 loc) · 36.4 KB
/
Copy pathindex.html
File metadata and controls
510 lines (498 loc) · 36.4 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
<!doctype html>
<html lang="en" class="no-js">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>How BuildLang works</title>
<meta name="description" content="An animated walk through BuildLang, a systems language with typed capability effects and native C output: a file read rejected until the function declares FileSystem, a policy profile that denies it, a check receipt that catches an edited source, HLSL from a fragment function, and a scientific-runtime receipt that re-runs a heat-equation kernel to MATCH while a forged receipt fails its seal. Built from buildlang at commit 1aa2b6b.">
<link rel="canonical" href="https://harperz9.github.io/repo-explainers/buildlang.html">
<style>
@font-face{font-family:"Hanken Grotesk";src:url("https://harperz9.github.io/system/fonts/hanken-grotesk.woff2") format("woff2");font-weight:100 900;font-style:normal;font-display:swap}
@font-face{font-family:"Conso";src:url("https://harperz9.github.io/system/fonts/conso-regular.woff2") format("woff2");font-weight:400;font-style:normal;font-display:swap}
@font-face{font-family:"Conso";src:url("https://harperz9.github.io/system/fonts/conso-semibold.woff2") format("woff2");font-weight:600;font-style:normal;font-display:swap}
:root{
color-scheme:light;
--ground:#f2efe6;--sheet:#f8f6f0;--sunk:#e8e3d7;
--ink:#111014;--ink-soft:#35322d;--muted:#5a544b;
--line:#d2c9b7;--line-strong:#8a8072;
--verified:#0f5f6a;--drift:#a2421c;--unverifiable:#5c636c;
--font-sans:"Hanken Grotesk",system-ui,-apple-system,"Segoe UI",sans-serif;
--font-mono:"Conso","JetBrains Mono",ui-monospace,"SFMono-Regular",Menlo,Consolas,monospace;
--ease:cubic-bezier(.2,.7,.2,1);
}
@media (prefers-color-scheme:dark){:root:not([data-theme="light"]){
color-scheme:dark;
--ground:#0b070a;--sheet:#120d10;--sunk:#070406;
--ink:#eaf5f6;--ink-soft:#c8dcdf;--muted:#94afb4;
--line:rgba(142,227,242,.18);--line-strong:rgba(142,227,242,.38);
--verified:#8ee3f2;--drift:#e08a62;--unverifiable:#9aa6aa;
}}
:root[data-theme="dark"]{
color-scheme:dark;
--ground:#0b070a;--sheet:#120d10;--sunk:#070406;
--ink:#eaf5f6;--ink-soft:#c8dcdf;--muted:#94afb4;
--line:rgba(142,227,242,.18);--line-strong:rgba(142,227,242,.38);
--verified:#8ee3f2;--drift:#e08a62;--unverifiable:#9aa6aa;
}
*,*::before,*::after{box-sizing:border-box}
html{-webkit-text-size-adjust:100%}
body{margin:0;background:var(--ground);color:var(--ink);font-family:var(--font-sans);font-size:17px;line-height:1.6;overflow-x:clip}
a{color:inherit;text-decoration-thickness:1px;text-underline-offset:.18em}
a:hover{text-decoration-thickness:2px}
:focus-visible{outline:2px solid var(--ink);outline-offset:3px}
code,kbd,pre,.mono{font-family:var(--font-mono);font-size:.88em}
.skip{position:absolute;left:-999px;top:0;background:var(--ink);color:var(--ground);padding:.5rem .8rem;z-index:9}
.skip:focus{left:1rem;top:1rem}
:root{--gutter:16px}
@media (min-width:700px){:root{--gutter:2rem}}
.wrap{max-width:74rem;margin:0 auto;padding:0 var(--gutter)}
header.top{padding:2.2rem 0 1.4rem;border-bottom:1px solid var(--line)}
.crumbs{font-family:var(--font-mono);font-size:.8rem;color:var(--muted);display:flex;flex-wrap:wrap;gap:.3rem 1.1rem}
h1{font-size:clamp(2.2rem,6vw,3.6rem);line-height:1.02;letter-spacing:-.02em;margin:.9rem 0 .5rem;font-weight:750}
.lede{font-size:clamp(1.15rem,2.4vw,1.4rem);line-height:1.4;max-width:40ch;margin:0;color:var(--ink-soft)}
h2{font-size:clamp(1.5rem,3.2vw,2rem);letter-spacing:-.01em;line-height:1.15;margin:0 0 .8rem;font-weight:700}
h3{font-size:1.15rem;line-height:1.3;margin:0 0 .5rem;font-weight:700}
section.block{padding:3rem 0;border-bottom:1px solid var(--line)}
.measure{max-width:62ch}
.measure p{margin:0 0 1rem}
.uses{list-style:none;padding:0;margin:1.2rem 0 0;display:grid;gap:1rem;grid-template-columns:repeat(auto-fit,minmax(15rem,1fr))}
.uses li{border-top:2px solid var(--ink);padding-top:.6rem}
.uses b{display:block;margin-bottom:.2rem}
.src{font-family:var(--font-mono);font-size:.74rem;color:var(--muted);margin-top:.6rem;overflow-wrap:anywhere}
.src a{color:var(--muted)}
/* verdict marks: the only colour on the page */
.v{font-family:var(--font-mono);font-weight:600;letter-spacing:.02em;white-space:nowrap}
.v-ok{color:var(--verified)}.v-drift{color:var(--drift)}.v-unv{color:var(--unverifiable)}
.vbox{display:inline-block;padding:.05rem .45rem;border:1.5px solid currentColor;border-radius:2px}
.vbox.v-unv{border-style:dashed}
/* the walk: a sticky stage and the steps that drive it */
.walk{display:grid;gap:2rem;grid-template-columns:minmax(0,1.2fr) minmax(0,1fr);align-items:start;margin-top:1.5rem}
.stage-wrap{position:sticky;top:1rem;height:calc(100vh - 2rem);height:calc(100svh - 2rem);display:flex;flex-direction:column;gap:.6rem;z-index:2}
.stage{position:relative;flex:1;min-height:0;background:var(--sheet);border:1px solid var(--line-strong);overflow:hidden}
.scene{position:absolute;inset:0;padding:1.1rem;overflow:auto;opacity:0;visibility:hidden;transition:opacity .45s var(--ease),visibility 0s linear .45s}
.scene.is-on{opacity:1;visibility:visible;transition:opacity .45s var(--ease),visibility 0s}
.scene svg{display:block;width:100%;height:100%}
.stage-bar{display:flex;align-items:center;gap:.6rem;font-family:var(--font-mono);font-size:.8rem}
.stage-bar .cap{flex:1;min-width:0;white-space:nowrap;overflow:hidden;text-overflow:ellipsis;color:var(--ink-soft)}
.btn{font:inherit;font-family:var(--font-mono);font-size:.8rem;color:var(--ink);background:transparent;border:1px solid var(--line-strong);border-radius:2px;padding:.45rem .7rem;cursor:pointer;min-height:2.4rem}
.btn:hover:not([disabled]){border-color:var(--ink)}
.btn[disabled]{opacity:.35;cursor:default}
.btn[aria-pressed="true"]{background:var(--ink);color:var(--ground);border-color:var(--ink)}
.steps{list-style:none;margin:0;padding:0}
.step{min-height:82vh;padding:18vh 0 2rem;outline:none}
.step:first-child{padding-top:2vh}
.step:last-child{min-height:60vh}
.step .num{font-family:var(--font-mono);font-size:.8rem;color:var(--muted)}
.step .card{border-left:2px solid var(--line);padding-left:1rem;transition:border-color .3s}
.step.is-active .card{border-left-color:var(--ink)}
.step p{margin:0 0 .8rem}
.no-js .stage-wrap{display:none}
.no-js .walk{grid-template-columns:1fr}
.no-js .step{min-height:0;padding:1rem 0}
@media (max-width:859px){
.walk{grid-template-columns:1fr;gap:0}
.stage-wrap{top:0;height:52vh;height:52svh;padding:.6rem 0;background:var(--ground);margin:0 calc(-1 * var(--gutter));padding-left:var(--gutter);padding-right:var(--gutter);border-bottom:1px solid var(--line)}
.scene{padding:.7rem}
.step{min-height:68vh;padding:4vh 0 2rem}
.step .card{background:var(--ground)}
}
/* shared stage parts */
.tag{font-family:var(--font-mono);font-size:.72rem;color:var(--muted)}
.kv{display:grid;grid-template-columns:max-content minmax(0,1fr);gap:.15rem .9rem;font-family:var(--font-mono);font-size:.8rem;margin:0}
.kv dt{color:var(--muted)}.kv dd{margin:0;overflow-wrap:anywhere}
.reveal>*{opacity:0;transform:translateY(6px);transition:opacity .4s var(--ease),transform .4s var(--ease)}
.reveal.in>*{opacity:1;transform:none}
.pick{display:flex;flex-wrap:wrap;gap:.4rem;margin-top:.8rem}
.pick .btn{font-size:.74rem;padding:.35rem .55rem;min-height:2.2rem}
/* try, limits, recall */
pre.cmd{background:var(--sunk);border:1px solid var(--line);padding:.9rem 1rem;overflow-x:auto;line-height:1.5;margin:.4rem 0 1rem;position:relative}
pre.cmd code{font-size:.85rem;white-space:pre}
.copy{position:absolute;top:.4rem;right:.4rem;font-size:.7rem;min-height:2rem;padding:.25rem .5rem;background:var(--sheet)}
.out{color:var(--ink-soft)}
.limits{padding-left:1.1rem;max-width:66ch}
.limits li{margin:0 0 .7rem}
.recall details{border-top:1px solid var(--line);padding:.8rem 0;max-width:66ch}
.recall details:last-child{border-bottom:1px solid var(--line)}
.recall summary{cursor:pointer;font-weight:650;list-style-position:outside;margin-left:1.1rem}
.recall details p{margin:.6rem 0 0 1.1rem;color:var(--ink-soft)}
footer.foot{padding:2.5rem 0 3rem;font-size:.85rem;color:var(--muted)}
footer.foot p{max-width:70ch;margin:0 0 .6rem}
.theme{margin-left:auto}
@media (prefers-reduced-motion:reduce){
*,*::before,*::after{transition-duration:0s!important;animation-duration:0s!important;animation-iteration-count:1!important;scroll-behavior:auto!important}
}
/* generic scene kit: a pipeline strip, an input/output panel, a case picker, a table */
.kscene{display:flex;flex-direction:column;gap:.8rem}
.pipe{display:grid;grid-template-columns:repeat(var(--n),minmax(0,1fr));gap:.9rem;position:relative}
.pipe .st{border:1px solid var(--line-strong);background:var(--sheet);padding:.5rem .55rem;font-size:.82rem;line-height:1.25;position:relative;transition:border-color .35s,opacity .35s;min-height:3.4rem}
.pipe .st .n{display:block;font-family:var(--font-mono);font-size:.68rem;color:var(--muted)}
.pipe .st+.st::before{content:"";position:absolute;left:-.9rem;top:50%;width:.9rem;border-top:1px solid var(--line-strong)}
.pipe .st.done{opacity:.55}
.pipe .st.on{border-color:var(--ink);border-width:2px;opacity:1}
.pipe .st.on::after{content:"";position:absolute;left:-.62rem;top:calc(50% - 4px);width:8px;height:8px;border-radius:50%;background:var(--ink);animation:kdot 1.1s var(--ease) both}
.pipe .st:first-child.on::after{display:none}
@keyframes kdot{from{transform:translateX(-14px);opacity:0}to{transform:none;opacity:1}}
@media (max-width:640px){.pipe{grid-template-columns:repeat(2,minmax(0,1fr))}.pipe .st+.st::before{display:none}.pipe .st.on::after{display:none}}
.pnote{font-family:var(--font-mono);font-size:.74rem;color:var(--muted)}
.io{border:1px solid var(--line);background:var(--sunk);font-family:var(--font-mono);font-size:.78rem;line-height:1.5;padding:.6rem .7rem;overflow-x:auto}
.io .c{color:var(--ink);font-weight:600;white-space:pre-wrap;overflow-wrap:anywhere}
.io .l{white-space:pre-wrap;overflow-wrap:anywhere;color:var(--ink-soft);opacity:0;transform:translateY(4px);transition:opacity .3s var(--ease),transform .3s var(--ease)}
.io .l.on{opacity:1;transform:none}
.io .l.hi{color:var(--ink);font-weight:600}
.io .l.dim{color:var(--muted)}
.kverdict{font-size:1.15rem;opacity:0;transition:opacity .4s}
.kverdict.on{opacity:1}
.kcap{font-size:.92rem;color:var(--ink-soft)}
.ktable{border-collapse:collapse;font-family:var(--font-mono);font-size:.76rem;width:100%}
.ktable th,.ktable td{text-align:left;border-bottom:1px solid var(--line);padding:.32rem .4rem;vertical-align:top;overflow-wrap:anywhere}
.ktable th{color:var(--muted);font-weight:400}
.ktable tr{opacity:0;transition:opacity .3s}
.ktable tr.on,.ktable thead tr{opacity:1}
</style>
</head>
<body>
<a class="skip" href="#main">Skip to content</a>
<header class="top wrap">
<div class="crumbs"><a href="https://github.com/HarperZ9/buildlang">HarperZ9/buildlang</a><span>Explainer, built from commit <a href="https://github.com/HarperZ9/buildlang/tree/1aa2b6bbb11d1ea4faaaa615b991cc48dcb950f1">1aa2b6b</a></span><a href="https://harperz9.github.io/repo-explainers.html">All repository explainers</a><button type="button" class="btn theme" data-theme-toggle>Dark page</button></div>
<h1>BuildLang</h1>
<p class="lede">A systems language where ambient access is part of a function's type.</p>
</header>
<main id="main">
<section class="block wrap" aria-labelledby="for-you">
<h2 id="for-you">What it does for you</h2>
<div class="measure">
<p>When code can read files, open sockets or call into C, you want to see that in its signature and stop it at review time. In BuildLang a function that reads a file must say <code>~ FileSystem</code>, and a policy can deny that effect for a whole program. Programs compile to native binaries through C, or to HLSL and GLSL for shaders, and a checked build or a numeric run can write a receipt that someone else re-verifies later.</p>
</div>
<ul class="uses">
<li><b>Typed capability effects</b>FileSystem, Network, Foreign and the rest are tracked through calls, closures and callbacks.</li>
<li><b>Policy profiles</b>pure, console-only, offline, ci-review and strict-accountability gate a build.</li>
<li><b>Native through C</b><code>buildc run</code> compiles to C, calls gcc, clang or MSVC, and runs the result.</li>
<li><b>Receipts you can re-run</b>A receipt seals digests and results; <code>buildc receipt verify</code> re-derives them.</li>
</ul>
<p class="src">Source: <a href="https://github.com/HarperZ9/buildlang/blob/1aa2b6bbb11d1ea4faaaa615b991cc48dcb950f1/README.md">README.md</a> at 1aa2b6b (version 1.4.0)</p>
</section>
<section class="block wrap" aria-labelledby="how">
<h2 id="how">How it works, one step at a time</h2>
<p class="measure">Scroll, or use the step buttons. Every line is output from buildc 1.4.0 built from commit 1aa2b6b, on Windows with gcc 13.2. Steps one and two use two small programs written for this page; the rest use the repository's own examples.</p>
<div class="walk">
<div class="stage-wrap">
<div class="stage" aria-label="Animated diagram for the current step">
<div class="scene" data-scene="k0" aria-hidden="true"><div class="kscene"></div></div>
<div class="scene" data-scene="k1" aria-hidden="true"><div class="kscene"></div></div>
<div class="scene" data-scene="k2" aria-hidden="true"><div class="kscene"></div></div>
<div class="scene" data-scene="k3" aria-hidden="true"><div class="kscene"></div></div>
<div class="scene" data-scene="k4" aria-hidden="true"><div class="kscene"></div></div>
<div class="scene" data-scene="k5" aria-hidden="true"><div class="kscene"></div></div>
</div>
<div class="stage-bar">
<button type="button" class="btn" data-prev>Previous</button>
<span class="cap" data-cap aria-live="polite"></span>
<span data-count></span>
<button type="button" class="btn" data-next>Next</button>
</div>
</div>
<ol class="steps">
<li class="step" tabindex="-1" data-scene="k0" data-state="s"><div class="card">
<span class="num">01</span><h3>A file read must be declared</h3>
<p>Here <code>load_config</code> calls <code>read_file</code> but its signature declares nothing. The checker rejects it, names the effect, and shows the fix: add <code>~ FileSystem</code> or handle the effect. With the effect declared on <code>load_config</code> and on <code>main</code>, the check passes.</p>
<p class="src">Source: <a href="https://github.com/HarperZ9/buildlang/blob/1aa2b6bbb11d1ea4faaaa615b991cc48dcb950f1/docs/EFFECTS_GUIDE.md">docs/EFFECTS_GUIDE.md</a></p>
</div></li>
<li class="step" tabindex="-1" data-scene="k1" data-state="s"><div class="card">
<span class="num">02</span><h3>A policy decides what is allowed</h3>
<p>Declaring an effect makes it visible; a policy decides whether it is acceptable. The same program fails the <code>console-only</code> profile on three counts, where the effect is observed, declared and propagated, and passes <code>offline</code>, which allows local file work and denies network, process, FFI and GPU.</p>
<p class="src">Source: <a href="https://github.com/HarperZ9/buildlang/blob/1aa2b6bbb11d1ea4faaaa615b991cc48dcb950f1/docs/EFFECTS_GUIDE.md">docs/EFFECTS_GUIDE.md</a>; <code>buildc policy list</code></p>
</div></li>
<li class="step" tabindex="-1" data-scene="k2" data-state="s"><div class="card">
<span class="num">03</span><h3>A check receipt catches an edit</h3>
<p><code>buildc check --receipt</code> seals what the check saw: the source digest, declared effects and observed capabilities. <code>buildc receipt verify</code> re-runs the check against the current bytes. After one string in the source changed, the digest no longer matches and verification fails.</p>
<p class="src">Source: <a href="https://github.com/HarperZ9/buildlang/blob/1aa2b6bbb11d1ea4faaaa615b991cc48dcb950f1/USAGE.md">USAGE.md</a>, <code>receipt verify</code></p>
</div></li>
<li class="step" tabindex="-1" data-scene="k3" data-state="s"><div class="card">
<span class="num">04</span><h3>Shaders from the same language</h3>
<p>A <code>#[fragment]</code> function compiles straight to HLSL for ReShade and DirectX, or to GLSL. The quickstart vignette becomes a pixel shader with the texture read and screen semantics filled in.</p>
<p class="src">Source: <a href="https://github.com/HarperZ9/buildlang/blob/1aa2b6bbb11d1ea4faaaa615b991cc48dcb950f1/examples/quickstart/vignette_shader.bld">examples/quickstart/vignette_shader.bld</a></p>
</div></li>
<li class="step" tabindex="-1" data-scene="k4" data-state="s"><div class="card">
<span class="num">05</span><h3>A numeric run with a stated invariant</h3>
<p>The heat-equation kernel prints the discrete energy at each of 400 steps. Run with <code>--invariant energy-monotone</code>, buildc compiles it through gcc, checks that no step increases energy, and seals a receipt with the source, compiler, toolchain and output digests. Energy falls from 0.5308 to 0.4069 with no violations.</p>
<p>The paired unstable kernel uses a step size past the stability limit. Its energy grows to 2.5e28, with 200 violations, and the receipt says FAIL.</p>
<p class="src">Source: <a href="https://github.com/HarperZ9/buildlang/blob/1aa2b6bbb11d1ea4faaaa615b991cc48dcb950f1/examples/heat_equation_energy.bld">examples/heat_equation_energy.bld</a>, <a href="https://github.com/HarperZ9/buildlang/blob/1aa2b6bbb11d1ea4faaaa615b991cc48dcb950f1/docs/SCIENTIFIC-RECEIPT.md">docs/SCIENTIFIC-RECEIPT.md</a></p>
</div></li>
<li class="step" tabindex="-1" data-scene="k5" data-state="s"><div class="card">
<span class="num">06</span><h3>Re-verify, and catch a forgery</h3>
<p><code>buildc receipt verify</code> recompiles and re-runs the kernel, then compares. The honest receipt reproduces: MATCH. Change the recorded final energy in the receipt to 0.5 and the seal no longer matches and verification fails.</p>
<p class="src">Source: <a href="https://github.com/HarperZ9/buildlang/blob/1aa2b6bbb11d1ea4faaaa615b991cc48dcb950f1/docs/SCIENTIFIC-RECEIPT.md">docs/SCIENTIFIC-RECEIPT.md</a></p>
</div></li>
</ol>
</div>
</section>
<section class="block wrap" aria-labelledby="try">
<h2 id="try">Try it</h2>
<div class="measure"><p>Install 1.9.0 from crates.io, then clone the repository for the examples. <code>buildc run</code> needs a C compiler (gcc, clang or MSVC) on your PATH. The standard library is compiled into <code>buildc</code> from 1.6.0, so no environment variable is needed. The page's output was recorded with 1.4.0; these commands were rerun with the crates.io 1.9.0 build on 2026-10-23 and give the same results.</p></div>
<pre class="cmd"><code>$ cargo install buildlang
$ git clone https://github.com/HarperZ9/buildlang && cd buildlang
$ buildc run examples/quickstart/ledger.bld
<span class="out">balance: 115</span>
$ buildc check examples/quickstart/hello.bld --profile console-only --receipt -
$ buildc run examples/heat_equation_energy.bld --emit-receipt receipt.json --invariant energy-monotone --problem 1d-heat-equation-energy
$ buildc receipt verify receipt.json</code></pre>
<p class="src">Output from buildc built with cargo build --release from compiler/ at 1aa2b6b, on Windows 11 with MinGW gcc 13.2. The compiler test suite was not rerun for this page; README.md records 1,818 passing in the release baseline.</p>
</section>
<section class="block wrap" aria-labelledby="limits">
<h2 id="limits">What it does not do</h2>
<ul class="limits">
<li>The C backend, effect checking, HLSL and GLSL output and the receipt tooling are the verified core. SPIR-V, LLVM IR, WebAssembly, Rust, x86-64, ARM64, GPU dispatch and <code>#[linear]</code> types are experimental.</li>
<li>A scientific receipt shows that one run's output met the stated invariant. It claims no physical law, numerical correctness or convergence.</li>
<li>The receipt layer refuses programs that use the Model capability: models propose, and the receipt only covers what an oracle can re-check.</li>
<li>While writing this page, <code>println!(read_file("ops.toml"))</code> printed the literal path ops.toml, and the file's contents were lost. The build at 1aa2b6b still does this. PR #61 makes it a compile error with a fix hint: the first argument of <code>println!</code> must be a string literal, as in <code>println!("{}", read_file("ops.toml"))</code>.</li>
</ul>
<p class="src">Source: README.md at 1aa2b6b, "Status and maturity" and "Scientific-runtime receipts"; the println! finding from the run above</p>
</section>
<section class="block wrap recall" aria-labelledby="recall">
<h2 id="recall">Check what stuck</h2>
<p class="measure">Answer each one in your head before you open it.</p>
<details><summary>A function calls read_file with no effect in its signature. What does buildc check say?</summary><p>It rejects the function and asks for ~ FileSystem or a handler.</p></details>
<details><summary>The program declares FileSystem. Does it pass the console-only profile?</summary><p>No. The policy denies FileSystem; offline would allow it.</p></details>
<details><summary>Someone edits the final value inside a scientific receipt. What fails first?</summary><p>The seal: verify reports SEAL_MISMATCH.</p></details>
</section>
</main>
<footer class="foot wrap">
<p>Built from <a href="https://github.com/HarperZ9/buildlang/tree/1aa2b6bbb11d1ea4faaaa615b991cc48dcb950f1">HarperZ9/buildlang at 1aa2b6b</a> (version 1.4.0). The source of this page is <code>docs/explainer/index.html</code> in that repository. Version 1.4.0 was released under the BuildLang Fair-Source License, Version 1.0. Releases after 1.8.0 are AGPL-3.0-only.</p>
<p>Zain Dana Harper. <a href="https://harperz9.github.io/repo-explainers.html">More repository explainers</a>.</p>
</footer>
<script>
(function () {
"use strict";
var root = document.documentElement;
root.classList.remove("no-js");
root.classList.add("js");
var rm = window.matchMedia("(prefers-reduced-motion: reduce)");
var EX = window.EX = window.EX || {};
EX.scenes = EX.scenes || {};
EX.reduced = function () { return rm.matches; };
// A timer set that one call can cancel, so a scene that loses the stage stops moving.
var timers = [];
EX.later = function (fn, ms) { var t = setTimeout(fn, ms); timers.push(t); return t; };
EX.clear = function () { timers.forEach(clearTimeout); timers = []; };
EX.el = function (tag, attrs, text) {
var svg = /^(svg|g|rect|circle|line|path|text|polyline|polygon|tspan|defs|pattern)$/.test(tag);
var n = svg ? document.createElementNS("http://www.w3.org/2000/svg", tag) : document.createElement(tag);
if (attrs) Object.keys(attrs).forEach(function (k) { n.setAttribute(k, attrs[k]); });
if (text != null) n.textContent = text;
return n;
};
// Theme: follows the system unless the reader picks one.
var tbtn = document.querySelector("[data-theme-toggle]");
if (tbtn) {
var saved = null;
try { saved = localStorage.getItem("ex-theme"); } catch (e) { saved = null; }
if (saved) root.setAttribute("data-theme", saved);
var label = function () {
var dark = root.getAttribute("data-theme") ? root.getAttribute("data-theme") === "dark"
: window.matchMedia("(prefers-color-scheme: dark)").matches;
tbtn.textContent = dark ? "Light page" : "Dark page";
return dark;
};
label();
tbtn.addEventListener("click", function () {
var next = label() ? "light" : "dark";
root.setAttribute("data-theme", next);
try { localStorage.setItem("ex-theme", next); } catch (e) { /* storage blocked: the choice lasts this visit */ }
label();
});
}
// Copy buttons on command blocks.
Array.prototype.forEach.call(document.querySelectorAll("pre.cmd"), function (pre) {
var b = EX.el("button", { type: "button", class: "btn copy" }, "Copy");
b.addEventListener("click", function () {
// Only the lines a reader types (they start with "$ ") go to the clipboard.
var all = pre.querySelector("code").innerText;
var lines = all.split("\n").filter(function (l) { return l.indexOf("$ ") === 0; })
.map(function (l) { return l.slice(2); });
var payload = lines.length ? lines.join("\n") : all;
if (navigator.clipboard) {
navigator.clipboard.writeText(payload).then(function () { b.textContent = "Copied"; },
function () { b.textContent = "Select and copy"; });
} else { b.textContent = "Select and copy"; }
setTimeout(function () { b.textContent = "Copy"; }, 1800);
});
pre.appendChild(b);
});
// The walk: a scroll position picks the active step, the step picks the scene.
function init() {
var walk = document.querySelector(".walk");
if (!walk) return;
var steps = Array.prototype.slice.call(walk.querySelectorAll(".step"));
var scenes = Array.prototype.slice.call(walk.querySelectorAll(".scene"));
var wrap = walk.querySelector(".stage-wrap");
var prev = walk.querySelector("[data-prev]");
var next = walk.querySelector("[data-next]");
var count = walk.querySelector("[data-count]");
var cap = walk.querySelector("[data-cap]");
var cur = -1;
function activate(i) {
if (i === cur) return;
cur = i;
EX.clear();
steps.forEach(function (s, k) { s.classList.toggle("is-active", k === i); });
var s = steps[i];
var name = s.getAttribute("data-scene");
scenes.forEach(function (sc) {
var on = sc.getAttribute("data-scene") === name;
sc.classList.toggle("is-on", on);
sc.setAttribute("aria-hidden", on ? "false" : "true");
if (on) sc.removeAttribute("inert"); else sc.setAttribute("inert", "");
});
count.textContent = "Step " + (i + 1) + " of " + steps.length;
cap.textContent = s.querySelector("h3").textContent;
prev.disabled = i === 0;
next.disabled = i === steps.length - 1;
var fn = EX.scenes[name];
if (fn) {
try { fn(s.getAttribute("data-state"), rm.matches); }
catch (err) { console.error("explainer scene failed", name, s.getAttribute("data-state"), err); }
}
}
function line() {
if (window.innerWidth < 860) {
// The stage sticks to the top on narrow screens, so measure it as stuck.
var h = wrap.offsetHeight;
return h + (window.innerHeight - h) * 0.35;
}
return window.innerHeight * 0.5;
}
var lockUntil = 0;
function pick() {
if (Date.now() < lockUntil) return;
var t = line(), idx = 0;
steps.forEach(function (s, k) { if (s.getBoundingClientRect().top < t) idx = k; });
activate(idx);
}
var queued = false;
window.addEventListener("scroll", function () {
if (queued) return;
queued = true;
requestAnimationFrame(function () { queued = false; pick(); });
}, { passive: true });
window.addEventListener("resize", function () { var c = cur; cur = -1; activate(c < 0 ? 0 : c); });
function go(k) {
if (k < 0 || k >= steps.length) return;
var s = steps[k];
var y = window.scrollY + s.getBoundingClientRect().top - line() + 12;
// Hold the chosen step while the smooth scroll passes the steps between.
lockUntil = Date.now() + (rm.matches ? 0 : 2500);
window.scrollTo({ top: y, behavior: rm.matches ? "auto" : "smooth" });
activate(k);
s.focus({ preventScroll: true });
}
window.addEventListener("scrollend", function () { if (lockUntil) { lockUntil = 0; pick(); } });
prev.addEventListener("click", function () { go(cur - 1); });
next.addEventListener("click", function () { go(cur + 1); });
EX.replay = function () { var c = cur; cur = -1; activate(c); };
pick();
}
if (document.readyState === "loading") document.addEventListener("DOMContentLoaded", init);
else init();
})();
</script>
<script>
window.KSCENES = {"k0": [{"pipe": {"stages": ["source", "effects", "policy", "C or shader", "run", "receipt", "re-verify"], "active": 1}}, {"cases": {"label": "Choose the source", "items": [{"label": "fn load_config() { ... }", "blocks": [{"io": {"cmd": "buildc check a.bld", "lines": ["Type errors found:", " 1:1: function `load_config` performs effect `FileSystem` but does not declare it", " help: either add `~ FileSystem` to the function signature"], "verdict": ["rejected", "drift"]}}]}, {"label": "fn load_config() ~ FileSystem { ... }", "blocks": [{"io": {"cmd": "buildc check b.bld", "lines": ["Type checking... OK", "No errors found in 'b.bld'"], "verdict": ["passes", "ok"]}}]}]}}], "k1": [{"pipe": {"stages": ["source", "effects", "policy", "C or shader", "run", "receipt", "re-verify"], "active": 2}}, {"cases": {"label": "Choose a profile", "items": [{"label": "console-only", "blocks": [{"io": {"cmd": "buildc check b.bld --profile console-only", "lines": ["Policy violation: policy denies effect `FileSystem` (observed_capabilities in load_config)", "Policy violation: policy denies effect `FileSystem` (declared_effects in main)", "Policy violation: policy denies effect `FileSystem` (propagated_effects in main)"], "verdict": ["exit 1", "drift"]}}]}, {"label": "offline", "blocks": [{"io": {"cmd": "buildc check b.bld --profile offline", "lines": ["No errors found in 'b.bld'"], "verdict": ["passes", "ok"]}}]}]}}], "k2": [{"pipe": {"stages": ["source", "effects", "policy", "C or shader", "run", "receipt", "re-verify"], "active": 6}}, {"cases": {"label": "Choose the source", "items": [{"label": "unchanged", "blocks": [{"io": {"cmd": "buildc receipt verify b.receipt.json --expect-profile offline", "lines": ["Receipt verified: b.receipt.json"], "verdict": ["verified", "ok"]}}]}, {"label": "one string edited", "blocks": [{"io": {"cmd": "buildc receipt verify b.receipt.json --expect-profile offline", "lines": ["Error: source digest mismatch: expected sha256:c1b77bf4..., actual sha256:a68ab835..."], "verdict": ["exit 1", "drift"]}}]}]}}], "k3": [{"pipe": {"stages": ["source", "effects", "policy", "C or shader", "run", "receipt", "re-verify"], "active": 3}}, {"io": {"cmd": "buildc examples/quickstart/vignette_shader.bld --target hlsl -o vignette.hlsl", "lines": ["// Target: HLSL (DirectX / ReShade)", "float4 PS_Vignette(float4 pos : SV_Position, float2 uv : TEXCOORD) : SV_Target0 {", " float4 color = tex2D(ReShade::BackBuffer, uv);", " float vig = vignette(uv.x, uv.y, 0.5, 0.6);", " return float4((color.x * vig), (color.y * vig), (color.z * vig), 1.0);"]}}], "k4": [{"pipe": {"stages": ["source", "effects", "policy", "C or shader", "run", "receipt", "re-verify"], "active": 5}}, {"cases": {"label": "Choose the kernel", "items": [{"label": "stable, r = 0.45", "blocks": [{"io": {"cmd": "buildc run examples/heat_equation_energy.bld --emit-receipt receipt.json --invariant energy-monotone", "lines": ["observed 400 values, 0.5308267 to 0.4069449", "violation_count 0", "not_claimed: numerical_correctness, convergence, pde_accuracy ..."], "verdict": ["PASS", "ok"]}}]}, {"label": "unstable, r = 0.55", "blocks": [{"io": {"cmd": "buildc run examples/heat_equation_energy_unstable.bld --emit-receipt unstable.json --invariant energy-monotone", "lines": ["observed 400 values, 0.5307 to 2.507e+28", "violation_count 200, first at step 199"], "verdict": ["FAIL", "drift", "the invariant did not hold"]}}]}]}}], "k5": [{"pipe": {"stages": ["source", "effects", "policy", "C or shader", "run", "receipt", "re-verify"], "active": 6}}, {"cases": {"label": "Choose the receipt", "items": [{"label": "as emitted", "blocks": [{"io": {"cmd": "buildc receipt verify receipt.json", "lines": ["MATCH: scientific-runtime receipt re-runs and re-checks clean", "(PASS, violation_count=0; toolchain_matched=true, raw_stdout_reproduced=true)"], "verdict": ["MATCH", "ok"]}}]}, {"label": "final value edited", "blocks": [{"io": {"cmd": "buildc receipt verify forged.json", "lines": ["Error: seal mismatch: receipt sha256:b37544c6..., recomputed sha256:52e95946...", "failure_class: SEAL_MISMATCH"], "verdict": ["exit 1", "drift"]}}]}]}}]};
</script>
<script>
(function () {
"use strict";
// Data-driven scenes: each scene is a list of blocks rendered into its .kscene node.
var EX = window.EX;
var el = function () { return EX.el.apply(null, arguments); };
var VCLS = { ok: "v-ok", drift: "v-drift", unv: "v-unv", ink: "" };
function verdictNode(v) {
var d = el("div", { class: "kverdict" });
d.appendChild(el("span", { class: "v vbox " + (VCLS[v[1]] || "") }, v[0]));
if (v[2]) d.appendChild(el("span", { class: "tag" }, " " + v[2]));
return d;
}
function render(root, blocks, reduce, t0) {
var t = t0 || 0;
var show = function (n, at) {
if (reduce) { n.classList.add("on"); return; }
EX.later(function () { n.classList.add("on"); }, at);
};
blocks.forEach(function (b) {
if (b.pipe) {
var p = el("div", { class: "pipe", style: "--n:" + b.pipe.stages.length, role: "list" });
b.pipe.stages.forEach(function (s, i) {
var cls = "st" + (i < b.pipe.active ? " done" : "") + (i === b.pipe.active ? " on" : "");
var st = el("div", { class: cls, role: "listitem" });
st.appendChild(el("span", { class: "n" }, String(i + 1).padStart(2, "0")));
st.appendChild(document.createTextNode(s));
if (i === b.pipe.active) st.setAttribute("aria-current", "step");
p.appendChild(st);
});
root.appendChild(p);
if (b.pipe.note) root.appendChild(el("div", { class: "pnote" }, b.pipe.note));
} else if (b.io) {
var io = el("div", { class: "io" });
if (b.io.cmd) io.appendChild(el("div", { class: "c" }, "$ " + b.io.cmd));
(b.io.lines || []).forEach(function (ln) {
var line = Array.isArray(ln) ? ln : [ln, ""];
var n = el("div", { class: "l " + (line[1] || "") }, line[0]);
io.appendChild(n);
t += 140; show(n, t);
});
root.appendChild(io);
if (b.io.verdict) { var v = verdictNode(b.io.verdict); root.appendChild(v); t += 260; show(v, t); }
} else if (b.verdict) {
var vv = verdictNode(b.verdict); root.appendChild(vv); t += 200; show(vv, t);
} else if (b.cap) {
root.appendChild(el("div", { class: "kcap" }, b.cap));
} else if (b.table) {
var tb = el("table", { class: "ktable" });
var th = el("thead"), hr = el("tr");
b.table.head.forEach(function (h) { hr.appendChild(el("th", null, h)); });
th.appendChild(hr); tb.appendChild(th);
var body = el("tbody");
b.table.rows.forEach(function (r) {
var tr = el("tr");
r.forEach(function (c) {
var td = el("td");
// colour stays on the summary verdict; a table cell carries the word in weight only
if (Array.isArray(c)) td.appendChild(el("span", { class: "v" }, c[0]));
else td.textContent = c;
tr.appendChild(td);
});
body.appendChild(tr); t += 120; show(tr, t);
});
tb.appendChild(body); root.appendChild(tb);
} else if (b.cases) {
var wrapc = el("div");
var pick = el("div", { class: "pick", role: "group", "aria-label": b.cases.label || "Choose a case" });
var out = el("div", { class: "kscene" });
var choose = function (k, rd) {
EX.clear();
while (out.firstChild) out.removeChild(out.firstChild);
Array.prototype.forEach.call(pick.children, function (btn, j) { btn.setAttribute("aria-pressed", j === k ? "true" : "false"); });
render(out, b.cases.items[k].blocks, rd, 0);
};
b.cases.items.forEach(function (it, k) {
var btn = el("button", { type: "button", class: "btn", "aria-pressed": "false" }, it.label);
btn.addEventListener("click", function () { choose(k, EX.reduced()); });
pick.appendChild(btn);
});
wrapc.appendChild(pick); wrapc.appendChild(out); root.appendChild(wrapc);
choose(b.cases.start || 0, reduce);
}
});
return t;
}
var specs = window.KSCENES || {};
Object.keys(specs).forEach(function (id) {
EX.scenes[id] = function (state, reduce) {
var root = document.querySelector('.scene[data-scene="' + id + '"] .kscene');
while (root.firstChild) root.removeChild(root.firstChild);
render(root, specs[id], reduce, 0);
};
});
})();
</script>
</body>
</html>