support natspec preconditions

[anvacaru]

This feature adds support for parsing and enforcing Solidity NatSpec preconditions (marked with @custom:kontrol-precondition) during symbolic execution.

1. Define the NatSpec Grammar (natspec-grammar.md)
   Created a K syntax module that defines how to parse Solidity expressions, including operators, precedence rules, and symbol annotations.

2. Set up KDist Build Target
   Added an independent KDist target for NATSPEC that uses gen_glr_bison_parser to compile the grammar into a binary parser.

3. Extract Preconditions from Solidity
   Modified solc-to-k to fetch preconditions from NatSpec devdocs, specifically looking for the custom:kontrol-precondition tag.

4. Parse Precondition Strings
   When generating the initial proof state (init_cterm), parse each precondition string using the compiled parser binary.

5. Convert Kore to KAST
   Transform the parser's Kore output into Kast using kore_to_kast.

6. Map Operators to K Symbols
   Use the NATSPEC_TO_K_OPERATORS dictionary to translate Solidity operators (e.g., SolidityLE/_<=Exp_) to their K framework equivalents (e.g., _<=Int_).

7. Transform Arguments Recursively
   For each argument in the parsed expression:

• Id tokens: Look up the identifier in the method's input parameters and replace with the corresponding KVariable
• Native tokens (Int, Bool): Keep as-is
• Nested KApply: Apply this transformation recursively

Create a new KApply with the translated operator and transformed arguments.

8. Add Constraints to Initial State
   Append the transformed preconditions as constraints to init_cterm, ensuring the symbolic execution respects these conditions.

[anvacaru]

As we don't run this test with CSE, this is the only precondition processed.

[tothtamas28]

Did you consider the following alternatives:

1. Using a Solidity parser library (e.g. https://github.com/OpenZeppelin/sgp)
2. Implementing the parser using a parser generator (e.g. https://github.com/lark-parser/lark)

With both approaches, you can avoid the burden of kompiling and distributing the parser. With (1), you get support for all the remaining features (x[1][2], etc.) out of the box.

[anvacaru]

I wasn't aware of sgp, but I will look into it. There was a previous attempt at implementing this feature in #662 using Antlr. But we already have the Bison/Flex parsers shipped with K that we could use.