feat(rules)!: regroup, demote and retire rules after the audit

.github/workflows/ci.yml

@@ -12,3 +12,8 @@ on:
 jobs:
   check:
     uses: Emerging-Patterns/actions/.github/workflows/nix-flake-check.yml@5b0aa4f0eaee72662e06479ecebcfd15e9762fe7
+    with:
+      # the shared default still names macos-14, which GitHub retires on
+      # 2026-11-02 and fails in brownouts before then (no runner is assigned);
+      # macos-15 is arm64 too, so aarch64-darwin is still checked
+      runners: '["ubuntu-latest", "ubuntu-24.04-arm", "macos-15"]'

AGENTS.md

@@ -9,7 +9,8 @@ writing Bend. Then this.
 If Bend can state it as a quantified law (a `for` or `exs` binder, IO
 values included), it goes in a law file under `laws/` and its proof under
 `proofs/`. A law with no
-binder is a unit test the checker runs, not a guarantee: `closed` reports
+binder is a unit test the checker runs, not a guarantee: `closed` (opt-in,
+on in this repo's bolt.bend) reports
 it, and it does not go in at all (docs/rfc/bolt-spec.md).
 
 `tests/*.bend` and `#|` exist only for claims Bend cannot prove:
@@ -174,7 +175,7 @@ Design specs and plans are not kept in this repo; they live under
   it) stay right for expensive work that does not recurse. The same goes for
   any expensive expression in a branch: a scan of the whole token list inside
   a per-token pick runs for every token (bind's notes were 20 s that way,
-  20 ms as one pass). `bolt`'s `strict` rule catches the Bool.and/or shape.
+  20 ms as one pass). `bolt`'s `strict` rule (pedantic) catches the Bool.and/or shape.
 - A destructure or a `match` needs a variable, never a call:
   `Out{a, b} = f(x)` is "a match cannot scrutinize a computed value"; bind the
   call first, or take it apart in a helper that receives it as a parameter.

LAWS.bend

@@ -76,19 +76,18 @@ import ./laws/ForeignReportsMissingBackend.bend as ForeignReportsMissingBackend
 import ./laws/FromrevExempt.bend as FromrevExempt
 import ./laws/FromrevReportsReversedStringBuild.bend as FromrevReportsReversedStringBuild
 import ./laws/FuelReportsLiteralBudgets.bend as FuelReportsLiteralBudgets
-import ./laws/HoistReportsTablesInLoops.bend as HoistReportsTablesInLoops
 import ./laws/HoleReportsEachTodo.bend as HoleReportsEachTodo
 import ./laws/IndexReportsGetsInRecursion.bend as IndexReportsGetsInRecursion
 import ./laws/InertConcatCont.bend as InertConcatCont
 import ./laws/InertFromrev.bend as InertFromrev
 import ./laws/InertTranscong.bend as InertTranscong
+import ./laws/ImportReachIsClosed.bend as ImportReachIsClosed
 import ./laws/LawNamesEveryItem.bend as LawNamesEveryItem
 import ./laws/ParamReportsShortNames.bend as ParamReportsShortNames
 import ./laws/PickReportsSelfCalls.bend as PickReportsSelfCalls
 import ./laws/PickReportsBoundSearches.bend as PickReportsBoundSearches
 import ./laws/PutReportsMapPutCalls.bend as PutReportsMapPutCalls
 import ./laws/RewalkReportsRepeatedWalks.bend as RewalkReportsRepeatedWalks
-import ./laws/RingReportsDropAppendRotation.bend as RingReportsDropAppendRotation
 import ./laws/RoleClosed.bend as RoleClosed
 import ./laws/RoleClosedExempt.bend as RoleClosedExempt
 import ./laws/RoleConcat.bend as RoleConcat
@@ -97,7 +96,6 @@ import ./laws/RoleDocExempt.bend as RoleDocExempt
 import ./laws/RoleEager.bend as RoleEager
 import ./laws/RoleFromrev.bend as RoleFromrev
 import ./laws/RoleFromrevExempt.bend as RoleFromrevExempt
