0 | ||| Types for the DFA string searching algorithm.
  1 | module Data.ByteString.Search.DFA.Types
  2 |
  3 | import Data.Array.Core
  4 | import Data.Bits
  5 | import Data.ByteString
  6 | import Data.DArray
  7 | import Data.Enum
  8 | import Data.Linear.Ref1
  9 |
 10 | %hide Data.Buffer.Core.get
 11 | %hide Data.Buffer.Core.set
 12 | %hide Data.List.Elem.get
 13 |
 14 | %default total
 15 |
 16 | ||| One greater than the maximum number of DFA states whose flattened
 17 | ||| 256-way transition table can be represented without overflow in
 18 | ||| `Bits32`.
 19 | |||
 20 | ||| A DFA must have fewer than 2^24 states because every state owns 256
 21 | ||| transition entries:
 22 | |||
 23 | |||     states * 256 < 2^32
 24 | |||
 25 | public export
 26 | dfaStateLimit : Bits32
 27 | dfaStateLimit = 0x01000000
 28 |
 29 | ||| Evidence that a DFA state count can safely be used to construct a
 30 | ||| flattened 256-way transition table using `Bits32` indexing.
 31 | |||
 32 | ||| The proof stored by `Index` is erased at runtime.
 33 | |||
 34 | public export
 35 | DFAStateCount : Type
 36 | DFAStateCount = Index dfaStateLimit
 37 |
 38 | ||| A valid state in a DFA containing `states` states.
 39 | |||
 40 | ||| The underlying state number is represented by `Index`, so its proof that
 41 | ||| the state lies in `[0, states)` is erased at runtime.
 42 | |||
 43 | public export
 44 | DFAState : Bits32 -> Type
 45 | DFAState = Index
 46 |
 47 | ||| A valid DFA transition coordinate.
 48 | |||
 49 | ||| `state` is already known to be within the DFA's state range, while `byte`
 50 | ||| is intrinsically limited to the 256 possible byte values.
 51 | |||
 52 | public export
 53 | record DFAIndex (states : Bits32) where
 54 |   constructor MkDFAIndex
 55 |   state : Index states
 56 |   byte  : Bits8
 57 |
 58 | ||| Proof that flattening a valid DFA state and input byte yields a valid
 59 | ||| transition-table index.
 60 | |||
 61 | ||| `statesPrf` guarantees that `states * 256` cannot overflow `Bits32`.
 62 | ||| `statePrf` guarantees that `state < states`, while a `Bits8` value is
 63 | ||| intrinsically smaller than 256.
 64 | |||
 65 | ||| This function and all of its proof arguments are erased at runtime.
 66 | |||
 67 | 0 dfaIndexLT :  (state : Bits32)
 68 |              -> {states : Bits32}
 69 |              -> (0 statesPrf : states < Data.ByteString.Search.DFA.Types.dfaStateLimit)
 70 |              -> (0 statePrf : state < states)
 71 |              -> (byte : Bits8)
 72 |              -> ((state * 256) + cast byte) < (states * 256)
 73 | dfaIndexLT state statesPrf statePrf byte =
 74 |   believe_me ()
 75 |
 76 | ||| Flatten a DFA state and input byte into a transition-table index.
 77 | |||
 78 | ||| The resulting `Index` is constructed directly from statically carried
 79 | ||| bounds evidence. No dynamic range check is performed.
 80 | |||
 81 | ||| The DFA state-count proof guarantees that multiplication by 256 cannot
 82 | ||| overflow `Bits32`.
 83 | |||
 84 | export %inline
 85 | dfaIndex :  {states : Bits32}
 86 |          -> {auto 0 statesPrf : states < Data.ByteString.Search.DFA.Types.dfaStateLimit}
 87 |          -> DFAIndex states
 88 |          -> Index (states * 256)
 89 | dfaIndex (MkDFAIndex (I state {prf}) byte) =
 90 |   I ((state * 256) + cast byte) {prf = dfaIndexLT state statesPrf prf byte}
 91 |
 92 | ||| Return the runtime state number represented by a valid DFA state.
 93 | |||
 94 | ||| The bound proof carried by `Index` is erased, so this operation is
 95 | ||| simply extraction of the underlying `Bits32` value.
 96 | |||
 97 | export %inline
 98 | dfaStateValue : DFAState states -> Bits32
 99 | dfaStateValue (I state) = state
