LAWS.execve_nonroot_permitted: law of bend-osdev-caps@0.1.0.0
Import: import bend-osdev-caps@0.1.0.0/LAWS.bend as LAWS
Lines 124-140 of bend-osdev-caps@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-caps@0.1.0.0/LAWS.bend&start_line=124&end_line=140

import Base
import bend-osdev-caps@0.1.0.0/caps.bend as C
import bend-osdev-caps@0.1.0.0/exec.bend as E

# "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
  for +sv: U32
  for +nr: Bool
  for +na: Bool
  for +u: U32
  for +ign: Bool
  {C.CapState.permitted(E.Caps.execve.sets(k, C.CapCred{r, e, sv, nr, na, s}, C.CapFile{u, False{}, False{}, None{}}, ign)) == C.CapState.ambient(s) : C.CapSet()}

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&name=ex.nonroot_p
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapCred
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapFile
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapSet
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapState
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapState.ambient
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapState.permitted
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapsKernel
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/exec.bend&name=Caps.execve.sets