refactor: one file per guarantee under laws/ and proofs/

LAWS.bend

@@ -0,0 +1,136 @@
+# shake's laws. Each guarantee is one file under laws/, its prose on top and
+# its quantified laws under it, proved by the file of the same name under
+# proofs/; LAWS.bend and PROOF.bend only import them. The gate: the first line
+# `bend PROOF.bend` prints is exactly `ALL PROOFS CHECK`. Tests and fixtures
+# are never evidence for a guarantee; what shake cannot prove is said where it
+# is assumed, on the code.
+#
+# Every guarantee is about the interface in main.bend: its types, builders,
+# `parse`, `parse_env`, `check`, `check_reads`, the readers, `help`,
+# `err_text`, `help_path`, `err_path`, `version_of`, `suggestion`, `argv` and
+# `env_vars`. Every module under src/ is internal and carries no promise.
+#
+# A spec is well-formed when `check` reports nothing for it
+# (laws/CheckReportsSpecErrors.bend). The parse guarantees hold for
+# well-formed specs; a spec that contradicts itself, such as two options
+# spelled `-n`, is its author's bug and not an input a user can give. Every
+# error a guarantee names but `NeedHelp` and `NeedVersion` also carries `at`,
+# the command path selected where the parse failed
+# (laws/ErrTextShowsUsage.bend); the guarantees write it only where it
+# matters. A plain word is `-`, or a word that does not start with `-`. The
+# current command is the command whose arguments `parse` matches words
+# against: the root, then each subcommand it selects. The selected path is the
+# names of the subcommands selected, in order. A successful parse answers the
+# root command's Matched, as clap answers `ArgMatches`: the bindings that
+# command made while it was current and, when a subcommand was selected under
+# it, that subcommand's name and its own Matched, and so on down the selected
+# path.
+#
+# The words `parse` receives are what the program passes it. In a compiled
+# program they come from `argv`, which drops the program name `IO.args` starts
+# with, after the runtime has taken its own words: those between `+RTS` and
+# `-RTS`, and a `--RTS` (trusted in src/args.bend). A `--` the user types
+# reaches `parse`.
+#
+# An argument's env var is the name `env` gives it; an argument built without
+# `env` has none. `parse_env` also receives vars, a list of name and value
+# pairs, which in a compiled program come from `env_vars` (trusted in
+# src/args.bend). An argument's env value is the value of the first pair in
+# vars named by its env var, when that value is not empty; an env var no pair
+# names, or whose first pair's value is empty, gives no env value.
+#
+# The reasoning behind each guarantee is in docs/rfc/shake-spec.md and
+# docs/rfc/shake-env-and-suggestions.md. Those name the guarantees by the
+# requirement IDs of docs/SPEC.md, the table these files replaced.
+import Base
+import ./laws/AllowedAny.bend as AllowedAny
+import ./laws/ArgLineMark.bend as ArgLineMark
+import ./laws/ArgvDropsProgram.bend as ArgvDropsProgram
+import ./laws/BindValuesAppend.bend as BindValuesAppend
+import ./laws/BindingsComeFromWords.bend as BindingsComeFromWords
+import ./laws/BuiltinsListed.bend as BuiltinsListed
+import ./laws/CheckReadsReportsBadReads.bend as CheckReadsReportsBadReads
+import ./laws/CheckReportsSpecErrors.bend as CheckReportsSpecErrors
+import ./laws/ChoiceRefused.bend as ChoiceRefused
+import ./laws/ClusterDead.bend as ClusterDead
+import ./laws/ClusterDone.bend as ClusterDone
+import ./laws/DeadWalk.bend as DeadWalk
+import ./laws/DefaultsFillUnbound.bend as DefaultsFillUnbound
+import ./laws/DoubleDashEndsOptions.bend as DoubleDashEndsOptions
+import ./laws/DropZero.bend as DropZero
+import ./laws/EnterMissing.bend as EnterMissing
+import ./laws/EnterStep.bend as EnterStep
+import ./laws/EnvFallsBetweenWordsAndDefault.bend as EnvFallsBetweenWordsAndDefault
+import ./laws/EnvValueOutsideChoicesFails.bend as EnvValueOutsideChoicesFails
+import ./laws/EnvVarsAskedInOrder.bend as EnvVarsAskedInOrder
+import ./laws/ErrTextEmptyForRequests.bend as ErrTextEmptyForRequests
+import ./laws/ErrTextNamesArgumentForm.bend as ErrTextNamesArgumentForm
+import ./laws/ErrTextShowsSuggestion.bend as ErrTextShowsSuggestion
+import ./laws/ErrTextShowsUsage.bend as ErrTextShowsUsage
+import ./laws/FailFrom.bend as FailFrom
+import ./laws/FailureIsFinal.bend as FailureIsFinal
+import ./laws/FlagLongValued.bend as FlagLongValued
+import ./laws/GetNil.bend as GetNil
+import ./laws/GetReadsOwnBindings.bend as GetReadsOwnBindings
+import ./laws/HelpFollowsPath.bend as HelpFollowsPath
+import ./laws/HelpListsEveryArgument.bend as HelpListsEveryArgument
+import ./laws/HelpPage.bend as HelpPage
+import ./laws/HelpShowsEnvVar.bend as HelpShowsEnvVar
+import ./laws/HelpUnknown.bend as HelpUnknown
+import ./laws/HelpWalk.bend as HelpWalk
+import ./laws/HelpWordAsksForHelp.bend as HelpWordAsksForHelp
+import ./laws/HitAppend.bend as HitAppend
+import ./laws/Kept.bend as Kept
+import ./laws/KeptAll.bend as KeptAll
+import ./laws/KeptSet.bend as KeptSet
+import ./laws/KeptUnset.bend as KeptUnset
+import ./laws/LastSnoc.bend as LastSnoc
+import ./laws/LetterFlagAgain.bend as LetterFlagAgain
+import ./laws/LetterFlagEq.bend as LetterFlagEq
+import ./laws/LetterOptAgain.bend as LetterOptAgain
+import ./laws/LetterUnknown.bend as LetterUnknown
+import ./laws/LetterValue.bend as LetterValue
+import ./laws/LetterValueBad.bend as LetterValueBad
+import ./laws/LetterValueEq.bend as LetterValueEq
+import ./laws/LongArgStep.bend as LongArgStep
+import ./laws/LongBinds.bend as LongBinds
+import ./laws/LongNoName.bend as LongNoName
+import ./laws/LongOptionSplitsAtEquals.bend as LongOptionSplitsAtEquals
+import ./laws/LongRefused.bend as LongRefused
+import ./laws/LooksFlagLong.bend as LooksFlagLong
+import ./laws/NoPosLeft.bend as NoPosLeft
+import ./laws/OnNil.bend as OnNil
+import ./laws/OnceDead.bend as OnceDead
+import ./laws/PlainWordIsNeverOption.bend as PlainWordIsNeverOption
+import ./laws/PosBinds.bend as PosBinds
+import ./laws/PosNext.bend as PosNext
+import ./laws/PositionalsBindInOrder.bend as PositionalsBindInOrder
+import ./laws/PrefixEmpty.bend as PrefixEmpty
+import ./laws/RawBinds.bend as RawBinds
+import ./laws/RawNext.bend as RawNext
+import ./laws/RawNoPos.bend as RawNoPos
+import ./laws/RawRefused.bend as RawRefused
+import ./laws/Refused.bend as Refused
+import ./laws/RepeatedLongFlag.bend as RepeatedLongFlag
+import ./laws/RepeatedLongOpt.bend as RepeatedLongOpt
+import ./laws/RequiredMissing.bend as RequiredMissing
+import ./laws/RequiredMustBind.bend as RequiredMustBind
+import ./laws/RestTakesRemainingWords.bend as RestTakesRemainingWords
+import ./laws/ShortClusterReadsLetters.bend as ShortClusterReadsLetters
+import ./laws/SpecErrWhere.bend as SpecErrWhere
+import ./laws/StepDies.bend as StepDies
+import ./laws/SubcommandResultsNavigate.bend as SubcommandResultsNavigate
+import ./laws/SubcommandSelects.bend as SubcommandSelects
+import ./laws/SuggestionPicksClosestLong.bend as SuggestionPicksClosestLong
+import ./laws/UnknownLong.bend as UnknownLong
+import ./laws/UnknownLongDies.bend as UnknownLongDies
+import ./laws/UnknownLongStep.bend as UnknownLongStep
+import ./laws/UnknownShort.bend as UnknownShort
+import ./laws/UnknownShortStep.bend as UnknownShortStep
+import ./laws/ValueAbsent.bend as ValueAbsent
+import ./laws/ValueBinds.bend as ValueBinds
+import ./laws/ValueFlagShaped.bend as ValueFlagShaped
+import ./laws/ValueRefused.bend as ValueRefused
+import ./laws/VersionOfNamesRelease.bend as VersionOfNamesRelease
+import ./laws/VersionWordAsksForVersion.bend as VersionWordAsksForVersion
+import ./laws/WalkAppend.bend as WalkAppend