-import ./laws/RoleHoist.bend as RoleHoist
 import ./laws/RoleHole.bend as RoleHole
 import ./laws/RoleHoleExempt.bend as RoleHoleExempt
 import ./laws/RoleIndex.bend as RoleIndex
@@ -110,27 +108,18 @@ import ./laws/RolePick.bend as RolePick
 import ./laws/RoleProofNamed.bend as RoleProofNamed
 import ./laws/RoleReached.bend as RoleReached
 import ./laws/RoleRewalk.bend as RoleRewalk
-import ./laws/RoleRing.bend as RoleRing
-import ./laws/RoleScan.bend as RoleScan
-import ./laws/RoleScanExempt.bend as RoleScanExempt
 import ./laws/RoleStrict.bend as RoleStrict
-import ./laws/RoleTable.bend as RoleTable
 import ./laws/RoleTail.bend as RoleTail
 import ./laws/RoleThunk.bend as RoleThunk
-import ./laws/RoleUnit.bend as RoleUnit
-import ./laws/ScanReportsCarriedArgumentWalks.bend as ScanReportsCarriedArgumentWalks
 import ./laws/ScopeConcatCont.bend as ScopeConcatCont
 import ./laws/ScopeExemptionsFollowPaths.bend as ScopeExemptionsFollowPaths
 import ./laws/SpaceReportsBlanksAndWidth.bend as SpaceReportsBlanksAndWidth
 import ./laws/StrictReportsEagerSelfCalls.bend as StrictReportsEagerSelfCalls
 import ./laws/StringsReportLongLiteralArms.bend as StringsReportLongLiteralArms
-import ./laws/TableReportsFixedTableAccess.bend as TableReportsFixedTableAccess
 import ./laws/TailReportsNonTailCalls.bend as TailReportsNonTailCalls
 import ./laws/ThunkReportsIgnoredSelfCallLambdas.bend as ThunkReportsIgnoredSelfCallLambdas
 import ./laws/TranscongReportsTransCongChains.bend as TranscongReportsTransCongChains
 import ./laws/TwiceReportsRepeatedListLiteral.bend as TwiceReportsRepeatedListLiteral
-import ./laws/UnitReportsMultiplyByOne.bend as UnitReportsMultiplyByOne
-import ./laws/UnsafeReportsReachableForeignDefs.bend as UnsafeReportsReachableForeignDefs
 import ./laws/UnusedReportsDeadBinders.bend as UnusedReportsDeadBinders
 import ./laws/WrapReportsBrokenHeaderShape.bend as WrapReportsBrokenHeaderShape
 import ./laws/LspAnswersEachRequestOnce.bend as LspAnswersEachRequestOnce
@@ -140,6 +129,7 @@ import ./laws/LspFramesCountBytes.bend as LspFramesCountBytes
 import ./laws/LspNavigationUsesBinder.bend as LspNavigationUsesBinder
 import ./laws/LspPositionsUseNegotiatedEncoding.bend as LspPositionsUseNegotiatedEncoding
 import ./laws/LspPublishesOnDocumentEvents.bend as LspPublishesOnDocumentEvents
+import ./laws/LspKeepsRoleMarks.bend as LspKeepsRoleMarks
 import ./laws/LspUnitsMatchCharsBelowAstral.bend as LspUnitsMatchCharsBelowAstral
 import ./laws/ArrowTerm.bend as ArrowTerm
 import ./laws/AttributeDef.bend as AttributeDef

PROOF.bend

@@ -61,19 +61,18 @@ import ./proofs/ForeignReportsMissingBackend.bend as PForeignReportsMissingBacke
 import ./proofs/FromrevExempt.bend as PFromrevExempt
 import ./proofs/FromrevReportsReversedStringBuild.bend as PFromrevReportsReversedStringBuild
 import ./proofs/FuelReportsLiteralBudgets.bend as PFuelReportsLiteralBudgets
