Repository navigation
Expand file tree
/
Copy pathLAWS.bend
More file actions
10678 lines (8475 loc) · 428 KB
/
Copy pathLAWS.bend
File metadata and controls
10678 lines (8475 loc) · 428 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
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
import Base
import ./src/core/auth.bend as AUTH
import ./src/core/http.bend as HTTPAUTH
import ./src/core/pcb2d.bend as PCB2 # PCB viewer text
import ./src/app/side_rows.bend as SR
import ./src/app/side_row_types.bend as SRT
import ./src/server/botnet.bend as MPLOG # mail perf runtime count
# ---- native phone i18n imports ----
import ./src/mobile/app.bend as NATIVEI18N
# ---- end native phone i18n imports ----
import ./src/core/fallback.bend as FALL
import ./src/server/server.bend as MPCREDIT # mail perf
# ---- i18n web phone imports ----
import ./src/web/view.bend as WPH
# ---- end i18n web phone imports ----
import ./src/core/schematic.bend as SC # kicad fork viewers
import ./src/core/charter.bend as CH # mail 2c
import ./src/core/mailrun.bend as MRUN # mail 2c
import ./src/app/mailroom.bend as MRUI # mail ui
import ./src/server/mailstore.bend as MIX # mail index
import ./src/app/mm.bend as MM # window memos
import ./src/core/kexport.bend as KEX
import ./src/core/i18n.bend as I18
import ./test/fixtures/i18n_fallback.bend as I18F
import ./src/core/usage.bend as UZ
import ./src/core/refview.bend as RC # links (cards, trail)
import ./src/core/order.bend as ORD # ordering (project card, buy threads)
import ./src/core/mail.bend as ML # mail 1
import ./src/core/mailbody.bend as MB # mail 2a
import ./src/core/mailview.bend as MVW # mail view
import ./src/core/ref.bend as REF
# ---- i18n cjk ----
import ./src/core/cjk.bend as CJK
# ---- end i18n cjk ----
# ---- i18n ime ----
import ./src/core/ime.bend as IMEL
import ./src/app/win.bend as WINL
# ---- end i18n ime ----
import ./src/core/kihealth.bend as KH
import ./src/core/kserve.bend as KSL
import ./src/core/tz.bend as TZ
import ./src/core/when.bend as WH
import ./src/core/sched.bend as SCH
import ./src/core/exe.bend as EX
import ./src/core/locks.bend as LCK
import ./src/core/wake.bend as WAK
import ./src/core/bothub.bend as BHS
import ./src/core/bot.bend as BOT
import ./src/core/far.bend as FR
import ./src/core/fview.bend as FVW
import ./src/core/rview.bend as RVW
import ./src/core/botui.bend as BU
import ./src/core/model.bend as M
import ./src/app/viewer.bend as V
import ./src/app/theme.bend as TH
import ./src/core/semver.bend as SV
import ./src/core/clipath.bend as CPA
import ./src/app/nui.bend as N
import ./src/app/bots.bend as BV
import ./src/app/cats.bend as VCAT
import ./src/core/sexpr.bend as KSEX # kicad fork footprint placement
import ./src/core/board.bend as B
import ./src/core/hub.bend as H
import ./src/core/deploy.bend as DP
import ./src/core/ship.bend as SHP # deploy main
import ./src/core/cmds.bend as CM
import ./src/core/errtail.bend as ERT
import ./src/core/keyring.bend as KRG
import ./src/core/ride.bend as RD
import ./src/core/adopt.bend as AD
import ./src/core/utf8.bend as UT
import ./src/core/refs.bend as RF
import ./src/core/todo.bend as TD
import ./src/core/apikeys.bend as AK
import ./src/core/onboard.bend as OBD
import ./src/core/fm.bend as FMG
import ./src/core/acp.bend as AC
import ./src/core/msp.bend as MSP
import ./src/core/mcp.bend as MC
import ./src/core/fmcp.bend as FMC
import ./src/core/handoff.bend as HD
import ./src/core/agent.bend as AG
import ./src/core/tailnet.bend as TN
import ./src/core/fuzzy.bend as FZ
import ./src/mobile/notify.bend as Nt
import ./src/core/notice.bend as NO
import ./src/core/codec.bend as C
import ./src/core/json.bend as J
import ./src/core/attach.bend as AT
import ./src/gfx/tiles.bend as T
import ./src/gfx/raster.bend as R
import ./src/gfx/draw.bend as D
import ./src/app/layout.bend as L
import ./src/core/eq.bend as Q
import ./src/core/uber.bend as UBR
import ./src/core/ubersync.bend as UBS
import ./src/core/ubop.bend as UBO
import ./src/core/plane.bend as PLN
import ./src/core/svg.bend as SVG
import ./src/core/icons.bend as ICO
import ./src/core/tools.bend as TOOL
import ./src/core/lightbox.bend as LBX
import ./src/core/links.bend as LK
import ./src/web/dom.bend as DM
import ./src/core/client.bend as U
import ./src/mobile/screen.bend as MSC
import ./src/core/gh.bend as GH
import ./src/gfx/text.bend as X
import ./src/core/fold.bend as FO
import ./src/core/subs.bend as SB
import ./src/core/http.bend as WS
import ./src/core/plot.bend as PL
import ./src/core/look.bend as LO
import ./src/core/hist.bend as HS
import ./src/mobile/view.bend as MV
import ./src/core/pcb3d.bend as P3
import ./src/gfx/mesh.bend as MS
import ./src/gfx/face.bend as FA
import ./src/core/glb.bend as G
import ./src/core/menu.bend as MN
import ./src/app/win.bend as W
import ./src/core/badge.bend as BG
import ./src/mobile/picker.bend as MP
import ./src/mobile/hubs.bend as Hb
import ./src/core/hier.bend as HI
import ./src/core/boot.bend as BT
import ./src/core/store.bend as ST
import ./src/core/sign.bend as SG
import ./src/core/ring.bend as RG
import ./src/core/cron.bend as CR
import ./src/core/space.bend as SPC
import ./src/core/google.bend as GO
import ./src/core/cat.bend as CAT
import ./src/core/perf.bend as PF
import ./src/core/prompt.bend as PM
import ./src/core/mech.bend as MCH
import ./src/core/png.bend as PNG
import ./src/core/voice.bend as VO
import ./src/core/once.bend as ON
import ./src/core/desk.bend as DK
import ./src/core/emb.bend as EMB
import ./src/core/outbox.bend as OB
import ./src/core/live.bend as LV
import ./src/core/farlive.bend as FLV
import ./src/core/qr.bend as QR
import ./src/core/layers.bend as LY
import ./src/core/bom.bend as BOM
import ./src/core/cad.bend as CAD
import ./src/core/checks.bend as CHK
import ./src/core/release.bend as REL
import ./src/core/review.bend as RV
import ./src/core/slash.bend as SL
import ./src/core/agy.bend as AGY
import ./src/core/told.bend as TLD
import ./src/core/rules.bend as RLS
import ./src/core/tboard.bend as TBD
import ./src/core/task.bend as TSK
import ./src/core/teach.bend as TCH
import ./src/core/cef.bend as CEF # browser-cef
import ./src/mobile/bots.bend as MBT
import ./src/core/cli.bend as CLI # one-hub
import ./src/core/onehub.bend as OHB # one-hub
import ./src/core/standin.bend as SIN # one-hub
# Backplane's rules, stated over the real code. `bend PROOF.bend` proves each
# one. Humans own this file: an agent may add laws, never weaken or delete
# one without the user's explicit consent.
# Equality
# --------
# a string always equals itself (viewer keys and ids rely on it)
law string_eq_refl:
for +s: String
{String.eq(s, s) == True{} : Bool}
# Settling
# --------
# a thread settles once the window has fully passed since its last activity
law settle_at_window:
for +last: Nat
for +w: Nat
{M.Settle.stale(Nat.add(last, w), last, w) == True{} : Bool}
# a thread touched just now never settles, for any non-empty window
law settle_fresh:
for +now: Nat
for +w: Nat
{M.Settle.stale(now, now, 1n+w) == False{} : Bool}
# once stale, a thread stays stale as time moves forward
law settle_monotone:
for +now: Nat
for +last: Nat
for +w: Nat
for +d: Nat
for h: {M.Settle.stale(now, last, w) == True{} : Bool}
{M.Settle.stale(Nat.add(now, d), last, w) == True{} : Bool}
# a running turn never auto-settles
law settle_never_running:
for +now: Nat
for +w: Nat
for pending: Nat
for archived: Bool
for o: M.Override
{M.Settle.auto.k(M.Thread.busy(M.Running{}, pending), archived, o, M.Settle.stale(now, now, w)) == False{} : Bool}
# a thread waiting on the user (approval, question) never auto-settles
law settle_never_pending:
for t: M.TurnState
for +p: Nat
for archived: Bool
for o: M.Override
for stale: Bool
{M.Settle.auto.k(M.Thread.busy(t, 1n+p), archived, o, stale) == False{} : Bool}
# a thread the user brought back stays back: no auto-settle overrides them
law settle_respects_unsettle:
for busy: Bool
for archived: Bool
for stale: Bool
{M.Settle.auto.k(busy, archived, M.ForcedActive{}, stale) == False{} : Bool}
# Event sourcing
# --------------
# folding one more event equals replaying the longer log: the live read
# model and a cold replay of the database can never disagree
law replay_snoc:
for es: List<&2, M.Change>
for s: M.State
for e: M.Change
{M.State.replay(List.append(&2, M.Change, es, [e]), s) == M.State.apply(M.State.replay(es, s), e) : M.State}
# Sidebar
# -------
# every thread lands on exactly one shelf: none lost, none duplicated
law sidebar_split_count:
for ts: List<&2, M.Thread>
{M.Shelves.count(M.Sidebar.split(ts)) == List.length(&2, M.Thread, ts) : Nat}
# every thread lands on exactly one shelf with snoozes too: none lost,
# none duplicated
law sidebar_split_at_count:
for ts: List<&2, M.Thread>
for +navs: Map<&2, M.Nav>
for +now: Nat
{M.Shelves.count(M.Sidebar.split.at(ts, navs, now)) == List.length(&2, M.Thread, ts) : Nat}
# Snooze
# ------
# a snoozed thread never auto-settles while its snooze lasts
law settle_never_snoozed:
for +now: Nat
for +w: Nat
for t: M.Thread
for +until: Nat
for h: {Nat.is_ge(now, until) == False{} : Bool}
{M.Settle.auto.at(now, w, t, until) == False{} : Bool}
# a snooze ends by the clock alone: once its time has come the thread is
# awake, with no event needed
law snooze_wakes:
for +now: Nat
for +until: Nat
for h: {Nat.is_ge(now, until) == True{} : Bool}
{M.Snooze.on(now, until) == False{} : Bool}
# Manual order
# ------------
# past any place on a shelf there is a later one
law key_after:
for s: List<&2, Bool>
{M.Key.lt(s, M.Key.after(s)) == True{} : Bool}
# the key made between two places sorts after the first...
law key_mid_above:
for a: List<&2, Bool>
for b: List<&2, Bool>
for h: {M.Key.lt(a, b) == True{} : Bool}
{M.Key.lt(a, M.Key.mid(a, b)) == True{} : Bool}
# ...and before the second: a dragged thread lands strictly between its
# neighbours, and they keep their keys
law key_mid_below:
for a: List<&2, Bool>
for b: List<&2, Bool>
for h: {M.Key.lt(a, b) == True{} : Bool}
{M.Key.lt(M.Key.mid(a, b), b) == True{} : Bool}
# a project dragged into place sits above every project never dragged
law project_keyed_first:
for x: Bool
for xs: List<&2, Bool>
for a: U.SRow
for b: U.SRow
{U.PSlot.before(U.PSlot{x <> xs, a}, U.PSlot{Nil{}, b}) == True{} : Bool}
# and one never dragged sits below every one that was
law project_unkeyed_below:
for a: U.SRow
for y: Bool
for ys: List<&2, Bool>
for b: U.SRow
{U.PSlot.before(U.PSlot{Nil{}, a}, U.PSlot{y <> ys, b}) == False{} : Bool}
# Sidebar status
# --------------
# an approval waiting outranks everything on a thread's dot
law status_approval_first:
for i: Bool
for t: M.TurnState
for q: Bool
{M.Status.of(True{}, i, t, q) == M.StApproval{} : M.Status}
# then a question or plan waiting, even while a turn runs
law status_input_before_work:
for t: M.TurnState
for q: Bool
{M.Status.of(False{}, True{}, t, q) == M.StInput{} : M.Status}
# then a running turn, even with messages queued
law status_working_before_queued:
for q: Bool
{M.Status.of(False{}, False{}, M.Running{}, q) == M.StWorking{} : M.Status}
# a failed turn shows as failed even with messages queued
law status_failed_before_queued:
for q: Bool
{M.Status.of(False{}, False{}, M.Failed{}, q) == M.StFailed{} : M.Status}
# nothing on a thread outranks an approval
law status_approval_top:
for a: Bool
for i: Bool
for t: M.TurnState
for q: Bool
{Nat.is_ge(M.Status.rank(M.StApproval{}), M.Status.rank(M.Status.of(a, i, t, q))) == True{} : Bool}
# Thread phase
# ------------
# an approval waiting outranks everything on a thread's phase line
law phase_approval_first:
for i: Bool
for n: Nat
for t: M.TurnState
for q: Bool
{M.Phase.of(True{}, i, n, t, q) == M.PhApproval{} : M.Phase}
# then a question or plan waiting, even while a turn or tasks run
law phase_input_before_work:
for n: Nat
for t: M.TurnState
for q: Bool
{M.Phase.of(False{}, True{}, n, t, q) == M.PhInput{} : M.Phase}
# a running turn is working, whatever its child tasks do
law phase_working_before_tasks:
for n: Nat
for q: Bool
{M.Phase.of(False{}, False{}, n, M.Running{}, q) == M.PhWorking{} : M.Phase}
# a finished turn with child tasks still running is monitoring them, not complete
law phase_monitoring_before_complete:
for n: Nat
for q: Bool
{M.Phase.of(False{}, False{}, 1n+n, M.Completed{}, q) == M.PhMonitoring{1n+n} : M.Phase}
# a finished turn with nothing left running or queued is complete
law phase_complete:
{M.Phase.of(False{}, False{}, 0n, M.Completed{}, False{}) == M.PhComplete{} : M.Phase}
# a failed turn shows as failed even with messages queued
law phase_failed_before_queued:
{M.Phase.of(False{}, False{}, 0n, M.Failed{}, True{}) == M.PhFailed{} : M.Phase}
# only a thread with nothing yet has no phase line
law phase_silent_only_idle:
for a: Bool
for i: Bool
for n: Nat
for t: M.TurnState
for q: Bool
{String.is_empty(M.Phase.label(M.Phase.of(a, i, n, t, q))) == String.eq(M.Phase.name(M.Phase.of(a, i, n, t, q)), "idle") : Bool}
# Board viewer
# ------------
# re-reading an unchanged board changes nothing: every item keeps its birth
# time, so nothing re-fades or flickers (the viewer's no-jitter promise)
law scene_merge_self:
for ss: List<&2, V.Seen>
for +now: Nat
{V.Scene.update(ss, V.Scene.items(ss), now) == ss : List<&2, V.Seen>}
# a new item starts invisible
law fade_start:
for +born: Nat
{V.Fade.alpha(born, born) == 0 : U32}
# and is fully drawn once its fade time has passed, at any later time
law fade_done:
for +born: Nat
for +k: Nat
{V.Fade.alpha(Nat.add(Nat.add(born, V.Fade.ms()), k), born) == 255 : U32}
# Layers the user turns on and off
# --------------------------------
# with nothing flipped every layer looks exactly as by default
law look_flip_none:
for +kind: U32
for +layer: U32
{V.Look.on(kind, layer, 0) == V.Look.of(kind, layer) : U32 & U32}
# flipping a shown layer hides it (F.Cu)...
law look_flip_hides:
{V.Look.shows(0, 12, V.Look.toggle(0, 12)) == False{} : Bool}
# ...and flipping a hidden one shows it (F.CrtYd)
law look_flip_shows:
{V.Look.shows(0, 17, V.Look.toggle(0, 17)) == True{} : Bool}
# the viewer's light ground shows and hides the same layers as the dark
# one (F.Cu, B.Cu and a hidden courtyard), and neither ground's bit is a
# layer's flip
law look_light_same_alpha:
{[V.Look.alpha(0, 12, V.Look.light.bit()), V.Look.alpha(0, 5, V.Look.light.bit()), V.Look.alpha(0, 17, V.Look.light.bit()), V.Look.alpha(1, 14, V.Look.light.bit())]
== [V.Look.alpha(0, 12, 0), V.Look.alpha(0, 5, 0), V.Look.alpha(0, 17, 0), V.Look.alpha(1, 14, 0)] : List<&2, U32>}
law look_grounds_not_layers:
{V.Look.shows(0, 12, U32.or(V.Look.light.bit(), V.Look.ui.bit())) == True{} : Bool}
# the dark theme draws every colour as it is
law theme_dark_as_is:
for +c: U32
{TH.Th.of(False{}, c) == c : U32}
# flipping a layer twice gives it back
law look_flip_twice:
{V.Look.toggle(V.Look.toggle(4096, 12), 12) == 4096 : U32}
# an item on a hidden layer draws nothing, wherever it is and however new
law ops_hidden_draws_nothing:
for +p: B.Prim
for +l: U32
for +v: V.View
for +c: D.Clip
for +now: Nat
for +born: Nat
for +kind: U32
for +flip: U32
for +rest: List<&2, R.Op>
for h: {V.Look.shows(kind, l, flip) == False{} : Bool}
{V.Ops.gate(True{}, p, l, v, c, now, born, kind, flip, rest) == rest : List<&2, R.Op>}
# and a click never picks it: the best pick so far stays
law pick_hidden_skipped:
for hit: Bool
for +area: F32
for +key: String
for bk: String
for +ba: F32
{V.Pick.better((hit, area), False{}, key, (bk, ba)) == (bk, ba) : String & F32}
# Updates
# -------
# a version is equal to itself
law semver_cmp_refl:
for +v: SV.Ver
{SV.Ver.cmp(v, v) == EQ{} : Cmp}
# the updater never offers the version already running
law update_never_same:
for +v: SV.Ver
{SV.Ver.newer(v, v) == False{} : Bool}
# a packaged install never updates itself: BACKPLANE_NO_UPDATE set, or
# running as an AppImage
law update_off_managed:
for +c: Char
for +t: String
for +a: String
{SV.Chan.managed(SCon{c, t}, a) == True{} : Bool}
law update_appimage_managed:
for +o: String
for +c: Char
for +t: String
{SV.Chan.managed(o, SCon{c, t}) == True{} : Bool}
# a prerelease (a nightly) sorts before the release of its version
law semver_pre_before_release:
for +a: Nat
for +b: Nat
for +c: Nat
for +d: Nat
for +n: Nat
{SV.Ver.newer(SV.Ver{a, b, c, False{}, 0n, 0n}, SV.Ver{a, b, c, True{}, d, n}) == True{} : Bool}
# a later nightly build of the same day is newer
law semver_nightly_later:
for +a: Nat
for +b: Nat
for +c: Nat
for +d: Nat
for +n: Nat
{SV.Ver.newer(SV.Ver{a, b, c, True{}, d, 1n+n}, SV.Ver{a, b, c, True{}, d, n}) == True{} : Bool}
# a nightly from a later day is newer, whatever its build number
law semver_nightly_next_day:
for +a: Nat
for +b: Nat
for +c: Nat
for +d: Nat
for +n: Nat
for +m: Nat
{SV.Ver.newer(SV.Ver{a, b, c, True{}, 1n+d, m}, SV.Ver{a, b, c, True{}, d, n}) == True{} : Bool}
# Attachments
# -----------
# a stored attachment's name uses only letters, digits, '.', '_' and '-',
# so no name can reach outside its thread's directory
law attach_clean_ok:
for s: String
{AT.Att.all_ok(AT.Att.clean(s)) == True{} : Bool}
# a dropped uri-list line that is not a file: URI (http:, a '#' comment,
# anything not starting with 'f') attaches nothing
law drop_non_file_ignored:
for c: Char
for s: String
for rest: List<&2, String>
for h: {Char.is_eq(c, 'f') == False{} : Bool}
{AT.Att.uri.one(SCon{c, s}, rest) == rest : List<&2, String>}
# a file manager's drop: file: URIs (any host) come back as their decoded
# paths, in order; comments and other schemes are dropped
law drop_uri_list_example:
{AT.Att.uri_list("# nautilus\r\nfile:///home/me/My%20Board%C3%A9.png\r\nhttps://x.org/a.png\r\nfile://localhost/tmp/b%25.txt\r\n") == ["/home/me/My Boardé.png", "/tmp/b%.txt"] : List<&2, String>}
# Models working together
# -----------------------
# a finished, failed or cancelled task never changes state again
law task_terminal_absorbing:
for cur: M.TaskState
for want: M.TaskState
for h: {M.TaskState.terminal(cur) == True{} : Bool}
{M.TaskState.next(cur, want) == cur : M.TaskState}
# a running task never goes back to the queue
law task_never_requeued:
{M.TaskState.next(M.TaskRunning{}, M.TaskQueued{}) == M.TaskRunning{} : M.TaskState}
# once delivered to its parent, a task's result is never delivered again
law task_delivered_once:
for t: M.Task
{M.Task.pending(M.Task.delivered_set(t)) == False{} : Bool}
# delegation stops at the depth limit: no chain of models spawning models
# grows without end
law delegation_bounded:
for +k: Nat
{M.Task.may_delegate(Nat.add(M.Task.max_depth(), k)) == False{} : Bool}
# Settings
# --------
# a setting never set reads as its default (settings are events, so a
# fresh or replayed store agrees on every unset key)
law setting_default:
for +k: String
for +d: String
{M.Setting.get(M.State.empty(), k, d) == d : String}
# Viewer sources
# --------------
# giving the window back its own viewer changes nothing
law nui_with_own_vw:
for n: N.Nui
{N.Nui.with_vw(n, N.Nui.vw(n)) == n : N.Nui}
# a scene read for a source the viewer no longer shows changes nothing:
# switching views or projects can never show a stale file
law stale_board_ignored:
for n: N.Nui
for +key: String
for items: List<&2, B.Item>
for +now: Nat
for h: {N.Vw.fresh_for(N.Nui.vw(n), key) == False{} : Bool}
{N.Nui.board(n, key, items, now) == n : N.Nui}
# Delivery
# --------
# a client that reconnects with the first changes already folded, and
# folds only what it missed, holds exactly what a cold replay gives
law resume_is_replay:
for a: List<&2, M.Change>
for b: List<&2, M.Change>
for s: M.State
{M.State.replay(List.append(&2, M.Change, a, b), s) == M.State.replay(b, M.State.replay(a, s)) : M.State}
# a message for a running thread is delivered into the turn at once; no
# message ever waits (Hub.deliver)
law post_running_delivers:
for +s: M.State
for +now: Nat
for +th: String
for +msg: String
for role: M.Role
for +text: String
for h1: {H.Hub.running(H.Hub.thread(s, th)) == True{} : Bool}
for h2: {M.Worktree.pending(H.Hub.thread(s, th), now) == False{} : Bool}
{H.Hub.post(s, now, th, msg, role, text) == H.Hub.deliver.r(True{}, s, now, th, msg, role, text) : H.Step}
# whatever the thread runs, delivery holds nothing back
law deliver_never_waits:
for run: Bool
for +s: M.State
for +now: Nat
for +th: String
for +msg: String
for role: M.Role
for +text: String
{H.Deliver.held(H.Queue.changes(H.Hub.deliver(run, False{}, s, now, th, msg, role, text))) == False{} : Bool}
law deliver_held_go:
for b: Bool
for +th: String
for +now: Nat
{H.Deliver.held(List.append(&2, M.Change, Bool.pick(List<&2, M.Change>, b, [], [M.QueueTaken{th, now}]), [M.TurnChanged{th, M.Running{}, now}])) == False{} : Bool}
law deliver_held_steer:
for b1: Bool
for b2: Bool
for +th: String
for +id: String
for +now: Nat
{H.Deliver.held(List.append(&2, M.Change, Bool.pick(List<&2, M.Change>, b1, [], [M.QueueTaken{th, now}]), List.append(&2, M.Change, Bool.pick(List<&2, M.Change>, b2, [], [M.ActivityLogged{th, id, "info", "steer", "Steered: the turn starts again with this message", now}]), [M.TurnChanged{th, M.Running{}, now}]))) == False{} : Bool}
law deliver_held_steer_k:
for c: Bool
for +s: M.State
for +now: Nat
for +th: String
for +msg: String
for role: M.Role
for +text: String
{H.Deliver.held(H.Queue.changes(H.Hub.deliver.steer(c, s, now, th, msg, role, text))) == False{} : Bool}
# Claude takes it on its input, mid-turn
law deliver_claude_running:
{H.Queue.changes(H.Hub.post(H.Demo.state("claude", M.Running{}), 5n, "t1", "m1", M.User{}, "hi")) == [M.MessagePosted{"t1", "m1", M.User{}, "hi", 5n}, M.TurnChanged{"t1", M.Running{}, 5n}] : List<&2, M.Change>}
# a message the server already stored (resent after a dropped link) is not
# stored again, and starts nothing
law resend_stored_once:
for +s: M.State
for +now: Nat
for +client: U32
for +id: String
for +th: String
for +text: String
for +msg: String
for h1: {String.is_empty(msg) == False{} : Bool}
for h2: {H.Hub.has_msg(H.Hub.entries(s), msg) == True{} : Bool}
{H.Queue.changes(H.Hub.turn(s, now, client, id, th, text, msg)) == [] : List<&2, M.Change>}
# an unnamed message is never taken for one already stored: only a named
# one is looked up
law has_msg_unnamed_skips:
for s: M.State
for msg: String
{H.Hub.dup(False{}, s, msg) == False{} : Bool}
# a thread's last reply is its newest assistant message, read from its own
# entries; what it sent another thread is not its reply
law mcp_last_newest:
{MC.Mcp.last(M.State.mine(M.State.replay([M.MessagePosted{"t1", "m1", M.Assistant{}, "first", 3n}, M.MessagePosted{"t1", "m2", M.Assistant{}, "second", 4n}, M.MessagePosted{"t2", M.Link.id("t1", "x"), M.Assistant{}, "to t2", 5n}], H.Demo.state("claude", M.Completed{})), "t1"), "t1") == "second" : String}
# a step that ends no turn finishes no task: it comes back as it was
law task_finish_not_ended_same:
for +s: M.State
for +now: Nat
for +thread: String
for +cs: List<&2, M.Change>
for os: List<&2, H.Out>
for h: {H.Task.ended(cs) == H.NotEnded{} : H.Ended}
{H.Task.finish(s, now, thread, H.Step{cs, os}) == H.Step{cs, os} : H.Step}
# a message from another thread is delivered into the target's running
# turn like any other
law inbox_running_delivers:
for +s: M.State
for +now: Nat
for +from: String
for +to: String
for role: M.Role
for +text: String
for +msg: String
for h1: {H.Hub.running(H.Hub.thread(s, to)) == True{} : Bool}
for h2: {M.Worktree.pending(H.Hub.thread(s, to), now) == False{} : Bool}
{H.Hub.inbox.id(s, now, from, to, role, text, msg) == H.Hub.deliver.r(True{}, s, now, to, msg, role, text) : H.Step}
# Worktrees
# ---------
# a thread in the project folder never waits for a worktree
law worktree_pending_local:
for +wt: String
for +c: Nat
for +now: Nat
{M.Worktree.pending.k(M.Local{}, wt, c, now) == False{} : Bool}
# no thread waits for its worktree past the wait: its messages then run in
# the project folder
law worktree_pending_ends:
for e: M.EnvMode
for +wt: String
for +c: Nat
for +now: Nat
for h: {Nat.is_lt(now, Nat.add(c, M.Worktree.wait())) == False{} : Bool}
{M.Worktree.pending.k(e, wt, c, now) == False{} : Bool}
# a message to a thread whose worktree is still being made starts nothing:
# it waits in the thread's queue
law worktree_waits:
for +s: M.State
for +now: Nat
for +th: String
for +msg: String
for role: M.Role
for +text: String
for h: {M.Worktree.pending(H.Hub.thread(s, th), now) == True{} : Bool}
{H.Step.outs_of(H.Hub.post(s, now, th, msg, role, text)) == [] : List<&2, H.Out>}
# only "local" asks for the project folder; every other mode (the default
# "auto" included) asks for a worktree
law worktree_by_default:
{H.Hub.env.of("auto") == M.Worktree{} : M.EnvMode}
# a message to a thread whose worktree was removed makes it again from the
# kept branch, and does nothing else: the turn waits for the worktree and
# never runs in the project folder
law worktree_revives:
for +s: M.State
for +now: Nat
for +th: String
for +msg: String
for role: M.Role
for +text: String
for h1: {H.Hub.running(H.Hub.thread(s, th)) == False{} : Bool}
for h2: {M.Worktree.gone(H.Hub.thread(s, th)) == True{} : Bool}
for h3: {M.Worktree.pending(H.Hub.thread(s, th), now) == False{} : Bool}
{H.Step.outs_of(H.Hub.post(s, now, th, msg, role, text)) == [H.Wt.revive(s, th)] : List<&2, H.Out>}
# a worktree is never removed while its thread works or waits on the user
law worktree_kept_while_busy:
for sh: M.Shelf
for +ours: Bool
for merged: Bool
for aged: Bool
{M.Worktree.drop.k(True{}, sh, ours, merged, aged) == False{} : Bool}
# a worktree is never removed while its thread is out (active, pinned,
# snoozed): only settled or hidden threads lose theirs
law worktree_kept_out:
for busy: Bool
for sh: M.Shelf
for +ours: Bool
for merged: Bool
for aged: Bool
for h: {M.Worktree.parked(sh) == False{} : Bool}
{M.Worktree.drop.k(busy, sh, ours, merged, aged) == False{} : Bool}
# only a directory Backplane made (under .backplane/worktrees) is removed
law worktree_kept_unless_ours:
for busy: Bool
for sh: M.Shelf
for +wt: String
for merged: Bool
for aged: Bool
for h: {M.Worktree.ours(wt) == False{} : Bool}
{M.Worktree.drop.k(busy, sh, M.Worktree.ours(wt), merged, aged) == False{} : Bool}
# a settled thread that was not merged keeps its worktree for the window
law worktree_kept_fresh:
for +ours: Bool
{M.Worktree.drop.k(False{}, M.Settled{}, ours, False{}, False{}) == False{} : Bool}
# a merged (so settled) idle thread's worktree goes at once
law worktree_dropped_on_merge:
for aged: Bool
{M.Worktree.drop.k(False{}, M.Settled{}, True{}, True{}, aged) == True{} : Bool}
# a settled idle thread's worktree goes once the window has passed
law worktree_dropped_when_aged:
for merged: Bool
{M.Worktree.drop.k(False{}, M.Settled{}, True{}, merged, True{}) == True{} : Bool}
# so does a hidden (archived or deleted) thread's
law worktree_dropped_when_hidden:
for merged: Bool
{M.Worktree.drop.k(False{}, M.Hidden{}, True{}, merged, True{}) == True{} : Bool}
# Merges
# ------
# a merged thread settles, pinned or brought back before or not
law merge_settles:
for t: M.Thread
for +at: Nat
for h: {M.Thread.hidden(t) == False{} : Bool}
{M.Shelf.of(M.Thread.settled(True{}, at, t)) == M.Settled{} : M.Shelf}
# a recorded merge is never due again, so it settles a thread once
law merge_once:
for sh: M.Shelf
for +branch: String
for +url: String
for h: {String.is_empty(url) == False{} : Bool}
{M.Merge.due.k(sh, branch, url) == False{} : Bool}
# a thread without a branch is never merged
law merge_needs_branch:
for sh: M.Shelf
for +merged: String
{M.Merge.due.k(sh, "", merged) == False{} : Bool}
# GitHub accounts
# ---------------
# the account a repository worked with before is tried first
law gh_pick_saved:
for owner_in: Bool
for +saved: String
for +owner: String
for +active: String
{GH.Gh.pick(True{}, saved, owner_in, owner, active) == saved : String}
# else the account named like the remote's owner
law gh_pick_owner:
for +saved: String
for +owner: String
for +active: String
{GH.Gh.pick(False{}, saved, True{}, owner, active) == owner : String}
# else gh's active account: Backplane never switches it
law gh_pick_active:
for +saved: String
for +owner: String
for +active: String
{GH.Gh.pick(False{}, saved, False{}, owner, active) == active : String}
# the first choice is tried first
law gh_order_first:
for +first: String
for us: List<&2, String>
{List.head(&2, String, GH.Gh.order.k(first, us)) == Some{first} : Maybe<&2, String>}
# and never again: the rest leaves it out
law gh_without_drops:
for us: List<&2, String>
for +u: String
{GH.Gh.has(GH.Gh.without(us, u), u) == False{} : Bool}
# Phone alerts
# ------------
# a phone alerts only for a turn it saw running: connecting, or a thread
# that never ran, raises nothing
law alert_needs_running:
for t: M.TurnState
{Nt.Note.kind(False{}, t) == "" : String}
# a turn still running never alerts
law alert_never_running:
for b: Bool
{Nt.Note.kind(b, M.Running{}) == "" : String}
# a stop the user asked for is not news
law alert_not_on_stop:
for b: Bool
{Nt.Note.kind(b, M.Interrupted{}) == "" : String}
# connecting (no turn seen running yet) raises no alerts, however many
# threads and finished turns the log holds
law alert_none_on_connect:
for ts: List<&2, M.Thread>
for +st: M.State
for +es: List<&2, M.Entry>
for +desk: String
{Nt.Note.alerts(ts, [], st, es, desk) == [] : List<&2, J.Json>}
# One item, one alert (core/notice.bend). Notice.decide(failed, bot,
# asking, posted, first, msg): 0 no alert, 1 an alert, 2 a failure.
# a failed turn always alerts, as a failure
law notice_fail_always:
for bot: Bool
for asking: Bool
for posted: Bool
for first: Bool
for msg: Bool
{NO.Notice.decide(True{}, bot, asking, posted, first, msg) == 2n : Nat}
# a thread that is not a bot's alerts when it finishes: work the person started
law notice_thread_kept:
for asking: Bool
for posted: Bool
for first: Bool
for msg: Bool
{NO.Notice.decide(False{}, False{}, asking, posted, first, msg) == 1n : Nat}
# a bot waiting on the person alerts, whatever else its turn did
law notice_ask_kept:
for posted: Bool
for first: Bool
for msg: Bool
{NO.Notice.decide(False{}, True{}, True{}, posted, first, msg) == 1n : Nat}
# a room exchange alerts once: a bot post after the exchange's first is quiet
law notice_room_once:
for msg: Bool
{NO.Notice.decide(False{}, True{}, False{}, True{}, False{}, msg) == 0n : Nat}
# a bot woken by a room or bot message that posted nothing is quiet
law notice_chatter_quiet:
for first: Bool
{NO.Notice.decide(False{}, True{}, False{}, False{}, first, True{}) == 0n : Nat}
# an earlier bot post in the same room (not the person's, not this turn's)
# means the exchange already alerted
law notice_earlier_bot_quiet:
{NO.Vd.room(True{}, False{}, False{}, True{}) == NO.VNo{} : NO.Vd}
# a person's post starts a new exchange
law notice_person_opens:
for own: Bool
for bot: Bool
{NO.Vd.room(True{}, True{}, own, bot) == NO.VYes{} : NO.Vd}
# past the window, older posts no longer hold an alert back
law notice_window_opens:
for +room: String
for +name: String
for +start: Nat
for local: Bool
for p: BOT.Post
{NO.Vd.post(True{}, room, name, start, local, p) == NO.VYes{} : NO.Vd}
# a phone paired with several hubs names every thread and project by its
# hub ("key|id"), but "nothing selected" stays nothing, on any hub
law hubs_no_id:
for +k: String
{Hb.Hubs.id(k, "") == "" : String}
# the screen's id walk knows every name it treats apart: the hash that
# turns keys away first never turns one of them away
law q_kind_names:
{Hb.Q.own(Hb.QN{"value", 2n} <> Hb.QN{"id", 2n} <> Hb.Q.names()) == True{} : Bool}
# a phone builds no screen for streamed text from a hub not in focus...
law hubs_delta_elsewhere:
for +hs: Hb.Hubs
for +key: String
for +o: J.Json
for h: {String.eq(key, Hb.Hubs.cur(hs)) == False{} : Bool}
{Hb.Hubs.shows(hs, key, o) == False{} : Bool}
# ...nor for a thread other than the one open on the hub in focus
law hubs_delta_other_thread:
for +hs: Hb.Hubs
for +th: String
for +text: String
for h: {String.eq(th, U.Ui.sel(Hb.Hubs.ui(hs, Hb.Hubs.cur(hs)))) == False{} : Bool}
{Hb.Hubs.shows(hs, Hb.Hubs.cur(hs), J.Json.obj([J.KV{"t", J.Str{"delta"}}, J.KV{"thread", J.Str{th}}, J.KV{"text", J.Str{text}}])) == False{} : Bool}
# the phone redraws for any message from any paired hub (the merged
# sidebar and the island show them all); streamed text only as Hubs.shows
# says: not from a hub out of focus, nor for another thread
law hubs_redraw_changes_elsewhere:
for +hs: Hb.Hubs
for +key: String
for +items: List<&2, J.Json>
{Hb.Hubs.redraw(hs, key, J.Json.obj([J.KV{"t", J.Str{"changes"}}, J.KV{"items", J.Json.arr(items)}])) == True{} : Bool}