PROOF.bend

@@ -0,0 +1,95 @@
+# shake's proofs: each file under proofs/ fills the laws of the file of the
+# same name under laws/.
+import Base
+import ./LAWS.bend as Laws
+import ./proofs/AllowedAny.bend as PAllowedAny
+import ./proofs/ArgLineMark.bend as PArgLineMark
+import ./proofs/ArgvDropsProgram.bend as PArgvDropsProgram
+import ./proofs/BindValuesAppend.bend as PBindValuesAppend
+import ./proofs/BindingsComeFromWords.bend as PBindingsComeFromWords
+import ./proofs/BuiltinsListed.bend as PBuiltinsListed
+import ./proofs/CheckReadsReportsBadReads.bend as PCheckReadsReportsBadReads
+import ./proofs/CheckReportsSpecErrors.bend as PCheckReportsSpecErrors
+import ./proofs/ChoiceRefused.bend as PChoiceRefused
+import ./proofs/ClusterDead.bend as PClusterDead
+import ./proofs/ClusterDone.bend as PClusterDone
+import ./proofs/DeadWalk.bend as PDeadWalk
+import ./proofs/DefaultsFillUnbound.bend as PDefaultsFillUnbound
+import ./proofs/DoubleDashEndsOptions.bend as PDoubleDashEndsOptions
+import ./proofs/DropZero.bend as PDropZero
+import ./proofs/EnterMissing.bend as PEnterMissing
+import ./proofs/EnterStep.bend as PEnterStep
+import ./proofs/EnvFallsBetweenWordsAndDefault.bend as PEnvFallsBetweenWordsAndDefault
+import ./proofs/EnvValueOutsideChoicesFails.bend as PEnvValueOutsideChoicesFails
+import ./proofs/EnvVarsAskedInOrder.bend as PEnvVarsAskedInOrder
+import ./proofs/ErrTextEmptyForRequests.bend as PErrTextEmptyForRequests
+import ./proofs/ErrTextNamesArgumentForm.bend as PErrTextNamesArgumentForm
+import ./proofs/ErrTextShowsSuggestion.bend as PErrTextShowsSuggestion
+import ./proofs/ErrTextShowsUsage.bend as PErrTextShowsUsage
+import ./proofs/FailFrom.bend as PFailFrom
+import ./proofs/FailureIsFinal.bend as PFailureIsFinal
+import ./proofs/FlagLongValued.bend as PFlagLongValued
+import ./proofs/GetNil.bend as PGetNil
+import ./proofs/GetReadsOwnBindings.bend as PGetReadsOwnBindings
+import ./proofs/HelpFollowsPath.bend as PHelpFollowsPath
+import ./proofs/HelpListsEveryArgument.bend as PHelpListsEveryArgument
+import ./proofs/HelpPage.bend as PHelpPage
+import ./proofs/HelpShowsEnvVar.bend as PHelpShowsEnvVar
+import ./proofs/HelpUnknown.bend as PHelpUnknown
+import ./proofs/HelpWalk.bend as PHelpWalk
+import ./proofs/HelpWordAsksForHelp.bend as PHelpWordAsksForHelp
+import ./proofs/HitAppend.bend as PHitAppend
+import ./proofs/Kept.bend as PKept
+import ./proofs/KeptAll.bend as PKeptAll
+import ./proofs/KeptSet.bend as PKeptSet
+import ./proofs/KeptUnset.bend as PKeptUnset
+import ./proofs/LastSnoc.bend as PLastSnoc
+import ./proofs/LetterFlagAgain.bend as PLetterFlagAgain
+import ./proofs/LetterFlagEq.bend as PLetterFlagEq
+import ./proofs/LetterOptAgain.bend as PLetterOptAgain
+import ./proofs/LetterUnknown.bend as PLetterUnknown
+import ./proofs/LetterValue.bend as PLetterValue
+import ./proofs/LetterValueBad.bend as PLetterValueBad
+import ./proofs/LetterValueEq.bend as PLetterValueEq
+import ./proofs/LongArgStep.bend as PLongArgStep
+import ./proofs/LongBinds.bend as PLongBinds
+import ./proofs/LongNoName.bend as PLongNoName
+import ./proofs/LongOptionSplitsAtEquals.bend as PLongOptionSplitsAtEquals
+import ./proofs/LongRefused.bend as PLongRefused
+import ./proofs/LooksFlagLong.bend as PLooksFlagLong
+import ./proofs/NoPosLeft.bend as PNoPosLeft
+import ./proofs/OnNil.bend as POnNil
+import ./proofs/OnceDead.bend as POnceDead
+import ./proofs/PlainWordIsNeverOption.bend as PPlainWordIsNeverOption
+import ./proofs/PosBinds.bend as PPosBinds
+import ./proofs/PosNext.bend as PPosNext
+import ./proofs/PositionalsBindInOrder.bend as PPositionalsBindInOrder
+import ./proofs/PrefixEmpty.bend as PPrefixEmpty
+import ./proofs/RawBinds.bend as PRawBinds
+import ./proofs/RawNext.bend as PRawNext
+import ./proofs/RawNoPos.bend as PRawNoPos
+import ./proofs/RawRefused.bend as PRawRefused
+import ./proofs/Refused.bend as PRefused
+import ./proofs/RepeatedLongFlag.bend as PRepeatedLongFlag
+import ./proofs/RepeatedLongOpt.bend as PRepeatedLongOpt
+import ./proofs/RequiredMissing.bend as PRequiredMissing
+import ./proofs/RequiredMustBind.bend as PRequiredMustBind
+import ./proofs/RestTakesRemainingWords.bend as PRestTakesRemainingWords
+import ./proofs/ShortClusterReadsLetters.bend as PShortClusterReadsLetters
+import ./proofs/SpecErrWhere.bend as PSpecErrWhere
+import ./proofs/StepDies.bend as PStepDies
+import ./proofs/SubcommandResultsNavigate.bend as PSubcommandResultsNavigate
+import ./proofs/SubcommandSelects.bend as PSubcommandSelects
+import ./proofs/SuggestionPicksClosestLong.bend as PSuggestionPicksClosestLong
+import ./proofs/UnknownLong.bend as PUnknownLong
+import ./proofs/UnknownLongDies.bend as PUnknownLongDies
+import ./proofs/UnknownLongStep.bend as PUnknownLongStep
+import ./proofs/UnknownShort.bend as PUnknownShort
+import ./proofs/UnknownShortStep.bend as PUnknownShortStep
+import ./proofs/ValueAbsent.bend as PValueAbsent
+import ./proofs/ValueBinds.bend as PValueBinds
+import ./proofs/ValueFlagShaped.bend as PValueFlagShaped
+import ./proofs/ValueRefused.bend as PValueRefused
+import ./proofs/VersionOfNamesRelease.bend as PVersionOfNamesRelease
+import ./proofs/VersionWordAsksForVersion.bend as PVersionWordAsksForVersion
+import ./proofs/WalkAppend.bend as PWalkAppend

