~/bend-docscommunity

src/CONTRACTS_PROOF.bend checks

raw source on the hub · import 0x36c893ade1f158581b4c8c34eb3b510e/src/CONTRACTS_PROOF.bend as CONTRACTS_PROOF

3 imports
import Base
import ./contracts.bend as C
import ./ROUTING_PROOF.bend as Routing

Laws

law protected_denies provedsource · line 5 · raw

@-S:Data -> @-B:Data -> @+state:S -> @next:(@_:S -> 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Decision<S, B>) -> {0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.authorize(S, B, True{}, False{}, state, next) == 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Decision{state, 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Error{401n, "unauthorized", []}} : 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Decision<S, B>}

law read_preserves provedsource · line 15 · raw

@-S:Data -> @-B:Data -> @+state:S -> @proposed:0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Decision<S, B> -> {0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.state(S, B, 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.preserve(S, B, True{}, state, proposed)) == state : S}

law dispatch_read_preserves provedsource · line 25 · raw

@-S:Data -> @-B:Data -> @selection:0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Selection -> @valid:Bool -> @+state:S -> @next:(@_:0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Route -> @_:List<&2, 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Param> -> @_:S -> 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Decision<S, B>) -> {0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.state(S, B, 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.run(S, B, selection, True{}, valid, state, next)) == state : S}

law get_is_read provedsource · line 46 · raw

{0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.readonly("GET") == True{} : Bool}

law head_is_read provedsource · line 51 · raw

{0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.readonly("HEAD") == True{} : Bool}

law unknown_is_404 provedsource · line 56 · raw

@-S:Data -> @-B:Data -> @read:Bool -> @valid:Bool -> @+state:S -> @next:(@_:0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Route -> @_:List<&2, 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Param> -> @_:S -> 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Decision<S, B>) -> {0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.run(S, B, 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Missing{}, read, valid, state, next) == 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Decision{state, 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Error{404n, "not_found", []}} : 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Decision<S, B>}

law wrong_method_is_405 provedsource · line 68 · raw

@-S:Data -> @-B:Data -> @+methods:List<&2, String> -> @read:Bool -> @valid:Bool -> @+state:S -> @next:(@_:0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Route -> @_:List<&2, 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Param> -> @_:S -> 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Decision<S, B>) -> {0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.run(S, B, 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.WrongMethod{methods}, read, valid, state, next) == 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Decision{state, 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Error{405n, "method_not_allowed", methods}} : 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Decision<S, B>}

law protected_route_denies provedsource · line 81 · raw

@-S:Data -> @-B:Data -> @id:Nat -> @method:String -> @pattern:String -> @statuses:List<&2, Nat> -> @params:List<&2, 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Param> -> @read:Bool -> @+state:S -> @next:(@_:0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Route -> @_:List<&2, 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Param> -> @_:S -> 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Decision<S, B>) -> {0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.run(S, B, 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Found{0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Route{id, method, pattern, True{}, statuses}, params}, read, False{}, state, next) == 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Decision{state, 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Error{401n, "unauthorized", []}} : 0x36c893ade1f158581b4c8c34eb3b510e/src/contracts.Decision<S, B>}