regexp.synthesis: Synthesizing the certified hardware



Overview

  • synthesize: Takes a set of matching Rules and generate the machine out of it

The state machine

  • machine: The data type the captures the synthesized NFA together with the scanTable.
  • state: The state type of the machine.
  • start: Gives the starting state of the input machine
  • transition: Gives the transition function of the machine
  • isFinal: Checks whether a state of a given machine is accepting

Acceptance/rejection

  • accept: Check whether the machine accepts a given input
  • reject: Check whether the machine rejects a given input (for unit testing only not synthesis)

The correctness proof

  • correctness: Theorem that proves the correctness of the synthesized hardware. See the appropriate section for more details.


Record machine {I b s} := { scanTable : b ~> I → bool;
                            nfa : NFA b s
  }.

Arguments machine : clear implicits.


Definition state := clash.subset.t.
Definition start {I b s} : machine I b s → state s
  := clash.automata.start \o nfa.
Definition isFinal {I b s} : machine I b s → state s → bool
  := clash.automata.success \o nfa.

Definition mapper {Inp b} (tfn : (b ~> Inp → bool)) : Inp → clash.subset.t b := fun inp ⇒ function.map (fun f ⇒ f inp) tfn.
Definition scanner {I B s} (mac : machine I B s) := mapper (scanTable mac).

Definition transition {Inp b s} : [knownNat b, isSucc b, knownNat s, isSucc s ⇒ machine Inp b s → _ ] :=
  fun mac st ⇒ process (nfa mac) st \o scanner mac.


Definition runOnList {Inp b s} : [knownNat b, isSucc b, knownNat s, isSucc s ⇒
                                    machine Inp b s → seq Inp → clash.subset.t s ]
  := fun mac ⇒ foldl (transition mac) (start mac).

Definition accept {Inp b s} : [knownNat b, isSucc b, knownNat s, isSucc s ⇒
                                 machine Inp b s → seq Inp → bool ]
  := fun mac ⇒ success (nfa mac) \o runOnList mac.

Definition reject {Inp b s} : [knownNat b, isSucc b, knownNat s, isSucc s ⇒
                                 machine Inp b s → seq Inp → bool ]
  := fun mac xs ⇒ ~~ accept mac xs.

Definition synthesize {I} (rls : Rule I)
  := {|
    scanTable := function.syn (atomTable rls);
    nfa := automata.syn (re2nfa (regexp rls))
  |}.


Proof of correctness

Fix a set of rules rls
Section Correctness.

  Context {I : Type} (rls : Rule I).

The two languages of interest are
1. The language associated with the rules rls given by the rule.language rls.
2. The language accepted by the synthesized hardware given by accept (synthesize rls).
The correctness of the hardware essentially states that these two languages are the same.

  Theorem correctness : (accept (synthesize rls) ≡ rule.language rls)%lan.

    set mac := synthesize rls.     have haccept_comap : (accept mac ≡ lang.comap (scanner mac) (clash.automata.accept (nfa mac)))%lan
      by move ⇒ Ws; rewrite ?/accept /comap //= /runOnList /consume /start /comp -?foldl_map.
    rewrite haccept_comap {haccept_comap}.

    set scan := rule.encode (atomTable rls).
    have hscanner_spec : scanner mac =1 subset.syn \o scan
      by move ⇒ i; rewrite /comp /scanner /scan /mapper map_spec.

    by rewrite hscanner_spec
         lang.comap_comap
         clash.automata.correctness
         concrete.automata.simulation.correctness
         automata.build.correctness
         rule.interpretation /iLanguage /interpret /scan /wLanguage /comp.
  Qed.

End Correctness.