bend-osdev-apparmor Releases (1): 0.1.0.0 0x2b280a281d356b8e5cd7b338ab267df1 indexed https://jend.leeeet.dev/files.txt?path=bend-osdev-apparmor@0.1.0.0 Definitions (1104, 1 to 100 shown): LAWS.glob_seq_model (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_seq_model) law glob_seq_model: for seq: List<&2, G.AaGTok> for s: List<&2, U32> {G.AaGSeq.matches(seq, s) == G.AaGSeq.model(seq, s) : Bool} LAWS.glob_run (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_run) law glob_run: for seq: List<&2, G.AaGTok> for s: List<&2, U32> {G.AaGSeq.run(seq, s) == G.AaGSeq.matches(seq, s) : Bool} LAWS.glob_model (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_model) law glob_model: for g: G.AaGlob for s: List<&2, U32> {G.AaGlob.matches(g, s) == G.AaGlob.model(g, s) : Bool} LAWS.glob_ref_model (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_ref_model) law glob_ref_model: for g: G.AaGlob for s: List<&2, U32> {G.AaGlob.matches_ref(g, s) == G.AaGlob.model(g, s) : Bool} LAWS.granted_never_denied (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=granted_never_denied) law granted_never_denied: for gs: List<&2, P.AaGrant> {P.AaPerms.meets(V.AaEval.granted(gs), V.AaEval.denied(gs)) == False{} : Bool} LAWS.deny_wins (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=deny_wins) law deny_wins: for opts: O.AaOptions for gs: List<&2, P.AaGrant> for flags: PR.AaFlags for req: P.AaPerms for h1: {V.AaEval.deny_applies(opts, PR.AaFlags.mode(flags)) == True{} : Bool} for h2: {P.AaPerms.meets(req, V.AaEval.denied(gs)) == True{} : Bool} {V.AaDecision.allowed(V.AaEval.decide(opts, flags, req, gs)) == False{} : Bool} LAWS.unmatched_denied (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=unmatched_denied) law unmatched_denied: for opts: O.AaOptions for flags: PR.AaFlags for req: P.AaPerms for h1: {PR.AaMode.enforcing(PR.AaFlags.mode(flags)) == True{} : Bool} for h2: {P.AaPerms.any(req) == True{} : Bool} {V.AaDecision.allowed(V.AaEval.decide(opts, flags, req, Nil{})) == False{} : Bool} LAWS.complain_decided_by_deny (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=complain_decided_by_deny) law complain_decided_by_deny: for opts: O.AaOptions for flags: PR.AaFlags for req: P.AaPerms for gs: List<&2, P.AaGrant> for h: {PR.AaMode.is_complain(PR.AaFlags.mode(flags)) == True{} : Bool} {V.AaDecision.allowed(V.AaEval.decide(opts, flags, req, gs)) == Bool.not(Bool.and(O.AaOptions.complain_deny(opts), P.AaPerms.meets(req, V.AaEval.denied(gs)))) : Bool} LAWS.complain_never_denies (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=complain_never_denies) law complain_never_denies: for opts: O.AaOptions for flags: PR.AaFlags for req: P.AaPerms for gs: List<&2, P.AaGrant> for h1: {O.AaOptions.complain_deny(opts) == False{} : Bool} for h2: {PR.AaMode.is_complain(PR.AaFlags.mode(flags)) == True{} : Bool} {V.AaDecision.allowed(V.AaEval.decide(opts, flags, req, gs)) == True{} : Bool} LAWS.file_deny_wins (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=file_deny_wins) law file_deny_wins: for opts: O.AaOptions for p: PR.AaProfile for q: F.AaFileQuery for h1: {V.AaEval.deny_applies(opts, PR.AaFlags.mode(PR.AaProfile.flags(p))) == True{} : Bool} for h2: {P.AaPerms.meets(F.AaFileQuery.req(q), V.AaEval.denied(F.AaFileRule.grants(PR.AaRules.files(PR.AaProfile.rules(p)), q))) == True{} : Bool} {V.AaDecision.allowed(V.AaEval.file(opts, p, q)) == False{} : Bool} LAWS.file_unmatched_denied (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=file_unmatched_denied) law file_unmatched_denied: for opts: O.AaOptions for p: PR.AaProfile for q: F.AaFileQuery for h1: {PR.AaMode.enforcing(PR.AaFlags.mode(PR.AaProfile.flags(p))) == True{} : Bool} for h2: {F.AaFileRule.matching(PR.AaRules.files(PR.AaProfile.rules(p)), q) == Nil{} : List<&2, F.AaFileRule>} for h3: {P.AaPerms.any(F.AaFileQuery.req(q)) == True{} : Bool} {V.AaDecision.allowed(V.AaEval.file(opts, p, q)) == False{} : Bool} LAWS.include_idempotent_file (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=include_idempotent_file) law include_idempotent_file: for opts: O.AaOptions for p: PR.AaProfile for r: PR.AaRules for q: F.AaFileQuery {V.AaEval.file(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.file(opts, PR.AaProfile.include(p, r), q) : V.AaDecision} LAWS.include_idempotent_capability (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=include_idempotent_capability) law include_idempotent_capability: for opts: O.AaOptions for p: PR.AaProfile for r: PR.AaRules for q: RC.AaCapQuery {V.AaEval.capability(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.capability(opts, PR.AaProfile.include(p, r), q) : V.AaDecision} LAWS.include_idempotent_network (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=include_idempotent_network) law include_idempotent_network: for opts: O.AaOptions for p: PR.AaProfile for r: PR.AaRules for q: RN.AaNetQuery {V.AaEval.network(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.network(opts, PR.AaProfile.include(p, r), q) : V.AaDecision} LAWS.include_idempotent_signal (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=include_idempotent_signal) law include_idempotent_signal: for opts: O.AaOptions for p: PR.AaProfile for r: PR.AaRules for q: RS.AaSignalQuery {V.AaEval.signal(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.signal(opts, PR.AaProfile.include(p, r), q) : V.AaDecision} LAWS.include_idempotent_ptrace (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=include_idempotent_ptrace) law include_idempotent_ptrace: for opts: O.AaOptions for p: PR.AaProfile for r: PR.AaRules for q: RP.AaPtraceQuery {V.AaEval.ptrace(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.ptrace(opts, PR.AaProfile.include(p, r), q) : V.AaDecision} LAWS.include_idempotent_mount (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=include_idempotent_mount) law include_idempotent_mount: for opts: O.AaOptions for p: PR.AaProfile for r: PR.AaRules for q: RM.AaMountQuery {V.AaEval.mount(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.mount(opts, PR.AaProfile.include(p, r), q) : V.AaDecision} LAWS.include_idempotent_dbus (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=include_idempotent_dbus) law include_idempotent_dbus: for opts: O.AaOptions for p: PR.AaProfile for r: PR.AaRules for q: RD.AaDbusQuery {V.AaEval.dbus(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.dbus(opts, PR.AaProfile.include(p, r), q) : V.AaDecision} LAWS.include_idempotent_change_profile (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=include_idempotent_change_profile) law include_idempotent_change_profile: for opts: O.AaOptions for p: PR.AaProfile for r: PR.AaRules for q: RX.AaChangeQuery {V.AaEval.change_profile(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.change_profile(opts, PR.AaProfile.include(p, r), q) : V.AaDecision} LAWS.exec_needs_x (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=exec_needs_x) law exec_needs_x: for opts: O.AaOptions for pol: PR.AaPolicy for name: List<&2, U32> for owner: Bool for path: List<&2, U32> for p: PR.AaProfile for h1: {PR.AaPolicy.lookup(pol, name) == Some{p} : Maybe<&2, PR.AaProfile>} for h2: {TR.AaTrans.is_unconfined(PR.AaFlags.mode(PR.AaProfile.flags(p))) == False{} : Bool} for h3: {V.AaDecision.allowed(V.AaEval.file(opts, p, F.AaFileQuery{path, owner, P.AaPerms.bit(6n)})) == False{} : Bool} {TR.AaExecResult.ok(TR.AaTrans.exec(opts, pol, name, owner, path)) == False{} : Bool} LAWS.deny_wins_sat (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=deny_wins_sat) law deny_wins_sat: {Bool.and(V.AaEval.deny_applies(O.AaOptions.default(), PR.AaFlags.mode(PR.AaProfile.flags(EX.AaExample.profile(PR.AaModeEnforce{})))), P.AaPerms.meets(F.AaFileQuery.req(EX.AaExample.query("/etc/x", "w")), V.AaEval.denied(F.AaFileRule.grants(PR.AaRules.files(PR.AaProfile.rules(EX.AaExample.profile(PR.AaModeEnforce{}))), EX.AaExample.query("/etc/x", "w"))))) == True{} : Bool} LAWS.deny_wins_example (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=deny_wins_example) law deny_wins_example: {V.AaEval.file(O.AaOptions.default(), EX.AaExample.profile(PR.AaModeEnforce{}), EX.AaExample.query("/etc/x", "w")) == V.AaDeny{False{}} : V.AaDecision} LAWS.allow_example (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=allow_example) law allow_example: {V.AaEval.file(O.AaOptions.default(), EX.AaExample.profile(PR.AaModeEnforce{}), EX.AaExample.query("/etc/x", "r")) == V.AaAllow{} : V.AaDecision} LAWS.audit_example (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=audit_example) law audit_example: {V.AaEval.file(O.AaOptions.default(), EX.AaExample.profile(PR.AaModeEnforce{}), EX.AaExample.query("/var/log/x", "w")) == V.AaAudit{} : V.AaDecision} LAWS.unmatched_sat (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=unmatched_sat) law unmatched_sat: {Bool.and(PR.AaMode.enforcing(PR.AaFlags.mode(PR.AaProfile.flags(EX.AaExample.profile(PR.AaModeEnforce{})))), P.AaPerms.any(F.AaFileQuery.req(EX.AaExample.query("/etc/y", "r")))) == True{} : Bool} LAWS.file_unmatched_sat (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=file_unmatched_sat) law file_unmatched_sat: {F.AaFileRule.matching(PR.AaRules.files(PR.AaProfile.rules(EX.AaExample.profile(PR.AaModeEnforce{}))), EX.AaExample.query("/etc/y", "r")) == Nil{} : List<&2, F.AaFileRule>} LAWS.unmatched_example (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=unmatched_example) law unmatched_example: {V.AaEval.file(O.AaOptions.default(), EX.AaExample.profile(PR.AaModeEnforce{}), EX.AaExample.query("/etc/y", "r")) == V.AaDeny{True{}} : V.AaDecision} LAWS.complain_sat (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=complain_sat) law complain_sat: {Bool.and(PR.AaMode.is_complain(PR.AaFlags.mode(PR.AaProfile.flags(EX.AaExample.profile(PR.AaModeComplain{})))), Bool.not(O.AaOptions.complain_deny(O.AaOptions.with_complain_deny(O.AaOptions.default(), False{})))) == True{} : Bool} LAWS.complain_example_unmatched (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=complain_example_unmatched) law complain_example_unmatched: {V.AaEval.file(O.AaOptions.default(), EX.AaExample.profile(PR.AaModeComplain{}), EX.AaExample.query("/etc/y", "r")) == V.AaComplain{} : V.AaDecision} LAWS.complain_example_deny_rule (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=complain_example_deny_rule) law complain_example_deny_rule: {V.AaEval.file(O.AaOptions.default(), EX.AaExample.profile(PR.AaModeComplain{}), EX.AaExample.query("/etc/x", "w")) == V.AaDeny{False{}} : V.AaDecision} LAWS.complain_example_no_deny (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=complain_example_no_deny) law complain_example_no_deny: {V.AaEval.file(O.AaOptions.with_complain_deny(O.AaOptions.default(), False{}), EX.AaExample.profile(PR.AaModeComplain{}), EX.AaExample.query("/etc/x", "w")) == V.AaComplain{} : V.AaDecision} LAWS.kill_example (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=kill_example) law kill_example: {V.AaEval.file(O.AaOptions.default(), EX.AaExample.profile(PR.AaModeKill{}), EX.AaExample.query("/etc/y", "r")) == V.AaKill{} : V.AaDecision} LAWS.exec_needs_x_sat (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=exec_needs_x_sat) law exec_needs_x_sat: {PR.AaPolicy.lookup(EX.AaExample.policy(), X.AaText.of_string("ex")) == Some{EX.AaExample.profile(PR.AaModeEnforce{})} : Maybe<&2, PR.AaProfile>} LAWS.exec_needs_x_sat2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=exec_needs_x_sat2) law exec_needs_x_sat2: {Bool.and(Bool.not(TR.AaTrans.is_unconfined(PR.AaFlags.mode(PR.AaProfile.flags(EX.AaExample.profile(PR.AaModeEnforce{}))))), Bool.not(V.AaDecision.allowed(V.AaEval.file(O.AaOptions.default(), EX.AaExample.profile(PR.AaModeEnforce{}), F.AaFileQuery{X.AaText.of_string("/bin/sh"), False{}, P.AaPerms.bit(6n)})))) == True{} : Bool} LAWS.glob_star_not_empty_segment (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_star_not_empty_segment) law glob_star_not_empty_segment: {G.AaGlob.match_text(X.AaText.of_string("/tmp/*"), X.AaText.of_string("/tmp/")) == False{} : Bool} LAWS.glob_star_file (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_star_file) law glob_star_file: {G.AaGlob.match_text(X.AaText.of_string("/tmp/*"), X.AaText.of_string("/tmp/x")) == True{} : Bool} LAWS.glob_star_no_slash (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_star_no_slash) law glob_star_no_slash: {G.AaGlob.match_text(X.AaText.of_string("/tmp/*"), X.AaText.of_string("/tmp/x/y")) == False{} : Bool} LAWS.glob_star2_not_dir_itself (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_star2_not_dir_itself) law glob_star2_not_dir_itself: {G.AaGlob.match_text(X.AaText.of_string("/tmp/**"), X.AaText.of_string("/tmp/")) == False{} : Bool} LAWS.glob_star2_deep (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_star2_deep) law glob_star2_deep: {G.AaGlob.match_text(X.AaText.of_string("/tmp/**"), X.AaText.of_string("/tmp/a/b/")) == True{} : Bool} LAWS.glob_star_inside_segment (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_star_inside_segment) law glob_star_inside_segment: {G.AaGlob.match_text(X.AaText.of_string("/a/*b"), X.AaText.of_string("/a/b")) == True{} : Bool} LAWS.glob_star_in_braces (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_star_in_braces) law glob_star_in_braces: {G.AaGlob.match_text(X.AaText.of_string("/a/{b,*}"), X.AaText.of_string("/a/")) == True{} : Bool} LAWS.glob_negated_class_slash (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_negated_class_slash) law glob_negated_class_slash: {G.AaGlob.match_text(X.AaText.of_string("/a/[^b]c"), X.AaText.of_string("/a//c")) == True{} : Bool} LAWS.glob_slashes_collapse (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_slashes_collapse) law glob_slashes_collapse: {G.AaGlob.match_text(X.AaText.of_string("/a//b"), X.AaText.of_string("/a/b")) == True{} : Bool} LAWS.glob_class_range (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_class_range) law glob_class_range: {Bool.and(G.AaGlob.match_text(X.AaText.of_string("/a/[a-c]x"), X.AaText.of_string("/a/bx")), Bool.not(G.AaGlob.match_text(X.AaText.of_string("/a/[a-c]x"), X.AaText.of_string("/a/dx")))) == True{} : Bool} LAWS.glob_nested_braces (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_nested_braces) law glob_nested_braces: {G.AaGlob.match_text(X.AaText.of_string("/a/{b,c{d,e}}"), X.AaText.of_string("/a/ce")) == True{} : Bool} LAWS.glob_question (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_question) law glob_question: {Bool.and(G.AaGlob.match_text(X.AaText.of_string("/a/?b"), X.AaText.of_string("/a/xb")), Bool.not(G.AaGlob.match_text(X.AaText.of_string("/a/?b"), X.AaText.of_string("/a//b")))) == True{} : Bool} LAWS.glob_one_alternative_rejected (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_one_alternative_rejected) law glob_one_alternative_rejected: {G.AaGlob.parse(X.AaText.of_string("/a/{b}")) == None{} : Maybe<&2, G.AaGlob>} LAWS.glob_trailing_dash_rejected (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_trailing_dash_rejected) law glob_trailing_dash_rejected: {G.AaGlob.parse(X.AaText.of_string("/a/[a-]")) == None{} : Maybe<&2, G.AaGlob>} LAWS.glob_empty_class_rejected (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=glob_empty_class_rejected) law glob_empty_class_rejected: {G.AaGlob.parse(X.AaText.of_string("/a/[]]")) == None{} : Maybe<&2, G.AaGlob>} LAWS.policy_file_vectors (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=policy_file_vectors) law policy_file_vectors: {[EX.AaExample.small_file("/usr/bin/foo", "/lib/x/y.so", "mr"), EX.AaExample.small_file("/usr/bin/foo", "/etc/shadow", "r"), EX.AaExample.small_file("/usr/bin/foo", "/home/al/f", "rw"), EX.AaExample.small_file("/usr/bin/foo", "/root/f", "a"), EX.AaExample.small_file("/usr/bin/foo", "/etc/x", "r"), EX.AaExample.small_file("bar", "/etc/x", "r")] == [Some{V.AaAllow{}}, Some{V.AaDeny{False{}}}, Some{V.AaAllow{}}, Some{V.AaAllow{}}, Some{V.AaDeny{True{}}}, Some{V.AaComplain{}}] : List<&2, Maybe<&2, V.AaDecision>>} LAWS.policy_exec_vectors (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/LAWS.bend&name=policy_exec_vectors) law policy_exec_vectors: {[EX.AaExample.small_exec("/usr/bin/foo", "/bin/x"), EX.AaExample.small_exec("/usr/bin/foo", "/bin/y")] == ["profile bar", "denied (deny)"] : List<&2, String>} PROOF.b.or_assoc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.or_assoc) def b.or_assoc(+a: Bool, +b: Bool, +c: Bool) -> {Bool.or(Bool.or(a, b), c) == Bool.or(a, Bool.or(b, c)) : Bool}: PROOF.b.or_false_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.or_false_r) def b.or_false_r(+a: Bool) -> {Bool.or(a, False{}) == a : Bool}: PROOF.b.and_false_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.and_false_r) def b.and_false_r(+a: Bool) -> {Bool.and(a, False{}) == False{} : Bool}: PROOF.b.and_true_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.and_true_r) def b.and_true_r(+a: Bool) -> {Bool.and(a, True{}) == a : Bool}: PROOF.b.factor (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.factor) # (p and n and f) or (p and q) is p and ((n and f) or q) def b.factor(+p: Bool, +n: Bool, +f: Bool, +q: Bool) -> {Bool.or(Bool.and(Bool.and(p, n), f), Bool.and(p, q)) == Bool.and(p, Bool.or(Bool.and(n, f), q)) : Bool}: PROOF.b.disc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.disc) def b.disc(+b: Bool) -> Type: PROOF.b.ft (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.ft) def b.ft(+e: {False{} == True{} : Bool}) -> b.disc(True{}): PROOF.b.absurd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.absurd) def b.absurd(-T: Type, -x: T, -y: T, +e: {False{} == True{} : Bool}) -> {x == y : T}: PROOF.b.absurd_tf (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.absurd_tf) def b.absurd_tf(-T: Type, -x: T, -y: T, +e: {True{} == False{} : Bool}) -> {x == y : T}: PROOF.fe (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=fe) # the pieces d fit the tokens r after an empty first piece def fe(+r: List<&2, G.AaGTok>, d: List<&2, List<&2, U32>>) -> Bool: PROOF.fe_any (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=fe_any) def fe_any(+r: List<&2, G.AaGTok>, ds: List<&2, List<&2, List<&2, U32>>>) -> Bool: PROOF.fa_app (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=fa_app) def fa_app(+seq: List<&2, G.AaGTok>, +xs: List<&2, List<&2, List<&2, U32>>>, +ys: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(seq, G.AaGCuts.append(xs, ys)) == Bool.or(G.AaGSeq.fits_any(seq, xs), G.AaGSeq.fits_any(seq, ys)) : Bool}: PROOF.fe_app (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=fe_app) def fe_app(+r: List<&2, G.AaGTok>, +xs: List<&2, List<&2, List<&2, U32>>>, +ys: List<&2, List<&2, List<&2, U32>>>) -> {fe_any(r, G.AaGCuts.append(xs, ys)) == Bool.or(fe_any(r, xs), fe_any(r, ys)) : Bool}: PROOF.ef_char (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=ef_char) # an empty first piece: no single-byte token fits it def ef_char(+c: U32, +r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(ds)) == False{} : Bool}: PROOF.ef_any (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=ef_any) def ef_any(+r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(ds)) == False{} : Bool}: PROOF.ef_class (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=ef_class) def ef_class(+n: Bool, +rs: List<&2, G.AaGRange>, +r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(ds)) == False{} : Bool}: PROOF.ef_star (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=ef_star) # ... and a star takes it def ef_star(+r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(ds)) == G.AaGSeq.fits_any(r, ds) : Bool}: PROOF.ef_star2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=ef_star2) def ef_star2(+r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(ds)) == G.AaGSeq.fits_any(r, ds) : Bool}: PROOF.gr_char (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=gr_char) # a first piece that starts with h: a single-byte token takes h and leaves # an empty piece def gr_char(+c: U32, +r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, ds)) == Bool.and(U32.is_eq(h, c), fe_any(r, ds)) : Bool}: PROOF.gr_any (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=gr_any) def gr_any(+r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, ds)) == Bool.and(U32.is_ne(h, 47), fe_any(r, ds)) : Bool}: PROOF.gr_class (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=gr_class) def gr_class(+n: Bool, +rs: List<&2, G.AaGRange>, +r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, ds)) == Bool.and(G.AaGClass.has(n, rs, h), fe_any(r, ds)) : Bool}: PROOF.gr_star (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=gr_star) # ... a star takes h if it is not '/', and goes on def gr_star(+r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, ds)) == Bool.and(U32.is_ne(h, 47), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, ds)) : Bool}: PROOF.gr_star2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=gr_star2) # ... a double star takes any h def gr_star2(+r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, ds)) == G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, ds) : Bool}: PROOF.fe_ef (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=fe_ef) # cutting into one more piece and asking for an empty first piece is cutting into as many def fe_ef(+r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {fe_any(r, G.AaGCuts.empty_first(ds)) == G.AaGSeq.fits_any(r, ds) : Bool}: PROOF.fe_gr (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=fe_gr) def fe_gr(+r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {fe_any(r, G.AaGCuts.grow(h, ds)) == False{} : Bool}: PROOF.fe_cuts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=fe_cuts) def fe_cuts(+r: List<&2, G.AaGTok>, +s: List<&2, U32>) -> {fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), s)) == G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), s)) : Bool}: PROOF.glob.thm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=glob.thm) # the matcher agrees with the list model: induction on the sequence, and on # the path under a star def glob.thm(+seq: List<&2, G.AaGTok>, +s: List<&2, U32>) -> {G.AaGSeq.matches(seq, s) == G.AaGSeq.model(seq, s) : Bool}: PROOF.nfa.taut_nil (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=nfa.taut_nil) def nfa.taut_nil(+a: Bool, +n: Bool, +c: Bool, +b: Bool) -> {Bool.and(a, n) == Bool.or(Bool.and(a, n), Bool.or(Bool.and(c, False{}), Bool.and(b, False{}))) : Bool}: PROOF.nfa.taut_adv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=nfa.taut_adv) def nfa.taut_adv(+hb: Bool, +cin: Bool, +ain: Bool, +e: Bool, +p: Bool, +q: Bool, +r: Bool, +z: Bool) -> {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(hb, cin), False{}), ain), p), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), e), q), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), False{}), r), z))) == Bool.or(Bool.and(ain, p), Bool.or(Bool.and(cin, Bool.and(e, q)), Bool.or(Bool.and(hb, Bool.and(e, q)), z))) : Bool}: PROOF.nfa.taut_star (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=nfa.taut_star) def nfa.taut_star(+hb: Bool, +cin: Bool, +ain: Bool, +e: Bool, +p: Bool, +q: Bool, +r: Bool, +z: Bool) -> {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(hb, cin), e), ain), p), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), False{}), q), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), True{}), r), z))) == Bool.or(Bool.and(ain, p), Bool.or(Bool.and(cin, Bool.or(r, Bool.and(e, p))), Bool.or(Bool.and(hb, Bool.or(r, Bool.and(e, p))), z))) : Bool}: PROOF.nfa.taut_star2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=nfa.taut_star2) def nfa.taut_star2(+hb: Bool, +cin: Bool, +ain: Bool, +p: Bool, +q: Bool, +r: Bool, +z: Bool) -> {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(hb, cin), True{}), ain), p), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), False{}), q), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), True{}), r), z))) == Bool.or(Bool.and(ain, p), Bool.or(Bool.and(cin, Bool.or(r, p)), Bool.or(Bool.and(hb, Bool.or(r, p)), z))) : Bool}: PROOF.nfa.step (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=nfa.step) # one byte: the positions after it accept t exactly when, before it, the # positions (with the carried ones) accept h then t def nfa.step(+seq: List<&2, G.AaGTok>, +bs: List<&2, Bool>, +cin: Bool, +ain: Bool, +h: U32, +t: List<&2, U32>) -> {G.AaGNfa.sem(seq, G.AaGNfa.next(seq, bs, cin, ain, h), t) == Bool.or(Bool.and(ain, G.AaGSeq.matches(seq, t)), Bool.or(Bool.and(cin, G.AaGSeq.matches(seq, Con{h, t})), G.AaGNfa.sem(seq, bs, Con{h, t}))) : Bool}: PROOF.nfa.dead (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=nfa.dead) # no position active: nothing accepted def nfa.dead(+seq: List<&2, G.AaGTok>, +bs: List<&2, Bool>, +s: List<&2, U32>, +e: {G.AaGNfa.alive(bs) == False{} : Bool}) -> {G.AaGNfa.sem(seq, bs, s) == False{} : Bool}: PROOF.nfa.run (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=nfa.run) # the run: the positions accept the path (a: whether some position is active) def nfa.run(+s: List<&2, U32>, +a: Bool, +seq: List<&2, G.AaGTok>, +bs: List<&2, Bool>, +e: {G.AaGNfa.alive(bs) == a : Bool}) -> {G.AaGNfa.run(s, a, seq, bs) == G.AaGNfa.sem(seq, bs, s) : Bool}: PROOF.nfa.falses_dead (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=nfa.falses_dead) def nfa.falses_dead(+seq: List<&2, G.AaGTok>) -> {G.AaGNfa.alive(G.AaGNfa.falses(seq)) == False{} : Bool}: PROOF.nfa.start (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=nfa.start) # only the whole sequence active: what the backtracking matcher accepts def nfa.start(+seq: List<&2, G.AaGTok>, +s: List<&2, U32>) -> {G.AaGNfa.sem(seq, G.AaGNfa.start(seq), s) == G.AaGSeq.matches(seq, s) : Bool}: PROOF.nfa.start_alive (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=nfa.start_alive) def nfa.start_alive(+seq: List<&2, G.AaGTok>) -> {G.AaGNfa.alive(G.AaGNfa.start(seq)) == True{} : Bool}: PROOF.nfa.thm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=nfa.thm) def nfa.thm(+seq: List<&2, G.AaGTok>, +s: List<&2, U32>) -> {G.AaGSeq.run(seq, s) == G.AaGSeq.matches(seq, s) : Bool}: PROOF.glob.alts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=glob.alts) def glob.alts(+alts: List<&2, List<&2, G.AaGTok>>, +s: List<&2, U32>) -> {G.AaGlob.matches.go(alts, s) == G.AaGlob.model.go(alts, s) : Bool}: PROOF.glob.alts_ref (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=glob.alts_ref) def glob.alts_ref(+alts: List<&2, List<&2, G.AaGTok>>, +s: List<&2, U32>) -> {G.AaGlob.matches_ref.go(alts, s) == G.AaGlob.model.go(alts, s) : Bool}: PROOF.bits.minus_meets (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=bits.minus_meets) # what minus leaves never meets what it took away def bits.minus_meets(+a: List<&2, Bool>, +d: List<&2, Bool>) -> {P.AaBits.meets(P.AaBits.minus(a, d), d) == False{} : Bool}: PROOF.bits.nany_meets (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=bits.nany_meets) # a request with no bit set meets nothing def bits.nany_meets(+r: List<&2, Bool>, +d: List<&2, Bool>) -> {Bool.and(Bool.not(P.AaBits.any(r)), P.AaBits.meets(r, d)) == False{} : Bool}: PROOF.bits.covers_meets (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=bits.covers_meets) # a request that minus(a, d) covers does not meet d def bits.covers_meets(+a: List<&2, Bool>, +d: List<&2, Bool>, +r: List<&2, Bool>) -> {Bool.and(P.AaBits.covers(P.AaBits.minus(a, d), r), P.AaBits.meets(r, d)) == False{} : Bool}: PROOF.bits.or_assoc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=bits.or_assoc) def bits.or_assoc(+a: List<&2, Bool>, +b: List<&2, Bool>, +c: List<&2, Bool>) -> {P.AaBits.or(P.AaBits.or(a, b), c) == P.AaBits.or(a, P.AaBits.or(b, c)) : List<&2, Bool>}: PROOF.b.or_idem (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.or_idem) def b.or_idem(+a: Bool) -> {Bool.or(a, a) == a : Bool}: PROOF.bits.or_idem (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=bits.or_idem) def bits.or_idem(+a: List<&2, Bool>) -> {P.AaBits.or(a, a) == a : List<&2, Bool>}: PROOF.bits.or_nil_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=bits.or_nil_r) def bits.or_nil_r(+a: List<&2, Bool>) -> {P.AaBits.or(a, Nil{}) == a : List<&2, Bool>}: PROOF.pm.covers_meets (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=pm.covers_meets) def pm.covers_meets(+a: P.AaPerms, +d: P.AaPerms, +r: P.AaPerms) -> {Bool.and(P.AaPerms.covers(P.AaPerms.minus(a, d), r), P.AaPerms.meets(r, d)) == False{} : Bool}: PROOF.pm.minus_meets (https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=pm.minus_meets) def pm.minus_meets(+a: P.AaPerms, +d: P.AaPerms) -> {P.AaPerms.meets(P.AaPerms.minus(a, d), d) == False{} : Bool}: More: https://jend.leeeet.dev/packages/bend-osdev-apparmor.txt?definitions_offset=100