~/bend-docscommunity

src/ROUTING_PROOF.bend checks

raw source on the hub · import 0x600981079d65a285d008308db02b846c/src/ROUTING_PROOF.bend as ROUTING_PROOF

3 imports
import Base
import ./contracts.bend as C
import ./routing_spec.bend as S

Laws

law nonempty_matches provedsource · line 31 · raw

@+name:String -> @+value:String -> {Bool.and(Bool.not(String.is_empty(name)), Bool.not(String.is_empty(value))) == 0x600981079d65a285d008308db02b846c/src/routing_spec.nonempty(name, value) : Bool}

law literal_matches provedsource · line 42 · raw

@+same:Bool -> @+rest:0x600981079d65a285d008308db02b846c/src/contracts.Match -> {0x600981079d65a285d008308db02b846c/src/contracts.literal(same, u => rest) == 0x600981079d65a285d008308db02b846c/src/routing_spec.combine(0x600981079d65a285d008308db02b846c/src/routing_spec.exact(same), rest) : 0x600981079d65a285d008308db02b846c/src/contracts.Match}

law parameter_matches provedsource · line 54 · raw

@+ok:Bool -> @+name:String -> @+value:String -> @+rest:0x600981079d65a285d008308db02b846c/src/contracts.Match -> {0x600981079d65a285d008308db02b846c/src/contracts.literal(ok, u => 0x600981079d65a285d008308db02b846c/src/contracts.prepend(name, value, rest)) == 0x600981079d65a285d008308db02b846c/src/routing_spec.combine(0x600981079d65a285d008308db02b846c/src/routing_spec.parameter(ok, name, value), rest) : 0x600981079d65a285d008308db02b846c/src/contracts.Match}

law capture_matches provedsource · line 67 · raw

@+parameter:Bool -> @+head:Char -> @+name:String -> @+value:String -> @+rest:0x600981079d65a285d008308db02b846c/src/contracts.Match -> {0x600981079d65a285d008308db02b846c/src/contracts.capture(parameter, SCon{head, name}, name, value, u => rest) == 0x600981079d65a285d008308db02b846c/src/routing_spec.combine(0x600981079d65a285d008308db02b846c/src/routing_spec.part_kind(parameter, head, name, value), rest) : 0x600981079d65a285d008308db02b846c/src/contracts.Match}

law segment_matches provedsource · line 83 · raw

@+pattern:String -> @+value:String -> @+rest:0x600981079d65a285d008308db02b846c/src/contracts.Match -> {0x600981079d65a285d008308db02b846c/src/contracts.segment(pattern, value, u => rest) == 0x600981079d65a285d008308db02b846c/src/routing_spec.combine(0x600981079d65a285d008308db02b846c/src/routing_spec.part(pattern, value), rest) : 0x600981079d65a285d008308db02b846c/src/contracts.Match}

law values_match_spec provedsource · line 93 · raw

@+patterns:List<&2, String> -> @+path:List<&2, String> -> {0x600981079d65a285d008308db02b846c/src/contracts.values(patterns, path) == 0x600981079d65a285d008308db02b846c/src/routing_spec.segments(patterns, path) : 0x600981079d65a285d008308db02b846c/src/contracts.Match}

law match_path_matches_spec provedsource · line 107 · raw

@+pattern:String -> @+path:String -> {0x600981079d65a285d008308db02b846c/src/contracts.match_path(pattern, path) == 0x600981079d65a285d008308db02b846c/src/routing_spec.path(pattern, path) : 0x600981079d65a285d008308db02b846c/src/contracts.Match}

law membership_matches provedsource · line 114 · raw

@+verb:String -> @+methods:List<&2, String> -> {0x600981079d65a285d008308db02b846c/src/contracts.has_method(verb, methods) == 0x600981079d65a285d008308db02b846c/src/routing_spec.member(verb, methods) : Bool}

law unique_matches provedsource · line 124 · raw

