This is the list of every behavior ez guarantees, each under a stable requirement ID. Every requirement has one of two levels. A Proved requirement holds for every input, and is backed by a quantified law in a LAWS.bend that passes the proof gate. A Trusted requirement is an assumption about something ez cannot check from inside its own gate, and it is listed in the trust boundary below. A Proved requirement whose law has not landed yet has status pending: we intend to prove it, and until then it is not guaranteed. The proof gate is this check: for every PROOF.bend in the tree, the first line bend PROOF.bend prints is exactly ALL PROOFS CHECK. bend 2.0.32 and later print that verdict only when every def the file loads, its imports included, checks and reaches no @unsafe def and no foreign code, so a law never imports a module that runs a program or opens a socket. ez prove runs the gate, and it is the check CI runs.
The reasoning behind each requirement, and the decisions that shaped them, are in docs/rfc/ez-spec.md.
A quantified law that proves a requirement carries the requirement's ID in a comment directly above its law line:
# EZ-HASH-1
law hash_perm:
A law with no binder claims one computed case and no requirement, so ez has none. bolt's closed rule (L002), on at error in bolt.bend, rejects any law in a LAWS.bend without a for or exs binder, equality or not, and nothing exempts one.
A pending requirement may already have tagged quantified laws that prove part of it. The Law column names them, and "Left to prove" below says what is missing before the status becomes proved.
The Law column lists <path> <law> entries, the path relative to this file, joined by ; . bolt's trace rule (L005), on at error in bolt.bend, reads this file and checks it against the tags. Every law a Proved row names, proved or pending, must exist, have a binder and carry the row's ID; a proved row must name at least one; a Trusted row names none and has a row in the trust boundary; and no law may carry an ID that is not a Proved row here.
Untagged quantified laws are allowed. They pass the proof gate like any law, but nothing here protects them, so a change may edit or delete them freely.
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| EZ-HASH-1 | The 0x hash of a file list with distinct paths depends only on its (path, sum) pairs, not on the order they were found in. | Proved | proved | src/pkg/LAWS.bend hash_perm |
| EZ-HASH-2 | The NAR serialization of a directory does not depend on the order its entries are listed in. | Proved | proved | src/sha/LAWS.bend nar_dir_order_free |
| EZ-HASH-3 | When ez writes a package under <lib>/<h>, h is the 0x hash of the file list whose manifest it writes beside the files. |
Proved | proved | src/pkg/LAWS.bend walked_named_by_texts; src/pkg/LAWS.bend walked_manifest_of_texts; src/add/LAWS.bend add_lays_named; src/fetch/LAWS.bend fetch_lays_named; src/lock/LAWS.bend lock_lays_named; src/add/LAWS.bend add_named_lays_named |
| EZ-HASH-4 | ez's 0x hash for an entry equals the hash bend --publish assigns to it. |
Trusted | ||
| EZ-HASH-5 | ez's narHash equals nix hash path --type sha256 --sri of the same tree. |
Trusted | ||
| EZ-HASH-6 | Sha.hex(s) is the SHA-256 of the UTF-8 bytes of s. For a file's text that is SHA-256 of the file's bytes, which is what bend --publish and the hub compute. |
Trusted | ||
| EZ-HASH-7 | The NAR walk reads every name and symlink target as the tree listing prints it: nothing is trimmed, and a newline stays inside the name that holds it. | Proved | proved | src/sha/LAWS.bend nar_field_verbatim; src/sha/LAWS.bend nar_listing_verbatim |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| EZ-LED-1 | A ledger that does not parse is never read into a model, and renders as nothing, so no command writes a guess over it. | Proved | proved | src/ledger/LAWS.bend read_refuses_a_problem; src/ledger/LAWS.bend render_of_unread_is_blank; src/remove/LAWS.bend remove_refuses_unread; src/add/LAWS.bend add_refuses_unread; src/lock/LAWS.bend lock_refuses_unread |
| EZ-LED-2 | Adding a dependency to a ledger model twice is adding it once. | Proved | proved | src/ledger/LAWS.bend add_keep_idem; src/add/LAWS.bend add_edits_ledger; src/add/LAWS.bend add_named_edits_ledger |
| EZ-LED-3 | Removing a dependency from a ledger model twice is removing it once. | Proved | proved | src/ledger/LAWS.bend remove_idem; src/remove/LAWS.bend remove_edits_ledger |
| EZ-LED-4 | Every ledger ez writes is one Rend.renderable accepts, and so reads back to the model it was rendered from wherever eztoml's round trip holds (EZ-TRUST-8). |
Proved | proved | src/init/LAWS.bend init_ledger_reads_back; src/add/LAWS.bend add_ledger_reads_back; src/remove/LAWS.bend remove_ledger_reads_back; src/add/LAWS.bend add_named_reads_back; src/add/LAWS.bend add_named_refuses_unrenderable |
| EZ-LED-5 | A [tools.*] section is a tool, never a dependency, and needs no hash. |
Proved | proved | src/ledger/LAWS.bend tool_section_not_dep; src/ledger/LAWS.bend tool_section_is_tool; src/ledger/LAWS.bend tool_needs_no_hash; src/lock/LAWS.bend lock_origins_skip_tools; src/lock/LAWS.bend upgrade_origins_skip_tools; src/add/LAWS.bend add_keeps_tools; src/remove/LAWS.bend remove_keeps_tools; src/remove/LAWS.bend remove_refuses_tool; src/doctor/LAWS.bend doctor_ignores_tools |
| EZ-LED-6 | ez init writes nothing when a ledger exists, and ez add, ez remove, ez fetch and ez lock, with or without --upgrade, refuse and write nothing when there is none. |
Proved | proved | src/init/LAWS.bend init_keeps_ledger; src/remove/LAWS.bend remove_needs_ledger; src/add/LAWS.bend add_needs_ledger; src/add/LAWS.bend add_needs_ledger_asks_nothing; src/lock/LAWS.bend lock_needs_ledger; src/fetch/LAWS.bend fetch_needs_ledger; src/fetch/LAWS.bend fetch_needs_ledger_asks_nothing |
| EZ-LED-7 | A dependency's ledger name is --rename when given, which must be a TOML bare key; otherwise the name the ledger already records for that source; otherwise the target's [package] name when it is a TOML bare key; otherwise the repository's name; otherwise the directory's name. A hub package added by its <name>@<version> is named by --rename when given; otherwise by the name the ledger already records for a dependency added by the same name part, so another version replaces it; otherwise by the name part. A name the ledger gives a different source is refused, and so is a --rename of a source the ledger records under another name. |
Proved | proved | src/ez/LAWS.bend rename_wins; src/ez/LAWS.bend rename_dotted; src/ez/LAWS.bend rename_moved; src/ez/LAWS.bend rename_clash; src/ez/LAWS.bend name_keeps; src/ez/LAWS.bend own_package; src/ez/LAWS.bend own_invalid; src/ez/LAWS.bend leaf_is_last; src/ez/LAWS.bend clash_same; src/ez/LAWS.bend clash_other; src/ez/LAWS.bend clash_hub; src/add/LAWS.bend add_records_named; src/add/LAWS.bend add_refuses_named; src/ez/LAWS.bend hub_rename_wins; src/ez/LAWS.bend hub_key_keeps; src/ez/LAWS.bend hub_key_fresh; src/ez/LAWS.bend hub_clash_git; src/add/LAWS.bend add_named_key; src/add/LAWS.bend add_named_refuses_clash |
| EZ-LED-8 | A path target is recorded in the ledger as it was given, with a leading ~/ expanded, and a relative path resolves against the project root wherever git reads it: ez add, ez lock, ez fetch and ez lock --upgrade. |
Proved | proved | src/ez/LAWS.bend anchor_url; src/ez/LAWS.bend anchor_absolute; src/ez/LAWS.bend anchor_relative; src/add/LAWS.bend add_records_as_given; src/add/LAWS.bend add_path_as_given; src/add/LAWS.bend add_asks_anchored; src/fetch/LAWS.bend fetch_asks_anchored; src/fetch/LAWS.bend fetch_keeps_records; src/lock/LAWS.bend lock_asks_anchored; src/lock/LAWS.bend upgrade_asks_its_questions; src/lock/LAWS.bend upgrade_asks_anchored; src/lock/LAWS.bend lock_records_as_given; src/lock/LAWS.bend upgrade_records_as_given; src/lock/LAWS.bend upgrade_records_tools_as_given |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| EZ-INIT-1 | The entry ez init writes opens with the line # <name>: <description>, the description --description gives, or TODO describe <name> when none is given, so that line is what the hub describes the package by. A description holding a newline is refused, and nothing is written. |
Proved | proved | src/init/LAWS.bend init_stub_heads; src/init/LAWS.bend init_header_given; src/init/LAWS.bend init_header_placeholder; src/init/LAWS.bend init_one_line |
| EZ-INIT-2 | With nothing at the entry, the entry at the project's top and nothing at src/lib.bend, ez init writes src/lib.bend and an entry that imports it; an entry in a directory of its own is written alone. It never writes over an entry or a src/lib.bend that is already there. |
Proved | proved | src/init/LAWS.bend init_lays_src; src/init/LAWS.bend init_lays_main; src/init/LAWS.bend init_keeps_src; src/init/LAWS.bend init_keeps_entry |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| EZ-DOC-1 | Parsing a rendered lock yields the packages, hub, names and tools that were rendered. | Trusted | ||
| EZ-DOC-2 | Packages are written in hash order and each package's files in path order, so the lock's text does not depend on the order the walk found them in. | Proved | proved | src/lock/LAWS.bend lock_order_free; src/lock/LAWS.bend pack_order_free; src/lock/LAWS.bend plain_lock_hashes_distinct |
| EZ-DOC-3 | ez lock output is a function of the ledger and the committed tree. A fresh clone reproduces the lock byte for byte. |
Proved | proved | src/lock/LAWS.bend lock_reproducible; src/lock/LAWS.bend clone_reproduces; src/lock/LAWS.bend root_reads_as_bend |
| EZ-DOC-4 | ez lock is idempotent: run on the world it just produced, it writes the same bytes. |
Proved | proved | src/lock/LAWS.bend lock_idempotent; src/lock/LAWS.bend relock_lays_nothing; src/lock/LAWS.bend upgrade_idempotent; src/lock/LAWS.bend reupgrade_moves_nothing; src/lock/LAWS.bend upgrade_settles; src/lock/LAWS.bend reupgrade_lays_nothing; src/lock/LAWS.bend reupgrade_writes_only_lock |
| EZ-DOC-5 | ez lock without --upgrade never writes ez.toml, and records every dependency's and tool's pin exactly as ez.toml has it. |
Proved | proved | src/lock/LAWS.bend plain_lock_keeps_ledger; src/lock/LAWS.bend plain_lock_pins_ledger_sources |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| EZ-RES-1 | ez add with no ref pins the greatest semver-ish release tag on the remote; with no release, the greatest pre-release; with no semver-ish tag, the remote's default branch as its HEAD symref names it. A named ref resolves exactly, as refs/tags/<ref> and then refs/heads/<ref>. A 40-hex ref is used as a commit without asking the remote. |
Proved | proved | src/git/LAWS.bend is_rev_needs_40; src/git/LAWS.bend is_rev_needs_hex; src/git/LAWS.bend is_rev_hex40; src/git/LAWS.bend choose_release; src/git/LAWS.bend choose_prerelease; src/git/LAWS.bend branch_of_symref; src/git/LAWS.bend branch_skips_other; src/git/LAWS.bend branch_skips_commit; src/git/LAWS.bend exact_skips; src/git/LAWS.bend exact_tag_first; src/git/LAWS.bend exact_branch; src/git/LAWS.bend latest_greatest; src/git/LAWS.bend latest_rel_greatest; src/git/LAWS.bend choose_greatest_release; src/git/LAWS.bend choose_greatest_prerelease; src/git/LAWS.bend choose_is_a_tag; src/add/LAWS.bend add_pins_chosen; src/add/LAWS.bend add_pins_chosen_rev; src/add/LAWS.bend add_pins_head_rev; src/add/LAWS.bend add_pins_named; src/add/LAWS.bend add_pins_commit; src/add/LAWS.bend add_commit_asks_nothing |
| EZ-RES-2 | ez add with no entry uses the revision's [package] entry, then [package] bin, then main.bend, and refuses if that file is not in the revision. An add that succeeds prints the import line for that entry's path inside the package, the line ez publish prints. ez add <name>@<version> with no entry uses the package's main.bend, then its first top-level .bend file, and records none when it has neither; it refuses an entry given that the package does not hold, and prints the import line with the name in place of the hash. |
Proved | proved | src/pkg/LAWS.bend absent_entry_refused; src/git/LAWS.bend entry_pick_entry; src/git/LAWS.bend entry_pick_bin; src/git/LAWS.bend entry_pick_main; src/add/LAWS.bend add_entry_default; src/add/LAWS.bend add_entry_absent; src/add/LAWS.bend add_says_import; src/add/LAWS.bend add_named_entry_default; src/add/LAWS.bend add_named_entry_absent; src/add/LAWS.bend add_named_says_import |
| EZ-RES-3 | A target containing :// or starting git@ is a git URL. A target starting /, ./, ../ or ~/ is a path. A target of exactly two segments of letters, digits, -, _ and ., neither of them . or .., is https://github.com/<target>, unless its second segment ends in .bend, which makes it a path. Anything else is a path, except the empty word, which is refused. For ez add, a path bend reads as a hub package's <name>@<version> names that package on the hub; a git URL, owner/repo or other path never does. |
Proved | proved | src/ez/LAWS.bend classify_url; src/ez/LAWS.bend classify_scp; src/ez/LAWS.bend classify_abs; src/ez/LAWS.bend classify_here; src/ez/LAWS.bend classify_up; src/ez/LAWS.bend classify_home; src/ez/LAWS.bend classify_github; src/ez/LAWS.bend classify_else; src/ez/LAWS.bend aim_named; src/ez/LAWS.bend aim_path; src/ez/LAWS.bend aim_remote; src/ez/LAWS.bend aim_bad; src/ez/LAWS.bend aim_scp |
| EZ-RES-4 | ez lock --upgrade never moves a hub dependency. |
Proved | proved | src/lock/LAWS.bend upgrade_holds_hub |
| EZ-RES-5 | An upgraded rev-only dependency moves to the default branch tip only when its pin is an ancestor of that tip, and stays a commit pin. Otherwise the upgrade refuses with exit 1. | Proved | proved | src/lock/LAWS.bend upgrade_forward_moves_onward; src/lock/LAWS.bend upgrade_forward_refuses_off; src/lock/LAWS.bend upgrade_forward_reaches_tip; src/git/LAWS.bend tip_of_head; src/git/LAWS.bend tip_skips_other; src/git/LAWS.bend tip_skips_symref |
| EZ-RES-6 | --package NAME asks the remote to resolve only the named dependency or tool, and every other ledger entry keeps its rev, tag and hash. Resolving is asking for refs, the default branch, ancestry, or a checkout at a new rev. |
Proved | proved | src/lock/LAWS.bend upgrade_one_frames_deps; src/lock/LAWS.bend upgrade_one_frames_tools; src/lock/LAWS.bend upgrade_one_asks_alone |
| EZ-RES-7 | Tags, refs, and ancestry reported by git are accurate. | Trusted | ||
| EZ-RES-8 | An upgraded tagged dependency re-resolves its tag. A tag that now names a commit the pin does not descend to, or a pinned commit whose tree no longer hashes to the pin, stops the upgrade with exit 1. | Proved | proved | src/lock/LAWS.bend upgrade_tag_follows; src/lock/LAWS.bend upgrade_tag_resolves; src/lock/LAWS.bend upgrade_tag_refuses_off; src/lock/LAWS.bend upgrade_tag_refuses_drift |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| EZ-VEN-1 | After ez add, ez remove or ez lock --upgrade, the .gitignore allowlist names exactly the hashes of dependencies marked vendor = true, and every other line of .gitignore is unchanged. |
Proved | proved | src/ledger/LAWS.bend allowlist_is_the_ledger; src/ledger/LAWS.bend allowlist_keeps_other_lines; src/ledger/LAWS.bend sync_allowlist_is_the_ledger; src/ledger/LAWS.bend sync_keeps_other_lines; src/ledger/LAWS.bend sync_idempotent; src/ledger/LAWS.bend vended_once; src/remove/LAWS.bend remove_syncs_allowlist; src/lock/LAWS.bend upgrade_allowlist_is_the_ledger; src/lock/LAWS.bend upgrade_allowlist_keeps_other_lines; src/lock/LAWS.bend upgrade_vends_the_ledger; src/add/LAWS.bend add_syncs_allowlist; src/lock/LAWS.bend upgrade_allowlist_kept_in_sync; src/lock/LAWS.bend upgrade_unmoved_vends_the_ledger |
| EZ-VEN-2 | When an upgrade moves a hash, every line of a .bend file outside .ez and .git that starts import <old>/ names <new> afterwards. |
Proved | proved | src/ledger/LAWS.bend rewrite_names_new; src/lock/LAWS.bend upgrade_rewrites_imports |
| EZ-VEN-3 | Import rewriting leaves every other line of every file byte-identical, and does not write a file with no matching line. | Proved | proved | src/ledger/LAWS.bend rewrite_keeps_other_lines; src/ledger/LAWS.bend rewrite_keeps_line_count; src/ledger/LAWS.bend rewrite_nothing_named; src/lock/LAWS.bend upgrade_leaves_other_lines; src/lock/LAWS.bend upgrade_keeps_line_count; src/lock/LAWS.bend upgrade_writes_only_hits |
| EZ-VEN-4 | ez doctor never writes to the project's source files. |
Proved | proved | src/doctor/LAWS.bend doctor_writes_nothing |
| EZ-VEN-5 | ez doctor reports every hash an import line names that the ledger does not, and every ledger dependency no import line names, and exits 1 when it reports any. |
Proved | proved | src/doctor/LAWS.bend doctor_reports_unrecorded; src/doctor/LAWS.bend doctor_reports_unused; src/doctor/LAWS.bend doctor_drift_fails |
| EZ-VEN-6 | ez doctor reports a lock that ez lock would not write as it stands, judged without the network from the ledger, the committed sources and the trees under BEND_LIB, and exits 1 when it reports one or cannot judge it. |
Proved | proved | src/doctor/LAWS.bend doctor_passes_fresh_lock; src/doctor/LAWS.bend doctor_says_fresh_lock; src/doctor/LAWS.bend doctor_reports_stale_lock; src/doctor/LAWS.bend doctor_stale_lock_fails; src/doctor/LAWS.bend doctor_unchecked_lock_fails; src/doctor/LAWS.bend doctor_unchecked_names_fail |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| EZ-FETCH-1 | ez fetch writes a package file under BEND_LIB only when its digest matches the lock: a hub body's digest starts with the lock's sum, a git file's digest equals it, and a git package's checkout weighs to the narHash the lock records. |
Proved | proved | src/fetch/LAWS.bend fetch_lays_the_lock; src/fetch/LAWS.bend fetch_lays_weighed; src/fetch/LAWS.bend fetch_weighs_the_checkout; src/fetch/LAWS.bend fetch_refuses_unweighed |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| EZ-HUB-1 | A named import <name>@<version>/... resolves to one hash: the one ez.toml records for that name, else the one the lock being rewritten records, else the one the hub answers. The lock walks that package, records the pair under [names], and ez fetch lays that hash in the name's file. ez add <name>@<version> asks the hub the ledger names, and records the name with the hash the hub answers. |
Proved | proved | src/lock/LAWS.bend named_kid_queued; src/lock/LAWS.bend lock_names_agree; src/lock/LAWS.bend ledger_names_first; src/fetch/LAWS.bend fetch_names_the_lock; src/add/LAWS.bend add_named_records_name; src/add/LAWS.bend add_named_asks_hub |
| EZ-HUB-2 | ez lock asks the hub what a name names only when neither ez.toml nor the lock being rewritten records it. |
Proved | proved | src/lock/LAWS.bend lock_answer_names; src/lock/LAWS.bend resolved_not_asked |
| EZ-HUB-3 | An import whose first path segment holds @ is a hub dependency and never a file of the project. A name bend would refuse is refused, in bend's words, before any package is hashed around it. |
Proved | proved | src/pkg/LAWS.bend named_is_no_module; src/pkg/LAWS.bend unnamed_stops; src/pkg/LAWS.bend unnamed_refused; src/lock/LAWS.bend lock_reads_named |
| EZ-HUB-4 | ez lock and ez fetch lay BEND_LIB/names/<name>@<version> holding the hash the lock records, for every name it records, and ez add <name>@<version> lays the file of the name it adds. ez fetch rewrites a file that names another hash, and says so. ez doctor fails when a file is missing or names another hash. |
Proved | proved | src/lock/LAWS.bend lock_lays_its_names; src/fetch/LAWS.bend fetch_lays_missing_name; src/fetch/LAWS.bend fetch_rewrites_name; src/fetch/LAWS.bend fetch_refuses_unread_name; src/fetch/LAWS.bend fetch_lays_the_names; src/doctor/LAWS.bend doctor_wrong_name_fails; src/add/LAWS.bend add_named_lays_name |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| EZ-TOOL-1 | The link directory is $EZ_TOOL_BIN, else $XDG_BIN_HOME, else $HOME/.local/bin, an empty value counting as unset. ez tool install and ez tool upgrade link there, and refuse before anything is built when all three are empty. |
Proved | proved | src/tool/LAWS.bend bin_dir_ez; src/tool/LAWS.bend bin_dir_xdg; src/tool/LAWS.bend bin_dir_home; src/tool/LAWS.bend bin_dir_none; src/tool/LAWS.bend tool_links_in_bin_dir; src/tool/LAWS.bend tool_needs_bin_dir |
| EZ-TOOL-2 | A cached binary is reused only when the recorded commit, built file and bend version all equal the resolved ones, and never when the resolved commit is empty. A cached checkout is reused only when its recorded commit equals the resolved one. | Proved | proved | src/ez/LAWS.bend key_rev_differs; src/ez/LAWS.bend key_file_differs; src/ez/LAWS.bend key_bend_differs; src/ez/LAWS.bend key_no_rev; src/ez/LAWS.bend key_same_reuses; src/ez/LAWS.bend checkout_differs; src/ez/LAWS.bend checkout_same; src/tool/LAWS.bend tool_reuses_record; src/tool/LAWS.bend tool_builds_on_miss |
| EZ-TOOL-3 | A local target with uncommitted or untracked changes, whatever the repository's own settings hide, or a path that is not the top of a checkout, resolves to no commit and is rebuilt on every run. | Proved | proved | src/tool/LAWS.bend local_rev_dirty; src/tool/LAWS.bend local_rev_unchecked; src/tool/LAWS.bend local_rev_elsewhere; src/tool/LAWS.bend tool_unrevved_builds |
| EZ-TOOL-4 | A target naming a [tools.*] pin in ez.toml builds the lock's rev, url, entry and bin. An owner/repo or URL target builds the commit git ls-remote <url> HEAD names. A path builds its clean HEAD. A checkout with no ez.toml is a plain Bend repository: it is built with no lock fetched and with BEND_LIB at a library of its own under the cache, where bend fetches its hub imports. A checkout with an ez.toml and no ez.lock.toml is refused when its binary is to be built. |
Proved | proved | src/tool/LAWS.bend tool_pin_src; src/tool/LAWS.bend tool_pin_rev; src/tool/LAWS.bend tool_pin_url; src/tool/LAWS.bend tool_pin_over; src/tool/LAWS.bend tool_free_src; src/tool/LAWS.bend tool_free_rev; src/tool/LAWS.bend tool_path_rev; src/tool/LAWS.bend local_rev_clean; src/tool/LAWS.bend tool_plain_no_lock; src/tool/LAWS.bend tool_plain_lib; src/tool/LAWS.bend tool_ledger_needs_lock |
| EZ-TOOL-5 | ez tool run exits with the built program's status; any failure before the program runs exits 1. |
Proved | proved | src/tool/LAWS.bend tool_run_exits_with_program; src/tool/LAWS.bend tool_refusal_exits_one |
| EZ-TOOL-6 | ez tool install and ez tool upgrade never run the built binary. |
Proved | proved | src/tool/LAWS.bend tool_link_never_runs |
| EZ-TOOL-7 | The built file is the pin's bin, then the pin's entry, then the file --entry names, then the checkout's bin, then its entry, then main.bend, and a built file that is not in the checkout is refused. The link is named after the checkout's package name, or app; a plain repository's is the built file's name without .bend, or the repository's name when that is main; and a name that is not a TOML bare key is refused. |
Proved | proved | src/tool/LAWS.bend file_pin_bin; src/tool/LAWS.bend file_pin_entry; src/tool/LAWS.bend file_bin; src/tool/LAWS.bend file_entry; src/tool/LAWS.bend file_main; src/tool/LAWS.bend file_flag_over_ledger; src/tool/LAWS.bend file_pin_over_flag; src/tool/LAWS.bend tool_builds_file; src/tool/LAWS.bend tool_plain_builds_main; src/tool/LAWS.bend tool_plain_builds_entry; src/tool/LAWS.bend tool_refuses_missing_entry; src/tool/LAWS.bend out_name_own; src/tool/LAWS.bend out_name_app; src/tool/LAWS.bend plain_name_stem; src/tool/LAWS.bend plain_name_repo; src/tool/LAWS.bend tool_plain_named; src/tool/LAWS.bend tool_links_named; src/tool/LAWS.bend tool_refuses_unsafe_name |
| EZ-TOOL-8 | A remote target whose cache slug is empty, absolute, or climbs with .. is refused. |
Proved | proved | src/tool/LAWS.bend remote_refuses_slug; src/tool/LAWS.bend tool_refuses_bad_slug; src/tool/LAWS.bend tool_refuses_nowhere |
| EZ-TOOL-9 | ez tool run [--entry <file>] <target> passes every word after the target to the program, dropping one leading --. ez run passes every word after run to the entry ez.toml names, or main.bend when it names none. |
Proved | proved | src/tool/LAWS.bend tool_rest_dash; src/tool/LAWS.bend tool_rest_word; src/tool/LAWS.bend tool_rest_none; src/tool/LAWS.bend tool_rest_entry; src/tool/LAWS.bend tool_run_passes_words; src/tool/LAWS.bend run_line_rest; src/ez/LAWS.bend run_starts_entry; src/ez/LAWS.bend run_starts_main |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| EZ-PUB-1 | ez publish refuses, and sends nothing, when git status --porcelain --untracked-files=normal names any path, when git cannot answer it, or when a file of the package is one git does not track as unchanged (git ls-files -v tag H), an ignored file included. |
Proved | proved | src/pub/LAWS.bend clean_is_all_blank; src/pub/LAWS.bend untracked_is_dirty; src/pub/LAWS.bend modified_is_dirty; src/pub/LAWS.bend staged_is_dirty; src/pub/LAWS.bend assumed_is_untracked; src/pub/LAWS.bend skipped_is_untracked; src/pub/LAWS.bend pub_dirty_refuses; src/pub/LAWS.bend pub_gitless_refuses; src/pub/LAWS.bend pub_stray_sends_nothing; src/pub/LAWS.bend pub_stop_sends_nothing; src/pub/LAWS.bend pub_unsent_refuses |
| EZ-PUB-2 | ez publish succeeds only when bend exits 0, a line of its output is exactly a 0x name, and every such line equals ez's own hash; it then prints that hash and the import line for the entry's path inside the package, by the package's name when EZ-PUB-3 gives it one and by that hash otherwise. Any other answer exits 1. |
Proved | proved | src/pub/LAWS.bend unread_never_agrees; src/pub/LAWS.bend differs_never_agrees; src/pub/LAWS.bend ours_agrees; src/pub/LAWS.bend progress_is_not_an_answer; src/pub/LAWS.bend import_is_not_an_answer; src/pub/LAWS.bend is_name_needs_0x; src/pub/LAWS.bend is_name_needs_length; src/pub/LAWS.bend is_name_needs_hex; src/pub/LAWS.bend is_name_hex34; src/pub/LAWS.bend pub_needs_agreement; src/pub/LAWS.bend pub_reports_ours; src/pub/LAWS.bend pub_reports_hash |
| EZ-PUB-3 | ez publish publishes under a name when the ledger's [package] table gives both publish-as and version: it runs bend <entry> --publish <publish-as>@<version>.0 and, on success, prints the hash and the import line by that name. publish-as must be a hub name as bend's NAMED rule reads one, and version MAJOR.MINOR.PATCH with no leading zeros and no pre-release or build suffix. With only one of the two keys, or with either one malformed, it refuses before it asks git anything or sends anything. With neither it publishes by hash as before. |
Proved | proved | src/pub/LAWS.bend semver_needs_digits; src/pub/LAWS.bend prerelease_refused; src/pub/LAWS.bend build_refused; src/pub/LAWS.bend neither_is_hash; src/pub/LAWS.bend name_needs_version; src/pub/LAWS.bend version_needs_name; src/pub/LAWS.bend bad_name_refused; src/pub/LAWS.bend bad_version_refused; src/pub/LAWS.bend named_is_four_part; src/pub/LAWS.bend upload_by_hash; src/pub/LAWS.bend upload_by_name; src/pub/LAWS.bend pub_misnamed_stops; src/pub/LAWS.bend pub_named_uploads_named; src/pub/LAWS.bend pub_unnamed_uploads_by_hash; src/pub/LAWS.bend pub_reports_name; src/init/LAWS.bend init_publishes_by_hash |
| EZ-PUB-4 | Once every check before the upload has passed, and just before the upload runs, ez publish prints hub description: <line> on stderr, the line the hub will describe the package by: the first line of the package's first file by path, in plain string order, passing over every file named LICENSE. A publish refused before the upload prints only why. |
Proved | proved | src/pub/LAWS.bend line_first_cut; src/pub/LAWS.bend hub_license_named; src/pub/LAWS.bend hub_skips_license; src/pub/LAWS.bend hub_first_by_path; src/pub/LAWS.bend pub_upload_says_description |
| EZ-PUB-5 | ez publish uploads only when every hub package the package imports is on the hub the ledger names: for each 0x<hash>/... import in the package's files the hub serves a manifest that hashes to that name, and for each <name>@<version>/... import the hub resolves the name to a 0x name, the one the lock or the ledger resolved it to when either records one. Before the upload it asks the hub about each; a package the hub does not have, and a hub that could not be asked, refuse with exit 1, naming each such import and the dependency key and origin the ledger records for it, and nothing is sent. |
Proved | proved | src/pub/LAWS.bend pub_sends_only_on_hub; src/pub/LAWS.bend pub_offhub_sends_nothing; src/pub/LAWS.bend pub_offhub_refuses; src/pub/LAWS.bend hub_one_off_is_off; src/pub/LAWS.bend hub_404_is_absent; src/pub/LAWS.bend hub_unreachable_is_off; src/pub/LAWS.bend hub_name_elsewhere_is_off; src/pub/LAWS.bend hub_name_there |
| ID | Requirement | Level | Status | Law |
|---|---|---|---|---|
| EZ-OUT-1 | Every command exits 0 on success and 1 on any failure ez detects, except ez run and ez tool run, which exit with the program's status. |
Proved | proved | src/init/LAWS.bend init_exits_as_it_refuses; src/lock/LAWS.bend lock_exits_as_it_refuses; src/remove/LAWS.bend remove_exits_as_it_refuses; src/add/LAWS.bend add_exits_as_it_refuses; src/fetch/LAWS.bend fetch_exits_as_it_refuses; src/tool/LAWS.bend tool_refusal_status_one; src/tool/LAWS.bend tool_run_status_is_program; src/tool/LAWS.bend tool_link_status_zero; src/tool/LAWS.bend sync_exits_as_it_refuses; src/tool/LAWS.bend sync_needs_ledger; src/pub/LAWS.bend pub_exits_as_it_refuses; src/doctor/LAWS.bend doctor_exits_as_it_fails; src/ez/LAWS.bend build_exits_as_bend; src/ez/LAWS.bend check_exits_as_it_passes; src/ez/LAWS.bend gate_exits_as_it_counts; src/ez/LAWS.bend package_needs_upgrade; src/ez/LAWS.bend start_needs_ledger; src/ez/LAWS.bend start_needs_parse; src/ez/LAWS.bend run_refusal_exits_one; src/ez/LAWS.bend run_exits_with_program; src/ez/LAWS.bend help_exits_zero; src/ez/LAWS.bend usage_error_exits_one; src/ez/LAWS.bend bare_exits_zero; src/ez/LAWS.bend group_exits_one; src/ez/LAWS.bend command_runs; src/ez/LAWS.bend command_ends_its_own |
| EZ-OUT-2 | A command that refuses writes nothing: every file it would otherwise write or remove is left as it found it. | Proved | proved | src/init/LAWS.bend init_refusal_writes_nothing; src/lock/LAWS.bend lock_refusal_writes_nothing; src/remove/LAWS.bend remove_refusal_writes_nothing; src/add/LAWS.bend add_refusal_writes_nothing; src/fetch/LAWS.bend fetch_refusal_writes_nothing; src/tool/LAWS.bend tool_refusal_writes_nothing; src/tool/LAWS.bend tool_missing_entry_writes_nothing; src/tool/LAWS.bend sync_refusal_installs_nothing; src/pub/LAWS.bend pub_refusal_writes_nothing; src/pub/LAWS.bend pub_misnamed_writes_nothing; src/pub/LAWS.bend pub_offhub_writes_nothing; src/add/LAWS.bend add_named_refusal_writes_nothing; src/add/LAWS.bend add_named_refuses_unknown; src/add/LAWS.bend add_named_refuses_unhashed; src/add/LAWS.bend add_named_refuses_manifest |
No requirement is pending. The paragraphs below record how each proved requirement that took more than one command was closed, and what its laws rest on.
EZ-HASH-3 is proved of every command that lays a tree. Over the package walk (src/pkg/pkg.bend), the 0x name of the files it found, and their manifest, are the name and the manifest of the files it lays, each weighed by its own text. ez add, ez fetch and ez lock, plain or --upgrade: every tree the plan lays has the manifest of the texts it lays as its last file, each weighed by its own text, and is named by that manifest's 0x hash (add_lays_named, add_named_lays_named, fetch_lays_named, lock_lays_named, all over P.lays.named). ez add <name>@<version> judges the package the hub serves as ez lock judges a hub package, so one whose manifest does not hash to the name the hub answered is refused, never laid (add_named_refuses_manifest). The lock checks, besides the manifest's digest and each file's sum, that the files it lays hash to the name, and lays the manifest of those files, so a package whose manifest hashes to its name but is not written the way the name is taken is refused, not locked (see docs/rfc/ez-spec.md, "Decided behavior changes").
EZ-HASH-4 stays Trusted, since bend is another program, but the walk's side of it is stated in laws. bend 2.0.27 publishes every file named exactly LICENSE beside a file of the package, at the same path, and refuses a file under a directory named license in any case. The walk takes such a LICENSE along beside a module (license_goes_along) and beside a foreign body (foreign_license_goes_along), asks for one it was not given rather than hashing without it (license_asked), finds a file whose directory holds none as it always did (no_license_as_before), and refuses a package with a file under a license directory, naming it (licensed_names, license_dir_refused, license_dir_passes). A ledger written before names a git package without its LICENSE files, and the name decides: ez lock judges a checkout whose walked manifest is not the one its name is the digest of without them (bare_drops_license, bare_keeps_sources, git_named_without_license), and ez lock --upgrade weighs a pinned commit the same way (upgrade_named_without_license).
EZ-HASH-7 is proved of the reading the NAR walk (src/sha/nar.bend) makes of its listing: every field is cut at the NUL that ends it and nowhere else (nar_field_verbatim), so a listing is read back as the fields it was printed from (nar_listing_verbatim), whatever spaces or newlines a name or target holds. That the listing is what the filesystem holds, and that the walk builds the NAR from it as nix's dumper does, is EZ-HASH-5.
EZ-LED-8 is proved for every command that reads a source. P.anchor keeps a URL and an absolute path and joins a relative path to the project root. ez add records the target as given, a path with only ~ expanded against HOME (add_records_as_given, add_path_as_given). ez fetch writes no file (fetch_keeps_records). ez lock, plain or --upgrade, records in the lock the source the ledger it is made from records for each package (lock_records_as_given), and ez lock --upgrade renders a model whose dependencies and tool pins record ez.toml's sources in ez.toml's order (upgrade_records_as_given, upgrade_records_tools_as_given), which is what ez.toml's bytes read back as (EZ-LED-4). Every question git is asked names the source anchored at the project, as the planner computes it: ez add's (add_asks_anchored), ez fetch's checkouts (fetch_asks_anchored), ez lock's package questions (lock_asks_anchored), and the upgrade's, each put to git as Up.anchor of the question the upgrade looks its answer up by, which are exactly P.wants.up (upgrade_asks_anchored, upgrade_asks_its_questions). That the interpreter hands git the source a question names is EZ-TRUST-2.
EZ-DOC-3 reads the committed tree as bend reads it. A hub import line is a root of the lock whatever run of spaces and tabs stands between import, the path, as and the name, however the line is indented and whatever blanks trail it, so long as the lines above it leave the header open (root_reads_as_bend). The scan trims a line and cuts it at the white space bend's loader splits on, JavaScript's \s, so spaces and tabs are the case the law states and not the only one the scan reads. ez doctor reads the same roots (P.roots), so EZ-VEN-5's import lines are these too.
EZ-VEN-1 is proved for ez add, ez remove and ez lock --upgrade. Over the line-level function I.lines (src/ledger/ignore.bend), its allowlist lines are exactly the vendored hashes, each once, in the order the ledger first names them, and every other line is kept in order; the file I.sync writes reads back (I.file.lines) as those lines, whatever the file it read ended with, and applying it twice is applying it once; each for a ledger whose vendored hashes hold no newline. ez remove and ez add leave .gitignore holding exactly I.sync's text over the ledger they leave (remove_syncs_allowlist, add_syncs_allowlist). ez lock --upgrade: every .gitignore its plan writes has the allowlist of the hashes the upgrade commits and keeps every other line of the file it read, when no source it read is at .gitignore; an upgrade that does not refuse and leaves .gitignore unwritten read one whose allowlist is already those hashes (upgrade_allowlist_kept_in_sync); and the hashes it commits are the vendored hashes of the model it renders when it writes ez.toml (upgrade_vends_the_ledger) and of ez.toml as it is when it does not (upgrade_unmoved_vends_the_ledger). ez add's half and the upgrade's hold of ez.toml's bytes, since the ledger they leave reads back as the model they render (EZ-LED-4).
EZ-DOC-1 is trusted, not proved: the lock is written as eztoml's render of the document ez assembles (T.normal, src/toml/toml.bend) and read through eztoml's parse, so it reads back when eztoml's round trip holds, which is EZ-TRUST-8, proved in eztoml v0.8.0. ez still writes no lock that lockable.named refuses: lockable refuses a hash, key or value holding ", \ or a newline, a hash written twice, and a file path holding =. eztoml escapes strings and reads a quoted key whole, so these refusals are no longer needed for eztoml; they are kept for bootstrap.sh, whose awk cuts a pair at its first = and reads no escape. What the lock records is the packages in hash order with each one's files in path order and each once, each tool pin without vendor, and the names in name order and each once. Until ez moved to eztoml 0.4 this row was proved against the v0.1.0 reader (lock_reads_back and its tools, names and hub laws); the maintainer chose to move ahead of eztoml's proofs, and those laws went with the reader they unfolded.
EZ-LED-4 is proved relative to EZ-TRUST-8. src/ledger/LAWS.bend states the read-back as a premise, ReadsBack: every ledger Rend.renderable accepts reads back, from the text Rend.show writes, as itself. Rend.show is eztoml's render of the document ez assembles (Rend.text) and M.parse reads through eztoml's parse, so the premise is eztoml's round trip, proved in eztoml v0.8.0, and ez's gate does not re-check it. What ez proves is the rest: every command that writes ez.toml refuses a ledger that is not renderable, with no effect (EZ-OUT-2), and writes one that reads back, given the premise, as the model its laws are stated over: ez init the package and entry it was given (init_ledger_reads_back), ez add the ledger with the dependency added (add_ledger_reads_back, add_named_reads_back), and ez remove the ledger with it dropped (remove_ledger_reads_back). renderable refuses a name or value holding ", \ or a newline, a dependency with no hash, and a git source that names no repo or no root. A ledger written before ez used eztoml 0.4 reads to the same model: src/toml/toml.bend passes over the tables a dotted header implies, and tests/toml.bend reads an old ledger and lock and their new forms to the same sections.
The upgrade laws of phase three, for EZ-RES-4, EZ-RES-5, EZ-RES-6, EZ-RES-8 and the ez lock --upgrade half of EZ-VEN-1, are stated over the ledger model the upgrade renders into ez.toml, and hold of the file's bytes because those bytes read back as that model (EZ-LED-4). The design is in docs/rfc/ez-lock-planner.md. EZ-RES-4 and EZ-RES-6 are proved so: their laws (src/lock/LAWS.bend) are over P.ledger.next, the model an upgrade renders, and over P.wants.up, the questions it asks, and what they say of ez.toml's bytes, and of the lock made from those bytes read back, holds by EZ-LED-4. EZ-RES-6's NAME is a nonempty --package; an empty one is no filter, as ez lock --upgrade alone.
EZ-RES-5 and EZ-RES-8 are proved in the same way. Their laws are over P.ledger.next, the model ez lock --upgrade renders into ez.toml: a pin by its commit alone moves only to the default branch tip the remote named, when the remote said the tip descends from it, keeps no tag, and, when the upgrade asks about it and does not refuse, is at that tip; a pin through a tag keeps its tag, moves only to the commit the remote names for the tag along its history, and is at that commit when the upgrade does not refuse; and a tip off the pin's history, or a pinned commit whose checkout no longer agrees with the pin, makes P.refuses true, which is a plan with no effect (EZ-OUT-2) that the interpreter ends with exit 1 (EZ-TRUST-2). That the bytes of ez.toml read back as that model is EZ-LED-4, and that the remote's refs and ancestry are true of the repository is EZ-RES-7.
EZ-DOC-4 is proved for a plain lock and for ez lock --upgrade. after (src/lock/LAWS.bend) is the World a lock leaves for the next to read: a refused lock leaves the World it read; one that succeeded leaves every tree it laid read from BEND_LIB with the bytes laid, and an upgrade also leaves the ledger it wrote, the committed sources as it rewrote them, and .gitignore as it left it. The remote does not change between the two runs: every question the second upgrade asks a remote is answered as the first run's answers say. Run again on that World, ez lock --upgrade writes the same bytes to ez.lock.toml (upgrade_idempotent), renders the same ledger model (reupgrade_moves_nothing), so writes no ez.toml (upgrade_settles), lays nothing new (reupgrade_lays_nothing), and writes no path but the lock (reupgrade_writes_only_lock), the last for a ledger whose vendored hashes hold no newline, as EZ-VEN-1's text layer requires. Each rests on the ez.toml the first run wrote reading back as the model it rendered, which is EZ-LED-4, and each takes that as its premise ReadsBack (EZ-TRUST-8). The key step is that a pin at its own tip is kept: the second run asks each selected pin the question the first asked, gets the tip it moved to, and checks the tree out again, which agrees with the hash, narHash and root the first run wrote. That a vendored tree laid under .ez/lib is read from BEND_LIB holds when BEND_LIB is .ez/lib, its default; with BEND_LIB elsewhere it is cloned again, and clone_reproduces says the lock is the same.
EZ-FETCH-1 is proved over the plan ez fetch runs (src/fetch/plan.bend): every tree it lays holds the files the lock records under that hash, in the lock's order, each with a text whose digest equals the lock's sum for it (fetch_lays_the_lock). The law asks the same of a hub body and a git file, and a digest that equals the lock's sum starts with it, so it covers those halves of the row. A git package is laid only from a checkout that weighed to the narHash the lock records for it (fetch_lays_weighed), which is a lock that records one and a checkout whose narHash is that one (fetch_weighs_the_checkout); any other checkout stops the package with the reason (fetch_refuses_unweighed), and a stopped package refuses the fetch, which lays nothing (EZ-OUT-2). So a fetch pins the tree around the bytes it lays, the tree nix rebuilds the package from, and not only the bytes. A tree already under BEND_LIB is checked file by file before it is kept, and one that fails is fetched again rather than trusted; it was not fetched, so it has no checkout to weigh. That the interpreter reads what the hub served and what the checkout holds, weighs the checkout as Nar.path does, and lays each text as the plan says, is EZ-TRUST-2.
EZ-TOOL-1 to EZ-TOOL-9 are proved over the plan ez tool run, install and upgrade run (src/tool/plan.bend), over what it resolves a target to, and over the words ez tool run and ez run hand on (src/share/args.bend). ez run starts bend on the entry ez.toml names, or main.bend when it names none, with every word after run (run_starts_entry, run_starts_main), a line src/ez/start.bend decides from the ledger the interpreter read and the words it was given. What the laws take from the interpreter is EZ-TRUST-2: that it asks git status with --untracked-files=normal, so an untracked file counts whatever the repository hides; that it reads the real path, the checkout's top and HEAD as git gives them; that it starts the program last and exits with its status, and exits 1 when a fetch, build or link it runs fails; and that ez tool run and ez run are handed the words the runtime passes them (Args.tool.rest and Args.run.line over IO.args() with the program's own name, which bend 2.0.32 and later put first, dropped by Args.all), and ez run's line run with the project's BEND_LIB in front of it (Env.line); and that a build runs bend with the library the plan names as BEND_LIB, so a plain repository's hub imports are fetched there by bend, which checks each against its name.
EZ-OUT-1 is proved for every command, each over the end its planner, or the pure half of its interpreter, gives it. A planner's plan ends with an outcome, and P.status is the status the interpreter exits with (Run.end): ez init, ez add, ez remove, ez lock, plain or --upgrade, ez fetch, ez publish and ez doctor exit 1 exactly when their planner refuses, or for doctor fails the command, and 0 when it does not (init_exits_as_it_refuses, add_exits_as_it_refuses, remove_exits_as_it_refuses, lock_exits_as_it_refuses, fetch_exits_as_it_refuses, pub_exits_as_it_refuses, doctor_exits_as_it_fails). ez tool run, install and upgrade exit with TP.code of the plan's end and the status of the program the plan started: a refusal exits 1 whatever a program would have said, since none is started (tool_refusal_status_one), ez tool run that goes on exits with the program's status (tool_run_status_is_program), and install and upgrade that go on exit 0 (tool_link_status_zero). ez tool sync exits 1 exactly when it refuses (sync_exits_as_it_refuses), which it does with no ez.toml (sync_needs_ledger); each install it runs ends as ez tool install does, so the first that refuses ends the sync with 1. ez check, ez build, ez run, ez test and ez prove are not planners. ez check, ez build and ez run first decide from ez.toml what to start (src/ez/start.bend): with no ez.toml, or one that does not parse, each refuses, starts nothing and exits 1 (start_needs_ledger, start_needs_parse). ez check, ez build, ez test and ez prove end with an outcome src/ez/ends.bend makes from what bend answered, and exit 1 exactly when the check did not pass, bend did not exit 0, or a file did not pass (check_exits_as_it_passes, build_exits_as_bend, gate_exits_as_it_counts). ez run exits with S.code of what it decided and the status of the program it started: 1 for a refusal, since none is started (run_refusal_exits_one), and the program's own status otherwise, as cargo run does (run_exits_with_program); a program bend could not check is bend's failure, and exits with bend's status. ez lock --package without --upgrade exits 1 before anything is read (package_needs_upgrade). Before any command runs, src/ez/line.bend decides how the line ends. Help exits 0: a bare ez, a line that selected no command, and every request for help Shake answers (bare_exits_zero, help_exits_zero). A misused line exits 1: a bare group such as ez tool, and every line Shake refuses, an unknown command or flag, a word too many, a missing argument or value, an option given twice, or ez help of a word that names no command there, which Shake refuses as Unexpected rather than answering as a request for help (group_exits_one, usage_error_exits_one; the last case is shake's SHAKE-PARSE-8, trusted as EZ-TRUST-7). A line that names a command runs it, with the bindings Shake made for that command, and leaves the status to it (command_runs, command_ends_its_own). What the laws take from the interpreter is EZ-TRUST-2: that it exits with the status these functions give; that it hands TP.code the status the program exited with, and S.code the status bend exited with, 128 plus the signal for one a signal ended and 127 for one that could not be started; that a failure it meets itself, a write the system rejects, a build or link that fails, a fetch inside ez tool, or a loop that runs out of fuel, exits 1; and that the answer src/ez/ends.bend reads is what bend printed and the status it exited with. A flag the native runtime takes is not ez's: the runtime takes --threads and --gpu with the value after each, and answers --gpu-build and --bend-help itself, anywhere on the line before a --, before ez sees it. --help reaches ez, and Shake reads it as it reads help: before any positional of the command is bound, ez --help and ez add --help are requests for help, exiting 0 by help_exits_zero, while ez add owner/repo --help is a usage error (shake's SHAKE-PARSE-8, trusted as EZ-TRUST-7). A --help after a -- is a word like any other, and one among the words ez run and ez tool run forward is the program's.
EZ-OUT-2 is proved for every command, each over the plan its planner makes. ez lock, plain or --upgrade: a World on which the planner refuses has a plan with no write, lay or remove effect, so it writes nothing, not the lock, ez.toml, .gitignore, a source or a tree. The upgrade's refusals (a pin off its history, a drift, a hub digest that does not match, an answer IO could not give, an unknown --package, a ledger model that is not renderable) and the lock's refusals after an upgrade are all such Worlds. ez remove and ez init: the same, for every World on which their planners refuse: no ledger, one that does not parse, a name it does not have, or a ledger left that is not renderable, for ez remove; a ledger that is there, a name or entry a ledger cannot carry, or a description holding a newline, for ez init. ez add: the same for every World on which its planner refuses, before a question (no ledger, one that does not parse, a target that names nothing, a --rename that is no key or a clash the ledger decides) or after (a ref the remote does not have, an entry the checkout lacks, a walk that refuses, a name Named.why.as objects to, a ledger that is not renderable), so a refused add lays no tree, not even in the cache (add_refusal_writes_nothing). ez add <name>@<version> is planned by H.plan (src/add/hub.bend), and the same holds of it: no ledger, one that does not parse, a key Named.hub.why objects to, a name the hub has no package for or answers with no 0x name, a package whose manifest does not hash to that name, an entry the package lacks, or a ledger that is not renderable, and it lays no tree and no name's file (add_named_refusal_writes_nothing, add_named_refuses_unknown, add_named_refuses_unhashed, add_named_refuses_manifest, add_named_refuses_clash, add_named_entry_absent, add_named_refuses_unrenderable). ez fetch: the same for every World on which its planner refuses (no ledger, no lock, a package that could not be fetched, one whose files do not match the lock, leave the package or do not hash to its name, or one whose checkout does not weigh to the lock's narHash), so a refused fetch lays no tree, not one of a package that checked before the one that failed, and removes none already under BEND_LIB (fetch_refusal_writes_nothing). ez tool run, install and upgrade: the same for every World on which their planner refuses (nowhere to link, no cache root, a project ledger that does not parse, a target that names nothing or whose slug could leave the cache, a name the lock does not pin or pins at no commit, a checkout git could not give, a file to build that is not in the checkout, a package name that is not a TOML bare key, an ez project's build with no lock), so a refused tool command lays no checkout under the cache, builds nothing and links nothing (tool_refusal_writes_nothing, and tool_missing_entry_writes_nothing for a missing file); and ez tool sync, which refuses before it installs anything when the ledger does not parse or names a pin the lock lacks (sync_refusal_installs_nothing). ez publish: its plan writes no file at all, only the two lines a publish that agreed says, so a refused publish writes nothing (pub_refusal_writes_nothing), and one refused because a hub import is off the hub has a plan with no effect at all (pub_offhub_writes_nothing); and every refusal that can be decided before the upload is decided before it, so a refused publish sends nothing unless bend's own answer is what it refuses (EZ-PUB-1, EZ-PUB-2, EZ-PUB-5). A sync that goes on runs one install per pin, each its own plan, so a later install that refuses leaves the earlier ones installed, as cargo install a b does. A write the interpreter attempts and the system rejects is EZ-OUT-1's, and what it leaves is EZ-TRUST-2's.
EZ-PUB-1 and EZ-PUB-2 are proved over the plan ez publish runs (src/pub/plan.bend). A World whose git status names a path, or that git cannot answer, is refused outright: nothing more is asked and nothing is sent (pub_dirty_refuses, pub_gitless_refuses, pub_stop_sends_nothing). A package holding a file git does not track as unchanged never reaches the upload (pub_stray_sends_nothing), and a World that does not reach it refuses (pub_unsent_refuses). A publish succeeds only when the upload's answer agrees with the hash ez computed (pub_needs_agreement), and the laws over agrees say what agreeing is: at least one line is a 0x name and every such line is ez's hash. It then says ez's hash, never bend's (pub_reports_ours). bend 2.0.27 cannot report a package's hash without uploading it, so the upload is the last question the planner asks and the check is made on its answer; EZ-PUB-2 promises that a disagreement exits 1 and prints no import line, not that nothing was sent. What the laws take from the interpreter is EZ-TRUST-2: that it asks git status with --untracked-files=normal and git ls-files -v in the project, and runs the upload with the entry the planner names.
EZ-PUB-3 is proved over the same plan. PP.naming reads the two [package] keys the ledger model carries: neither is a publish by hash (neither_is_hash), one without the other is refused naming the key that is missing (name_needs_version, version_needs_name), a publish-as that K.name.part refuses, the NAMED name rule the package walk already reads imports by, is refused (bad_name_refused), and so is a version that PP.semver refuses: one with a character other than a digit or a dot anywhere (semver_needs_digits, prerelease_refused, build_refused), or one that is not three numbers each as K.ver.num reads one (bad_version_refused). Both good are <publish-as>@<version>.0 (named_is_four_part). Over a World whose ledger text parses to a model with those keys, a refusal stops before git is asked (pub_misnamed_stops) and its plan is the refusal alone (pub_misnamed_writes_nothing); a name is asked for in the upload question (pub_named_uploads_named), and no name asks for the upload by hash (pub_unnamed_uploads_by_hash); the words the upload runs are upload_by_name and upload_by_hash. A named publish that succeeds prints the import line by the name (pub_reports_name), and one by hash by the hash (pub_reports_hash). The two keys read back from the ledger ez writes under EZ-LED-4, since Rend.renderable checks them and ReadsBack covers the whole model, and the ledger ez init writes names neither (init_publishes_by_hash). What the laws take from the interpreter is EZ-TRUST-2: that it runs the words PP.upload.line makes of the question.
EZ-PUB-4 is proved over the same plan and src/pub/blurb.bend. The upload question carries the line (pub_upload_says_description), B.blurb of the files the walk made, which are the files bend sends: the entry, what it imports, and since bend 2.0.27 the LICENSE beside each (EZ-HASH-4). A LICENSE never gives the line (hub_license_named, hub_skips_license), and a file that is not one, whose path comes no later than any other file's, does, with its first line (hub_first_by_path), which is what comes before its first newline (line_first_cut). Paths are compared by String.is_le, the order the manifest is written in, which is JavaScript's for every path whose characters are in the Basic Multilingual Plane. The upload is the last question the planner asks, so a World the planner refuses before it never carries the line (pub_stop_sends_nothing, pub_stray_sends_nothing). That the hub picks the line this way is the hub's, not ez's: ez says what it expects the hub to show. What the laws take from the interpreter is EZ-TRUST-2: that it prints the line the question carries just before it runs the upload, and at no other time.
EZ-PUB-5 is proved over the same plan. Past the check that git tracks every file, the planner collects the hub imports of the files the walk made, each 0x name and each <name>@<version> once, reads the lock when there is a name among them, and asks the ledger's hub about each (PP.hubbed). A World gets as far as the upload only when every one is on the hub (pub_sends_only_on_hub), so one that is off it sends nothing (pub_offhub_sends_nothing) and refuses (pub_offhub_refuses), and one import off the hub is enough wherever it stands among them (hub_one_off_is_off). What counts as off is stated over the answer: a 404 is a package the hub does not have (hub_404_is_absent), any other answer that is not a 200, the hub unreachable among them, is a hub that could not be asked, which refuses too (hub_unreachable_is_off), and a name the hub resolves to a hash other than the one the lock records is not the package imported (hub_name_elsewhere_is_off), while one it resolves to that hash is (hub_name_there). A manifest the hub serves for a 0x name counts only when it hashes to that name, as ez lock checks it. What the laws take from the interpreter is EZ-TRUST-2: that it GETs the url each question names under the ledger's hub, as ez lock does, and reads the lock from ez.lock.toml.
EZ-INIT-1 and EZ-INIT-2 are proved over the plan ez init runs. The stub is its line for the hub, a newline, and the program, so its first line is that line whenever the line is one line (init_stub_heads, with line_first_cut), and the planner refuses, with no effect, a project whose line is not (init_one_line, init_refusal_writes_nothing). The line is the description given (init_header_given) or the placeholder (init_header_placeholder). A fresh project that fits writes src/lib.bend and a main.bend that imports it (init_lays_src, init_lays_main); in the package that entry makes, main.bend comes before src/lib.bend, so the hub shows the entry's first line. A src/lib.bend or an entry that is there is left as it was, whatever else the World holds (init_keeps_src, init_keeps_entry); the law for src/lib.bend excepts an entry asked for at that path, which the entry's own text decides, and the one for the entry excepts ez.toml and .gitignore, which the plan writes itself. What the laws take from the interpreter is EZ-TRUST-2: that it reads the entry and src/lib.bend from the paths the planner names.
EZ-RES-2's import line is proved over the plan ez add runs (src/add/plan.bend): an add that does not refuse ends what it says with Git.import.line of the hash its walk made and the entry's path inside the package, K.inside of the walk's root and the entry (add_says_import). ez publish prints the same function of the same two, so both commands name a package's entry where the hub serves it: by its name alone, or, for a package whose imports climb out of the entry's directory, under the directories the package re-rooted above it. ez add <name>@<version> prints the same function with the name in place of the hash, for the entry it records (add_named_says_import).
EZ-VEN-4 and EZ-VEN-5 are proved over the plan ez doctor runs (src/doctor/plan.bend). Its plan is lines said and how the command ends, so it writes, lays and removes nothing (doctor_writes_nothing). An import line names a hash when ez lock reads it so: the header imports of a .bend file git tracks outside .ez/, as the package walk scans them (P.roots). Over a ledger that reads, every such hash the ledger's dependencies lack has its line (doctor_reports_unrecorded), every dependency whose hash no such line names has its line (doctor_reports_unused), and a report with any line fails the command (doctor_drift_fails). A ledger that is not there or does not read fails the command before any comparison. That the interpreter hands doctor the tracked files as git lists them and their texts as they are on disk is EZ-TRUST-2.
EZ-VEN-6 is proved over the same plan. DP.relock(w, fs) is the World doctor puts to the lock planner: a plain ez lock over the ledger's text, the sources fs git listed, and every tree doctor read from BEND_LIB, a hub package's judged as the hub's bytes and a git package's as ez lock judges one it finds there. When a lock is there and the lock planner asks nothing more, a lock whose text is the one P.decide makes is said to be up to date, and that line is not a problem (doctor_passes_fresh_lock, doctor_says_fresh_lock); a lock whose text differs by any byte is said to be out of date and fails the command (doctor_reports_stale_lock, doctor_stale_lock_fails). When the lock planner still asks about a package, which doctor asks BEND_LIB for and never the network, the lock is not checked and the command fails (doctor_unchecked_lock_fails). The lock planner answers the names it asks about from the lock and the names files under BEND_LIB, never the hub, and when it still asks about one the lock is not checked either (doctor_unchecked_names_fail); the laws before it hold when it asks nothing more about names. What the laws take from the interpreter is EZ-TRUST-2: that a tree's answer is its manifest and files as they are under BEND_LIB, and that a tree it reports absent has no manifest there.
EZ-HUB-1 to EZ-HUB-4 are proved over the package walk, the lock planner, and the plans ez fetch and ez doctor run. A named import is one whose first path segment holds @ with a / after it, as bend reads it; the walk queues no file for it (named_is_no_module) and stops, in bend's words, on a name bend would refuse (unnamed_stops, unnamed_refused). The lock resolves a name by a table: the names ez.toml records, each with the hash beside it, first (ledger_names_first), then the names the lock being rewritten records (lock_answer_names), then the hub's answers to GET $BEND_HUB/name/<name>@<version>. A name the table already resolves is never put to the hub (resolved_not_asked). The walk queues the package the table gives a name (named_kid_queued), the lock records each name with that hash (lock_names_agree), and [names] reads back as rendered (EZ-DOC-1, trusted). A lock that is made lays the names file of every name it records (lock_lays_its_names); ez fetch lays the lock's hash in a missing file and over one that names another hash, refuses a name bend would not read back, and lays no other (fetch_names_the_lock, fetch_lays_missing_name, fetch_rewrites_name, fetch_refuses_unread_name, fetch_lays_the_names); and ez doctor fails when a file is missing or names another hash (doctor_wrong_name_fails). A named import in the project's own files must be an ez.toml dependency, or ez lock refuses and says so; ez doctor reads named imports as import lines for EZ-VEN-5 too. ez lock --upgrade leaves named dependencies as they are, and rewriting import lines stays about 0x hashes. ez add <name>@<version> asks the hub the ledger names for the name, then for the package (add_named_asks_hub), records the name with the hash the hub answered (add_named_records_name), so the next ez lock reads the pair from ez.toml and puts nothing to the hub, and lays the name's file (add_named_lays_name). That a name the hub answered once keeps its hash is EZ-TRUST-6; that the interpreter writes a names file as 0x<hash> and a newline, and reads one as it is on disk, is EZ-TRUST-2.
EZ-LED-5 is proved over the ledger reader and over every command that reads a ledger's dependencies. The reader files a [tools.*] section among the tools, never among the dependencies, and never refuses it for lacking a hash, wherever it stands (tool_section_not_dep, tool_section_is_tool, tool_needs_no_hash). ez lock, plain or --upgrade, reads packages by the origins of the dependencies alone (lock_origins_skip_tools, upgrade_origins_skip_tools); ez add and ez remove edit the dependencies and write the tools back as they read them (add_keeps_tools, remove_keeps_tools), and ez remove refuses a name only a tool has (remove_refuses_tool); and two ledgers that differ only in their tools make the same ez doctor plan around the same lock check (doctor_ignores_tools), the check alone reading them, since the lock records them. ez fetch reads no dependency of the ledger, and ez tool reads only its tools.
These assumptions sit outside the proofs. They are the complete list of Trusted requirements, and a passing proof gate says nothing about them.
| ID | Assumption | Why it is trusted |
|---|---|---|
| EZ-TRUST-1 | The Bend checker is sound. | We cannot check it from inside Bend. The BendTT paper and a Lean formalization exist, and the release notes report mismatches between the formalization and the implementation. |
| EZ-TRUST-2 | The interpreter reads the World and executes plans faithfully. | It makes no decisions and is kept small enough to review line by line. |
| EZ-TRUST-3 | The hub serves, for a hash, what was published under it. | ez checks every hub body against the hash it asked for (EZ-FETCH-1), so this reduces to availability and EZ-HASH-6. |
| EZ-TRUST-4 | ez prove runs bend on every PROOF.bend in the tree and passes only on an exact ALL PROOFS CHECK first line. |
It is ez code run by mkProofs, not a law. CI builds from a clean tree, so nothing is cached. |
| EZ-TRUST-5 | HTTP framing and URL parsing are correct. | Proved in ezhttp v0.8.0, the rev ez.toml pins; ez's gate does not re-check it. ez imports its interface, main.bend, and src/client.bend and src/url.bend for the two types whose constructors src/hub/get.bend matches, which main.bend names but does not define. |
| EZ-TRUST-6 | A <name>@<version> the hub answered once names the same hash forever. |
The hub never moves a name once it is taken, so a name is resolved once and pinned in the lock. The package it names is still checked against its hash (EZ-FETCH-1). |
| EZ-TRUST-7 | Command-line parsing is correct: parse binds a line as shake's spec says, help_path names a request for help and only one, path_of and at follow the selected path, and get, on and help read and render it. |
Proved in shake v0.4.0, the rev ez.toml pins (SHAKE-PARSE-1 to SHAKE-PARSE-10, SHAKE-GET-1, SHAKE-GET-2, SHAKE-HELP-1, SHAKE-ERR-1, SHAKE-ERR-2); ez imports only its interface, main.bend, and its gate does not re-check it. In particular ez help <path> with a word that names no command there fails as Unexpected, not as a request for help, and a bare --help before any positional of the command is a request for help as help is (SHAKE-PARSE-8). |
| EZ-TRUST-8 | A document eztoml renders reads back as itself, and a text it reads without error renders back as the same document: its TOML-RT-1, TOML-RT-2 and TOML-RT-3. | Proved in eztoml v0.8.0, the rev ez.toml pins; ez imports only its interface, main.bend, and its gate does not re-check it. ez relies on them for EZ-DOC-1 and EZ-LED-4. ez's step between its sections and eztoml's document (src/toml/toml.bend) is ez code with no law: tests/toml.bend checks it on an old and a new ledger and lock. |
| EZ-TRUST-9 | A law may read snap's answers, code, text and ok, from src/answer.bend, the pure module snap's main.bend returns them from unchanged. |
ez imports that module deliberately, in src/ez/ends.bend, src/ez/LAWS.bend and src/ez/PROOF.bend: bend 2.0.32's verdict fails every proof whose imports reach snap's foreign effects, which main.bend holds, so no law may import main.bend. That main.bend's code, text and ok are src/answer.bend's is snap's SNAP-TRUST-5, a one-line delegate each in snap v1.1.0, the rev ez.toml pins; the interpreters read the same answers through main.bend. |
| EZ-DOC-1 | Parsing a rendered lock yields the packages, hub, names and tools that were rendered. | It is EZ-TRUST-8 for the document ez assembles for the lock. |
| EZ-RES-7 | git reports refs, tags, and ancestry accurately. | The World model takes git's answers as given. |
| EZ-HASH-4 | ez's 0x hash matches bend --publish. |
The publisher is a separate program. |
| EZ-HASH-5 | ez's narHash matches nix. | nix is a separate program. What ez trusts of its own walk is GNU find's listing of the tree, each path's type, %M mode, name and link target, and the file effect's read of each file's bytes. The walk takes the executable bit from the owner's exec bit of that mode, as nix's dumper does, and reads names and targets as listed (EZ-HASH-7). Submodules are not part of the tree: ez weighs a checkout without them, and its nix side asks fetchgit for the same. |
| EZ-HASH-6 | Sha.raw computes the SHA-256 digest of its bytes, and Sha.hex of its text's UTF-8. |
Proved in noah-emp/bend-sha256 against an executable FIPS 180-4 specification, at the hash ez vendors; ez's gate does not re-check it. Collision resistance is also assumed. |
EZ-VEN-2 and EZ-VEN-3 are proved for the moves an upgrade makes (src/ledger/LAWS.bend moves.ok): each old hash names something, no hash holds / or a newline, as a 0x name never does, and no move's new hash is the old hash of a move after it. That last is the premise the spec's notes call for: swaps apply one after another, so a new hash that is a later move's old one would be moved again. The text laws are over U.reimport.many, and the plan laws carry them to what ez lock --upgrade leaves at a .bend source it read and the World names once (found, with pre and post around it), when the lock does not refuse; that the sources the upgrade reads are the .bend files outside .ez and .git is the interpreter's (EZ-TRUST-2). A line names a hash when it starts import <hash>/ at column 0; the new hash a line names is the one the first move of its old hash sends it to.