100 |
101 | ||| Construct the valid flattened transition-table index for a DFA state and
102 | ||| input byte.
103 | |||
104 | ||| No dynamic bounds check is performed. The state-count bound and state
105 | ||| bound are carried exclusively as erased evidence.
106 | |||
107 | export %inline
108 | dfaTransitionIndex :  {states : Bits32}
109 |                    -> {auto 0 statesPrf : states < Data.ByteString.Search.DFA.Types.dfaStateLimit}
110 |                    -> DFAState states
111 |                    -> Bits8
112 |                    -> Index (states * 256)
113 | dfaTransitionIndex state byte =
114 |   dfaIndex (MkDFAIndex state byte)
115 |
116 | ||| Mutable DFA transition storage.
117 | |||
118 | ||| The underlying pointer is an Idris primitive array containing
119 | ||| `states * 256` transitions.
120 | |||
121 | public export
122 | record DFATable (s : Type) (states : Bits32) where
123 |   constructor MkDFATable
124 |   arr : AnyPtr
125 |
126 | ||| Allocate an uninitialized DFA transition table.
127 | |||
128 | export
129 | newDFATable :  {states : Bits32}
130 |             -> {auto 0 statesPrf : states < Data.ByteString.Search.DFA.Types.dfaStateLimit}
131 |             -> F1 s (DFATable s states)
132 | newDFATable {states} t =
133 |   let arr # t := ffi (prim__emptyArray $ cast (states * 256)) t
134 |     in MkDFATable arr # t
135 |
136 | ||| Read the next DFA state for a current state and input byte.
137 | |||
138 | ||| The flattened transition index is already bounded, so no explicit
139 | ||| `tryIndex` or `tryNatToFin` conversion occurs in the search loop.
140 | |||
141 | ||| The primitive array is accessed directly using the prevalidated
142 | ||| flattened `Index`.
143 | |||
144 | export %inline
145 | dfaTransition :  {states : Bits32}
146 |               -> {auto 0 statesPrf : states < Data.ByteString.Search.DFA.Types.dfaStateLimit}
147 |               -> DFATable s states
148 |               -> DFAState states
149 |               -> Bits8
150 |               -> F1 s (DFAState states)
151 | dfaTransition table state byte t =
152 |   let I index = dfaTransitionIndex state byte
153 |     in believe_me (prim__arrayGet table.arr (cast index)) # t
154 |
155 | ||| Write a DFA transition.
156 | |||
157 | ||| The flattened index is derived from an already-bounded DFA state and
158 | ||| byte, avoiding any explicit dynamic bounds conversion.
159 | |||
160 | ||| The primitive array is written directly using the prevalidated
161 | ||| flattened `Index`.
162 | |||
163 | export %inline
164 | setDFATransition :  {states : Bits32}
165 |                  -> {auto 0 statesPrf : states < Data.ByteString.Search.DFA.Types.dfaStateLimit}
166 |                  -> DFATable s states
167 |                  -> DFAState states
168 |                  -> Bits8
169 |                  -> DFAState states
170 |                  -> F1' s
171 | setDFATransition table state byte next =
172 |   let I index = dfaTransitionIndex state byte
173 |     in ffi (prim__arraySet table.arr (cast index) (believe_me next))
174 |
175 | ||| Runtime description of a valid DFA state space.
176 | |||
177 | ||| `states` is the number of states in the DFA. The erased proofs establish
178 | ||| that the state count is positive and small enough for the flattened
179 | ||| 256-way transition table to fit within the `Bits32` index space.
180 | |||
181 | public export
182 | record DFAStateSpace where
183 |   constructor MkDFAStateSpace
184 |   states : Bits32
185 |   0 statesPositive : 0 < states
186 |   0 statesBounded : states < Data.ByteString.Search.DFA.Types.dfaStateLimit
187 |
188 | ||| Construct the state space for a DFA matching `bs`.
189 | |||
190 | ||| A pattern of length `n` requires `n + 1` states, including state zero.
191 | ||| The upper-bound check is performed once during DFA construction. All
192 | ||| subsequent state and transition indexing carries erased `Index` proofs
193 | ||| and requires no repeated bounds validation.
194 | |||
195 | export
196 | dfaStateSpace : ByteString -> Maybe DFAStateSpace
197 | dfaStateSpace bs =
198 |   let states : Bits32
199 |       states = cast $ S (length bs)
200 |     in case tryIndex {r = dfaStateLimit} states of
201 |          Nothing                =>
202 |            Nothing
203 |          Just (I states' {prf}) =>
204 |            Just (MkDFAStateSpace states' (believe_me ()) prf)
205 |
206 | ||| A constructed DFA transition automaton.
207 | |||
208 | ||| The runtime state-space description is packaged together with a
209 | ||| transition table indexed by that state count.
210 | |||
211 | ||| Every transition stored in the table is itself a valid `DFAState`,
212 | ||| allowing a lookup result to feed directly into the next lookup.
213 | |||
214 | public export
215 | record DFAutomaton (s : Type) where
216 |   constructor MkDFAutomaton
217 |   space : DFAStateSpace
218 |   table : DFATable s space.states
219 |
220 | ||| Convert a `Nat` state number into a valid state of the supplied DFA
221 | ||| state space.
222 | |||
223 | ||| This helper is used only while constructing the DFA. Search-time
224 | ||| transitions already produce bounded states directly and therefore do not
225 | ||| require this check.
226 | |||
227 | export
228 | toDFAState :  (space : DFAStateSpace)
229 |            -> Nat
230 |            -> Maybe (DFAState space.states)
231 | toDFAState space n =
232 |   tryIndex {r = space.states} (cast n)
233 |
234 | ||| State zero for a valid DFA state space.
235 | |||
236 | ||| No dynamic check is required because every DFA state space is known to
237 | ||| contain at least one state.
238 | |||
239 | export
240 | zeroDFAState :  (space : DFAStateSpace)
241 |              -> DFAState space.states
242 | zeroDFAState space =
243 |   I 0 {prf = space.statesPositive}
244 |