darcsweb - verified/path_pure_proofs.v

(** Correctness proofs for path validation functions. *)

From Stdlib Require Import Ascii String Bool List.
Require Import path_pure.

Import ListNotations.
Open Scope string_scope.
Open Scope bool_scope.

(** -- split_path -- *)

Lemma split_path_empty : split_path "" = nil.
Proof. reflexivity. Qed.

Lemma split_path_single : split_path "a" = "a" :: nil.
Proof. vm_compute. reflexivity. Qed.

Lemma split_path_simple : split_path "a/b" = "a" :: "b" :: nil.
Proof. vm_compute. reflexivity. Qed.

Lemma split_path_three : split_path "src/main/hs" = "src" :: "main" :: "hs" :: nil.
Proof. vm_compute. reflexivity. Qed.

Lemma split_path_leading_slash : split_path "/foo" = "" :: "foo" :: nil.
Proof. vm_compute. reflexivity. Qed.

Lemma split_path_trailing_slash : split_path "foo/" = "foo" :: "" :: nil.
Proof. vm_compute. reflexivity. Qed.

(** -- is_safe_sub_path: rejection of dangerous paths -- *)

Lemma safe_rejects_empty : is_safe_sub_path "" = false.
Proof. reflexivity. Qed.

Lemma safe_rejects_dotdot : is_safe_sub_path ".." = false.
Proof. vm_compute. reflexivity. Qed.

Lemma safe_rejects_dot : is_safe_sub_path "." = false.
Proof. vm_compute. reflexivity. Qed.

Lemma safe_rejects_darcs : is_safe_sub_path "_darcs" = false.
Proof. vm_compute. reflexivity. Qed.

Lemma safe_rejects_git : is_safe_sub_path ".git" = false.
Proof. vm_compute. reflexivity. Qed.

Lemma safe_rejects_hidden : is_safe_sub_path ".hidden" = false.
Proof. vm_compute. reflexivity. Qed.

Lemma safe_rejects_nested_dotdot : is_safe_sub_path "foo/../bar" = false.
Proof. vm_compute. reflexivity. Qed.

Lemma safe_rejects_darcs_nested : is_safe_sub_path "repo/_darcs/prefs" = false.
Proof. vm_compute. reflexivity. Qed.

Lemma safe_rejects_hidden_nested : is_safe_sub_path "src/.secret/file" = false.
Proof. vm_compute. reflexivity. Qed.

(** -- is_safe_sub_path: acceptance of legitimate paths -- *)

Lemma safe_accepts_simple : is_safe_sub_path "src" = true.
Proof. vm_compute. reflexivity. Qed.

Lemma safe_accepts_nested : is_safe_sub_path "src/Main.hs" = true.
Proof. vm_compute. reflexivity. Qed.

Lemma safe_accepts_deep : is_safe_sub_path "src/DarcsWeb/Html.hs" = true.
Proof. vm_compute. reflexivity. Qed.

Lemma safe_accepts_underscore : is_safe_sub_path "my_module/test" = true.
Proof. vm_compute. reflexivity. Qed.

(** -- add_trailing_slash -- *)

Lemma trailing_slash_empty : add_trailing_slash "" = "/".
Proof. reflexivity. Qed.

Lemma trailing_slash_already : add_trailing_slash "/foo/" = "/foo/".
Proof. vm_compute. reflexivity. Qed.

Lemma trailing_slash_adds : add_trailing_slash "/foo" = "/foo/".
Proof. vm_compute. reflexivity. Qed.

Lemma trailing_slash_root : add_trailing_slash "/" = "/".
Proof. vm_compute. reflexivity. Qed.

Lemma trailing_slash_idempotent_example :
  add_trailing_slash (add_trailing_slash "/home/repos") =
  add_trailing_slash "/home/repos".
Proof. vm_compute. reflexivity. Qed.