模块分析：MenhirLib

1. 角色定位

MenhirLib/ 是 Menhir 解析器相关的验证与解释库，用于支持 cparser 的解析正确性与提取。

2. 内容概览

• Interpreter.v / Interpreter_complete.v：解析器解释器
• Validator_*：校验与一致性证明
• Grammar.v / Automaton.v：语法与自动机构造

3. 与仓库的耦合

• 供 cparser 的 Menhir 解析器使用
• 在解析正确性与一致性证明中被引用