@+duplicate:Bool -> @+verb:String -> @+methods:List<&2, String> -> {0x600981079d65a285d008308db02b846c/src/contracts.unique(duplicate, verb, methods) == 0x600981079d65a285d008308db02b846c/src/routing_spec.retain(duplicate, verb, methods) : List<&2, String>}

law allowed_matches provedsource · line 134 · raw

@+verb:String -> @+suffix:0x600981079d65a285d008308db02b846c/src/contracts.Selection -> {0x600981079d65a285d008308db02b846c/src/contracts.add_allowed(verb, suffix) == fallback(verb, suffix) : 0x600981079d65a285d008308db02b846c/src/contracts.Selection}

law chosen_matches provedsource · line 147 · raw

@+same:Bool -> @+route:0x600981079d65a285d008308db02b846c/src/contracts.Route -> @+params:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Param> -> @+suffix:0x600981079d65a285d008308db02b846c/src/contracts.Selection -> {0x600981079d65a285d008308db02b846c/src/contracts.chosen(same, route, params, suffix) == choose(same, route, params, suffix) : 0x600981079d65a285d008308db02b846c/src/contracts.Selection}

law selection_step provedsource · line 160 · raw

@+result:0x600981079d65a285d008308db02b846c/src/contracts.Match -> @+id:Nat -> @+verb:String -> @+pattern:String -> @+protected:Bool -> @+statuses:List<&2, Nat> -> @+method:String -> @+tail:List<&2, 0x600981079d65a285d008308db02b846c/src/routing_spec.Hit> -> {0x600981079d65a285d008308db02b846c/src/contracts.matched(result, String.eq(verb, method), 0x600981079d65a285d008308db02b846c/src/contracts.Route{id, verb, pattern, protected, statuses}, resolve(tail, method)) == resolve(0x600981079d65a285d008308db02b846c/src/routing_spec.include(result, 0x600981079d65a285d008308db02b846c/src/contracts.Route{id, verb, pattern, protected, statuses}, tail), method) : 0x600981079d65a285d008308db02b846c/src/contracts.Selection}

law select_matches_fold provedsource · line 177 · raw

@+routes:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Route> -> @+method:String -> @+path:String -> {0x600981079d65a285d008308db02b846c/src/contracts.select(routes, method, path) == fold_select(routes, method, path) : 0x600981079d65a285d008308db02b846c/src/contracts.Selection}

law fallback_nonempty provedsource · line 194 · raw

@+duplicate:Bool -> @+verb:String -> @+m:String -> @+ms:List<&2, String> -> {0x600981079d65a285d008308db02b846c/src/contracts.WrongMethod{0x600981079d65a285d008308db02b846c/src/routing_spec.retain(duplicate, verb, m <> ms)} == 0x600981079d65a285d008308db02b846c/src/routing_spec.summary(0x600981079d65a285d008308db02b846c/src/routing_spec.Absent{}, 0x600981079d65a285d008308db02b846c/src/routing_spec.retain(duplicate, verb, m <> ms)) : 0x600981079d65a285d008308db02b846c/src/contracts.Selection}

law fallback_summary provedsource · line 205 · raw

@+verb:String -> @+first:0x600981079d65a285d008308db02b846c/src/routing_spec.First -> @+methods:List<&2, String> -> {fallback(verb, 0x600981079d65a285d008308db02b846c/src/routing_spec.summary(first, methods)) == 0x600981079d65a285d008308db02b846c/src/routing_spec.summary(first, 0x600981079d65a285d008308db02b846c/src/routing_spec.dedup_head(verb, methods)) : 0x600981079d65a285d008308db02b846c/src/contracts.Selection}

law choose_summary provedsource · line 219 · raw

