mirror of
https://github.com/Z3Prover/z3
synced 2026-04-14 00:06:28 +00:00
4a2accf10c
- IEEE754.fst: fix multi-binding in assume val signatures (F* 2026 syntax),
change float from Type0 to eqtype for equality support, generalize fma NaN
axioms to handle any-NaN inputs (ax_fma_any_nan_y/x/z)
- FPARewriterRules.fst: add explicit #eb #sb type arguments to axiom calls
where F* 2026 cannot infer them, use ax_fma_any_nan_y for proofs where
y is an arbitrary NaN rather than the canonical nan constant
- RewriteCodeGen.fst: fix F* 2026 API changes: FStar.Sealed.unseal->unseal,
C_Bool->{C_True,C_False}, List.Tot.iter->iter, FStar.Reflection.V2.inspect
->inspect_ln for term_view, post from C_Lemma pre->post with Tv_Abs peel,
b2t unwrapping, lemma_ref via pack_fv instead of quote for polymorphic lemmas,
per-branch offset tracking for Pat_Var in match branches
- .github/workflows/fstar-extract.yml: update to F* 2026.03.24 with correct
archive name fstar-v{VERSION}-Linux-x86_64.tar.gz
- fstar/README.md and extract.sh: update version references to 2026.03.24
Extraction now produces correct output:
expr *c, *t, *e;
if (m().is_ite(arg1, c, t, e)) {
result = m().mk_ite(c, m_util.mk_is_nan(t), m_util.mk_is_nan(e));
return BR_REWRITE2;
}
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/0a30f342-3941-4952-a54f-1bee84b022ef
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
47 lines
1.2 KiB
Bash
Executable file
47 lines
1.2 KiB
Bash
Executable file
#!/usr/bin/env bash
|
|
# extract.sh
|
|
#
|
|
# Run the Meta-F* reflection-based extraction to generate C++ rewrite rules
|
|
# from the F* lemmas in this directory.
|
|
#
|
|
# Usage (from the fstar/ directory):
|
|
# ./extract.sh
|
|
#
|
|
# Usage (from the repo root):
|
|
# fstar/extract.sh
|
|
#
|
|
# Output:
|
|
# Prints the generated C++ rules to stdout.
|
|
# Exits non-zero if F* typechecking or tactic execution fails.
|
|
#
|
|
# Requirements:
|
|
# fstar.exe on PATH (F* 2024.09.05 or later recommended).
|
|
# The three source files must be present:
|
|
# IEEE754.fst, FPARewriterRules.fst, RewriteCodeGen.fst
|
|
|
|
set -euo pipefail
|
|
|
|
SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
|
|
cd "$SCRIPT_DIR"
|
|
|
|
if ! command -v fstar.exe &>/dev/null; then
|
|
echo "ERROR: fstar.exe not found on PATH." >&2
|
|
echo "Install F* 2026.03.24+ from https://github.com/FStarLang/FStar/releases" >&2
|
|
exit 1
|
|
fi
|
|
|
|
echo "=== F* version ===" >&2
|
|
fstar.exe --version >&2
|
|
|
|
echo "" >&2
|
|
echo "=== Running Meta-F* extraction ===" >&2
|
|
|
|
# F* writes tactic print() output to stdout.
|
|
# Verification progress and errors go to stderr.
|
|
fstar.exe --include . \
|
|
IEEE754.fst \
|
|
FPARewriterRules.fst \
|
|
RewriteCodeGen.fst
|
|
|
|
echo "" >&2
|
|
echo "=== Extraction complete ===" >&2
|