darcsweb - verified/path_pure.v

(** Verified pure functions for file path validation.
    Extracted to Haskell for use in the DarcsWeb application. *)

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

Import ListNotations.
Open Scope string_scope.
Open Scope bool_scope.

(** -- Helper functions -- *)

(** Check if a string is empty. *)
Definition string_is_empty (s : string) : bool :=
  match s with
  | EmptyString => true
  | _ => false
  end.

(** Remove '/' characters from a string. *)
Fixpoint remove_slashes (s : string) : string :=
  match s with
  | EmptyString => EmptyString
  | String c rest =>
    if Ascii.eqb c "/"%char then remove_slashes rest
    else String c (remove_slashes rest)
  end.

(** Check if a string starts with '.'. *)
Definition starts_with_dot (s : string) : bool :=
  match s with
  | String c _ => Ascii.eqb c "."%char
  | EmptyString => false
  end.

(** Get the last character of a string. *)
Fixpoint last_char (s : string) : option ascii :=
  match s with
  | EmptyString => None
  | String c EmptyString => Some c
  | String _ rest => last_char rest
  end.

(** -- Split path -- *)

(** Split a string on '/' into segments (accumulator-based). *)
Fixpoint split_path_aux (acc : string) (s : string) {struct s} : list string :=
  match s with
  | EmptyString => acc :: nil
  | String c rest =>
    if Ascii.eqb c "/"%char then
      acc :: split_path_aux EmptyString rest
    else
      split_path_aux (String.append acc (String c EmptyString)) rest
  end.

(** Split a file path on '/' separators. *)
Definition split_path (s : string) : list string :=
  match s with
  | EmptyString => nil
  | _ => split_path_aux EmptyString s
  end.

(** -- Safe subpath validation -- *)

(** Filter out empty strings from a list. *)
Fixpoint filter_nonempty (l : list string) : list string :=
  match l with
  | nil => nil
  | x :: xs =>
    if string_is_empty x then filter_nonempty xs
    else x :: filter_nonempty xs
  end.

(** Check if all elements satisfy a predicate. *)
Fixpoint all_true (f : string -> bool) (l : list string) : bool :=
  match l with
  | nil => true
  | x :: xs => f x && all_true f xs
  end.

(** Check if a single path segment is safe. *)
Definition is_safe_segment (seg : string) : bool :=
  let name := remove_slashes seg in
  negb (string_is_empty name)
  && negb (String.eqb name "..")
  && negb (String.eqb name ".")
  && negb (String.eqb name "_darcs")
  && negb (String.eqb name ".git")
  && negb (starts_with_dot name).

(** Check whether a subpath is safe (no hidden/internal segments). *)
Definition is_safe_sub_path (sub : string) : bool :=
  let segments := filter_nonempty (split_path sub) in
  match segments with
  | nil => false
  | _ => all_true is_safe_segment segments
  end.

(** -- Trailing slash -- *)

(** Ensure a path ends with exactly one '/'. *)
Definition add_trailing_slash (s : string) : string :=
  match s with
  | EmptyString => "/"
  | _ =>
    match last_char s with
    | Some c =>
      if Ascii.eqb c "/"%char then s
      else String.append s "/"
    | None => "/"
    end
  end.

(* -- Extraction setup -- *)
Set Extraction Output Directory "../gen".
Extraction Language Haskell.

Extract Inlined Constant String.append => "(Prelude.++)".

Extraction "PathPure"
  split_path
  is_safe_sub_path
  add_trailing_slash.