@+same:Bool -> @+route:0x600981079d65a285d008308db02b846c/src/contracts.Route -> @+params:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Param> -> @+first:0x600981079d65a285d008308db02b846c/src/routing_spec.First -> @+methods:List<&2, String> -> {choose(same, route, params, 0x600981079d65a285d008308db02b846c/src/routing_spec.summary(first, methods)) == 0x600981079d65a285d008308db02b846c/src/routing_spec.summary(0x600981079d65a285d008308db02b846c/src/routing_spec.first_step(same, 0x600981079d65a285d008308db02b846c/src/routing_spec.Hit{route, params}, first), 0x600981079d65a285d008308db02b846c/src/routing_spec.dedup_head(0x600981079d65a285d008308db02b846c/src/routing_spec.verb(route), methods)) : 0x600981079d65a285d008308db02b846c/src/contracts.Selection}

law resolve_matches_summary provedsource · line 234 · raw

@+hits:List<&2, 0x600981079d65a285d008308db02b846c/src/routing_spec.Hit> -> @+method:String -> {resolve(hits, method) == 0x600981079d65a285d008308db02b846c/src/routing_spec.summary(0x600981079d65a285d008308db02b846c/src/routing_spec.first(hits, method), 0x600981079d65a285d008308db02b846c/src/routing_spec.allowed(hits)) : 0x600981079d65a285d008308db02b846c/src/contracts.Selection}

law select_matches_spec provedsource · line 248 · raw

@+routes:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Route> -> @+method:String -> @+path:String -> {0x600981079d65a285d008308db02b846c/src/contracts.select(routes, method, path) == 0x600981079d65a285d008308db02b846c/src/routing_spec.select(routes, method, path) : 0x600981079d65a285d008308db02b846c/src/contracts.Selection}

law selected_first provedsource · line 257 · raw

@+routes:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Route> -> @+method:String -> @+path:String -> @+route:0x600981079d65a285d008308db02b846c/src/contracts.Route -> @+params:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Param> -> @first:{0x600981079d65a285d008308db02b846c/src/routing_spec.first(0x600981079d65a285d008308db02b846c/src/routing_spec.hits(routes, path), method) == 0x600981079d65a285d008308db02b846c/src/routing_spec.Present{0x600981079d65a285d008308db02b846c/src/routing_spec.Hit{route, params}} : 0x600981079d65a285d008308db02b846c/src/routing_spec.First} -> {0x600981079d65a285d008308db02b846c/src/contracts.select(routes, method, path) == 0x600981079d65a285d008308db02b846c/src/contracts.Found{route, params} : 0x600981079d65a285d008308db02b846c/src/contracts.Selection}

law missing_no_hits provedsource · line 272 · raw

@+routes:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Route> -> @+method:String -> @+path:String -> @unknown:{0x600981079d65a285d008308db02b846c/src/routing_spec.hits(routes, path) == [] : List<&2, 0x600981079d65a285d008308db02b846c/src/routing_spec.Hit>} -> {0x600981079d65a285d008308db02b846c/src/contracts.select(routes, method, path) == 0x600981079d65a285d008308db02b846c/src/contracts.Missing{} : 0x600981079d65a285d008308db02b846c/src/contracts.Selection}

law known_methods provedsource · line 283 · raw

@+verb:String -> @+methods:List<&2, String> -> {0x600981079d65a285d008308db02b846c/src/routing_spec.summary(0x600981079d65a285d008308db02b846c/src/routing_spec.Absent{}, 0x600981079d65a285d008308db02b846c/src/routing_spec.dedup_head(verb, methods)) == 0x600981079d65a285d008308db02b846c/src/contracts.WrongMethod{0x600981079d65a285d008308db02b846c/src/routing_spec.dedup_head(verb, methods)} : 0x600981079d65a285d008308db02b846c/src/contracts.Selection}

law known_summary provedsource · line 293 · raw