-import ./proofs/HoistReportsTablesInLoops.bend as PHoistReportsTablesInLoops
 import ./proofs/HoleReportsEachTodo.bend as PHoleReportsEachTodo
 import ./proofs/IndexReportsGetsInRecursion.bend as PIndexReportsGetsInRecursion
 import ./proofs/InertConcatCont.bend as PInertConcatCont
 import ./proofs/InertFromrev.bend as PInertFromrev
 import ./proofs/InertTranscong.bend as PInertTranscong
+import ./proofs/ImportReachIsClosed.bend as PImportReachIsClosed
 import ./proofs/LawNamesEveryItem.bend as PLawNamesEveryItem
 import ./proofs/ParamReportsShortNames.bend as PParamReportsShortNames
 import ./proofs/PickReportsSelfCalls.bend as PPickReportsSelfCalls
 import ./proofs/PickReportsBoundSearches.bend as PPickReportsBoundSearches
 import ./proofs/PutReportsMapPutCalls.bend as PPutReportsMapPutCalls
 import ./proofs/RewalkReportsRepeatedWalks.bend as PRewalkReportsRepeatedWalks
-import ./proofs/RingReportsDropAppendRotation.bend as PRingReportsDropAppendRotation
 import ./proofs/RoleClosed.bend as PRoleClosed
 import ./proofs/RoleClosedExempt.bend as PRoleClosedExempt
 import ./proofs/RoleConcat.bend as PRoleConcat
@@ -82,7 +81,6 @@ import ./proofs/RoleDocExempt.bend as PRoleDocExempt
 import ./proofs/RoleEager.bend as PRoleEager
 import ./proofs/RoleFromrev.bend as PRoleFromrev
 import ./proofs/RoleFromrevExempt.bend as PRoleFromrevExempt
-import ./proofs/RoleHoist.bend as PRoleHoist
 import ./proofs/RoleHole.bend as PRoleHole
 import ./proofs/RoleHoleExempt.bend as PRoleHoleExempt
 import ./proofs/RoleIndex.bend as PRoleIndex
@@ -95,27 +93,18 @@ import ./proofs/RolePick.bend as PRolePick
 import ./proofs/RoleProofNamed.bend as PRoleProofNamed
 import ./proofs/RoleReached.bend as PRoleReached
 import ./proofs/RoleRewalk.bend as PRoleRewalk
-import ./proofs/RoleRing.bend as PRoleRing
-import ./proofs/RoleScan.bend as PRoleScan
-import ./proofs/RoleScanExempt.bend as PRoleScanExempt
 import ./proofs/RoleStrict.bend as PRoleStrict
-import ./proofs/RoleTable.bend as PRoleTable
 import ./proofs/RoleTail.bend as PRoleTail
 import ./proofs/RoleThunk.bend as PRoleThunk
-import ./proofs/RoleUnit.bend as PRoleUnit
-import ./proofs/ScanReportsCarriedArgumentWalks.bend as PScanReportsCarriedArgumentWalks
 import ./proofs/ScopeConcatCont.bend as PScopeConcatCont
 import ./proofs/ScopeExemptionsFollowPaths.bend as PScopeExemptionsFollowPaths
 import ./proofs/SpaceReportsBlanksAndWidth.bend as PSpaceReportsBlanksAndWidth
 import ./proofs/StrictReportsEagerSelfCalls.bend as PStrictReportsEagerSelfCalls
 import ./proofs/StringsReportLongLiteralArms.bend as PStringsReportLongLiteralArms
-import ./proofs/TableReportsFixedTableAccess.bend as PTableReportsFixedTableAccess
 import ./proofs/TailReportsNonTailCalls.bend as PTailReportsNonTailCalls
 import ./proofs/ThunkReportsIgnoredSelfCallLambdas.bend as PThunkReportsIgnoredSelfCallLambdas
 import ./proofs/TranscongReportsTransCongChains.bend as PTranscongReportsTransCongChains
 import ./proofs/TwiceReportsRepeatedListLiteral.bend as PTwiceReportsRepeatedListLiteral
