proof · eukhe · Tangled

Coding agent with a memory of all things

eukhe proof

119 folders

gildrb.com · finish: the agent no longer stops while work remains · 1w ago

Remove docs/, strip stale docs references, minimize README

Merge origin/main into bend/spec

rlm, harness: context as data and rlm.query (prime-agent RLM); speculation then effect, argument repair, call lifting, 3-way rebase and provider quirks as proven Bend (omp²)

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

bridges: gone; auth reads and cron file and status writes run as proven entries

autoresearch: the snapshot's best is the current segment's; 15-digit metrics run in the core

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 origin/main into bend/spec

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)

rlm, harness: context as data and rlm.query (prime-agent RLM); speculation then effect, argument repair, call lifting, 3-way rebase and provider quirks as proven Bend (omp²)

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)

spec: one folder per pillar (durable, memory, settings, theme); the OptChat law vocabulary moves from bend/spec.bend to spec/memory/optchat.bend; the Lean twins of log and optchat go (their Bend specs are proven, and --verdict checks them with a Lean-proven kernel)

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

spec: one folder per pillar (durable, memory, settings, theme); the OptChat law vocabulary moves from bend/spec.bend to spec/memory/optchat.bend; the Lean twins of log and optchat go (their Bend specs are proven, and --verdict checks them with a Lean-proven kernel)

bridges: gone; auth reads and cron file and status writes run as proven entries

bridges: gone; auth reads and cron file and status writes run as proven entries

bridges: gone; auth reads and cron file and status writes run as proven entries

bridges: gone; auth reads and cron file and status writes run as proven entries

bridges: gone; auth reads and cron file and status writes run as proven entries

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)

Remove docs/, strip stale docs references, minimize README

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)

rlm, harness: context as data and rlm.query (prime-agent RLM); speculation then effect, argument repair, call lifting, 3-way rebase and provider quirks as proven Bend (omp²)

spec: formalize the durable task life, subagent admission and autoresearch as proven Bend entries

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

Merge origin/main into bend/spec

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)

finish: the agent no longer stops while work remains

headless_settle

finish: the agent no longer stops while work remains

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

spec: one folder per pillar (durable, memory, settings, theme); the OptChat law vocabulary moves from bend/spec.bend to spec/memory/optchat.bend; the Lean twins of log and optchat go (their Bend specs are proven, and --verdict checks them with a Lean-proven kernel)

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

rlm, harness: context as data and rlm.query (prime-agent RLM); speculation then effect, argument repair, call lifting, 3-way rebase and provider quirks as proven Bend (omp²)

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

spec: one folder per pillar (durable, memory, settings, theme); the OptChat law vocabulary moves from bend/spec.bend to spec/memory/optchat.bend; the Lean twins of log and optchat go (their Bend specs are proven, and --verdict checks them with a Lean-proven kernel)

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)

gate: secrets never ask again

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

rlm, harness: context as data and rlm.query (prime-agent RLM); speculation then effect, argument repair, call lifting, 3-way rebase and provider quirks as proven Bend (omp²)

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)

rlm, harness: context as data and rlm.query (prime-agent RLM); speculation then effect, argument repair, call lifting, 3-way rebase and provider quirks as proven Bend (omp²)

finish: the agent no longer stops while work remains

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

Merge origin/main into bend/spec

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

finish: the agent no longer stops while work remains

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/

spec: formalize the durable task life, subagent admission and autoresearch as proven Bend entries

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

spec: one folder per pillar (durable, memory, settings, theme); the OptChat law vocabulary moves from bend/spec.bend to spec/memory/optchat.bend; the Lean twins of log and optchat go (their Bend specs are proven, and --verdict checks them with a Lean-proven kernel)

spec: one folder per pillar (durable, memory, settings, theme); the OptChat law vocabulary moves from bend/spec.bend to spec/memory/optchat.bend; the Lean twins of log and optchat go (their Bend specs are proven, and --verdict checks them with a Lean-proven kernel)

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)

Merge origin/main into bend/spec

Merge origin/main into bend/spec

rlm, harness: context as data and rlm.query (prime-agent RLM); speculation then effect, argument repair, call lifting, 3-way rebase and provider quirks as proven Bend (omp²)

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

gate: secrets never ask again

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

finish: the agent no longer stops while work remains

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/