@+route:0x600981079d65a285d008308db02b846c/src/contracts.Route -> @+params:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Param> -> @+tail:List<&2, 0x600981079d65a285d008308db02b846c/src/routing_spec.Hit> -> {0x600981079d65a285d008308db02b846c/src/routing_spec.summary(0x600981079d65a285d008308db02b846c/src/routing_spec.Absent{}, 0x600981079d65a285d008308db02b846c/src/routing_spec.allowed(0x600981079d65a285d008308db02b846c/src/routing_spec.Hit{route, params} <> tail)) == 0x600981079d65a285d008308db02b846c/src/contracts.WrongMethod{0x600981079d65a285d008308db02b846c/src/routing_spec.allowed(0x600981079d65a285d008308db02b846c/src/routing_spec.Hit{route, params} <> tail)} : 0x600981079d65a285d008308db02b846c/src/contracts.Selection}

law wrong_method_exact_allow provedsource · line 304 · raw

@+routes:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Route> -> @+method:String -> @+path:String -> @+route:0x600981079d65a285d008308db02b846c/src/contracts.Route -> @+params:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Param> -> @+tail:List<&2, 0x600981079d65a285d008308db02b846c/src/routing_spec.Hit> -> @known:{0x600981079d65a285d008308db02b846c/src/routing_spec.hits(routes, path) == 0x600981079d65a285d008308db02b846c/src/routing_spec.Hit{route, params} <> tail : List<&2, 0x600981079d65a285d008308db02b846c/src/routing_spec.Hit>} -> @wrong:{0x600981079d65a285d008308db02b846c/src/routing_spec.first(0x600981079d65a285d008308db02b846c/src/routing_spec.Hit{route, params} <> tail, method) == 0x600981079d65a285d008308db02b846c/src/routing_spec.Absent{} : 0x600981079d65a285d008308db02b846c/src/routing_spec.First} -> {0x600981079d65a285d008308db02b846c/src/contracts.select(routes, method, path) == 0x600981079d65a285d008308db02b846c/src/contracts.WrongMethod{0x600981079d65a285d008308db02b846c/src/routing_spec.allowed(0x600981079d65a285d008308db02b846c/src/routing_spec.Hit{route, params} <> tail)} : 0x600981079d65a285d008308db02b846c/src/contracts.Selection}

law dispatch_unknown provedsource · line 323 · raw

@-State:Data -> @-Body:Data -> @+routes:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Route> -> @+method:String -> @+path:String -> @valid:Bool -> @+state:State -> @next:(@_:0x600981079d65a285d008308db02b846c/src/contracts.Route -> @_:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Param> -> @_:State -> 0x600981079d65a285d008308db02b846c/src/contracts.Decision<State, Body>) -> @unknown:{0x600981079d65a285d008308db02b846c/src/routing_spec.hits(routes, path) == [] : List<&2, 0x600981079d65a285d008308db02b846c/src/routing_spec.Hit>} -> {0x600981079d65a285d008308db02b846c/src/contracts.dispatch(State, Body, routes, method, path, valid, state, next) == 0x600981079d65a285d008308db02b846c/src/contracts.Decision{state, 0x600981079d65a285d008308db02b846c/src/contracts.Error{404n, "not_found", []}} : 0x600981079d65a285d008308db02b846c/src/contracts.Decision<State, Body>}

law dispatch_wrong_method provedsource · line 340 · raw

