libinput-rs 0.2.2

Fail-open Rust touchpad companion and drop-in libinput ABI replacement
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73

module fail_open_model
  implicit none
  private

  type, public :: input_state
    private
    logical :: sink_ready = .false.
    logical :: grabbed = .false.
  end type input_state

  public :: prepare_sink, attempt_grab, release_grab, forwarding_failed
  public :: invariant_holds, is_grabbed

contains

  subroutine prepare_sink(state)
    type(input_state), intent(inout) :: state
    state%sink_ready = .true.
  end subroutine prepare_sink

  logical function attempt_grab(state) result(accepted)
    type(input_state), intent(inout) :: state
    accepted = state%sink_ready .and. .not. state%grabbed
    if (accepted) state%grabbed = .true.
  end function attempt_grab

  subroutine release_grab(state)
    type(input_state), intent(inout) :: state
    state%grabbed = .false.
  end subroutine release_grab

  subroutine forwarding_failed(state)
    type(input_state), intent(inout) :: state
    call release_grab(state)
  end subroutine forwarding_failed

  pure logical function invariant_holds(state) result(valid)
    type(input_state), intent(in) :: state
    valid = .not. state%grabbed .or. state%sink_ready
  end function invariant_holds

  pure logical function is_grabbed(state) result(grabbed)
    type(input_state), intent(in) :: state
    grabbed = state%grabbed
  end function is_grabbed

end module fail_open_model

program verify_fail_open
  use fail_open_model
  implicit none

  type(input_state) :: state
  logical :: accepted

  if (.not. invariant_holds(state)) error stop "invalid initial state"

  accepted = attempt_grab(state)
  if (accepted) error stop "grab accepted without a prepared sink"
  if (is_grabbed(state)) error stop "failed grab changed ownership"

  call prepare_sink(state)
  accepted = attempt_grab(state)
  if (.not. accepted) error stop "grab rejected with a prepared sink"
  if (.not. invariant_holds(state)) error stop "grab violated invariant"

  accepted = attempt_grab(state)
  if (accepted) error stop "duplicate grab accepted"

  call forwarding_failed(state)
  if (is_grabbed(state)) error stop "forwarding failure retained grab"
  if (.not. invariant_holds(state)) error stop "release violated invariant"
end program verify_fail_open