-import ./proofs/UnitReportsMultiplyByOne.bend as PUnitReportsMultiplyByOne
-import ./proofs/UnsafeReportsReachableForeignDefs.bend as PUnsafeReportsReachableForeignDefs
 import ./proofs/UnusedReportsDeadBinders.bend as PUnusedReportsDeadBinders
 import ./proofs/WrapReportsBrokenHeaderShape.bend as PWrapReportsBrokenHeaderShape
 import ./proofs/LspAnswersEachRequestOnce.bend as PLspAnswersEachRequestOnce
@@ -125,6 +114,7 @@ import ./proofs/LspFramesCountBytes.bend as PLspFramesCountBytes
 import ./proofs/LspNavigationUsesBinder.bend as PLspNavigationUsesBinder
 import ./proofs/LspPositionsUseNegotiatedEncoding.bend as PLspPositionsUseNegotiatedEncoding
 import ./proofs/LspPublishesOnDocumentEvents.bend as PLspPublishesOnDocumentEvents
+import ./proofs/LspKeepsRoleMarks.bend as PLspKeepsRoleMarks
 import ./proofs/LspUnitsMatchCharsBelowAstral.bend as PLspUnitsMatchCharsBelowAstral
 import ./proofs/ArrowTerm.bend as PArrowTerm
 import ./proofs/AttributeDef.bend as PAttributeDef

README.md

