From 2e2ac5f11aa346678460886c789df71f3083d772 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 7 Aug 2024 08:44:23 +0200 Subject: [PATCH 1/6] feat(hax-lib-macros): add unsafe variants of `fstar!`, `coq!`, etc. --- hax-lib-macros/src/lib.rs | 2 +- hax-lib-macros/src/quote.rs | 12 +++++++++--- hax-lib/src/lib.rs | 6 ++++++ 3 files changed, 16 insertions(+), 4 deletions(-) diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs index 046c7c6d7..64ddc7eed 100644 --- a/hax-lib-macros/src/lib.rs +++ b/hax-lib-macros/src/lib.rs @@ -691,7 +691,7 @@ macro_rules! make_quoting_proc_macro { /// Types can be refered to with the syntax `$:{TYPE}`. #[proc_macro] pub fn $expr_name(payload: pm::TokenStream) -> pm::TokenStream { - let ts: TokenStream = quote::expression(payload).into(); + let ts: TokenStream = quote::expression(true, payload).into(); quote!{ #[cfg($cfg_name)] { diff --git a/hax-lib-macros/src/quote.rs b/hax-lib-macros/src/quote.rs index 24e0c81e4..307c856af 100644 --- a/hax-lib-macros/src/quote.rs +++ b/hax-lib-macros/src/quote.rs @@ -134,7 +134,7 @@ pub(super) fn item( payload: pm::TokenStream, item: pm::TokenStream, ) -> pm::TokenStream { - let expr = TokenStream::from(expression(payload)); + let expr = TokenStream::from(expression(true, payload)); let item = TokenStream::from(item); let uid = ItemUid::fresh(); let uid_attr = AttrPayload::Uid(uid.clone()); @@ -162,7 +162,7 @@ pub(super) fn item( .into() } -pub(super) fn expression(payload: pm::TokenStream) -> pm::TokenStream { +pub(super) fn expression(force_unit: bool, payload: pm::TokenStream) -> pm::TokenStream { let (mut backend_code, antiquotes) = { let payload = parse_macro_input!(payload as LitStr).value(); if payload.find(SPLIT_MARK).is_some() { @@ -187,5 +187,11 @@ pub(super) fn expression(payload: pm::TokenStream) -> pm::TokenStream { }; } - quote! {::hax_lib::inline(#[allow(unused_variables)]{#backend_code})}.into() + let function = if force_unit { + quote! {inline} + } else { + quote! {inline_unsafe} + }; + + quote! {::hax_lib::#function(#[allow(unused_variables)]{#backend_code})}.into() } diff --git a/hax-lib/src/lib.rs b/hax-lib/src/lib.rs index aa2654244..44eba43ab 100644 --- a/hax-lib/src/lib.rs +++ b/hax-lib/src/lib.rs @@ -141,6 +141,12 @@ pub fn implies(lhs: bool, rhs: impl Fn() -> bool) -> bool { #[doc(hidden)] pub fn inline(_: &str) {} +/// Similar to `inline`, but allows for any type. Do not use directly. +#[doc(hidden)] +pub fn inline_unsafe(_: &str) -> T { + unreachable!() +} + /// A type that implements `Refinement` should be a newtype for a /// type `T`. The field holding the value of type `T` should be /// private, and `Refinement` should be the only interface to the From 1454dfedda387de7bcb70771c9526d2b561064a5 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 7 Aug 2024 08:52:38 +0200 Subject: [PATCH 2/6] refactor(hax-lib-macros): use `paste` to simplify `macro_rules` macros --- Cargo.lock | 1 + hax-lib-macros/Cargo.toml | 1 + hax-lib-macros/src/lib.rs | 113 +++++++++++++++++++------------------- 3 files changed, 58 insertions(+), 57 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 9a09e2844..2e1015863 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -556,6 +556,7 @@ version = "0.1.0-pre.1" dependencies = [ "hax-lib", "hax-lib-macros-types", + "paste", "proc-macro-error", "proc-macro2", "quote", diff --git a/hax-lib-macros/Cargo.toml b/hax-lib-macros/Cargo.toml index a2f4a5af4..06c5841b6 100644 --- a/hax-lib-macros/Cargo.toml +++ b/hax-lib-macros/Cargo.toml @@ -23,6 +23,7 @@ syn = { version = "2.0", features = [ "parsing", ] } hax-lib-macros-types.workspace = true +paste = "1.0.15" [dev-dependencies] hax-lib = { path = "../hax-lib" } diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs index 64ddc7eed..f3cc5d217 100644 --- a/hax-lib-macros/src/lib.rs +++ b/hax-lib-macros/src/lib.rs @@ -657,70 +657,69 @@ macro_rules! make_quoting_item_proc_macro { } macro_rules! make_quoting_proc_macro { - ($backend:ident($expr_name:ident, $before_name:ident, $after_name:ident, $replace_name:ident, $cfg_name:ident)) => { - #[doc = concat!("Embed ", stringify!($backend), " expression inside a Rust expression. This macro takes only one argument: some raw ", stringify!($backend), " code as a string literal.")] - /// - - /// While it is possible to directly write raw backend code, - /// sometimes it can be inconvenient. For example, referencing - /// Rust names can be a bit cumbersome: for example, the name - /// `my_crate::my_module::CONSTANT` might be translated - /// differently in a backend (e.g. in the F* backend, it will - /// probably be `My_crate.My_module.v_CONSTANT`). - /// - - /// To facilitate this, you can write Rust names directly, - /// using the prefix `$`: `f $my_crate::my_module__CONSTANT + 3` - /// will be replaced with `f My_crate.My_module.v_CONSTANT + 3` - /// in the F* backend for instance. - - /// If you want to refer to the Rust constructor - /// `Enum::Variant`, you should write `$$Enum::Variant` (note - /// the double dollar). - - /// If the name refers to something polymorphic, you need to - /// signal it by adding _any_ type informations, - /// e.g. `${my_module::function<()>}`. The curly braces are - /// needed for such more complex expressions. - - /// You can also write Rust patterns with the `$?{SYNTAX}` - /// syntax, where `SYNTAX` is a Rust pattern. The syntax - /// `${EXPR}` also allows any Rust expressions - /// `EXPR` to be embedded. - - /// Types can be refered to with the syntax `$:{TYPE}`. - #[proc_macro] - pub fn $expr_name(payload: pm::TokenStream) -> pm::TokenStream { - let ts: TokenStream = quote::expression(true, payload).into(); - quote!{ - #[cfg($cfg_name)] - { - #ts - } - }.into() - } + ($backend:ident) => { + paste::paste! { + #[doc = concat!("Embed ", stringify!($backend), " expression inside a Rust expression. This macro takes only one argument: some raw ", stringify!($backend), " code as a string literal.")] + /// + + /// While it is possible to directly write raw backend code, + /// sometimes it can be inconvenient. For example, referencing + /// Rust names can be a bit cumbersome: for example, the name + /// `my_crate::my_module::CONSTANT` might be translated + /// differently in a backend (e.g. in the F* backend, it will + /// probably be `My_crate.My_module.v_CONSTANT`). + /// + + /// To facilitate this, you can write Rust names directly, + /// using the prefix `$`: `f $my_crate::my_module__CONSTANT + 3` + /// will be replaced with `f My_crate.My_module.v_CONSTANT + 3` + /// in the F* backend for instance. + + /// If you want to refer to the Rust constructor + /// `Enum::Variant`, you should write `$$Enum::Variant` (note + /// the double dollar). + + /// If the name refers to something polymorphic, you need to + /// signal it by adding _any_ type informations, + /// e.g. `${my_module::function<()>}`. The curly braces are + /// needed for such more complex expressions. + + /// You can also write Rust patterns with the `$?{SYNTAX}` + /// syntax, where `SYNTAX` is a Rust pattern. The syntax + /// `${EXPR}` also allows any Rust expressions + /// `EXPR` to be embedded. + + /// Types can be refered to with the syntax `$:{TYPE}`. + #[proc_macro] + pub fn [<$backend _expr>](payload: pm::TokenStream) -> pm::TokenStream { + let ts: TokenStream = quote::expression(true, payload).into(); + quote!{ + #[cfg([< hax_backend_ $backend >])] + { + #ts + } + }.into() + } - make_quoting_item_proc_macro!($backend, $before_name, ItemQuotePosition::Before, $cfg_name); - make_quoting_item_proc_macro!($backend, $after_name, ItemQuotePosition::After, $cfg_name); + make_quoting_item_proc_macro!($backend, [< $backend _before >], ItemQuotePosition::Before, [< hax_backend_ $backend >]); + make_quoting_item_proc_macro!($backend, [< $backend _after >], ItemQuotePosition::After, [< hax_backend_ $backend >]); - #[doc = concat!("Replaces a Rust expression with some verbatim ", stringify!($backend)," code.")] - #[proc_macro_error] - #[proc_macro_attribute] - pub fn $replace_name(payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { - let item: TokenStream = item.into(); - let attr = AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true }); - $before_name(payload, quote!{#attr #item}.into()) + #[doc = concat!("Replaces a Rust expression with some verbatim ", stringify!($backend)," code.")] + #[proc_macro_error] + #[proc_macro_attribute] + pub fn [< $backend _replace >](payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { + let item: TokenStream = item.into(); + let attr = AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true }); + [< $backend _before >](payload, quote!{#attr #item}.into()) + } } }; - ($backend:ident $payload:tt $($others:tt)+) => { - make_quoting_proc_macro!($backend$payload); - make_quoting_proc_macro!($($others)+); + ($($backend:ident)*) => { + $(make_quoting_proc_macro!($backend);)* } } -make_quoting_proc_macro!(fstar(fstar_expr, fstar_before, fstar_after, fstar_replace, hax_backend_fstar) - coq(coq_expr, coq_before, coq_after, coq_replace, hax_backend_coq) - proverif(proverif_expr, proverif_before, proverif_after, proverif_replace, hax_backend_proverif)); +make_quoting_proc_macro!(fstar coq proverif); /// Marks a newtype `struct RefinedT(T);` as a refinement type. The /// struct should have exactly one unnamed private field. From 107c300bb249ff45fdbe74af48b327bc378320ab Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 7 Aug 2024 10:16:09 +0200 Subject: [PATCH 3/6] refactor(hax-lib-macros): add `expect_future_expr` --- hax-lib-macros/src/utils.rs | 70 +++++++++++++++++++++++-------------- 1 file changed, 44 insertions(+), 26 deletions(-) diff --git a/hax-lib-macros/src/utils.rs b/hax-lib-macros/src/utils.rs index f1b9a5391..c4c7be89f 100644 --- a/hax-lib-macros/src/utils.rs +++ b/hax-lib-macros/src/utils.rs @@ -133,44 +133,62 @@ fn expect_fn_arg_var_pat(arg: &FnArg) -> Option<(String, syn::Type)> { } } +pub(crate) enum NotFutureExpr { + BadNumberOfArgs, + ArgNotIdent, +} + +/// `expect_future_expr(e)` tries to match the pattern +/// `future()` in expression `e` +pub(crate) fn expect_future_expr(e: &Expr) -> Option> { + if let Expr::Call(call) = e { + if call.func.is_ident("future") { + return Some(match call.args.iter().collect::>().as_slice() { + [arg] => arg.expect_ident().ok_or(NotFutureExpr::ArgNotIdent), + _ => Err(NotFutureExpr::BadNumberOfArgs), + }); + } + } + None +} + /// Rewrites `future(x)` nodes in an expression when (1) `x` is an /// ident and (2) the ident `x` is contained in the HashSet. struct RewriteFuture(HashSet); impl VisitMut for RewriteFuture { fn visit_expr_mut(&mut self, e: &mut Expr) { syn::visit_mut::visit_expr_mut(self, e); - if let Expr::Call(call) = e { - if call.func.is_ident("future") { - let help_message = || match self.0.iter().next() { + let error = match expect_future_expr(e) { + Some(Ok(arg)) => { + let arg = format!("{}", arg); + if self.0.contains(&arg) { + let arg = create_future_ident(&arg); + *e = parse_quote! {#arg}; + return; + } + Some(format!("Cannot find an input `{arg}` of type `&mut _`. In the context, `future` can be called on the following inputs: {:?}.", self.0)) + } + Some(Err(error_kind)) => { + let message = match error_kind { + NotFutureExpr::BadNumberOfArgs => { + "`future` can only be called with one argument: a `&mut` input name" + } + NotFutureExpr::ArgNotIdent => { + "`future` can only be called with an `&mut` input name" + } + }; + let help_message = match self.0.iter().next() { None => format!(" In the context, there is no `&mut` input."), Some(var) => { format!(" For example, in the context you can write `future({var})`.") } }; - let error = match call.args.iter().collect::>().as_slice() { - [arg] => { - if let Some(arg) = arg.expect_ident() { - let arg = format!("{}", arg); - if self.0.contains(&arg) { - let arg = create_future_ident(&arg); - *e = parse_quote! {#arg}; - return; - } - format!("Cannot find an input `{arg}` of type `&mut _`. In the context, `future` can be called on the following inputs: {:?}.", self.0) - } else { - format!( - "`future` can only be called with an `&mut` input name.{}", - help_message() - ) - } - } - _ => format!( - "`future` can only be called with one argument: a `&mut` input name.{}", - help_message() - ), - }; - *e = parse_quote! {::std::compile_error!(#error)}; + Some(format!("{message}.{}", help_message)) } + None => None, + }; + if let Some(error) = error { + *e = parse_quote! {::std::compile_error!(#error)}; } } } From da55db1c1d11294508be836f5b02f739b1bc151c Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 7 Aug 2024 10:41:48 +0200 Subject: [PATCH 4/6] feat(hax-lib-macros): allow any type for `fstar!` (&friends) in pre/posts --- .../phases/phase_transform_hax_lib_inline.ml | 3 +- engine/names/src/lib.rs | 1 + hax-lib-macros/Cargo.toml | 1 + hax-lib-macros/src/lib.rs | 21 +++++++++++ hax-lib-macros/src/quote.rs | 32 +++++++++++++++-- hax-lib-macros/src/utils.rs | 4 +++ hax-lib/src/proc_macros.rs | 10 +++--- .../toolchain__attributes into-fstar.snap | 36 +++++++++++++++++++ tests/Cargo.lock | 7 ++++ tests/attributes/src/lib.rs | 15 ++++++++ 10 files changed, 123 insertions(+), 7 deletions(-) diff --git a/engine/lib/phases/phase_transform_hax_lib_inline.ml b/engine/lib/phases/phase_transform_hax_lib_inline.ml index 0d448aa6a..d807212ac 100644 --- a/engine/lib/phases/phase_transform_hax_lib_inline.ml +++ b/engine/lib/phases/phase_transform_hax_lib_inline.ml @@ -80,7 +80,8 @@ module%inlined_contents Make (F : Features.T) = struct and quote_of_expr' span (expr : A.expr') = match expr with | App { f = { e = GlobalVar f; _ }; args = [ payload ]; _ } - when Global_ident.eq_name Hax_lib__inline f -> + when Global_ident.eq_name Hax_lib__inline f + || Global_ident.eq_name Hax_lib__inline_unsafe f -> let bindings, str = dexpr payload |> UB.collect_let_bindings in let str = match diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs index 958046354..6e53dd5f0 100644 --- a/engine/names/src/lib.rs +++ b/engine/names/src/lib.rs @@ -51,6 +51,7 @@ fn dummy_hax_concrete_ident_wrapper>(x: I, mu } let _ = hax_lib::inline(""); + let _: () = hax_lib::inline_unsafe(""); use hax_lib::{RefineAs, Refinement}; fn refinements>(x: T, y: U) -> T { diff --git a/hax-lib-macros/Cargo.toml b/hax-lib-macros/Cargo.toml index 06c5841b6..90350bf24 100644 --- a/hax-lib-macros/Cargo.toml +++ b/hax-lib-macros/Cargo.toml @@ -19,6 +19,7 @@ quote.workspace = true syn = { version = "2.0", features = [ "full", "visit-mut", + "visit", "extra-traits", "parsing", ] } diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs index f3cc5d217..87a75c71c 100644 --- a/hax-lib-macros/src/lib.rs +++ b/hax-lib-macros/src/lib.rs @@ -195,6 +195,10 @@ pub fn decreases(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStrea /// the `ensures` clause, you can refer to such an `&mut` input `x` as /// `x` for its "past" value and `future(x)` for its "future" value. /// +/// You can use the (unqualified) macro `fstar!` (`BACKEND!` for any +/// backend `BACKEND`) to inline F* (or Coq, ProVerif, etc.) code in +/// the precondition, e.g. `fstar!("true")`. +/// /// # Example /// /// ``` @@ -239,6 +243,10 @@ pub fn requires(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream /// Add a logical postcondition to a function. Note you can use the /// `forall` and `exists` operators. /// +/// You can use the (unqualified) macro `fstar!` (`BACKEND!` for any +/// backend `BACKEND`) to inline F* (or Coq, ProVerif, etc.) code in +/// the postcondition, e.g. `fstar!("true")`. +/// /// # Example /// /// ``` @@ -701,6 +709,19 @@ macro_rules! make_quoting_proc_macro { }.into() } + #[doc = concat!("The unsafe (because polymorphic: even computationally relevant code can be inlined!) version of `", stringify!($backend), "_expr`.")] + #[proc_macro] + #[doc(hidden)] + pub fn [<$backend _unsafe_expr>](payload: pm::TokenStream) -> pm::TokenStream { + let ts: TokenStream = quote::expression(false, payload).into(); + quote!{ + #[cfg([< hax_backend_ $backend >])] + { + #ts + } + }.into() + } + make_quoting_item_proc_macro!($backend, [< $backend _before >], ItemQuotePosition::Before, [< hax_backend_ $backend >]); make_quoting_item_proc_macro!($backend, [< $backend _after >], ItemQuotePosition::After, [< hax_backend_ $backend >]); diff --git a/hax-lib-macros/src/quote.rs b/hax-lib-macros/src/quote.rs index 307c856af..6bd5282f1 100644 --- a/hax-lib-macros/src/quote.rs +++ b/hax-lib-macros/src/quote.rs @@ -162,6 +162,21 @@ pub(super) fn item( .into() } +pub(super) fn detect_future_node_in_expression(e: &syn::Expr) -> bool { + struct Visitor(bool); + use syn::visit::*; + impl<'a> Visit<'a> for Visitor { + fn visit_expr(&mut self, e: &'a Expr) { + if let Some(Ok(_)) = crate::utils::expect_future_expr(e) { + self.0 = true; + } + } + } + let mut visitor = Visitor(false); + visitor.visit_expr(e); + visitor.0 +} + pub(super) fn expression(force_unit: bool, payload: pm::TokenStream) -> pm::TokenStream { let (mut backend_code, antiquotes) = { let payload = parse_macro_input!(payload as LitStr).value(); @@ -178,8 +193,18 @@ pub(super) fn expression(force_unit: bool, payload: pm::TokenStream) -> pm::Toke .collect(); (quote! {#string}, antiquotes) }; - for user in antiquotes.iter().rev() { + if !force_unit + && syn::parse(user.ts.clone()) + .as_ref() + .map(detect_future_node_in_expression) + .unwrap_or(false) + { + let ts: proc_macro2::TokenStream = user.ts.clone().into(); + return quote! { + ::std::compile_error!(concat!("The `future` operator cannot be used within a quote. Hint: move `", stringify!(#ts), "` to a let binding and use the binding name instead.")) + }.into(); + } let kind = &user.kind; backend_code = quote! { let #kind = #user; @@ -193,5 +218,8 @@ pub(super) fn expression(force_unit: bool, payload: pm::TokenStream) -> pm::Toke quote! {inline_unsafe} }; - quote! {::hax_lib::#function(#[allow(unused_variables)]{#backend_code})}.into() + quote! { + ::hax_lib::#function(#[allow(unused_variables)]{#backend_code}) + } + .into() } diff --git a/hax-lib-macros/src/utils.rs b/hax-lib-macros/src/utils.rs index c4c7be89f..e762c8191 100644 --- a/hax-lib-macros/src/utils.rs +++ b/hax-lib-macros/src/utils.rs @@ -17,6 +17,10 @@ impl ToTokens for HaxQuantifiers { fn exists bool>(f: F) -> bool { true } + + use ::hax_lib::fstar_unsafe_expr as fstar; + use ::hax_lib::coq_unsafe_expr as coq; + use ::hax_lib::proverif_unsafe_expr as proverif; } .to_tokens(tokens) } diff --git a/hax-lib/src/proc_macros.rs b/hax-lib/src/proc_macros.rs index f96953222..cfd544fe8 100644 --- a/hax-lib/src/proc_macros.rs +++ b/hax-lib/src/proc_macros.rs @@ -11,8 +11,10 @@ pub use hax_lib_macros::{ }; macro_rules! export_quoting_proc_macros { - ($backend:ident($expr_name:ident, $before_name:ident, $after_name:ident, $replace_name:ident, $cfg_name:ident)) => { + ($backend:ident($expr_name:ident, $expr_unsafe_name:ident, $before_name:ident, $after_name:ident, $replace_name:ident, $cfg_name:ident)) => { pub use hax_lib_macros::$expr_name as $backend; + #[doc(hidden)] + pub use hax_lib_macros::$expr_unsafe_name; #[doc=concat!("Procedural macros for ", stringify!($backend))] pub mod $backend { @@ -28,6 +30,6 @@ macro_rules! export_quoting_proc_macros { } } -export_quoting_proc_macros!(fstar(fstar_expr, fstar_before, fstar_after, fstar_replace, hax_backend_fstar) - coq(coq_expr, coq_before, coq_after, coq_replace, hax_backend_coq) - proverif(proverif_expr, proverif_before, proverif_after, proverif_replace, hax_backend_proverif)); +export_quoting_proc_macros!(fstar(fstar_expr, fstar_unsafe_expr, fstar_before, fstar_after, fstar_replace, hax_backend_fstar) + coq(coq_expr, coq_unsafe_expr, coq_before, coq_after, coq_replace, hax_backend_coq) + proverif(proverif_expr, proverif_unsafe_expr, proverif_before, proverif_after, proverif_replace, hax_backend_proverif)); diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap index 0cfc69aeb..ed5ec48ee 100644 --- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap @@ -26,6 +26,42 @@ exit = 0 diagnostics = [] [stdout.files] +"Attributes.Inlined_code_ensures_requires.fst" = ''' +module Attributes.Inlined_code_ensures_requires +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +let increment_array (v: t_Array u8 (sz 4)) + : Prims.Pure (t_Array u8 (sz 4)) + (requires forall i. FStar.Seq.index v i <. 254uy) + (ensures + fun temp_0_ -> + let vv_future, ():(t_Array u8 (sz 4) & Prims.unit) = temp_0_ in + let future_v:t_Array u8 (sz 4) = vv_future in + forall i. FStar.Seq.index future_v i >. 0uy) = + let v:t_Array u8 (sz 4) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v + (sz 0) + ((v.[ sz 0 ] <: u8) +! 1uy <: u8) + in + let v:t_Array u8 (sz 4) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v + (sz 1) + ((v.[ sz 1 ] <: u8) +! 1uy <: u8) + in + let v:t_Array u8 (sz 4) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v + (sz 2) + ((v.[ sz 2 ] <: u8) +! 1uy <: u8) + in + let v:t_Array u8 (sz 4) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v + (sz 3) + ((v.[ sz 3 ] <: u8) +! 1uy <: u8) + in + v +''' "Attributes.Int_model.fst" = ''' module Attributes.Int_model #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" diff --git a/tests/Cargo.lock b/tests/Cargo.lock index 43fd30c91..f48220811 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -322,6 +322,7 @@ name = "hax-lib-macros" version = "0.1.0-pre.1" dependencies = [ "hax-lib-macros-types", + "paste", "proc-macro-error", "proc-macro2", "quote", @@ -641,6 +642,12 @@ version = "6.6.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e2355d85b9a3786f481747ced0e0ff2ba35213a1f9bd406ed906554d7af805a1" +[[package]] +name = "paste" +version = "1.0.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a" + [[package]] name = "pattern-or" version = "0.1.0" diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs index e05040761..356cf494d 100644 --- a/tests/attributes/src/lib.rs +++ b/tests/attributes/src/lib.rs @@ -285,3 +285,18 @@ mod nested_refinement_elim { (DummyRefinement::new(x.get())).get() } } + +/// `ensures` and `requires` with inlined code (issue #825) +mod inlined_code_ensures_requires { + #[hax_lib::requires(fstar!("forall i. FStar.Seq.index $v i <. ${254u8}"))] + #[hax_lib::ensures(|()| { + let future_v = future(v); + fstar!("forall i. FStar.Seq.index ${future_v} i >. ${0u8}") + })] + fn increment_array(v: &mut [u8; 4]) { + v[0] += 1; + v[1] += 1; + v[2] += 1; + v[3] += 1; + } +} From 53ac07747ae3fb100d0afd80f95ff94efc002671 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 7 Aug 2024 10:46:34 +0200 Subject: [PATCH 5/6] fix(hax-lib): makes `inline_unsafe` a hax-only function --- hax-lib/src/lib.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/hax-lib/src/lib.rs b/hax-lib/src/lib.rs index 44eba43ab..e218bfe6c 100644 --- a/hax-lib/src/lib.rs +++ b/hax-lib/src/lib.rs @@ -143,6 +143,7 @@ pub fn inline(_: &str) {} /// Similar to `inline`, but allows for any type. Do not use directly. #[doc(hidden)] +#[cfg(hax)] pub fn inline_unsafe(_: &str) -> T { unreachable!() } From 88b4821690001dfc1cf4586807f01c0a7962f01e Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 7 Aug 2024 11:31:38 +0200 Subject: [PATCH 6/6] Revert "fix(hax-lib): makes `inline_unsafe` a hax-only function" This reverts commit 1d678493a7434364c089dd451467dcdea148a40d. `#[cfg(hax)]` makes the names crate not exporting the name, for some reason... I spent half an hour debbuging that, I have no clue what is going on. I give up for now. --- hax-lib/src/lib.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/hax-lib/src/lib.rs b/hax-lib/src/lib.rs index e218bfe6c..44eba43ab 100644 --- a/hax-lib/src/lib.rs +++ b/hax-lib/src/lib.rs @@ -143,7 +143,6 @@ pub fn inline(_: &str) {} /// Similar to `inline`, but allows for any type. Do not use directly. #[doc(hidden)] -#[cfg(hax)] pub fn inline_unsafe(_: &str) -> T { unreachable!() }