Instalacja
Wybierz klienta i sklonuj repozytorium do odpowiedniego katalogu skilli.
Instalacja
O skillu
Umiejętność do weryfikacji plików F* (.fst i .fsti) oraz interpretacji błędów zgłaszanych przez kompilator. Pozwala debugować niepowodzenia weryfikacji, sprawdzać kompletność dowodów i optymalizować wydajność za pomocą diagnostyki SMT. Obsługuje zaawansowane opcje takie jak statystyki zapytań, dzielenie zapytań i kontrolę limitów zasobów dla złożonych dowodów.
Jak używać
Przygotuj plik F* do weryfikacji — upewnij się, że masz plik z rozszerzeniem .fst lub .fsti zawierający kod, który chcesz zweryfikować.
Uruchom podstawową weryfikację poleceniem fstar.exe Module.fst, gdzie Module.fst to nazwa Twojego pliku. Kompilator przeanalizuje kod i zgłosi błędy weryfikacji, jeśli istnieją.
Jeśli napotkasz błąd "Could not prove post-condition", dodaj pośrednie asercje (assert statements) w kodzie, jawnie wywołaj odpowiednie lematy lub użyj funkcji porównania dla kolekcji takich jak Seq.equal czy Set.equal.
W przypadku błędu "Identifier not found" sprawdź importy modułów (open, module X = ...), kolejność definicji (F* jest wrażliwy na kolejność) i poprawność nazw symboli.
Jeśli weryfikacja jest zbyt wolna lub timeout (rlimit exhausted), podziel dowód na mniejsze lematy, zmniejsz fuel w opcjach (#push-options "--fuel 0 --ifuel 0") lub użyj opcji diagnostycznych: fstar.exe --query_stats --split_queries always Module.fst, aby zidentyfikować problematyczne zapytania SMT.
Dla zaawansowanego debugowania możesz dodać opcje takie jak --log_queries do analizy zapytań SMT, --z3refresh do odświeżenia Z3 między zapytaniami, lub ustawić limity zasobów w pliku za pomocą #push-options "--z3rlimit 10".