~/bend-docscommunity

src/LAWS.bend open laws/TODOs

raw source on the hub · import 0x958db28bf0cef817bff69fac7beb9846/src/LAWS.bend as LAWS

2 imports
import Base
import ./http.bend as Http

Laws

law timeout_is_explicit provedin src/PROOF.bendsource · line 4 · raw

@+ms:U32 -> @+request:0x958db28bf0cef817bff69fac7beb9846/src/http.Request -> {0x958db28bf0cef817bff69fac7beb9846/src/http.timeout(0x958db28bf0cef817bff69fac7beb9846/src/http.with_timeout(ms, request)) == ms : U32}

law body_limit_is_explicit provedin src/PROOF.bendsource · line 9 · raw

@+bytes:U32 -> @+request:0x958db28bf0cef817bff69fac7beb9846/src/http.Request -> {0x958db28bf0cef817bff69fac7beb9846/src/http.body_limit(0x958db28bf0cef817bff69fac7beb9846/src/http.with_max_bytes(bytes, request)) == bytes : U32}

law setting_timeout_preserves_body_limit provedin src/PROOF.bendsource · line 14 · raw

@+ms:U32 -> @+request:0x958db28bf0cef817bff69fac7beb9846/src/http.Request -> {0x958db28bf0cef817bff69fac7beb9846/src/http.body_limit(0x958db28bf0cef817bff69fac7beb9846/src/http.with_timeout(ms, request)) == 0x958db28bf0cef817bff69fac7beb9846/src/http.body_limit(request) : U32}

law setting_header_preserves_timeout provedin src/PROOF.bendsource · line 19 · raw

@+name:String -> @+value:String -> @+request:0x958db28bf0cef817bff69fac7beb9846/src/http.Request -> {0x958db28bf0cef817bff69fac7beb9846/src/http.timeout(0x958db28bf0cef817bff69fac7beb9846/src/http.with_header(name, value, request)) == 0x958db28bf0cef817bff69fac7beb9846/src/http.timeout(request) : U32}

law setting_header_preserves_body_limit provedin src/PROOF.bendsource · line 25 · raw

@+name:String -> @+value:String -> @+request:0x958db28bf0cef817bff69fac7beb9846/src/http.Request -> {0x958db28bf0cef817bff69fac7beb9846/src/http.body_limit(0x958db28bf0cef817bff69fac7beb9846/src/http.with_header(name, value, request)) == 0x958db28bf0cef817bff69fac7beb9846/src/http.body_limit(request) : U32}