rocq-simulate-author

Skill do tworzenia i aktualizacji plików simulate w repozytorium Rocq. Automatyzuje dodawanie definicji simulate, które odzwierciedlają zachowanie kodu Rust na odpowiednim poziomie abstrakcji, oraz generowanie odpowiadających im lematów eq łączących funkcje run* z definicjami simulate. Obsługuje eksplicytne importy, makra projektu (gas_macro, push_macro) i konwencje proof/admission. Kompiluje się z flagami projektu i utrzymuje spójność z istniejącymi plikami w folderze.

1. Zlokalizuj plik źródłowy links i przykładowe pliki simulate w sąsiedztwie. Przeczytaj odpowiadający plik links (w ścieżce .../links/...), aby wyodrębnić sygnaturę run_* i kolejność parametrów. Sprawdź jeden sąsiedni plik simulate w tym samym folderze, aby zapoznać się ze stylem projektu.

2. Zbuduj importy jawnie na początku pliku. Dodaj Require Import simulate.RocqOfRust. jako pierwszy import, następnie dodaj importy linków i simulate używane przez definicję. Dodawaj dodatkowe importy tylko wtedy, gdy błędy kompilacji tego wymagają.

3. Napisz definicję simulate, która odzwierciedla intencję kodu Rust i jest spójna z plikami w tym folderze. Używaj istniejących makr projektu (gas_macro, push_macro) konsekwentnie. Unikaj nadmiernego dopasowywania dowodów w samej definicji.

4. Napisz lemat _eq, który łączy run_* z definicją simulate. Dopasuj kolejność argumentów do funkcji run_*. Preferuj założenia Run na poziomie klasy w plikach Eq-style. Jeśli dowód nie jest gotowy, pozostaw Admitted, chyba że użytkownik wyraźnie tego nie chciał.

5. Skompiluj plik za pomocą: coqc -R . RocqOfRust -impredicative-set ścieżka/do/pliku.v. Napraw minimalne problemy (importy, adnotacje typów, kolejność argumentów) i iteruj aż do kompilacji bez błędów.