proof · eukhe · Tangled

Coding agent with a memory of all things

eukhe proof

105 folders

gildrb.com · chat memory: no root-turn lease; many windows turn at once (the user: never restrict multiple open threads) · 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 desk is a compiled Bend stepper (entry 53: call + stepper); shell_approval is its event loop and the approvals bridge goes

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/

chat memory: no root-turn lease; many windows turn at once (the user: never restrict multiple open threads)

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

ai: the cache-mark budget of a provider request runs as the compiled core (entry 230 cache_marks)

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)

laws: tui resolves pinned; color dist/to256 specs claimed only where exact (channels at most 255)

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

laws: config pins the setter over an unreadable file (save_exact) and every model helper the config laws read

laws: goal_entry_example and cron_entry_example with numbers the proven kernel unfolds (bend PROOF.bend --verdict ran out of fuel on them)

cron: each job's claim, recovery, finish (backoff and stop), cancel and resume decided by the compiled core (new entry cron id 82); the bridge keeps only the processes' interleaving on the jobs file

laws: cron_terms_exact (a third fresh adversary's `has` always False made cron_finish_refines vacuous and every cron law checked)

cvar: a settings document reads each cvar once, by its first declaration (cvar_document_exact corrected); the model's own terms pinned (cvar_terms_exact)

cvar: resolution decided by the compiled core (new cvar_layers entry id 64); the Rust copy, its bridge and the law-covered tests go

dash: each dashboard socket's pairing gate is a compiled Bend stepper (entry 101: call + stepper); http.rs and bridge.rs are its event loop and the pairing bridge goes

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

dash: each dashboard socket's pairing gate is a compiled Bend stepper (entry 101: call + stepper); http.rs and bridge.rs are its event loop and the pairing bridge goes

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/

bend: explicit error-text rules replace the eukhe-ai error regexes (entry 381 err_text)

ai: what a provider's HTTP error shows runs as the compiled core (entry 233 error_body)

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

bend: explicit error-text rules replace the eukhe-ai error regexes (entry 381 err_text)

goals: the goal prompts, usage line, tokens left and completion report run as the compiled core (entry 292 goal_text)

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

stream: a tool call's journal runs as a stepper of the compiled core; the stream bridge is gone

laws: job_model_terms_exact (the model terms the S2 job laws read, pinned; a fifth fresh adversary noted them loose)

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

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

mcp: the catalog's literal-host check runs as the compiled core (entry 290 mcp_url)

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

optchat: the chat-memory planner runs as a stepper of the compiled core; the planner's Rust copy and the optchat bridge are gone

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: overflow's message example fits the --verdict kernel's fuel

packages: package sources are parsed, checked and worded by the compiled core (entry 294 package_source)

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

bend: explicit error-text rules replace the eukhe-ai error regexes (entry 381 err_text)

progress: the work ledger and the goal check's prior decided by the compiled core (new work entry id 83, a Stepper and a call)

chat memory: no root-turn lease; many windows turn at once (the user: never restrict multiple open threads)

laws: the model's verdicts are pinned (quirks_verdicts_exact, quirks_fine_all_exact): a fresh adversary's verdicts.go that searched clashes from the rule itself passed every law with an entry that did not call it

auth: the pasted login redirect is cleaned, parsed, checked and worded by the compiled core (entry 293 redirect_input)

refinement: the /refine planner's decisions run as the compiled core (entry 295 refine_plan)

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: retry_terms_exact (a third fresh adversary's policy accessor read a failover budget of 0 as 1 and every retry law checked)

retry: the stream-idle deadline runs as a stepper of the compiled core; the retry bridge is gone

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: /goal and /autonomous arguments, goal objectives and command words run as the compiled core (entry 291 slash_args)

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

ai: the cause and message of a failed provider stream run as the compiled core (entry 232 stream_failure)

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/

ai: whether a reply is a context overflow runs as the compiled core (entry 231 overflow), on a proven text-pattern search (text_pat)

laws: theme and color helpers pinned to specs (a fresh adversary's prefix name, ignored background, constant mode, vacuous legibility, loose hex digits)

laws, color, theme: exact contrast past 2^32, load/valid/complete/rename pinned, at most 4096 theme files a load

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)

laws: tiny_worker_terms_exact (a fresh specification-completeness review proved every tiny law with a worker model that never starts a worker, `needs` and `last_tag` redefined to match)

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

stream: a tool call's journal runs as a stepper of the compiled core; the stream bridge is gone

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/

Merge branch 'bend/all-settings-theme' into bend/all-settings

wait: the race runs its wait as a stepper of the compiled core; the wait bridge is gone

wire: pin every numeric writer and reader to an independent decimal spec

progress: the work ledger and the goal check's prior decided by the compiled core (new work entry id 83, a Stepper and a call)

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/