bend-osdev-caps Releases (1): 0.1.0.0 0xaedcbedcbe1c3df31795343ff6f64678 indexed https://jend.leeeet.dev/files.txt?path=bend-osdev-caps@0.1.0.0 Definitions (282, 1 to 100 shown): LAWS.execve_result (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=execve_result) law execve_result: for +k: C.CapsKernel for +c: C.CapCred for +f: C.CapFile for +ign: Bool {C.Caps.sets_or(E.Caps.execve(k, c, f, ign), E.Caps.execve.sets(k, c, f, ign)) == E.Caps.execve.sets(k, c, f, ign) : C.CapState} LAWS.execve_effective_within_permitted (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=execve_effective_within_permitted) law execve_effective_within_permitted: for +k: C.CapsKernel for +c: C.CapCred for +f: C.CapFile for +ign: Bool {C.CapSet.subset(C.CapState.effective(E.Caps.execve.sets(k, c, f, ign)), C.CapState.permitted(E.Caps.execve.sets(k, c, f, ign))) == True{} : Bool} LAWS.execve_ambient_within_permitted (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=execve_ambient_within_permitted) law execve_ambient_within_permitted: for +k: C.CapsKernel for +c: C.CapCred for +f: C.CapFile for +ign: Bool {C.CapSet.subset(C.CapState.ambient(E.Caps.execve.sets(k, c, f, ign)), C.CapState.permitted(E.Caps.execve.sets(k, c, f, ign))) == True{} : Bool} LAWS.execve_ambient_within_inheritable (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=execve_ambient_within_inheritable) law execve_ambient_within_inheritable: for +k: C.CapsKernel for +c: C.CapCred for +f: C.CapFile for +ign: Bool for h: {C.CapSet.subset(C.CapState.ambient(C.CapCred.sets(c)), C.CapState.inheritable(C.CapCred.sets(c))) == True{} : Bool} {C.CapSet.subset(C.CapState.ambient(E.Caps.execve.sets(k, c, f, ign)), C.CapState.inheritable(E.Caps.execve.sets(k, c, f, ign))) == True{} : Bool} LAWS.execve_valid (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=execve_valid) law execve_valid: for +k: C.CapsKernel for +c: C.CapCred for +f: C.CapFile for +ign: Bool for h: {C.CapState.valid(C.CapCred.sets(c)) == True{} : Bool} {C.CapState.valid(E.Caps.execve.sets(k, c, f, ign)) == True{} : Bool} LAWS.execve_bounding_unchanged (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=execve_bounding_unchanged) law execve_bounding_unchanged: for +k: C.CapsKernel for +c: C.CapCred for +f: C.CapFile for +ign: Bool {C.CapState.bounding(E.Caps.execve.sets(k, c, f, ign)) == C.CapState.bounding(C.CapCred.sets(c)) : C.CapSet()} LAWS.execve_inheritable_unchanged (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=execve_inheritable_unchanged) law execve_inheritable_unchanged: for +k: C.CapsKernel for +c: C.CapCred for +f: C.CapFile for +ign: Bool {C.CapState.inheritable(E.Caps.execve.sets(k, c, f, ign)) == C.CapState.inheritable(C.CapCred.sets(c)) : C.CapSet()} LAWS.execve_permitted_bounded (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=execve_permitted_bounded) # a capability that is in none of the bounding, inheritable and ambient sets # never becomes permitted (the bounding set does not mask the inheritable # set: capabilities(7), "Capability bounding set") law execve_permitted_bounded: for +k: C.CapsKernel for +c: C.CapCred for +f: C.CapFile for +ign: Bool {C.CapSet.subset(C.CapState.permitted(E.Caps.execve.sets(k, c, f, ign)), C.CapSet.union(C.CapState.bounding(C.CapCred.sets(c)), C.CapSet.union(C.CapState.inheritable(C.CapCred.sets(c)), C.CapState.ambient(C.CapCred.sets(c))))) == True{} : Bool} LAWS.execve_permitted_bounded_valid (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=execve_permitted_bounded_valid) # with the ambient invariant, the bound is the bounding and inheritable sets law execve_permitted_bounded_valid: for +k: C.CapsKernel for +c: C.CapCred for +f: C.CapFile for +ign: Bool for h: {C.CapSet.subset(C.CapState.ambient(C.CapCred.sets(c)), C.CapState.inheritable(C.CapCred.sets(c))) == True{} : Bool} {C.CapSet.subset(C.CapState.permitted(E.Caps.execve.sets(k, c, f, ign)), C.CapSet.union(C.CapState.bounding(C.CapCred.sets(c)), C.CapState.inheritable(C.CapCred.sets(c)))) == True{} : Bool} LAWS.execve_root_permitted (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=execve_root_permitted) # "when a process whose real and effective UIDs are zero execve(2)s a # program": P'(permitted) = P(inheritable) | P(bounding), and # P'(effective) = P'(permitted). For every state with the ambient invariant, # every file that is not set-user-ID, without SECBIT_NOROOT. law execve_root_permitted: for +k: C.CapsKernel for +s: C.CapState for +sv: U32 for +na: Bool for +u: U32 for +sg: Bool … LAWS.execve_root_effective (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=execve_root_effective) law execve_root_effective: for +k: C.CapsKernel for +s: C.CapState for +sv: U32 for +na: Bool for +u: U32 for +sg: Bool for +fc: Maybe<&2, C.CapFileSets> for +ign: Bool for h: {C.CapSet.subset(C.CapState.ambient(s), C.CapState.inheritable(s)) == True{} : Bool} {C.CapState.effective(E.Caps.execve.sets(k, C.CapCred{0, 0, sv, False{}, na, s}, C.CapFile{u, False{}, sg, fc}, ign)) == C.CapSet.union(C.CapState.inheritable(s), C.CapState.bounding(s)) : C.CapSet()} LAWS.execve_nonroot_permitted (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=execve_nonroot_permitted) # "if a process with nonzero user IDs performs an execve(2) then any # capabilities that are present in its permitted and effective sets will be # cleared": of a file without set-ID bits or capabilities, only the ambient # set remains, as both permitted and effective. law execve_nonroot_permitted: for +k: C.CapsKernel for +r: U32 for +e: U32 for hr: {U32.is_eq(r, 0) == False{} : Bool} for he: {U32.is_eq(e, 0) == False{} : Bool} for +s: C.CapState … LAWS.execve_nonroot_effective (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=execve_nonroot_effective) law execve_nonroot_effective: for +k: C.CapsKernel for +r: U32 for +e: U32 for hr: {U32.is_eq(r, 0) == False{} : Bool} for he: {U32.is_eq(e, 0) == False{} : Bool} for +s: C.CapState for +sv: U32 for +nr: Bool for +na: Bool for +u: U32 … LAWS.capset_permitted_never_grows (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=capset_permitted_never_grows) law capset_permitted_never_grows: for +c: C.CapCred for +e: C.CapSet() for +p: C.CapSet() for +i: C.CapSet() {C.CapSet.subset(C.CapState.permitted(C.CapCred.sets(C.Caps.or(A.Caps.capset(c, e, p, i), c))), C.CapState.permitted(C.CapCred.sets(c))) == True{} : Bool} LAWS.capset_bounding_unchanged (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=capset_bounding_unchanged) law capset_bounding_unchanged: for +c: C.CapCred for +e: C.CapSet() for +p: C.CapSet() for +i: C.CapSet() {C.CapState.bounding(C.CapCred.sets(C.Caps.or(A.Caps.capset(c, e, p, i), c))) == C.CapState.bounding(C.CapCred.sets(c)) : C.CapSet()} LAWS.capset_valid (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=capset_valid) law capset_valid: for +c: C.CapCred for +e: C.CapSet() for +p: C.CapSet() for +i: C.CapSet() for h: {C.CapState.valid(C.CapCred.sets(c)) == True{} : Bool} {C.CapState.valid(C.CapCred.sets(C.Caps.or(A.Caps.capset(c, e, p, i), c))) == True{} : Bool} LAWS.bset_drop_never_grows (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=bset_drop_never_grows) law bset_drop_never_grows: for +k: C.CapsKernel for +c: C.CapCred for +x: U32 {C.CapSet.subset(C.CapState.bounding(C.CapCred.sets(C.Caps.or(A.Caps.bset_drop(k, c, x), c))), C.CapState.bounding(C.CapCred.sets(c))) == True{} : Bool} LAWS.bset_drop_rest_unchanged (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=bset_drop_rest_unchanged) # dropping from the bounding set changes no other set (in particular, not the # inheritable set) law bset_drop_rest_unchanged: for +k: C.CapsKernel for +c: C.CapCred for +x: U32 {C.CapState.with_bounding(C.CapCred.sets(C.Caps.or(A.Caps.bset_drop(k, c, x), c)), C.CapSet.empty()) == C.CapState.with_bounding(C.CapCred.sets(c), C.CapSet.empty()) : C.CapState} LAWS.ambient_raise_valid (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=ambient_raise_valid) law ambient_raise_valid: for +k: C.CapsKernel for +c: C.CapCred for +x: U32 for h: {C.CapState.valid(C.CapCred.sets(c)) == True{} : Bool} {C.CapState.valid(C.CapCred.sets(C.Caps.or(A.Caps.ambient_raise(k, c, x), c))) == True{} : Bool} LAWS.ambient_lower_valid (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=ambient_lower_valid) law ambient_lower_valid: for +k: C.CapsKernel for +c: C.CapCred for +x: U32 for h: {C.CapState.valid(C.CapCred.sets(c)) == True{} : Bool} {C.CapState.valid(C.CapCred.sets(C.Caps.or(A.Caps.ambient_lower(k, c, x), c))) == True{} : Bool} LAWS.ambient_raise_rest_unchanged (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=ambient_raise_rest_unchanged) law ambient_raise_rest_unchanged: for +k: C.CapsKernel for +c: C.CapCred for +x: U32 {C.CapState.with_ambient(C.CapCred.sets(C.Caps.or(A.Caps.ambient_raise(k, c, x), c)), C.CapSet.empty()) == C.CapState.with_ambient(C.CapCred.sets(c), C.CapSet.empty()) : C.CapState} LAWS.ambient_lower_rest_unchanged (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=ambient_lower_rest_unchanged) law ambient_lower_rest_unchanged: for +k: C.CapsKernel for +c: C.CapCred for +x: U32 {C.CapState.with_ambient(C.CapCred.sets(C.Caps.or(A.Caps.ambient_lower(k, c, x), c)), C.CapSet.empty()) == C.CapState.with_ambient(C.CapCred.sets(c), C.CapSet.empty()) : C.CapState} LAWS.ambient_clear_all_empty (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=ambient_clear_all_empty) law ambient_clear_all_empty: for +c: C.CapCred {C.CapState.ambient(C.CapCred.sets(A.Caps.ambient_clear_all(c))) == C.CapSet.empty() : C.CapSet()} LAWS.name_first (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=name_first) law name_first: {C.Cap.name(0) == Some{"CAP_CHOWN"} : Maybe<&2, String>} LAWS.name_last (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=name_last) law name_last: {C.Cap.name(40) == Some{"CAP_CHECKPOINT_RESTORE"} : Maybe<&2, String>} LAWS.name_beyond (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=name_beyond) law name_beyond: {C.Cap.name(41) == None{} : Maybe<&2, String>} LAWS.of_name_sys_admin (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=of_name_sys_admin) law of_name_sys_admin: {C.Cap.of_name("CAP_SYS_ADMIN") == Some{21} : Maybe<&2, U32>} LAWS.show_full (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=show_full) # the full set, as /proc//status shows it on Linux 5.9 and later law show_full: {C.CapSet.show(C.CapSet.full()) == "000001ffffffffff" : String} LAWS.show_two (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=show_two) # CAP_NET_RAW (13) and CAP_NET_BIND_SERVICE (10): 0x2400 law show_two: {C.CapSet.show(C.CapSet.from_list([13, 10])) == "0000000000002400" : String} LAWS.vector_dumb_binary (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=vector_dumb_binary) # A capability-dumb binary (cap_net_raw=ep) run by a non-root user whose # bounding set lacks CAP_NET_RAW: execve fails with EPERM. law vector_dumb_binary: {E.Caps.execve(C.CapsKernel.linux(), C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.empty(), C.CapSet.empty(), C.CapSet.empty(), C.CapSet.del(C.CapSet.full(), 13), C.CapSet.empty()}}, C.CapFile{0, False{}, False{}, Some{C.CapFileSets{C.CapSet.of(13), C.CapSet.empty(), True{}}}}, False{}) == Fail{C.CapsCapabilityDumb{}} : Result<&2, &2, C.CapsError, C.CapCred>} LAWS.vector_suid_root_with_caps (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=vector_suid_root_with_caps) # A set-user-ID-root program with file capabilities (cap_net_bind_service=ep) # run by user 1000: the effective and saved UIDs become 0, and the process # gains just the file's capabilities. law vector_suid_root_with_caps: {E.Caps.execve(C.CapsKernel.linux(), C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.empty(), C.CapSet.empty(), C.CapSet.empty(), C.CapSet.full(), C.CapSet.empty()}}, C.CapFile{0, True{}, False{}, Some{C.CapFileSets{C.CapSet.of(10), C.CapSet.empty(), True{}}}}, False{}) == Done{C.CapCred{1000, 0, 0, False{}, False{}, C.CapState{C.CapSet.of(10), C.CapSet.empty(), C.CapSet.of(10), C.CapSet.full(), C.CapSet.empty()}}} : Result<&2, &2, C.CapsError, C.CapCred>} LAWS.vector_suid_root_plain (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=vector_suid_root_plain) # The same program without file capabilities gains every capability in the # bounding set. law vector_suid_root_plain: {E.Caps.execve(C.CapsKernel.linux(), C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.empty(), C.CapSet.empty(), C.CapSet.empty(), C.CapSet.del(C.CapSet.full(), 21), C.CapSet.empty()}}, C.CapFile{0, True{}, False{}, None{}}, False{}) == Done{C.CapCred{1000, 0, 0, False{}, False{}, C.CapState{C.CapSet.del(C.CapSet.full(), 21), C.CapSet.empty(), C.CapSet.del(C.CapSet.full(), 21), C.CapSet.del(C.CapSet.full(), 21), C.CapSet.empty()}}} : Result<&2, &2, C.CapsError, C.CapCred>} LAWS.vector_suid_ignored (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=vector_suid_ignored) # With no_new_privs (ign), the set-user-ID bit is ignored: nothing is gained. law vector_suid_ignored: {E.Caps.execve(C.CapsKernel.linux(), C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.empty(), C.CapSet.empty(), C.CapSet.empty(), C.CapSet.full(), C.CapSet.empty()}}, C.CapFile{0, True{}, False{}, None{}}, True{}) == Done{C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.empty(), C.CapSet.empty(), C.CapSet.empty(), C.CapSet.full(), C.CapSet.empty()}}} : Result<&2, &2, C.CapsError, C.CapCred>} LAWS.vector_capset_grows (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=vector_capset_grows) # capset may not add to the permitted set law vector_capset_grows: {A.Caps.capset(C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.of(13), C.CapSet.empty(), C.CapSet.empty(), C.CapSet.full(), C.CapSet.empty()}}, C.CapSet.empty(), C.CapSet.from_list([13, 12]), C.CapSet.empty()) == Fail{C.CapsPermittedGrows{}} : Result<&2, &2, C.CapsError, C.CapCred>} LAWS.vector_ambient_not_inheritable (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=vector_ambient_not_inheritable) # an ambient capability must be permitted and inheritable law vector_ambient_not_inheritable: {A.Caps.ambient_raise(C.CapsKernel.linux(), C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.of(13), C.CapSet.empty(), C.CapSet.empty(), C.CapSet.full(), C.CapSet.empty()}}, 13) == Fail{C.CapsAmbientNotAllowed{}} : Result<&2, &2, C.CapsError, C.CapCred>} LAWS.vector_drop_invalid (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=vector_drop_invalid) # 41 is beyond CAP_CHECKPOINT_RESTORE law vector_drop_invalid: {A.Caps.bset_drop(C.CapsKernel.linux(), C.CapCred{0, 0, 0, False{}, False{}, C.CapState{C.CapSet.full(), C.CapSet.empty(), C.CapSet.full(), C.CapSet.full(), C.CapSet.empty()}}, 41) == Fail{C.CapsInvalidCap{}} : Result<&2, &2, C.CapsError, C.CapCred>} LAWS.witness_valid (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=witness_valid) # Witnesses: every hypothesis of the laws above holds for some input, so no # law is vacuous. A valid state with a nonempty ambient set (CAP_NET_BIND_ # SERVICE permitted, inheritable and ambient; CAP_NET_RAW permitted and # effective): law witness_valid: {C.CapState.valid(C.CapCred.sets(C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.from_list([10, 13]), C.CapSet.of(10), C.CapSet.of(13), C.CapSet.full(), C.CapSet.of(10)}})) == True{} : Bool} LAWS.witness_ambient_inheritable (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=witness_ambient_inheritable) # ambient within inheritable, for a credential's sets and for a state law witness_ambient_inheritable: {C.CapSet.subset(C.CapState.ambient(C.CapCred.sets(C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.from_list([10, 13]), C.CapSet.of(10), C.CapSet.of(13), C.CapSet.full(), C.CapSet.of(10)}})), C.CapState.inheritable(C.CapCred.sets(C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.from_list([10, 13]), C.CapSet.of(10), C.CapSet.of(13), C.CapSet.full(), C.CapSet.of(10)}}))) == True{} : Bool} LAWS.witness_ambient_inheritable_state (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=witness_ambient_inheritable_state) law witness_ambient_inheritable_state: {C.CapSet.subset(C.CapState.ambient(C.CapState{C.CapSet.of(10), C.CapSet.of(10), C.CapSet.empty(), C.CapSet.full(), C.CapSet.of(10)}), C.CapState.inheritable(C.CapState{C.CapSet.of(10), C.CapSet.of(10), C.CapSet.empty(), C.CapSet.full(), C.CapSet.of(10)})) == True{} : Bool} LAWS.witness_nonzero_uid (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&name=witness_nonzero_uid) # a nonzero user ID (the non-root laws' hypotheses on the real and effective # user IDs) law witness_nonzero_uid: {U32.is_eq(1000, 0) == False{} : Bool} PROOF.bits.disc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.disc) def bits.disc(b: Bool) -> Type: PROOF.bits.disc2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.disc2) def bits.disc2(b: Bool) -> Type: PROOF.bits.ft (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.ft) def bits.ft(+e: {False{} == True{} : Bool}) -> bits.disc(True{}): PROOF.bits.tf (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.tf) def bits.tf(+e: {True{} == False{} : Bool}) -> bits.disc2(False{}): PROOF.bits.absurd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.absurd) def bits.absurd(-x: Bool, +e: {False{} == True{} : Bool}) -> {x == True{} : Bool}: PROOF.bits.absurd_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.absurd_eq) def bits.absurd_eq(-T: Type, -x: T, -y: T, +e: {False{} == True{} : Bool}) -> {x == y : T}: PROOF.bits.absurd_tf (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.absurd_tf) def bits.absurd_tf(-T: Type, -x: T, -y: T, +e: {True{} == False{} : Bool}) -> {x == y : T}: PROOF.bool.and_l (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bool.and_l) def bool.and_l(+x: Bool, +y: Bool) -> {Bool.and(x, y) == True{} : Bool} -> {x == True{} : Bool}: PROOF.bool.and_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bool.and_r) def bool.and_r(+x: Bool, +y: Bool) -> {Bool.and(x, y) == True{} : Bool} -> {y == True{} : Bool}: PROOF.bool.and3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bool.and3) def bool.and3(+x: Bool, +y: Bool, +z: Bool) -> {x == True{} : Bool} -> {y == True{} : Bool} -> {z == True{} : Bool} -> {Bool.and(x, Bool.and(y, z)) == True{} : Bool}: PROOF.valid.intro (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=valid.intro) def valid.intro(+s: C.CapState) -> {C.CapSet.subset(C.CapState.effective(s), C.CapState.permitted(s)) == True{} : Bool} -> {C.CapSet.subset(C.CapState.ambient(s), C.CapState.permitted(s)) == True{} : Bool} -> {C.CapSet.subset(C.CapState.ambient(s), C.CapState.inheritable(s)) == True{} : Bool} -> {C.CapState.valid(s) == True{} : Bool}: PROOF.valid.ep (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=valid.ep) def valid.ep(+s: C.CapState) -> {C.CapState.valid(s) == True{} : Bool} -> {C.CapSet.subset(C.CapState.effective(s), C.CapState.permitted(s)) == True{} : Bool}: PROOF.valid.ap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=valid.ap) def valid.ap(+s: C.CapState) -> {C.CapState.valid(s) == True{} : Bool} -> {C.CapSet.subset(C.CapState.ambient(s), C.CapState.permitted(s)) == True{} : Bool}: PROOF.valid.ai (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=valid.ai) def valid.ai(+s: C.CapState) -> {C.CapState.valid(s) == True{} : Bool} -> {C.CapSet.subset(C.CapState.ambient(s), C.CapState.inheritable(s)) == True{} : Bool}: PROOF.bool.and2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bool.and2) def bool.and2(+x: Bool, +y: Bool) -> {x == True{} : Bool} -> {y == True{} : Bool} -> {Bool.and(x, y) == True{} : Bool}: PROOF.set.fin_ff (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.fin_ff) def set.fin_ff(+t: Cmp) -> {Cmp.is_eq(Word.cmp.fin(False{}, False{}, t)) == Cmp.is_eq(t) : Bool}: PROOF.set.fin_tf (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.fin_tf) def set.fin_tf(+t: Cmp) -> {Cmp.is_eq(Word.cmp.fin(True{}, False{}, t)) == False{} : Bool}: PROOF.set.bridge (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.bridge) def set.bridge(+n: Nat, +x: Word(n), +y: Word(n)) -> {Cmp.is_eq(Word.cmp(n, Word.and(n, x, Word.not(n, y)), Word.zero(n))) == C.CapBits.subset(n, x, y) : Bool}: PROOF.set.sub_intro (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.sub_intro) # a set within another, from its parts within theirs, and back def set.sub_intro(+al: Word(32n), +bl: Word(32n), +ah: Word(9n), +bh: Word(9n)) -> {C.CapBits.subset(32n, al, bl) == True{} : Bool} -> {C.CapBits.subset(9n, ah, bh) == True{} : Bool} -> {C.CapSet.subset(C.CapSetW{U32{al}, ah}, C.CapSetW{U32{bl}, bh}) == True{} : Bool}: PROOF.set.sub_lo (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.sub_lo) def set.sub_lo(+al: Word(32n), +bl: Word(32n), +ah: Word(9n), +bh: Word(9n)) -> {C.CapSet.subset(C.CapSetW{U32{al}, ah}, C.CapSetW{U32{bl}, bh}) == True{} : Bool} -> {C.CapBits.subset(32n, al, bl) == True{} : Bool}: PROOF.set.sub_hi (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.sub_hi) def set.sub_hi(+al: Word(32n), +bl: Word(32n), +ah: Word(9n), +bh: Word(9n)) -> {C.CapSet.subset(C.CapSetW{U32{al}, ah}, C.CapSetW{U32{bl}, bh}) == True{} : Bool} -> {C.CapBits.subset(9n, ah, bh) == True{} : Bool}: PROOF.set.eq_intro (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.eq_intro) # two sets are equal when their parts are def set.eq_intro(+l1: Word(32n), +l2: Word(32n), +h1: Word(9n), +h2: Word(9n), +e1: {l1 == l2 : Word(32n)}, +e2: {h1 == h2 : Word(9n)}) -> {C.CapSetW{U32{l1}, h1} == C.CapSetW{U32{l2}, h2} : C.CapSet()}: PROOF.bits.sub_refl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.sub_refl) def bits.sub_refl(+n: Nat, +x: Word(n)) -> {C.CapBits.subset(n, x, x) == True{} : Bool}: PROOF.bits.sub_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.sub_zero) def bits.sub_zero(+n: Nat, +x: Word(n)) -> {C.CapBits.subset(n, Word.zero(n), x) == True{} : Bool}: PROOF.bits.sub_or_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.sub_or_r) def bits.sub_or_r(+n: Nat, +x: Word(n), +c: Word(n)) -> {C.CapBits.subset(n, c, Word.or(n, x, c)) == True{} : Bool}: PROOF.bits.sub_minus (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.sub_minus) def bits.sub_minus(+n: Nat, +x: Word(n), +y: Word(n)) -> {C.CapBits.subset(n, Word.and(n, x, Word.not(n, y)), x) == True{} : Bool}: PROOF.bits.bound_a (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.bound_a) def bits.bound_a(+n: Nat, +i: Word(n), +fi: Word(n), +fp: Word(n), +b: Word(n), +a: Word(n)) -> {C.CapBits.subset(n, Word.or(n, Word.or(n, Word.and(n, i, fi), Word.and(n, fp, b)), a), Word.or(n, b, Word.or(n, i, a))) == True{} : Bool}: PROOF.bits.bound_z (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.bound_z) def bits.bound_z(+n: Nat, +i: Word(n), +fi: Word(n), +fp: Word(n), +b: Word(n), +a: Word(n)) -> {C.CapBits.subset(n, Word.or(n, Word.or(n, Word.and(n, i, fi), Word.and(n, fp, b)), Word.zero(n)), Word.or(n, b, Word.or(n, i, a))) == True{} : Bool}: PROOF.bits.bound_va (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.bound_va) def bits.bound_va(+n: Nat, +i: Word(n), +fi: Word(n), +fp: Word(n), +b: Word(n), +a: Word(n)) -> {C.CapBits.subset(n, a, i) == True{} : Bool} -> {C.CapBits.subset(n, Word.or(n, Word.or(n, Word.and(n, i, fi), Word.and(n, fp, b)), a), Word.or(n, b, i)) == True{} : Bool}: PROOF.bits.bound_vz (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.bound_vz) def bits.bound_vz(+n: Nat, +i: Word(n), +fi: Word(n), +fp: Word(n), +b: Word(n)) -> {C.CapBits.subset(n, Word.or(n, Word.or(n, Word.and(n, i, fi), Word.and(n, fp, b)), Word.zero(n)), Word.or(n, b, i)) == True{} : Bool}: PROOF.bits.amb_p (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.amb_p) def bits.amb_p(+n: Nat, +a: Word(n), +p: Word(n), +i: Word(n)) -> {C.CapBits.subset(n, Word.and(n, Word.and(n, a, p), i), p) == True{} : Bool}: PROOF.bits.amb_i (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.amb_i) def bits.amb_i(+n: Nat, +a: Word(n), +p: Word(n), +i: Word(n)) -> {C.CapBits.subset(n, Word.and(n, Word.and(n, a, p), i), i) == True{} : Bool}: PROOF.bits.lub (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.lub) def bits.lub(+n: Nat, +a: Word(n), +s: Word(n), +p: Word(n)) -> {C.CapBits.subset(n, a, p) == True{} : Bool} -> {C.CapBits.subset(n, s, p) == True{} : Bool} -> {C.CapBits.subset(n, Word.or(n, a, s), p) == True{} : Bool}: PROOF.bits.minus_within (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.minus_within) def bits.minus_within(+n: Nat, +a: Word(n), +y: Word(n), +p: Word(n)) -> {C.CapBits.subset(n, a, p) == True{} : Bool} -> {C.CapBits.subset(n, Word.and(n, a, Word.not(n, y)), p) == True{} : Bool}: PROOF.bits.root_a (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.root_a) def bits.root_a(+n: Nat, +i: Word(n), +b: Word(n), +a: Word(n)) -> {C.CapBits.subset(n, a, i) == True{} : Bool} -> {Word.or(n, Word.or(n, Word.and(n, i, C.CapBits.all(n)), Word.and(n, C.CapBits.all(n), b)), a) == Word.or(n, i, b) : Word(n)}: PROOF.bits.root_z (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.root_z) def bits.root_z(+n: Nat, +i: Word(n), +b: Word(n)) -> {Word.or(n, Word.or(n, Word.and(n, i, C.CapBits.all(n)), Word.and(n, C.CapBits.all(n), b)), Word.zero(n)) == Word.or(n, i, b) : Word(n)}: PROOF.bits.nonroot (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=bits.nonroot) def bits.nonroot(+n: Nat, +i: Word(n), +b: Word(n), +a: Word(n)) -> {Word.or(n, Word.or(n, Word.and(n, i, Word.zero(n)), Word.and(n, Word.zero(n), b)), a) == a : Word(n)}: PROOF.set.sub_refl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.sub_refl) def set.sub_refl(+x: C.CapSet()) -> {C.CapSet.subset(x, x) == True{} : Bool}: PROOF.set.sub_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.sub_zero) def set.sub_zero(+x: C.CapSet()) -> {C.CapSet.subset(C.CapSet.empty(), x) == True{} : Bool}: PROOF.set.sub_or_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.sub_or_r) def set.sub_or_r(+x: C.CapSet(), +c: C.CapSet()) -> {C.CapSet.subset(c, C.CapSet.union(x, c)) == True{} : Bool}: PROOF.set.sub_minus (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.sub_minus) def set.sub_minus(+x: C.CapSet(), +y: C.CapSet()) -> {C.CapSet.subset(C.CapSet.minus(x, y), x) == True{} : Bool}: PROOF.set.bound_a (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.bound_a) def set.bound_a(+i: C.CapSet(), +fi: C.CapSet(), +fp: C.CapSet(), +b: C.CapSet(), +a: C.CapSet()) -> {C.CapSet.subset(C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), a), C.CapSet.union(b, C.CapSet.union(i, a))) == True{} : Bool}: PROOF.set.bound_z (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.bound_z) def set.bound_z(+i: C.CapSet(), +fi: C.CapSet(), +fp: C.CapSet(), +b: C.CapSet(), +a: C.CapSet()) -> {C.CapSet.subset(C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), C.CapSet.empty()), C.CapSet.union(b, C.CapSet.union(i, a))) == True{} : Bool}: PROOF.set.bound_va (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.bound_va) def set.bound_va(+i: C.CapSet(), +fi: C.CapSet(), +fp: C.CapSet(), +b: C.CapSet(), +a: C.CapSet()) -> {C.CapSet.subset(a, i) == True{} : Bool} -> {C.CapSet.subset(C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), a), C.CapSet.union(b, i)) == True{} : Bool}: PROOF.set.bound_vz (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.bound_vz) def set.bound_vz(+i: C.CapSet(), +fi: C.CapSet(), +fp: C.CapSet(), +b: C.CapSet()) -> {C.CapSet.subset(C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), C.CapSet.empty()), C.CapSet.union(b, i)) == True{} : Bool}: PROOF.set.amb_p (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.amb_p) def set.amb_p(+a: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapSet.subset(C.CapSet.inter(C.CapSet.inter(a, p), i), p) == True{} : Bool}: PROOF.set.amb_i (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.amb_i) def set.amb_i(+a: C.CapSet(), +p: C.CapSet(), +i: C.CapSet()) -> {C.CapSet.subset(C.CapSet.inter(C.CapSet.inter(a, p), i), i) == True{} : Bool}: PROOF.set.lub (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.lub) def set.lub(+a: C.CapSet(), +s: C.CapSet(), +p: C.CapSet()) -> {C.CapSet.subset(a, p) == True{} : Bool} -> {C.CapSet.subset(s, p) == True{} : Bool} -> {C.CapSet.subset(C.CapSet.union(a, s), p) == True{} : Bool}: PROOF.set.minus_within (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.minus_within) def set.minus_within(+a: C.CapSet(), +y: C.CapSet(), +p: C.CapSet()) -> {C.CapSet.subset(a, p) == True{} : Bool} -> {C.CapSet.subset(C.CapSet.minus(a, y), p) == True{} : Bool}: PROOF.set.root_a (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.root_a) def set.root_a(+i: C.CapSet(), +b: C.CapSet(), +a: C.CapSet()) -> {C.CapSet.subset(a, i) == True{} : Bool} -> {C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, C.CapSet.full()), C.CapSet.inter(C.CapSet.full(), b)), a) == C.CapSet.union(i, b) : C.CapSet()}: PROOF.set.root_z (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.root_z) def set.root_z(+i: C.CapSet(), +b: C.CapSet()) -> {C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, C.CapSet.full()), C.CapSet.inter(C.CapSet.full(), b)), C.CapSet.empty()) == C.CapSet.union(i, b) : C.CapSet()}: PROOF.set.nonroot (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=set.nonroot) def set.nonroot(+i: C.CapSet(), +b: C.CapSet(), +a: C.CapSet()) -> {C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, C.CapSet.empty()), C.CapSet.inter(C.CapSet.empty(), b)), a) == a : C.CapSet()}: PROOF.caps.has_of (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=caps.has_of) # a set that has capability k contains the set {k} (has is that subset test) def caps.has_of(+v: Bool, +s: C.CapSet(), +x: U32) -> {C.CapSet.has.go(v, s, x) == True{} : Bool} -> {C.CapSet.subset(C.CapSet.of.go(v, x), s) == True{} : Bool}: PROOF.ex.eff (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=ex.eff) def ex.eff(+fl: E.CapExecFlags, +s: C.CapState) -> {C.CapSet.subset(C.CapState.effective(E.CapExec.sets(fl, s)), C.CapState.permitted(E.CapExec.sets(fl, s))) == True{} : Bool}: PROOF.ex.ap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=ex.ap) def ex.ap(+fl: E.CapExecFlags, +s: C.CapState) -> {C.CapSet.subset(C.CapState.ambient(E.CapExec.sets(fl, s)), C.CapState.permitted(E.CapExec.sets(fl, s))) == True{} : Bool}: PROOF.ex.ai (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=ex.ai) def ex.ai(+fl: E.CapExecFlags, +s: C.CapState) -> {C.CapSet.subset(C.CapState.ambient(s), C.CapState.inheritable(s)) == True{} : Bool} -> {C.CapSet.subset(C.CapState.ambient(E.CapExec.sets(fl, s)), C.CapState.inheritable(E.CapExec.sets(fl, s))) == True{} : Bool}: PROOF.ex.bnd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=ex.bnd) def ex.bnd(+fl: E.CapExecFlags, +s: C.CapState) -> {C.CapState.bounding(E.CapExec.sets(fl, s)) == C.CapState.bounding(s) : C.CapSet()}: PROOF.ex.inh (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=ex.inh) def ex.inh(+fl: E.CapExecFlags, +s: C.CapState) -> {C.CapState.inheritable(E.CapExec.sets(fl, s)) == C.CapState.inheritable(s) : C.CapSet()}: PROOF.ex.bound (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=ex.bound) def ex.bound(+fl: E.CapExecFlags, +s: C.CapState) -> {C.CapSet.subset(C.CapState.permitted(E.CapExec.sets(fl, s)), C.CapSet.union(C.CapState.bounding(s), C.CapSet.union(C.CapState.inheritable(s), C.CapState.ambient(s)))) == True{} : Bool}: PROOF.ex.bound_v (https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=ex.bound_v) def ex.bound_v(+fl: E.CapExecFlags, +s: C.CapState) -> {C.CapSet.subset(C.CapState.ambient(s), C.CapState.inheritable(s)) == True{} : Bool} -> {C.CapSet.subset(C.CapState.permitted(E.CapExec.sets(fl, s)), C.CapSet.union(C.CapState.bounding(s), C.CapState.inheritable(s))) == True{} : Bool}: More: https://jend.leeeet.dev/packages/bend-osdev-caps.txt?definitions_offset=100