README.md

@@ -73,7 +73,9 @@ does it for you. shake needs bend 2.0.32 or later for that reason.
 `suggestion`, `argv` and `env_vars`.
 Everything under `src/` is
 internal and may change in any release; import only `main.bend`.
-[SPEC.md](SPEC.md) lists what shake guarantees, and which of it is proved.
+[LAWS.bend](LAWS.bend) lists what shake guarantees: one file under
+[laws/](laws/) each, proved by the file of the same name under
+[proofs/](proofs/).
 
 `check(spec)` lists every way a spec contradicts itself (a rest positional
 that is not the last, a repeated name or spelling, a subcommand named
@@ -174,8 +176,9 @@ bin/demo.bin add 2 3 --times 2
 ## Layout
 
 - `main.bend`: the interface.
-- `src/`: the implementation, with `src/LAWS.bend` stating the parser's laws
-  and `src/PROOF.bend` proving them. `nix flake check` runs the proof gate.
+- `src/`: the implementation.
+- `laws/` and `proofs/`: one file per guarantee and its proof, imported by
+  `LAWS.bend` and `PROOF.bend`. `nix flake check` runs the proof gate.
 - `examples/demo/`: a small program that uses only `main.bend`.
 - `ez.toml` and `ez.lock.toml`: the ledger and lock; bolt, the linter, is
   pinned there as `[tools.bolt]`, and `nix flake check` runs it.

bolt.bend

@@ -28,7 +28,3 @@ def closed() -> String:
 # an @unsafe def a law file reaches
 def unsafe() -> String:
   "error"
-
-# SPEC.md's rows and the laws' tags agree
-def trace() -> String:
-  "error"

SPEC.md → docs/SPEC.md

@@ -10,7 +10,7 @@ The words `parse` receives are what the program passes it. In a compiled program
 
 An argument's **env var** is the name `env` gives it; an argument built without `env` has none. `parse_env` also receives **vars**, a list of name and value pairs, which in a compiled program come from `env_vars` (SHAKE-TRUST-5). An argument's **env value** is the value of the first pair in vars named by its env var, when that value is not empty; an env var no pair names, or whose first pair's value is empty, gives no env value.
 
-The reasoning behind each requirement, the verdict of each against the code at `b93357a`, and the decisions that shaped them are in [docs/rfc/shake-spec.md](docs/rfc/shake-spec.md). The RFC also records the audit behind them and the rollout that proved every row. The env and suggestion rows (SHAKE-PARSE-11, PARSE-12, HELP-3, ERR-3, ERR-4, ARGS-2, TRUST-5) are designed in [docs/rfc/shake-env-and-suggestions.md](docs/rfc/shake-env-and-suggestions.md).
+The reasoning behind each requirement, the verdict of each against the code at `b93357a`, and the decisions that shaped them are in [docs/rfc/shake-spec.md](rfc/shake-spec.md). The RFC also records the audit behind them and the rollout that proved every row. The env and suggestion rows (SHAKE-PARSE-11, PARSE-12, HELP-3, ERR-3, ERR-4, ARGS-2, TRUST-5) are designed in [docs/rfc/shake-env-and-suggestions.md](rfc/shake-env-and-suggestions.md).
 
 ## Format
 
@@ -111,7 +111,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n
 
 ## Left to prove
 
-No row is pending. The RFCs' Rollouts and [docs/rfc/shake-walker-proofs.md](docs/rfc/shake-walker-proofs.md) say in which phase each row's laws landed. Every walker law holds wherever the words before the word it is about leave the walker in the state its premise names.
+No row is pending. The RFCs' Rollouts and [docs/rfc/shake-walker-proofs.md](rfc/shake-walker-proofs.md) say in which phase each row's laws landed. Every walker law holds wherever the words before the word it is about leave the walker in the state its premise names.
 
 ## Trust boundary
 

examples/demo/main.bend

@@ -3,7 +3,7 @@ import Base
 import ../../main.bend as Shake
 
 # the program spec
-def spec() -> Shake.Cli:  # noqa: L001 the example program, not the library
+def spec() -> Shake.Cli:
   Shake.app("demo", "A tiny command-line program.", Some{"0.1.0"},
     [Shake.flag("verbose", Some{"v"}, Some{"verbose"}, "More output")],
     [
@@ -44,12 +44,12 @@ def greet.tags(tags: List<&2, String>) -> IO(Unit):
       IO.print("tags: " ++ String.join(hh <> tt, " "))
 
 # the value bound to `name`, or "" when nothing bound it
-def text(+mm: Shake.Matched, +name: String) -> String:  # noqa: L001 the example program, not the library
+def text(+mm: Shake.Matched, +name: String) -> String:
   Maybe.default(&2, String, Shake.get(mm, name), "")
 
 # a successful greet: `who` when given, else `--name`, which has a default;
 # verbose when the root's `-v` or greet's own is set
-def greet(+root: Shake.Matched, +mm: Shake.Matched) -> IO(Unit):  # noqa: L001 IO
+def greet(+root: Shake.Matched, +mm: Shake.Matched) -> IO(Unit):
   do IO<Unit>:
     +who : String <- IO.pure(String,
       Maybe.default(&2, String, Shake.get(mm, "who"), text(mm, "name")))
@@ -58,7 +58,7 @@ def greet(+root: Shake.Matched, +mm: Shake.Matched) -> IO(Unit):  # noqa: L001 I
     greet.v(Bool.or(Shake.on(root, "verbose"), Shake.on(mm, "verbose")))
 
 # a successful add
-def add(+mm: Shake.Matched) -> IO(Unit):  # noqa: L001 IO
+def add(+mm: Shake.Matched) -> IO(Unit):
   IO.print(text(mm, "a") ++ " + " ++ text(mm, "b") ++ " x" ++ text(mm, "times") ++ " base " ++
     text(mm, "base"))
 
@@ -92,7 +92,7 @@ def run.sub(+root: Shake.Matched, sel: Maybe<&2, String>) -> IO(Unit):
         run.add(Shake.sub_of(root, "add")))
 
 # the root's Matched: dispatch on its subcommand
-def run(+mm: Shake.Matched) -> IO(Unit):  # noqa: L001 IO
+def run(+mm: Shake.Matched) -> IO(Unit):
   run.sub(mm, Shake.sub_name(mm))
 
 # a hard error
@@ -118,11 +118,11 @@ def fail.at(+app: Shake.Cli, ask: Maybe<&2, List<&2, String>>, +ee: Shake.ParseE
       fail.ver(app, Shake.version_of(app, ee), ee)
 
 # a failed parse: help text, the version, or an error
-def fail(+app: Shake.Cli, +ee: Shake.ParseErr) -> IO(Unit):  # noqa: L001 IO
+def fail(+app: Shake.Cli, +ee: Shake.ParseErr) -> IO(Unit):
   fail.at(app, Shake.help_path(ee), ee)
 
 # the parse result
-def go(  # noqa: L001 IO
+def go(
   +app: Shake.Cli,
   rr: Result<&2, &2, Shake.ParseErr, Shake.Matched>
 ) -> IO(Unit):
@@ -132,7 +132,7 @@ def go(  # noqa: L001 IO
     case Done{m}:
       run(m)
 
-def main() -> IO(Unit):  # noqa: L001 IO
+def main() -> IO(Unit):
   do IO<Unit>:
     +app : Shake.Cli <- IO.pure(Shake.Cli, spec())
     av : List<&2, String> <- Shake.argv()

ez.lock.toml

@@ -4,8 +4,8 @@ hub = "https://hub.bend-lang.com"
 [tools]
 [tools.bolt]
 git = "https://github.com/Emerging-Patterns/bolt"
-rev = "7f5bb328187efa21598b4fed51cb1e154cf36330"
-tag = "v1.19.0"
+rev = "78fad9564b1a5b49f1e39bbd46a7fec45e615a4c"
+tag = "v1.22.0"
 root = "."
-narHash = "sha256-9d+ikveuzegJVH8nbEYSAxy8Pt0dYDyW4ISZml+MsNM="
+narHash = "sha256-OHkE75Urs5jTTU8Nygs2+enKYKOXeHOBDZ5t0ZwJVA4="
 entry = "main.bend"

ez.toml

@@ -4,8 +4,8 @@ entry = "main.bend"
 [tools]
 [tools.bolt]
 git = "https://github.com/Emerging-Patterns/bolt"
-rev = "7f5bb328187efa21598b4fed51cb1e154cf36330"
-tag = "v1.19.0"
+rev = "78fad9564b1a5b49f1e39bbd46a7fec45e615a4c"
+tag = "v1.22.0"
 root = "."
-narHash = "sha256-9d+ikveuzegJVH8nbEYSAxy8Pt0dYDyW4ISZml+MsNM="
+narHash = "sha256-OHkE75Urs5jTTU8Nygs2+enKYKOXeHOBDZ5t0ZwJVA4="
 entry = "main.bend"

laws/AllowedAny.bend

@@ -0,0 +1,7 @@
+import Base
+import ../src/cli.bend as S
+
+# LAW: empty choices accept every value
+law allowed_any:
+  for vv: String
+  {S.allowed([], vv) == True{} : Bool}