proof · eukhe · Tangled

Coding agent with a memory of all things

eukhe proof

80 folders

at bend/stackfix

gildrb.com · proof(gateway_backoff): example rewrites doubled waits, no deep compare · 2w ago

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

approvals: each session's decision on a question decided by the compiled core (new approvals entry id 53)

laws: flight_store_terms_exact (the store's accessors are its fields; a mutant Sto.fresh made flight_after_end_served vacuous)

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

Merge branch 'bend/p2-small' into bend/all

stream: the tool output bounder's window, counts, store/drop/trim and notice run as compiled Bend (new bound entry id 76, a call and a Stepper); its Rust copy and bridge go

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

codemode: the identifier of a tool and the identifier test run as compiled Bend (new entry codemode_id id 260)

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

command laws: after a word that names a child, the rest of the line is pinned in every table (spaces, a child, or argument text and unknown words by the named entry's own flags)

compactor: a line's steps and the failure cap run as compiled Bend (new compactor entry id 70); the Rust copy, its bridge and the law-covered tests go

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

dashboard: the pairing gate's choices run as the compiled core (new entry dash id 101)

proof: the wire lemmas that dash_access and gateway_answer borrowed from doc_commit move to proof/base

dashboard: the command policy and the Host/Origin checks run as the compiled core (entries 200 dash_policy, 201 dash_access)

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

proof: the wire lemmas that dash_access and gateway_answer borrowed from doc_commit move to proof/base

glob: ranking and pages run as the compiled Bend core (entry 42 doc_glob)

laws: persist_writes_with_carry, edit_exact, load_holds_first_end (a fresh adversary's persist that started the carry from LF passed every doc_lines law)

durable: the retry note's text and a staged document's content and publication run as compiled Bend (new entries retry_note id 263, doc_plan id 264)

read: a gap marker before every span that does not start right after the one before (doc_rows)

laws: search_scope_rule (a fresh adversary's model scope that ignored directory roots passed every doc_search law, since the entry computes the scope inline)

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

docs: grep's tag choice for each shown file runs as the compiled core (new entry doc_tags id 102)

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

facts: the rulebook flags, adaptive thinking, the Bedrock effort and the tier price row run as compiled Bend (new model_facts entry id 71); the Rust copies and the facts bridge go

fsmode: the model's own terms are pinned (fsmode_socket_dir_exact, fsmode_safe_exact, fsmode_modes_exact): a blind adversary's socket_dir that ignored the owner passed socket_dir_owned through its own Seen.safe

proof: the wire lemmas that dash_access and gateway_answer borrowed from doc_commit move to proof/base

gateway_backoff

proof(gateway_backoff): example rewrites doubled waits, no deep compare

gateway_commands

gateway: the phone commands parse as the compiled core (entry 205 gateway_commands)

proofs: files past 1,000 lines become folders by topic (proof/base/, proof/<area>/base/, proof/optchat/push_agrees_always/); P1 binders renamed

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

infer: the forced call, the repetition guard and early compaction run as compiled Bend (entries 73 infer_force, 74 infer_guard a Stepper, 75 infer_threshold); the Rust copies, bridge_infer and the law-covered tests go

infer: the forced call, the repetition guard and early compaction run as compiled Bend (entries 73 infer_force, 74 infer_guard a Stepper, 75 infer_threshold); the Rust copies, bridge_infer and the law-covered tests go

infer_threshold

infer: the forced call, the repetition guard and early compaction run as compiled Bend (entries 73 infer_force, 74 infer_guard a Stepper, 75 infer_threshold); the Rust copies, bridge_infer and the law-covered tests go

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

kernel_local, launcher: the models' own terms are pinned (kernel_terms_exact, kernel_sweep_terms_exact, launcher_adoption_exact), so the laws that read them say what they claim

kernel_local, launcher: the models' own terms are pinned (kernel_terms_exact, kernel_sweep_terms_exact, launcher_adoption_exact), so the laws that read them say what they claim

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

staging: runs as compiled Bend (ffi_staging, spec-speller entry laws); the Rust copy, its bridge and the law-covered tests go

log: the entry reads only numbers that fit the wire (log_ffi_reads_only_fitting_requests, log_stepper_reads_only_fitting_commits): a blind adversary read a 15-digit length

facts: the rulebook flags, adaptive thinking, the Bedrock effort and the tier price row run as compiled Bend (new model_facts entry id 71); the Rust copies and the facts bridge go

notice: runs as compiled Bend (ffi_notice, spec-speller entry laws); the Rust copy, its bridge and the law-covered tests go

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

approvals: nothing asks but a secret, like omp (default shell.autoEffects = read, write, exec, net, outside, protected; secret never grantable)

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

durable: the retry note's text and a staged document's content and publication run as compiled Bend (new entries retry_note id 263, doc_plan id 264)

laws: close the adversaries' gaps in revive, timeouts and auth_flight (the entries' freshness and values are the models', the refresh model's every step pinned)

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

runners: the ipython gate and the registry decided by the compiled core (new runners entry id 52)

laws: frames_verdict_serve_exact (a verdict serves its frame exactly when it is Serve; a fresh blind adversary's Verdict.serve of Duplicate and Kindless passed frames_admit_serves_accepted)

laws: scan_ffi_malformed_exact, scan_ffi_read_example, submission_ffi_malformed_exact, submission_ffi_read_example

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

selection: a copied line drops its trailing blanks wherever its soft wrap falls

semver: the entry reads only lengths and counts that fit the wire (semver_ffi_exact_fits), the gap a blind adversary found in the log entry

shell: the approval gate of a step decided by the compiled core (new shell entry id 50)

skill_load: the loaded list is pinned (skill_loaded_exact) and the membership the reporting law reads has witnesses (skill_in_first_example, skill_in_later_example): a blind adversary's empty membership made skill_failure_reported vacuous

slash commands: the suggestion for a mistyped name runs as the compiled core (entry 204 slash_suggest)

staging: runs as compiled Bend (ffi_staging, spec-speller entry laws); the Rust copy, its bridge and the law-covered tests go

laws: scan_ffi_malformed_exact, scan_ffi_read_example, submission_ffi_malformed_exact, submission_ffi_read_example

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

laws: close the adversaries' gaps in revive, timeouts and auth_flight (the entries' freshness and values are the models', the refresh model's every step pinned)

tiny: each choice of a process's worker election runs as the compiled core (new entry tiny_elect id 100)

laws: tokens_type_in_range (a fresh gap search passed type sizes past the largest font size a browser renders)

tools: the schema the harness sends and what dyn reaches decided by the compiled core (new tool_surface entry id 51)

approvals: nothing asks but a secret, like omp (default shell.autoEffects = read, write, exec, net, outside, protected; secret never grantable)

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

laws: a Nat on the wire is its decimal digits (every entry); the command reply readers read the spelled reply grammar; every command answer but the malformed error comes from an input that begins with a request

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/