@-State:Data -> @-Body:Data -> @+routes:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Route> -> @+method:String -> @+path:String -> @+route:0x600981079d65a285d008308db02b846c/src/contracts.Route -> @+params:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Param> -> @+tail:List<&2, 0x600981079d65a285d008308db02b846c/src/routing_spec.Hit> -> @valid:Bool -> @+state:State -> @next:(@_:0x600981079d65a285d008308db02b846c/src/contracts.Route -> @_:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Param> -> @_:State -> 0x600981079d65a285d008308db02b846c/src/contracts.Decision<State, Body>) -> @known:{0x600981079d65a285d008308db02b846c/src/routing_spec.hits(routes, path) == 0x600981079d65a285d008308db02b846c/src/routing_spec.Hit{route, params} <> tail : List<&2, 0x600981079d65a285d008308db02b846c/src/routing_spec.Hit>} -> @wrong:{0x600981079d65a285d008308db02b846c/src/routing_spec.first(0x600981079d65a285d008308db02b846c/src/routing_spec.Hit{route, params} <> tail, method) == 0x600981079d65a285d008308db02b846c/src/routing_spec.Absent{} : 0x600981079d65a285d008308db02b846c/src/routing_spec.First} -> {0x600981079d65a285d008308db02b846c/src/contracts.dispatch(State, Body, routes, method, path, valid, state, next) == 0x600981079d65a285d008308db02b846c/src/contracts.Decision{state, 0x600981079d65a285d008308db02b846c/src/contracts.Error{405n, "method_not_allowed", 0x600981079d65a285d008308db02b846c/src/routing_spec.allowed(0x600981079d65a285d008308db02b846c/src/routing_spec.Hit{route, params} <> tail)}} : 0x600981079d65a285d008308db02b846c/src/contracts.Decision<State, Body>}

law dispatch_protected provedsource · line 361 · raw

@-State:Data -> @-Body:Data -> @+routes:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Route> -> @+method:String -> @+path:String -> @+id:Nat -> @+verb:String -> @+pattern:String -> @+statuses:List<&2, Nat> -> @+params:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Param> -> @+state:State -> @next:(@_:0x600981079d65a285d008308db02b846c/src/contracts.Route -> @_:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Param> -> @_:State -> 0x600981079d65a285d008308db02b846c/src/contracts.Decision<State, Body>) -> @first:{0x600981079d65a285d008308db02b846c/src/routing_spec.first(0x600981079d65a285d008308db02b846c/src/routing_spec.hits(routes, path), method) == 0x600981079d65a285d008308db02b846c/src/routing_spec.Present{0x600981079d65a285d008308db02b846c/src/routing_spec.Hit{0x600981079d65a285d008308db02b846c/src/contracts.Route{id, verb, pattern, True{}, statuses}, params}} : 0x600981079d65a285d008308db02b846c/src/routing_spec.First} -> {0x600981079d65a285d008308db02b846c/src/contracts.dispatch(State, Body, routes, method, path, False{}, state, next) == 0x600981079d65a285d008308db02b846c/src/contracts.Decision{state, 0x600981079d65a285d008308db02b846c/src/contracts.Error{401n, "unauthorized", []}} : 0x600981079d65a285d008308db02b846c/src/contracts.Decision<State, Body>}

law fallback_never_missing provedsource · line 382 · raw

@+verb:String -> @suffix:0x600981079d65a285d008308db02b846c/src/contracts.Selection -> {0x600981079d65a285d008308db02b846c/src/routing_spec.missing(fallback(verb, suffix)) == False{} : Bool}

law choose_never_missing provedsource · line 392 · raw

@same:Bool -> @+route:0x600981079d65a285d008308db02b846c/src/contracts.Route -> @params:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Param> -> @suffix:0x600981079d65a285d008308db02b846c/src/contracts.Selection -> {0x600981079d65a285d008308db02b846c/src/routing_spec.missing(choose(same, route, params, suffix)) == False{} : Bool}

law resolve_missing_iff provedsource · line 405 · raw

@+hits:List<&2, 0x600981079d65a285d008308db02b846c/src/routing_spec.Hit> -> @+method:String -> {0x600981079d65a285d008308db02b846c/src/routing_spec.missing(resolve(hits, method)) == 0x600981079d65a285d008308db02b846c/src/routing_spec.empty(hits) : Bool}

law missing_iff_no_path provedsource · line 417 · raw

