regexp.synthesis.clash.automata: Automata in Clash

Overview

This module consists of NFA and its simulation code at the Clash level. Most interesting type here have an equivalent type in the concrete layer and the associated syn function allows us to synthesis this entity in the concrete layer to the synthesis layer.

transition.t b s : The transitions expressed at the clash level transition.syn : Synthesize a concrete transition to the clash level. NFA: The NFA at the synthesis layer. syn: Synthesize an NFA in the concrete layer to the clash level.

Simulation

Given a string Ws of worlds now in the synthesis layer, the goal of the simulation is to figure out what is the possible set of the state the machine is in.

next tr st W: Computes the set of states the NFA would be in on a single input world W starting from any one of the states in st
consume Run the automata on the give thickend string and give the result.
success Check whether the current state is a success.
accept The language of thickend strings on which the simulation is successful.
correctness The correctness of the simulation in this context means that our simulation in this layer matches with the simulation in the concrete layer.

Module transition.
   Definition t b s := (b ~> relation.binary.t s)%syn.

   Definition syn {b s}(tr : concrete.automata.transition.t b s) : t ⟨ b ⟩ ⟨ s ⟩
     := function.syn (concrete.function.map (relation.syn) tr).

End transition.

Record NFA b s := { trans : transition.t b s;
                    start : clash.subset.t s;
                    final : clash.subset.t s;
  }.

Arguments trans {b s}.
Arguments start {b s}.
Arguments final {b s}.

Check if a given state is accepting

Definition success {b s} : [isSucc s ⇒ NFA b s → clash.subset.t s → bool ] :=
  fun nfa st ⇒ inhabited (intersection st (final nfa)).

Section Defn.
  Check clash.relation.img.
  Context {b s: Type}.

  Definition next :
    [ knownNat b , isSucc b , knownNat s , isSucc s ⇒ (transition.t b s → clash.subset.t s → clash.subset.t b → clash.subset.t s ) ] :=
      fun tr st W ⇒ big.union (idx:=b) (clash.function.map (clash.relation.img ^~ st) tr) W.

  Definition process :
    [ knownNat b , isSucc b , knownNat s , isSucc s ⇒ NFA b s → clash.subset.t s → clash.subset.t b → clash.subset.t s ] :=
    fun (mac : NFA b s) ⇒ next (trans mac).

  Definition consume :
    [ knownNat b , isSucc b , knownNat s , isSucc s ⇒
        NFA b s → seq (clash.subset.t b) → clash.subset.t s ] :=
    fun (mac : NFA b s) ⇒ foldl (process mac) (start mac).

  Definition accept : [ knownNat b , isSucc b , knownNat s , isSucc s ⇒
                           NFA b s → lang.lang (clash.subset.t b) ] :=
                         fun mac ⇒ success mac \o consume mac.

End Defn.

Require Import regexp.concrete.universe.
Require regexp.concrete.function.
Require regexp.concrete.automata.

Synthesizing automata form the concrete layer

Section Synthesis.
  Context {B St : universe.sort}.

  Definition syn (mac : concrete.automata.NFA B St) : NFA ⟨ B ⟩ ⟨ St ⟩ :=
    {|
      trans := transition.syn (concrete.automata.trans mac);
      start := subset.syn (concrete.automata.start mac);
      final := subset.syn (concrete.automata.final mac)
    |}.

  Lemma success_spec (nfa : concrete.automata.NFA B St) st :
    success (syn nfa) (subset.syn st) = concrete.automata.simulation.success nfa st.
    by rewrite /success intersection_spec inhabited_spec.
  Qed.

  Lemma next_spec (tr : concrete.automata.transition.t B St) st W
    : automata.next (transition.syn tr)(subset.syn st)(subset.syn W) = subset.syn (concrete.automata.simulation.next tr st W).
  Proof.
    rewrite /automata.next -bigunion_spec ?axioms.map_spec -?/(comp (concrete.function.map _) (concrete.function.map _) tr)
                              ?concrete.function.map_compose.

    set tr0 := concrete.function.map _ tr.
    set tr1 := concrete.function.map _ tr.
    suffices H : tr0 = tr1 by rewrite H.
    apply /concrete.function.map_eqfun.
    move ⇒ rl; by rewrite /comp img_spec.
  Qed.

  Context (mac : concrete.automata.NFA B St).
  Lemma process_spec st W :
    process (syn mac) (subset.syn st) (subset.syn W) = subset.syn (concrete.automata.simulation.process mac st W).
  Proof.
    by rewrite /process next_spec.
  Qed.

  Lemma consume_spec (Ws : seq (concrete.subset.t B)) :
    consume (syn mac) (map subset.syn Ws) = subset.syn (concrete.automata.simulation.consume mac Ws).
    rewrite /consume /concrete.automata.simulation.consume /start //=.
    suffices hyp : ∀ Wss st, foldl (process (syn mac)) (subset.syn st) [seq subset.syn i | i <- Wss]
                         = subset.syn (foldl (concrete.automata.simulation.process mac) st Wss) by rewrite hyp.

    elim ⇒ [|W Wss IH].
    - rewrite //=.
    - by move ⇒ st; rewrite //= process_spec IH.
  Qed.

Correctness of the simulation.

The subset.syn function allows us to go from subsets in the concrete layer to the synthesis layer. Therefore the comap sybset.syn contravariantly maps the language in this layer to the concrete layer. Thus the correctness here means that our simulation in the synthesis layer matches with the corresponding simulation in the concrete layer.

  Theorem correctness :
    (comap subset.syn (accept (syn mac)) ≡ concrete.automata.simulation.accept mac)%lan.
    move ⇒ Ws.
    by rewrite /comap /accept /concrete.automata.simulation.accept //= consume_spec success_spec.
  Qed.

End Synthesis.