proof/dash_access · eukhe · Tangled

Coding agent with a memory of all things

eukhe proof dash_access

35 files

at bend/stackfix

gildrb.com · proof: the wire lemmas that dash_access and gateway_answer borrowed from doc_commit move to proof/base · 2w ago

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

dash_access_entry_answers.bend

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

dash_access_entry_exact.bend

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

dash_access_entry_example.bend

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

dash_access_entry_reads.bend

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

dash_access_entry_refuses.bend

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

dash_access_host_01_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_02_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_03_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_04_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_05_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_06_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_07_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_08_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_09_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_10_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_11_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_12_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_13_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_14_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_15_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_16_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_17_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_18_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_19_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_20_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_21_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_22_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_23_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_24_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_25_example.bend

laws: dash_access_host_example split into one law per case, so the kernel checks each alone (approved by the integrator; same cases, nothing weakened)

dash_access_host_long_port.bend

laws: universal laws for long ports and capped waits, so --verdict runs to the end

dash_access_host_spec.bend

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

dash_access_origin_example.bend

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

dash_access_origin_spec.bend

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