@@ -154,8 +154,10 @@ def space() -> String:
 ```
 
 The groups are `correctness` (`hole`, `pick`, `put`; error by default),
-`suspicious` (`unused`), `style` (`doc`, `space`, `wrap`, `param`) and `laws` (`coverage`), the
-rest warn by default. Every rule, and the config in full, is in
+`suspicious` (`unused`), `perf` (`strings`, `chars`), `style` (`doc`, `space`,
+`wrap`, `param`) and `laws`, the rest warn by default, and `pedantic` (`tail`,
+`strict`, `index`), off by default. The laws rules, `coverage` and `closed`,
+are opt-in: a project that keeps laws turns each on by name. Every rule, and the config in full, is in
 [src/README.md](src/README.md).
 
 ## Develop

bolt.bend

@@ -1,5 +1,6 @@
 # bolt.bend: how bolt lints this repo. Every rule is an error except `coverage`,
-# which warns until the laws exist: the gate must see no errors. See
+# which warns until the laws exist: the gate must see no errors. The opt-in
+# and pedantic rules are turned on by name or group below. See
 # src/config.bend for the groups and levels.
 import Base
 
@@ -11,20 +12,29 @@ def correctness() -> String:
 def suspicious() -> String:
   "error"
 
+# what is slow but right
+def perf() -> String:
+  "error"
+
 # comments and whitespace
 def style() -> String:
   "error"
 
+# advice that is noisy on idiomatic code, held here all the same: foreign,
+# strict, fuel, index and rewalk were errors here before they moved
+def pedantic() -> String:
+  "error"
+
+# but not a tail call on every step
+def tail() -> String:
+  "off"
+
 # a def named by no law, IO included: advice while guarantees are pending,
 # since deleting the closed laws left defs no law names. That rule
-# is `coverage` (L001), which `def coverage()` could also set on its own.
-def laws() -> String:
+# is `coverage` (L001), opt-in, so only its own setting turns it on.
+def coverage() -> String:
   "warn"
 
-# a law with no binder
+# a law with no binder (opt-in)
 def closed() -> String:
   "error"
-
-# an @unsafe def a law file reaches
-def unsafe() -> String:
-  "error"

laws/CharsReportManyCharArms.bend

@@ -7,7 +7,7 @@ import ../src/syntax/bind.bend as Bind
 import ../src/src.bend as Src
 import ../src/syntax/tree.bend as Tree
 import ../src/syntax/outline.bend as Outline
-import ../src/rules/correctness/chars.bend as Chars
+import ../src/rules/perf/chars.bend as Chars
 import ./defs/MatchArmRules.bend as D1
 
 # one when a case statement's first match column opens with a char literal,

laws/CodeRulesIgnoreCommentsAndStrings.bend

@@ -20,18 +20,13 @@ import ../src/rules/correctness/pick.bend as Pick
 import ../src/rules/pedantic/tail.bend as Tail
 import ../src/rules/suspicious/concat.bend as Concat
 import ../src/rules/suspicious/eager.bend as Eager
-import ../src/rules/suspicious/strict.bend as Strict
-import ../src/rules/suspicious/hoist.bend as Hoist
-import ../src/rules/suspicious/index.bend as Index
-import ../src/rules/suspicious/ring.bend as Ring
-import ../src/rules/suspicious/table.bend as Table
-import ../src/rules/suspicious/unit.bend as UnitRule
+import ../src/rules/pedantic/strict.bend as Strict
+import ../src/rules/pedantic/index.bend as Index
 import ../src/rules/suspicious/thunk.bend as Thunk
-import ../src/rules/suspicious/scan.bend as Scan
 import ../src/rules/tokens.bend as T
 import ../src/rules/correctness/arms.bend as Arms
 import ../src/rules/suspicious/unused.bend as Unused
-import ../src/rules/suspicious/fuel.bend as FuelRule
+import ../src/rules/pedantic/fuel.bend as FuelRule
 import ../src/rules/style/wrap.bend as Wrap
 import ./defs/InertText.bend as D1
 
@@ -220,27 +215,6 @@ law inert_param:
   for e: {inert.binds(b1) == inert.binds(b2) : List<&2, Bind.Bind>}
   {Param.check.on(b1, path) == Param.check.on(b2, path) : List<&2, F.Finding>}
 
-# LAW: table reads what no string says: two sources as the lexer makes them
-# whose trees read the same with strings cut have the same findings (a
-# string's text is only ever compared with a call's or a table's name)
-law inert_table:
-  for +path: String
-  for text: String
-  for +tree: Tree.Node
-  for toks: List<&2, Lex.Tok>
-  for bound: Bind.Bound
-  for items: List<&2, Outline.Item>
-  for text2: String
-  for +tree2: Tree.Node
-  for toks2: List<&2, Lex.Tok>
-  for bound2: Bind.Bound
-  for items2: List<&2, Outline.Item>
-  for +ok: {D1.inert.ok(tree) == True{} : Bool}
-  for +ok2: {D1.inert.ok(tree2) == True{} : Bool}
-  for e: {D1.inert.node(tree) == D1.inert.node(tree2) : Tree.Node}
-  {Table.check(Src.Src{path, text, toks, tree, bound, items})
-    == Table.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>}
-
 # LAW: index reads what no string says: two sources as the lexer makes them
 # whose trees read the same with strings cut have the same findings
 law inert_index:
@@ -281,26 +255,6 @@ law inert_concat:
   {Concat.check(Src.Src{path, text, toks, tree, bound, items})
     == Concat.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>}
 
-# LAW: unit reads what no string says: two sources as the lexer makes them
-# whose trees read the same with strings cut have the same findings
-law inert_unit:
-  for +path: String
-  for text: String
-  for +tree: Tree.Node
-  for toks: List<&2, Lex.Tok>
-  for bound: Bind.Bound
-  for items: List<&2, Outline.Item>
-  for text2: String
-  for +tree2: Tree.Node
-  for toks2: List<&2, Lex.Tok>
-  for bound2: Bind.Bound
-  for items2: List<&2, Outline.Item>
-  for +ok: {D1.inert.ok(tree) == True{} : Bool}
-  for +ok2: {D1.inert.ok(tree2) == True{} : Bool}
-  for e: {D1.inert.node(tree) == D1.inert.node(tree2) : Tree.Node}
-  {UnitRule.check(Src.Src{path, text, toks, tree, bound, items})
-    == UnitRule.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>}
-
 # LAW: thunk reads what no string says: two sources as the lexer makes them
 # whose trees read the same with strings cut have the same findings
 law inert_thunk:
@@ -361,26 +315,6 @@ law inert_fuel:
   {FuelRule.check(Src.Src{path, text, toks, tree, bound, items})
     == FuelRule.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>}
 
-# LAW: ring reads what no string says: two sources as the lexer makes them
-# whose trees read the same with strings cut have the same findings
-law inert_ring:
-  for +path: String
-  for text: String
-  for +tree: Tree.Node
-  for toks: List<&2, Lex.Tok>
-  for bound: Bind.Bound
-  for items: List<&2, Outline.Item>
-  for text2: String
-  for +tree2: Tree.Node
-  for toks2: List<&2, Lex.Tok>
-  for bound2: Bind.Bound
-  for items2: List<&2, Outline.Item>
-  for +ok: {D1.inert.ok(tree) == True{} : Bool}
-  for +ok2: {D1.inert.ok(tree2) == True{} : Bool}
-  for e: {D1.inert.node(tree) == D1.inert.node(tree2) : Tree.Node}
-  {Ring.check(Src.Src{path, text, toks, tree, bound, items})
-    == Ring.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>}
-
 # LAW: arms reads what no string says: two sources as the lexer makes them
 # whose trees read the same with strings cut have the same findings
 law inert_arms:
@@ -440,48 +374,6 @@ law inert_unused:
     == Unused.check(Src.Src{path, text2, toks2, tree2, Bind.Bound{binds2, uses, scopes2}, items2})
     : List<&2, F.Finding>}
 
-# LAW: hoist reads what no string says: two sources as the lexer makes them
-# whose trees read the same with strings cut have the same findings (a
-# string's text is only ever compared with a name, a keyword or a mark)
-law inert_hoist:
-  for +path: String
-  for text: String
-  for +tree: Tree.Node
-  for toks: List<&2, Lex.Tok>
-  for bound: Bind.Bound
-  for items: List<&2, Outline.Item>
-  for text2: String
-  for +tree2: Tree.Node
-  for toks2: List<&2, Lex.Tok>
-  for bound2: Bind.Bound
-  for items2: List<&2, Outline.Item>
-  for +ok: {D1.inert.ok(tree) == True{} : Bool}
-  for +ok2: {D1.inert.ok(tree2) == True{} : Bool}
-  for e: {D1.inert.node(tree) == D1.inert.node(tree2) : Tree.Node}
-  {Hoist.check(Src.Src{path, text, toks, tree, bound, items})
-    == Hoist.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>}
-
-# LAW: scan reads what no comment or string says: two sources as the lexer
-# makes them whose trees read the same with comments and strings cut have
-# the same findings
-law inert_scan:
-  for +path: String
-  for text: String
-  for +tree: Tree.Node
-  for toks: List<&2, Lex.Tok>
-  for bound: Bind.Bound
-  for items: List<&2, Outline.Item>
-  for text2: String
-  for +tree2: Tree.Node
-  for toks2: List<&2, Lex.Tok>
-  for bound2: Bind.Bound
-  for items2: List<&2, Outline.Item>
-  for +ok: {D1.inert.ok(tree) == True{} : Bool}
-  for +ok2: {D1.inert.ok(tree2) == True{} : Bool}
-  for e: {D1.inert.node(tree) == D1.inert.node(tree2) : Tree.Node}
-  {Scan.check(Src.Src{path, text, toks, tree, bound, items})
-    == Scan.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>}
-
 # the tokens of each item's header, with comments and strings cut
 def inert.sigs(its: List<&2, Outline.Item>) -> List<&2, List<&2, Lex.Tok>>:
   match its: