diff --git a/.github/workflows/fstar-extract.yml b/.github/workflows/fstar-extract.yml index 3e3072f07..ec4473ce5 100644 --- a/.github/workflows/fstar-extract.yml +++ b/.github/workflows/fstar-extract.yml @@ -44,14 +44,14 @@ jobs: # ----------------------------------------------------------------------- - name: Install F* env: - FSTAR_VERSION: "2024.09.05" + FSTAR_VERSION: "2026.03.24" run: | - ARCHIVE="fstar_v${FSTAR_VERSION}_Linux_x86_64.tar.gz" + ARCHIVE="fstar-v${FSTAR_VERSION}-Linux-x86_64.tar.gz" URL="https://github.com/FStarLang/FStar/releases/download/v${FSTAR_VERSION}/${ARCHIVE}" echo "Downloading F* ${FSTAR_VERSION} from ${URL}" >&2 curl -fsSL -o "/tmp/${ARCHIVE}" "${URL}" mkdir -p "$HOME/fstar" - tar -xzf "/tmp/${ARCHIVE}" -C "$HOME/fstar" --strip-components=1 + tar -xzf "/tmp/${ARCHIVE}" -C "$HOME/fstar" --strip-components=2 echo "$HOME/fstar/bin" >> "$GITHUB_PATH" - name: Verify F* installation diff --git a/fstar/FPARewriterRules.fst b/fstar/FPARewriterRules.fst index 8594ab182..766edf536 100644 --- a/fstar/FPARewriterRules.fst +++ b/fstar/FPARewriterRules.fst @@ -149,7 +149,7 @@ let lemma_fma_zero_const_nan_inf_arm (is_nan y = true || is_inf y = true)) (ensures is_nan (fp_fma rm zero_val y z) = true) = if is_nan y = true then - ax_fma_nan_y rm zero_val z + ax_fma_any_nan_y rm zero_val y z else begin ax_zero_mul_inf rm zero_val y; ax_fma_nan_mul rm zero_val y z @@ -182,7 +182,7 @@ let lemma_fma_zero_general_nan_inf_arm (is_nan y = true || is_inf y = true)) (ensures is_nan (fp_fma rm zero_val y z) = true) = if is_nan y = true then - ax_fma_nan_y rm zero_val z + ax_fma_any_nan_y rm zero_val y z else begin ax_zero_mul_inf rm zero_val y; ax_fma_nan_mul rm zero_val y z @@ -229,7 +229,7 @@ let lemma_fma_zero_product_sign let lemma_is_nan_to_fp_int (#eb #sb: pos) (rm: rounding_mode) (x: int) : Lemma (is_nan (to_fp_of_int #eb #sb rm x) = false) = - ax_to_fp_int_not_nan rm x + ax_to_fp_int_not_nan #eb #sb rm x (* --- 2b: isInf --- *) @@ -245,32 +245,32 @@ let lemma_is_inf_to_fp_int_rne (#eb #sb: pos) (x: int) : Lemma (is_inf (to_fp_of_int #eb #sb RNE x) = (x >= overflow_threshold eb sb || x <= -(overflow_threshold eb sb))) = - ax_is_inf_rne x + ax_is_inf_rne #eb #sb x (* RNA: same threshold as RNE (ties round away from zero to ∞). *) let lemma_is_inf_to_fp_int_rna (#eb #sb: pos) (x: int) : Lemma (is_inf (to_fp_of_int #eb #sb RNA x) = (x >= overflow_threshold eb sb || x <= -(overflow_threshold eb sb))) = - ax_is_inf_rna x + ax_is_inf_rna #eb #sb x (* RTP: positive overflow only (negative values round toward 0, not -∞). *) let lemma_is_inf_to_fp_int_rtp (#eb #sb: pos) (x: int) : Lemma (is_inf (to_fp_of_int #eb #sb RTP x) = (x > max_finite_int eb sb)) = - ax_is_inf_rtp x + ax_is_inf_rtp #eb #sb x (* RTN: negative overflow only (positive values round toward 0, not +∞). *) let lemma_is_inf_to_fp_int_rtn (#eb #sb: pos) (x: int) : Lemma (is_inf (to_fp_of_int #eb #sb RTN x) = (x < -(max_finite_int eb sb))) = - ax_is_inf_rtn x + ax_is_inf_rtn #eb #sb x (* RTZ: truncation toward zero never overflows to infinity. *) let lemma_is_inf_to_fp_int_rtz (#eb #sb: pos) (x: int) : Lemma (is_inf (to_fp_of_int #eb #sb RTZ x) = false) = - ax_is_inf_rtz x + ax_is_inf_rtz #eb #sb x (* --- 2c: isNormal --- *) @@ -295,21 +295,21 @@ let lemma_is_normal_to_fp_int : Lemma (is_normal (to_fp_of_int #eb #sb rm x) = (x <> 0 && not (is_inf (to_fp_of_int #eb #sb rm x)))) = let f = to_fp_of_int #eb #sb rm x in - ax_to_fp_int_not_nan rm x; (* is_nan f = false *) - ax_to_fp_int_not_subnormal rm x; (* is_subnormal f = false *) - ax_classification f; (* nan||inf||zero||normal||subnormal *) + ax_to_fp_int_not_nan #eb #sb rm x; (* is_nan f = false *) + ax_to_fp_int_not_subnormal #eb #sb rm x; (* is_subnormal f = false *) + ax_classification f; (* nan||inf||zero||normal||subnormal *) if x = 0 then begin - ax_to_fp_int_zero rm; (* is_zero f = true *) - ax_zero_exclusive f (* is_normal f = false, since is_zero f *) + ax_to_fp_int_zero #eb #sb rm; (* is_zero f = true *) + ax_zero_exclusive f (* is_normal f = false, since is_zero f *) end else begin - ax_to_fp_int_nonzero rm x; (* is_zero f = false *) + ax_to_fp_int_nonzero #eb #sb rm x; (* is_zero f = false *) (* At this point: not nan, not subnormal, not zero. ax_classification gives nan||inf||zero||normal||subnormal, which simplifies to inf||normal. We case-split on is_inf f. *) if is_inf f then - ax_inf_exclusive f (* is_inf f = true => is_normal f = false *) + ax_inf_exclusive f (* is_inf f = true => is_normal f = false *) else - () (* is_inf f = false; by classification, is_normal f = true *) + () (* is_inf f = false; by classification, is_normal f = true *) end @@ -390,7 +390,7 @@ let lemma_fma_zero_ite_nan_arm : Lemma (requires is_zero zero_val = true && is_finite y = false) (ensures is_nan (fp_fma rm zero_val y z) = true) = if is_nan y = true then - ax_fma_nan_y rm zero_val z + ax_fma_any_nan_y rm zero_val y z else begin (* is_finite y = false && is_nan y = false. By the transparent definition is_finite y = not (is_nan y) && not (is_inf y), @@ -409,12 +409,12 @@ let lemma_is_normal_to_fp_int_rne (x <> 0 && not (x >= overflow_threshold eb sb || x <= -(overflow_threshold eb sb)))) = - lemma_is_normal_to_fp_int RNE x; - ax_is_inf_rne x + lemma_is_normal_to_fp_int #eb #sb RNE x; + ax_is_inf_rne #eb #sb x (* The full isNormal(to_fp(rm, x)) rewrite for RTZ (never overflows). *) let lemma_is_normal_to_fp_int_rtz (#eb #sb: pos) (x: int) : Lemma (is_normal (to_fp_of_int #eb #sb RTZ x) = (x <> 0)) = - lemma_is_normal_to_fp_int RTZ x; - ax_is_inf_rtz x + lemma_is_normal_to_fp_int #eb #sb RTZ x; + ax_is_inf_rtz #eb #sb x diff --git a/fstar/IEEE754.fst b/fstar/IEEE754.fst index 0faf2cd84..185efc50c 100644 --- a/fstar/IEEE754.fst +++ b/fstar/IEEE754.fst @@ -25,7 +25,7 @@ module IEEE754 (* Abstract IEEE 754 float parameterized by format. A concrete model would be a triple (sign, biased_exponent, significand), but we keep the type opaque so the axioms are the only assumed properties. *) -assume val float : (eb: pos) -> (sb: pos) -> Type0 +assume val float : (eb: pos) -> (sb: pos) -> eqtype (* ------------------------------------------------------------------ *) (* Rounding modes (IEEE 754-2019 §4.3) *) @@ -154,17 +154,33 @@ assume val ax_mul_nan_r : Lemma (is_nan (fp_mul rm x (nan #eb #sb)) = true) assume val ax_fma_nan_x : - #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (y z: float eb sb) -> + #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (y: float eb sb) -> (z: float eb sb) -> Lemma (is_nan (fp_fma rm (nan #eb #sb) y z) = true) assume val ax_fma_nan_y : - #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x z: float eb sb) -> + #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: float eb sb) -> (z: float eb sb) -> Lemma (is_nan (fp_fma rm x (nan #eb #sb) z) = true) assume val ax_fma_nan_z : - #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x y: float eb sb) -> + #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: float eb sb) -> (y: float eb sb) -> Lemma (is_nan (fp_fma rm x y (nan #eb #sb)) = true) +(* General NaN propagation: if any argument is NaN, the result is NaN. *) +assume val ax_fma_any_nan_x : + #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: float eb sb) -> (y: float eb sb) -> (z: float eb sb) -> + Lemma (requires is_nan x = true) + (ensures is_nan (fp_fma rm x y z) = true) + +assume val ax_fma_any_nan_y : + #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: float eb sb) -> (y: float eb sb) -> (z: float eb sb) -> + Lemma (requires is_nan y = true) + (ensures is_nan (fp_fma rm x y z) = true) + +assume val ax_fma_any_nan_z : + #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: float eb sb) -> (y: float eb sb) -> (z: float eb sb) -> + Lemma (requires is_nan z = true) + (ensures is_nan (fp_fma rm x y z) = true) + (* ------------------------------------------------------------------ *) (* Special-value arithmetic axioms *) (* ------------------------------------------------------------------ *) @@ -181,7 +197,7 @@ assume val ax_zero_mul_inf : This covers the case where fp_mul rm x y = NaN and we need is_nan (fp_fma rm x y z) = true. *) assume val ax_fma_nan_mul : - #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x y z: float eb sb) -> + #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: float eb sb) -> (y: float eb sb) -> (z: float eb sb) -> Lemma (requires is_nan (fp_mul rm x y) = true) (ensures is_nan (fp_fma rm x y z) = true) @@ -189,7 +205,7 @@ assume val ax_fma_nan_mul : and fp_mul(rm, zero, y_finite) is ±0 (exact, IEEE 754-2019 §6.3). This is the core decomposition used by the rewriter. *) assume val ax_fma_zero_finite : - #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (zero_val y z: float eb sb) -> + #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (zero_val: float eb sb) -> (y: float eb sb) -> (z: float eb sb) -> Lemma (requires is_zero zero_val = true && is_finite y = true) (ensures fp_fma rm zero_val y z = fp_add rm (fp_mul rm zero_val y) z && is_zero (fp_mul rm zero_val y) = true) @@ -197,7 +213,7 @@ assume val ax_fma_zero_finite : (* Sign of 0 * y (IEEE 754-2019 §6.3): sign(0 * y) = sign(0) XOR sign(y) for finite nonzero y. *) assume val ax_zero_mul_sign : - #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (zero_val y: float eb sb) -> + #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (zero_val: float eb sb) -> (y: float eb sb) -> Lemma (requires is_zero zero_val = true && is_finite y = true && is_zero y = false) (ensures (let p = fp_mul rm zero_val y in is_zero p = true && @@ -208,7 +224,7 @@ assume val ax_zero_mul_sign : (* fp_add(rm, ±0, z) = z when z is finite and nonzero (IEEE 754-2019 §6.3). ±0 is an additive identity for nonzero finite values under all rounding modes. *) assume val ax_add_zero_nonzero : - #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (zero_val z: float eb sb) -> + #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (zero_val: float eb sb) -> (z: float eb sb) -> Lemma (requires is_zero zero_val = true && is_finite z = true && is_zero z = false) (ensures fp_add rm zero_val z = z) diff --git a/fstar/README.md b/fstar/README.md index f28c6b358..f4a34cd8a 100644 --- a/fstar/README.md +++ b/fstar/README.md @@ -240,7 +240,7 @@ the `fstar/` directory. It installs the F* binary, runs `extract.sh`, and uploads the generated C++ as a downloadable artifact `fstar-extracted-cpp-rules` for inspection. -F\* 2024.09.05 or later is required. The files have no external +F\* 2026.03.24 or later is required. The files have no external dependencies beyond the F\* standard library prelude. Because all IEEE 754 semantics are encoded as `assume val` axioms, the diff --git a/fstar/RewriteCodeGen.fst b/fstar/RewriteCodeGen.fst index 459d6f9e5..8a4b0cbb2 100644 --- a/fstar/RewriteCodeGen.fst +++ b/fstar/RewriteCodeGen.fst @@ -70,7 +70,7 @@ noeq type cexpr = This undoes the nested Tv_App structure that F* uses for multi-argument applications. *) let rec collect_app (t: term) : Tac (term & list argv) = - match inspect t with + match inspect_ln t with | Tv_App hd arg -> let (h, args) = collect_app hd in (h, args @ [arg]) @@ -86,53 +86,70 @@ let filter_explicit (args: list argv) : list term = (* Get the short name of a free variable, last component of the path. E.g. "IEEE754.is_nan" to "is_nan" *) let fv_short_name (t: term) : Tac (option string) = - match inspect t with + match inspect_ln t with | Tv_FVar fv -> (match List.Tot.rev (inspect_fv fv) with | last :: _ -> Some last | _ -> None) | _ -> None -(* Resolve a bound variable, de Bruijn indexed, using our index to name map. - F* reflection represents bound variables with de Bruijn indices: - the most recently bound variable has index 0. - - Given binders [eb; sb; c; t; e], inside the body: - e = BVar 0, t = BVar 1, c = BVar 2, sb = BVar 3, eb = BVar 4 *) -let bvar_name (idx_map: list (nat & string)) (t: term) : Tac (option string) = - match inspect t with - | Tv_BVar bv -> - let bvv = inspect_bv bv in - (match List.Tot.assoc #nat bvv.index idx_map with - | Some n -> Some n - | None -> - (* de Bruijn index not in our map; use the printer name as a fallback - and warn so the caller knows the index map may be incomplete. *) - let pp = FStar.Sealed.unseal bvv.ppname in - print ("WARNING: bvar_name fallback for index " - ^ string_of_int bvv.index ^ ", using ppname '" ^ pp ^ "'"); - Some pp) - | _ -> None +(* Resolve a variable name from a term. + In F* 2026, variables in lemma types returned by `tc env` may appear + as named variables (Tv_Var namedv) rather than de Bruijn indices, so + we first try the named view and fall back to de Bruijn lookup. *) +let var_name (idx_map: list (nat & string)) (offset: nat) (t: term) : Tac (option string) = + (* Try named-view first: Tv_Var gives a directly named variable. *) + (match FStar.Tactics.NamedView.inspect t with + | FStar.Tactics.NamedView.Tv_Var nv -> + let nm = unseal nv.ppname in + Some nm + | _ -> + (* Fall back to de Bruijn lookup for variables still in closed form. *) + match inspect_ln t with + | Tv_BVar bv -> + let bvv = inspect_bv bv in + if bvv.index < offset then None + else begin + let adj : nat = bvv.index - offset in + (match List.Tot.assoc #nat adj idx_map with + | Some n -> Some n + | None -> + let pp = unseal bvv.ppname in + print ("WARNING: var_name fallback for BVar index " + ^ string_of_int bvv.index ^ " (adj=" + ^ string_of_int adj ^ "), using ppname '" ^ pp ^ "'"); + Some pp) + end + | _ -> None) (* Detect if-then-else in reflected terms. In F*, `if c then t else e` desugars to: - match c with | true -> t | false -> e - which appears as Tv_Match with two branches. *) -let try_ite (t: term) : Tac (option (term & term & term)) = - match inspect t with + match c with | true -> t | (x:bool) -> e + where the false branch uses Pat_Var (not Pat_Constant), adding an extra + binder. We therefore return the additional binder count for each branch + body, so callers can adjust the de Bruijn offset accordingly: + - then-branch (Pat_Constant): 0 extra binders + - else-branch (Pat_Var): 1 extra binder *) +let try_ite (t: term) : Tac (option (term & nat & term & nat & term)) = + match inspect_ln t with | Tv_Match scrutinee _ret branches -> (match branches with - | [(_, body_t); (_, body_f)] -> - Some (scrutinee, body_t, body_f) + | [(pat_t, body_t); (pat_f, body_f)] -> + let extra_t : nat = match pat_t with | Pat_Var _ _ -> 1 | _ -> 0 in + let extra_f : nat = match pat_f with | Pat_Var _ _ -> 1 | _ -> 0 in + Some (scrutinee, extra_t, body_t, extra_f, body_f) | _ -> None) | _ -> None -(* Unwrap `squash p` to `p` if present. - The Lemma precondition may be wrapped in squash. *) +(* Unwrap `squash p` or `b2t p` to `p` if present. + The Lemma postcondition is often wrapped in squash or b2t. + In F* 2026, bool-valued propositions in Lemma postconditions are + wrapped in `b2t` which coerces `bool` to `prop`. *) let unwrap_squash (t: term) : Tac term = let (head, args) = collect_app t in match fv_short_name head with - | Some "squash" -> + | Some "squash" + | Some "b2t" -> (match filter_explicit args with | [inner] -> inner | _ -> t) | _ -> t @@ -162,51 +179,56 @@ let rec tac_map (#a #b: Type) (f: a -> Tac b) (l: list a) : Tac (list b) = (* Extract a pattern from the LHS argument. Recognizes: - - Bound variables -> PVar - - if-then-else -> PIte - - Function applications -> PApp *) -let rec extract_pat (m: list (nat & string)) (t: term) : Tac cpat = + - Variables (named or BVar) -> PVar + - if-then-else -> PIte + - Function applications -> PApp *) +let rec extract_pat (m: list (nat & string)) (offset: nat) (t: term) : Tac cpat = match try_ite t with - | Some (c, tb, fb) -> - PIte (extract_pat m c) (extract_pat m tb) (extract_pat m fb) + | Some (c, et, tb, ef, fb) -> + let off_t : nat = offset + et in + let off_f : nat = offset + ef in + PIte (extract_pat m offset c) (extract_pat m off_t tb) (extract_pat m off_f fb) | None -> let (head, raw_args) = collect_app t in let args = filter_explicit raw_args in if List.Tot.length args > 0 then (match fv_short_name head with - | Some fn -> PApp fn (tac_map (extract_pat m) args) + | Some fn -> PApp fn (tac_map (extract_pat m offset) args) | None -> - (match bvar_name m head with - | Some n -> PApp n (tac_map (extract_pat m) args) + (match var_name m offset head with + | Some n -> PApp n (tac_map (extract_pat m offset) args) | None -> fail ("pattern app: cannot resolve head: " ^ term_to_string head))) else - (match bvar_name m t with + (match var_name m offset t with | Some n -> PVar n | None -> fail ("pattern: cannot recognize: " ^ term_to_string t)) (* Extract an expression from the RHS. Recognizes: - - Bound variables -> EVar + - Variables (named or BVar) -> EVar - Boolean literals -> EBool - - if-then-else -> EIte - - Function applications (FVar) -> EApp *) -let rec extract_expr (m: list (nat & string)) (t: term) : Tac cexpr = + - if-then-else -> EIte + - Function applications (FVar) -> EApp *) +let rec extract_expr (m: list (nat & string)) (offset: nat) (t: term) : Tac cexpr = (* Check for boolean literals first *) - (match inspect t with - | Tv_Const (C_Bool b) -> EBool b + (match inspect_ln t with + | Tv_Const C_True -> EBool true + | Tv_Const C_False -> EBool false | _ -> match try_ite t with - | Some (c, tb, fb) -> - EIte (extract_expr m c) (extract_expr m tb) (extract_expr m fb) + | Some (c, et, tb, ef, fb) -> + let off_t : nat = offset + et in + let off_f : nat = offset + ef in + EIte (extract_expr m offset c) (extract_expr m off_t tb) (extract_expr m off_f fb) | None -> let (head, raw_args) = collect_app t in let args = filter_explicit raw_args in if List.Tot.length args > 0 then (match fv_short_name head with - | Some fn -> EApp fn (tac_map (extract_expr m) args) + | Some fn -> EApp fn (tac_map (extract_expr m offset) args) | None -> fail ("expr: application head is not FVar: " ^ term_to_string head)) else - (match bvar_name m t with + (match var_name m offset t with | Some n -> EVar n | None -> fail ("expr: cannot recognize: " ^ term_to_string t))) @@ -219,9 +241,9 @@ let rec extract_expr (m: list (nat & string)) (t: term) : Tac cexpr = -> Lemma (...) Returns: parameter names [eb;sb;c;t;e] and the final computation, C_Lemma. *) let rec strip_arrows (t: term) : Tac (list string & comp) = - match inspect t with + match inspect_ln t with | Tv_Arrow binder c -> - let name = FStar.Sealed.unseal (inspect_binder binder).ppname in + let name = unseal (inspect_binder binder).ppname in (match inspect_comp c with | C_Total ret -> let (names, final_c) = strip_arrows ret in @@ -260,17 +282,16 @@ let cpp_builder_name (fn: string) : string = | _ -> "m_util.mk_" ^ fn (* Collect all variable names from a pattern (for C++ declarations) *) -let rec pat_vars (p: cpat) : Tot (list string) = +let rec pat_vars (p: cpat) : Tot (list string) (decreases p) = match p with | PVar n -> [n] | PIte c t e -> pat_vars c @ pat_vars t @ pat_vars e - | PApp _ args -> - let rec collect (l: list cpat) : Tot (list string) (decreases l) = - match l with - | [] -> [] - | x :: xs -> pat_vars x @ collect xs - in - collect args + | PApp _ args -> pat_vars_list args + +and pat_vars_list (ps: list cpat) : Tot (list string) (decreases ps) = + match ps with + | [] -> [] + | x :: xs -> pat_vars x @ pat_vars_list xs (* Generate: expr *c, *t, *e; *) let gen_decls (p: cpat) : string = @@ -297,7 +318,7 @@ let gen_condition (arg: string) (p: cpat) : string = | _ -> "/* TODO: extend gen_condition for nested patterns */" (* Generate a C++ expression from the RHS IR *) -let rec gen_rhs_expr (e: cexpr) : Tot string = +let rec gen_rhs_expr (e: cexpr) : Tot string (decreases e) = match e with | EVar n -> n | EBool true -> "m().mk_true()" @@ -308,7 +329,13 @@ let rec gen_rhs_expr (e: cexpr) : Tot string = ^ gen_rhs_expr e ^ ")" | EApp fn args -> cpp_builder_name fn ^ "(" - ^ FStar.String.concat ", " (List.Tot.map gen_rhs_expr args) ^ ")" + ^ gen_rhs_expr_list args ^ ")" + +and gen_rhs_expr_list (es: list cexpr) : Tot string (decreases es) = + match es with + | [] -> "" + | [e] -> gen_rhs_expr e + | e :: rest -> gen_rhs_expr e ^ ", " ^ gen_rhs_expr_list rest (* Generate the complete C++ rewrite case *) let gen_cpp (top_fn: string) (arg: string) (pat: cpat) (rhs: cexpr) : string = @@ -353,14 +380,22 @@ let extract_rewrite (lemma: term) : Tac string = let (param_names, final_comp) = strip_arrows ty in let idx_map = build_idx_map param_names in - (* 2. Get the equality from the Lemma precondition *) - let pre = + (* 2. Get the equality from the Lemma postcondition. + For `Lemma P`, the comp is C_Lemma l_True (fun _ -> b2t P) []. + The postcondition is a function taking the return value as argument. + We peel off the leading Tv_Abs to get the raw proposition. + Inside the abs body, all de Bruijn indices are shifted by 1 relative + to the outer scope, so we pass offset=1 to extract_pat/extract_expr. *) + let (post, post_offset) = match inspect_comp final_comp with - | C_Lemma pre _ _ -> pre + | C_Lemma _ post _ -> + (match inspect_ln post with + | Tv_Abs _ body -> (body, 1) + | _ -> (post, 0)) | _ -> fail "expected Lemma computation type" in - (* 3. Extract LHS = RHS from the precondition *) - let (lhs, rhs) = extract_eq pre in + (* 3. Extract LHS = RHS from the postcondition *) + let (lhs, rhs) = extract_eq post in (* 4. Decompose LHS: top_fn(argument_pattern). The top_fn is the IEEE754 classification predicate whose @@ -381,8 +416,8 @@ let extract_rewrite (lemma: term) : Tac string = ^ " for top_fn=" ^ top_fn) in (* 5. Extract the argument pattern and the RHS expression *) - let pat = extract_pat idx_map arg_term in - let rhs_expr = extract_expr idx_map rhs in + let pat = extract_pat idx_map post_offset arg_term in + let rhs_expr = extract_expr idx_map post_offset rhs in (* 6. Emit C++ code. "arg1" is the standard name for the argument in mk_* functions of @@ -436,11 +471,19 @@ let print_rewrite (label: string) (lemma: term) : Tac unit = print ("\n=== " ^ label ^ " ===\n"); print (extract_rewrite lemma) +(* Construct a term reference to a top-level name in FPARewriterRules + without instantiating implicit arguments. Using pack_fv avoids the + elaboration that quote performs, which in F* 2026 fails for polymorphic + lemmas whose implicit type arguments (eb, sb: pos) cannot be inferred + from the call site. *) +let lemma_ref (name: string) : term = + pack_ln (Tv_FVar (pack_fv ["FPARewriterRules"; name])) + (* Demonstrate extraction of the three ite-pushthrough lemmas. Running this file with F* prints the generated C++ for each rule. *) let _ = run_tactic (fun () -> - List.Tot.iter (fun (label, lemma) -> print_rewrite label lemma) - [ ("lemma_is_nan_ite", quote lemma_is_nan_ite); - ("lemma_is_inf_ite", quote lemma_is_inf_ite); - ("lemma_is_normal_ite", quote lemma_is_normal_ite) ]) + iter (fun (label, lemma) -> print_rewrite label lemma) + [ ("lemma_is_nan_ite", lemma_ref "lemma_is_nan_ite"); + ("lemma_is_inf_ite", lemma_ref "lemma_is_inf_ite"); + ("lemma_is_normal_ite", lemma_ref "lemma_is_normal_ite") ]) diff --git a/fstar/extract.sh b/fstar/extract.sh index 0d8f5897e..741636984 100755 --- a/fstar/extract.sh +++ b/fstar/extract.sh @@ -26,7 +26,7 @@ cd "$SCRIPT_DIR" if ! command -v fstar.exe &>/dev/null; then echo "ERROR: fstar.exe not found on PATH." >&2 - echo "Install F* 2024.09.05+ from https://github.com/FStarLang/FStar/releases" >&2 + echo "Install F* 2026.03.24+ from https://github.com/FStarLang/FStar/releases" >&2 exit 1 fi