@+routes:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Route> -> @+method:String -> @+path:String -> {0x600981079d65a285d008308db02b846c/src/routing_spec.missing(0x600981079d65a285d008308db02b846c/src/contracts.select(routes, method, path)) == 0x600981079d65a285d008308db02b846c/src/routing_spec.empty(0x600981079d65a285d008308db02b846c/src/routing_spec.hits(routes, path)) : Bool}

law fallback_wrong_summary provedsource · line 427 · raw

@+verb:String -> @+first:0x600981079d65a285d008308db02b846c/src/routing_spec.First -> @methods:List<&2, String> -> {0x600981079d65a285d008308db02b846c/src/routing_spec.wrong(fallback(verb, 0x600981079d65a285d008308db02b846c/src/routing_spec.summary(first, methods))) == 0x600981079d65a285d008308db02b846c/src/routing_spec.absent(first) : Bool}

law choose_wrong_summary provedsource · line 440 · raw

@same:Bool -> @+route:0x600981079d65a285d008308db02b846c/src/contracts.Route -> @+params:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Param> -> @+first:0x600981079d65a285d008308db02b846c/src/routing_spec.First -> @methods:List<&2, String> -> {0x600981079d65a285d008308db02b846c/src/routing_spec.wrong(choose(same, route, params, 0x600981079d65a285d008308db02b846c/src/routing_spec.summary(first, methods))) == 0x600981079d65a285d008308db02b846c/src/routing_spec.absent(0x600981079d65a285d008308db02b846c/src/routing_spec.first_step(same, 0x600981079d65a285d008308db02b846c/src/routing_spec.Hit{route, params}, first)) : Bool}

law resolve_wrong_iff provedsource · line 454 · raw

@+hits:List<&2, 0x600981079d65a285d008308db02b846c/src/routing_spec.Hit> -> @+method:String -> {0x600981079d65a285d008308db02b846c/src/routing_spec.wrong(resolve(hits, method)) == Bool.and(Bool.not(0x600981079d65a285d008308db02b846c/src/routing_spec.empty(hits)), 0x600981079d65a285d008308db02b846c/src/routing_spec.absent(0x600981079d65a285d008308db02b846c/src/routing_spec.first(hits, method))) : Bool}

law wrong_method_iff provedsource · line 468 · raw

@+routes:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Route> -> @+method:String -> @+path:String -> {0x600981079d65a285d008308db02b846c/src/routing_spec.wrong(0x600981079d65a285d008308db02b846c/src/contracts.select(routes, method, path)) == Bool.and(Bool.not(0x600981079d65a285d008308db02b846c/src/routing_spec.empty(0x600981079d65a285d008308db02b846c/src/routing_spec.hits(routes, path))), 0x600981079d65a285d008308db02b846c/src/routing_spec.absent(0x600981079d65a285d008308db02b846c/src/routing_spec.first(0x600981079d65a285d008308db02b846c/src/routing_spec.hits(routes, path), method))) : Bool}

Definitions

def fallback source · line 6 · raw

@+verb:String -> @suffix:0x600981079d65a285d008308db02b846c/src/contracts.Selection -> 0x600981079d65a285d008308db02b846c/src/contracts.Selection

Induction helpers; these are not the independent specification.

def choose source · line 13 · raw

@same:Bool -> @+route:0x600981079d65a285d008308db02b846c/src/contracts.Route -> @params:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Param> -> @suffix:0x600981079d65a285d008308db02b846c/src/contracts.Selection -> 0x600981079d65a285d008308db02b846c/src/contracts.Selection

The head wins on exact method equality; otherwise inspect the suffix.

def resolve source · line 20 · raw

@hits:List<&2, 0x600981079d65a285d008308db02b846c/src/routing_spec.Hit> -> @+method:String -> 0x600981079d65a285d008308db02b846c/src/contracts.Selection

def fold_select source · line 28 · raw

@routes:List<&2, 0x600981079d65a285d008308db02b846c/src/contracts.Route> -> @method:String -> @value:String -> 0x600981079d65a285d008308db02b846c/src/contracts.Selection