From 0419f5efce96b7a87fb56c80df50b529a82efd30 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 09:33:50 +0100 Subject: [PATCH 01/36] better prop --- examples/Cargo.lock | 8 ++++---- hax-lib/src/implementation.rs | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/examples/Cargo.lock b/examples/Cargo.lock index d0f1ab5b7..616831a31 100644 --- a/examples/Cargo.lock +++ b/examples/Cargo.lock @@ -248,7 +248,7 @@ checksum = "f93e7192158dbcda357bdec5fb5788eebf8bbac027f3f33e719d29135ae84156" [[package]] name = "hax-bounded-integers" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "duplicate", "hax-lib", @@ -257,7 +257,7 @@ dependencies = [ [[package]] name = "hax-lib" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "hax-lib-macros", "num-bigint", @@ -266,7 +266,7 @@ dependencies = [ [[package]] name = "hax-lib-macros" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "hax-lib-macros-types", "paste", @@ -278,7 +278,7 @@ dependencies = [ [[package]] name = "hax-lib-macros-types" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "proc-macro2", "quote", diff --git a/hax-lib/src/implementation.rs b/hax-lib/src/implementation.rs index ef8fea13f..eef17e124 100644 --- a/hax-lib/src/implementation.rs +++ b/hax-lib/src/implementation.rs @@ -63,14 +63,14 @@ macro_rules! assert { /// This function exists only when compiled with `hax`, and is not /// meant to be used directly. It is called by `assert!` only in /// appropriate situations. -pub fn assert(_formula: Prop) {} +pub fn assert>(_formula: T) {} #[doc(hidden)] #[cfg(hax)] /// This function exists only when compiled with `hax`, and is not /// meant to be used directly. It is called by `assume!` only in /// appropriate situations. -pub fn assume(_formula: Prop) {} +pub fn assume>(_formula: T) {} #[cfg(hax)] #[macro_export] @@ -113,7 +113,7 @@ pub fn inline_unsafe(_: &str) -> T { /// A dummy function that holds a loop invariant. #[doc(hidden)] -pub fn _internal_loop_invariant Prop>(_: P) {} +pub fn _internal_loop_invariant, P: FnOnce(T) -> U>(_: P) {} /// A type that implements `Refinement` should be a newtype for a /// type `T`. The field holding the value of type `T` should be @@ -133,7 +133,7 @@ pub trait Refinement { /// Gets a mutable reference to a refinement fn get_mut(&mut self) -> &mut Self::InnerType; /// Tests wether a value satisfies the refinement - fn invariant(value: Self::InnerType) -> Prop; + fn invariant>(value: Self::InnerType) -> T; } /// A utilitary trait that provides a `into_checked` method on traits From 53c757b5f5a8a3e95956f6963cf579c7e73c3e4f Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 09:52:20 +0100 Subject: [PATCH 02/36] prop --- hax-lib/proofs/fstar/extraction/Hax_lib.fst | 6 +- hax-lib/src/abstraction.rs | 18 +++++ hax-lib/src/dummy.rs | 5 +- hax-lib/src/prop.rs | 73 +++++++++++++++++++++ 4 files changed, 95 insertions(+), 7 deletions(-) create mode 100644 hax-lib/src/abstraction.rs create mode 100644 hax-lib/src/prop.rs diff --git a/hax-lib/proofs/fstar/extraction/Hax_lib.fst b/hax-lib/proofs/fstar/extraction/Hax_lib.fst index f28018ec2..61de78ac6 100644 --- a/hax-lib/proofs/fstar/extraction/Hax_lib.fst +++ b/hax-lib/proofs/fstar/extraction/Hax_lib.fst @@ -11,6 +11,6 @@ val v_assume (p: bool) : Pure unit (requires True) (ensures (fun x -> p)) let v_assume (v__formula: bool) = assume v__formula -unfold let v_exists (v__f: 'a -> Type0): Type0 = exists (x: 'a). v__f x -unfold let v_forall (v__f: 'a -> Type0): Type0 = forall (x: 'a). v__f x -unfold let implies (lhs: Type0) (rhs: (x:unit{lhs} -> bool)): bool = (not lhs) || rhs () +unfold let v_exists (v__f: 'a -> t_Prop): t_Prop = exists (x: 'a). v__f x +unfold let v_forall (v__f: 'a -> t_Prop): t_Prop = forall (x: 'a). v__f x +unfold let implies (lhs: t_Prop) (rhs: (x:unit{lhs} -> t_Prop)): t_Prop = (~ lhs) \/ rhs () diff --git a/hax-lib/src/abstraction.rs b/hax-lib/src/abstraction.rs new file mode 100644 index 000000000..2c25fd12b --- /dev/null +++ b/hax-lib/src/abstraction.rs @@ -0,0 +1,18 @@ +/// Marks a type as abstractable: its values can be mapped to an +/// idealized version of the type. For instance, machine integers, +/// which have bounds, can be mapped to mathematical integers. +/// +/// Each type can have only one abstraction. +pub trait Abstraction { + /// What is the ideal type values should be mapped to? + type AbstractType; + /// Maps a concrete value to its abstract counterpart + fn lift(self) -> Self::AbstractType; +} + +/// Marks a type as abstract: its values can be lowered to concrete +/// values. This might panic. +pub trait Concretization { + /// Maps an abstract value and lowers it to its concrete counterpart. + fn concretize(self) -> T; +} diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index 4dc21c877..2fc11668c 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -55,12 +55,9 @@ pub mod int { pub struct Int(pub u128); impl Int { - pub fn new(x: impl Into) -> Self { + pub fn new(x: impl Into) -> Self { Int(x.into()) } - pub fn get(self) -> u8 { - self.0 - } } impl Add for Int { diff --git a/hax-lib/src/prop.rs b/hax-lib/src/prop.rs new file mode 100644 index 000000000..af361b123 --- /dev/null +++ b/hax-lib/src/prop.rs @@ -0,0 +1,73 @@ +use super::abstraction::*; +use core::ops::*; + +pub struct Prop(bool); + +pub trait ToProp { + fn to_prop(self) -> Prop; +} + +impl Abstraction for bool { + type AbstractType = Prop; + fn lift(self) -> Self::AbstractType { + Prop(self) + } +} + +impl ToProp for bool { + fn to_prop(self) -> Prop { + self.lift() + } +} + +impl From for Prop { + fn from(value: bool) -> Self { + Prop(value) + } +} + +impl> BitAnd for Prop { + type Output = Prop; + fn bitand(self, rhs: T) -> Self::Output { + Prop(self.0 & rhs.into().0) + } +} + +impl> BitOr for Prop { + type Output = Prop; + fn bitor(self, rhs: T) -> Self::Output { + Prop(self.0 | rhs.into().0) + } +} + +impl Not for Prop { + type Output = Prop; + fn not(self) -> Self::Output { + Prop(! self.0) + } +} + +/// The universal quantifier. This should be used only for Hax code: in +/// Rust, this is always true. +/// +/// # Example: +/// +/// The Rust expression `forall(|x: T| phi(x))` corresponds to `∀ (x: T), phi(x)`. +pub fn forall>(_f: impl Fn(T) -> U) -> Prop { + Prop(true) +} + +/// The existential quantifier. This should be used only for Hax code: in +/// Rust, this is always true. +/// +/// # Example: +/// +/// The Rust expression `exists(|x: T| phi(x))` corresponds to `∃ (x: T), phi(x)`. +pub fn exists>(_f: impl Fn(T) -> U) -> Prop { + Prop(true) +} + +/// The logical implication `a ==> b`. +pub fn implies, U:Into>(lhs: T, rhs: impl Fn() -> U) -> Prop { + !lhs.into() | rhs().into() +} \ No newline at end of file From 4b5ba227c487f7ab02a380697f987180e1fab857 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 09:55:23 +0100 Subject: [PATCH 03/36] fix abs --- hax-lib/src/prop.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hax-lib/src/prop.rs b/hax-lib/src/prop.rs index af361b123..95a57c333 100644 --- a/hax-lib/src/prop.rs +++ b/hax-lib/src/prop.rs @@ -1,4 +1,4 @@ -use super::abstraction::*; +use crate::abstraction::*; use core::ops::*; pub struct Prop(bool); From 491cfa5b44c2e66f59007b20bd167639eaf212a8 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 09:57:32 +0100 Subject: [PATCH 04/36] fix abs --- hax-lib/src/dummy.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index 2fc11668c..c63de8c91 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -1,3 +1,6 @@ +mod abstraction; +pub use abstraction::*; + mod prop; use prop::*; From 49473b2686aabc4bbdd9cd872ee4826292fd9393 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 10:09:56 +0100 Subject: [PATCH 05/36] fix abs --- hax-lib/src/dummy.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index c63de8c91..7013b28a9 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -143,7 +143,7 @@ pub mod int { ($ty:ident $method:ident) => { impl Concretization<$ty> for Int { fn concretize(self) -> $ty { - self.0 as $ty; + self.0 as $ty } } impl Int { From d5b38630a0c0bfc8a0b11edb3e4f05d26a5d9b94 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 10:21:03 +0100 Subject: [PATCH 06/36] dummy --- hax-lib/src/dummy.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index 7013b28a9..e3fccc22f 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -4,6 +4,8 @@ pub use abstraction::*; mod prop; use prop::*; +use int::*; + #[cfg(feature = "macros")] pub use crate::proc_macros::*; From f7b3a907413586097cc768540e399cedae5ce33b Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 10:26:58 +0100 Subject: [PATCH 07/36] dummy - make prop, int public --- hax-lib/src/dummy.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index 43dacccec..062452918 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -2,9 +2,9 @@ mod abstraction; pub use abstraction::*; mod prop; -use prop::*; +pub use prop::*; -use int::*; +pub use int::*; #[cfg(feature = "macros")] pub use crate::proc_macros::*; From 64821e97c28d3bbfb71d660bbe284e9504bc6774 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 10:27:48 +0100 Subject: [PATCH 08/36] dummy - make prop, int public --- hax-lib/src/implementation.rs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/hax-lib/src/implementation.rs b/hax-lib/src/implementation.rs index 8af6efbcc..1546fe0d9 100644 --- a/hax-lib/src/implementation.rs +++ b/hax-lib/src/implementation.rs @@ -1,4 +1,8 @@ -pub mod int; +mod int; +pub use int::*; + +mod prop; +pub use prop::*; #[cfg(feature = "macros")] pub use crate::proc_macros::*; From bf1a982e6c8c3db3aa1833ce8fb0b1cd3d678352 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 10:29:36 +0100 Subject: [PATCH 09/36] fmt --- hax-lib/src/implementation.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/hax-lib/src/implementation.rs b/hax-lib/src/implementation.rs index 1546fe0d9..2522b4669 100644 --- a/hax-lib/src/implementation.rs +++ b/hax-lib/src/implementation.rs @@ -1,3 +1,6 @@ +mod abstraction; +pub use abstraction::*; + mod int; pub use int::*; From ec22ff03e7e0ff10d684aa4db1b1f2589fd9d742 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 10:34:32 +0100 Subject: [PATCH 10/36] fmt --- hax-lib/src/dummy.rs | 79 +++++++++++++++++++++-------------- hax-lib/src/implementation.rs | 26 +----------- hax-lib/src/int/mod.rs | 29 +++++-------- 3 files changed, 60 insertions(+), 74 deletions(-) diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index 062452918..c67ac8209 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -1,10 +1,5 @@ -mod abstraction; -pub use abstraction::*; - mod prop; -pub use prop::*; - -pub use int::*; +use prop::*; #[cfg(feature = "macros")] pub use crate::proc_macros::*; @@ -30,18 +25,6 @@ macro_rules! assume { }; } -pub fn forall(_f: impl Fn(T) -> bool) -> bool { - true -} - -pub fn exists(_f: impl Fn(T) -> bool) -> bool { - true -} - -pub fn implies(lhs: bool, rhs: impl Fn() -> bool) -> bool { - !lhs || rhs() -} - #[doc(hidden)] pub fn inline(_: &str) {} @@ -69,19 +52,22 @@ pub mod int { use core::ops::*; #[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd)] - pub struct Int(pub u8); + pub struct Int(pub u128); impl Int { - pub fn new(x: impl Into) -> Self { + pub fn new(x: impl Into) -> Self { Int(x.into()) } + pub fn get(self) -> u8 { + self.0 + } } impl Add for Int { type Output = Self; fn add(self, other: Self) -> Self::Output { - Int(0) + Int(self.0 + other.0) } } @@ -89,7 +75,7 @@ pub mod int { type Output = Self; fn sub(self, other: Self) -> Self::Output { - Int(0) + Int(self.0 - other.0) } } @@ -97,7 +83,7 @@ pub mod int { type Output = Self; fn mul(self, other: Self) -> Self::Output { - Int(0) + Int(self.0 * other.0) } } @@ -105,7 +91,7 @@ pub mod int { type Output = Self; fn div(self, other: Self) -> Self::Output { - Int(0) + Int(self.0 / other.0) } } @@ -118,6 +104,10 @@ pub mod int { } } + pub trait ToInt { + fn to_int(self) -> Int; + } + pub trait Abstraction { type AbstractType; fn lift(self) -> Self::AbstractType; @@ -127,11 +117,23 @@ pub mod int { fn concretize(self) -> T; } - impl Abstraction for u8 { - type AbstractType = Int; - fn lift(self) -> Self::AbstractType { - Int(0) - } + macro_rules! implement_abstraction { + ($ty:ident) => { + impl Abstraction for $ty { + type AbstractType = Int; + fn lift(self) -> Self::AbstractType { + Int(0) + } + } + impl ToInt for $ty { + fn to_int(self) -> Int { + self.lift() + } + } + }; + ($($ty:ident)*) => { + $(implement_abstraction!($ty);)* + }; } implement_abstraction!(u8 u16 u32 u64 u128 usize); @@ -141,7 +143,7 @@ pub mod int { ($ty:ident $method:ident) => { impl Concretization<$ty> for Int { fn concretize(self) -> $ty { - self.0 as $ty + self.0 as $ty; } } impl Int { @@ -156,4 +158,19 @@ pub mod int { }; () => {}; } -} + + implement_concretize!( + u8 to_u8, + u16 to_u16, + u32 to_u32, + u64 to_u64, + u128 to_u128, + usize to_usize, + i8 to_i8, + i16 to_i16, + i32 to_i32, + i64 to_i64, + i128 to_i128, + isize to_isize, + ); +} \ No newline at end of file diff --git a/hax-lib/src/implementation.rs b/hax-lib/src/implementation.rs index 2522b4669..1f5657937 100644 --- a/hax-lib/src/implementation.rs +++ b/hax-lib/src/implementation.rs @@ -100,30 +100,6 @@ macro_rules! assume { }; } -/// The universal quantifier. This should be used only for Hax code: in -/// Rust, this is always true. -/// -/// # Example: -/// -/// The Rust expression `forall(|x: T| phi(x))` corresponds to `∀ (x: T), phi(x)`. -pub fn forall(_f: impl Fn(T) -> bool) -> bool { - true -} - -/// The existential quantifier. This should be used only for Hax code: in -/// Rust, this is always true. -/// -/// # Example: -/// -/// The Rust expression `exists(|x: T| phi(x))` corresponds to `∃ (x: T), phi(x)`. -pub fn exists(_f: impl Fn(T) -> bool) -> bool { - true -} - -/// The logical implication `a ==> b`. -pub fn implies(lhs: bool, rhs: impl Fn() -> bool) -> bool { - !lhs || rhs() -} /// Dummy function that carries a string to be printed as such in the output language #[doc(hidden)] @@ -177,4 +153,4 @@ pub trait RefineAs { /// refinement type `RefinedType` with the `refinement_type` macro /// and its `no_debug_runtime_check` option. fn into_checked(self) -> RefinedType; -} +} \ No newline at end of file diff --git a/hax-lib/src/int/mod.rs b/hax-lib/src/int/mod.rs index 25e0939a0..def4fd68b 100644 --- a/hax-lib/src/int/mod.rs +++ b/hax-lib/src/int/mod.rs @@ -4,6 +4,8 @@ use num_traits::cast::ToPrimitive; mod bigint; use bigint::*; +use super::abstraction::*; + #[cfg(feature = "macros")] pub use hax_lib_macros::int; @@ -70,23 +72,9 @@ impl Int { } } -/// Marks a type as abstractable: its values can be mapped to an -/// idealized version of the type. For instance, machine integers, -/// which have bounds, can be mapped to mathematical integers. -/// -/// Each type can have only one abstraction. -pub trait Abstraction { - /// What is the ideal type values should be mapped to? - type AbstractType; - /// Maps a concrete value to its abstract counterpart - fn lift(self) -> Self::AbstractType; -} - -/// Marks a type as abstract: its values can be lowered to concrete -/// values. This might panic. -pub trait Concretization { - /// Maps an abstract value and lowers it to its concrete counterpart. - fn concretize(self) -> T; +#[cfg(feature = "macros")] +pub trait ToInt { + fn to_int(self) -> Int; } /// Instead of defining one overloaded instance, which relies @@ -112,6 +100,11 @@ macro_rules! implement_abstraction { Int::new(num_bigint::BigInt::from(self)) } } + impl ToInt for $ty { + fn to_int(self) -> Int { + self.lift() + } + } }; ($($ty:ident)*) => { $(implement_abstraction!($ty);)* @@ -156,4 +149,4 @@ implement_concretize!( i64 to_i64, i128 to_i128, isize to_isize, -); +); \ No newline at end of file From 270cccdb3af46eb6379f059dded7e883120fdb72 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 10:43:37 +0100 Subject: [PATCH 11/36] pub int/prop/abstraction --- hax-lib/src/dummy.rs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index c67ac8209..40864df1c 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -1,5 +1,10 @@ +mod abstraction; +pub use abstraction::*; + mod prop; -use prop::*; +pub use prop::*; + +pub use int::*; #[cfg(feature = "macros")] pub use crate::proc_macros::*; From bf39a62dfa74180602fac4f52626d31c8bd5bb01 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 10:52:08 +0100 Subject: [PATCH 12/36] fix concretize --- hax-lib/src/dummy.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index 40864df1c..2f32816ed 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -148,7 +148,7 @@ pub mod int { ($ty:ident $method:ident) => { impl Concretization<$ty> for Int { fn concretize(self) -> $ty { - self.0 as $ty; + self.0 as $ty } } impl Int { From 6dbeb6aec66a076c8033ecf5254441b7017fe110 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 10:52:50 +0100 Subject: [PATCH 13/36] fix concretize --- hax-lib/src/dummy.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index 2f32816ed..e9e849ae1 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -57,7 +57,7 @@ pub mod int { use core::ops::*; #[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd)] - pub struct Int(pub u128); + pub struct Int(pub u8); impl Int { pub fn new(x: impl Into) -> Self { From 884863432c746869ea30fc697caaa7bff073fcc4 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 11:14:39 +0100 Subject: [PATCH 14/36] Int --- engine/names/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs index af1ea0919..f3334d46e 100644 --- a/engine/names/src/lib.rs +++ b/engine/names/src/lib.rs @@ -52,7 +52,7 @@ fn dummy_hax_concrete_ident_wrapper>(x: I, mu } { - use hax_lib::int::*; + use hax_lib::*; let a: Int = 3u8.lift(); let _ = a.clone().pow2(); let _ = Int::_unsafe_from_str("1"); From 98ed62adc83e22d5ffbca310eaebfb16c1af42e4 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 11:24:35 +0100 Subject: [PATCH 15/36] macro requires ensures --- hax-lib/macros/src/utils.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/hax-lib/macros/src/utils.rs b/hax-lib/macros/src/utils.rs index f4c2ff72b..1a6ce7678 100644 --- a/hax-lib/macros/src/utils.rs +++ b/hax-lib/macros/src/utils.rs @@ -9,12 +9,12 @@ impl ToTokens for HaxQuantifiers { quote! { #AttrHaxLang #status_attr - fn forall bool>(f: F) -> bool { + fn forall, F: Fn(T) -> U>(f: F) -> hax_lib::Prop { true } #AttrHaxLang #status_attr - fn exists bool>(f: F) -> bool { + fn exists, F: Fn(T) -> U>(f: F) -> hax_lib::Prop { true } @@ -279,7 +279,7 @@ pub fn make_fn_decoration( sig.output = if let FnDecorationKind::Decreases = &kind { syn::parse_quote! { -> Box } } else { - syn::parse_quote! { -> bool } + syn::parse_quote! { -> hax_lib::Prop } }; sig }; From e49ac46b8cadd6bee124e5babfe6dff8797b1c04 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 12:28:22 +0100 Subject: [PATCH 16/36] macro requires ensures --- hax-lib/src/dummy.rs | 2 +- hax-lib/src/implementation.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index e9e849ae1..66814f64e 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -39,7 +39,7 @@ pub fn inline_unsafe(_: &str) -> T { } #[doc(hidden)] -pub fn _internal_loop_invariant bool>(_: P) {} +pub fn _internal_loop_invariant Prop>(_: P) {} pub trait Refinement { type InnerType; diff --git a/hax-lib/src/implementation.rs b/hax-lib/src/implementation.rs index 1f5657937..bccecc947 100644 --- a/hax-lib/src/implementation.rs +++ b/hax-lib/src/implementation.rs @@ -113,7 +113,7 @@ pub fn inline_unsafe(_: &str) -> T { /// A dummy function that holds a loop invariant. #[doc(hidden)] -pub fn _internal_loop_invariant, P: FnOnce(T) -> U>(_: P) {} +pub fn _internal_loop_invariant Prop>(_: P) {} /// A type that implements `Refinement` should be a newtype for a /// type `T`. The field holding the value of type `T` should be From ffb6b2297ae797dd96fb395cf8f1466d54bff056 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 12 Feb 2025 14:17:48 +0100 Subject: [PATCH 17/36] fix(macros): forall and exists return props --- hax-lib/macros/src/utils.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/hax-lib/macros/src/utils.rs b/hax-lib/macros/src/utils.rs index 1a6ce7678..ad300ee3a 100644 --- a/hax-lib/macros/src/utils.rs +++ b/hax-lib/macros/src/utils.rs @@ -10,12 +10,12 @@ impl ToTokens for HaxQuantifiers { #AttrHaxLang #status_attr fn forall, F: Fn(T) -> U>(f: F) -> hax_lib::Prop { - true + true.into() } #AttrHaxLang #status_attr fn exists, F: Fn(T) -> U>(f: F) -> hax_lib::Prop { - true + true.into() } use ::hax_lib::fstar_unsafe_expr as fstar; From 02fd662208c6799589b89ce5c06a1c61f88f6bfe Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 12 Feb 2025 18:02:24 +0100 Subject: [PATCH 18/36] fix(hax-lib/macros): force Prop for `fstar!` in requires/ensures --- hax-lib/macros/src/quote.rs | 2 +- hax-lib/macros/src/utils.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/hax-lib/macros/src/quote.rs b/hax-lib/macros/src/quote.rs index 8d13591c4..2f4de831a 100644 --- a/hax-lib/macros/src/quote.rs +++ b/hax-lib/macros/src/quote.rs @@ -212,7 +212,7 @@ pub(super) fn expression(force_unit: bool, payload: pm::TokenStream) -> pm::Toke let function = if force_unit { quote! {inline} } else { - quote! {inline_unsafe} + quote! {inline_unsafe::<::hax_lib::Prop>} }; quote! { diff --git a/hax-lib/macros/src/utils.rs b/hax-lib/macros/src/utils.rs index ad300ee3a..48fba6aea 100644 --- a/hax-lib/macros/src/utils.rs +++ b/hax-lib/macros/src/utils.rs @@ -279,7 +279,7 @@ pub fn make_fn_decoration( sig.output = if let FnDecorationKind::Decreases = &kind { syn::parse_quote! { -> Box } } else { - syn::parse_quote! { -> hax_lib::Prop } + syn::parse_quote! { -> impl Into } }; sig }; From 2ec30c19a2ffc29d5fa1767bf199432ff4bf1057 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 17 Feb 2025 16:23:03 +0100 Subject: [PATCH 19/36] feat(engine/F*): mark `b2t` as a keyword --- engine/backends/fstar/fstar_backend.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index e24625420..e07f9bddc 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -81,7 +81,7 @@ module FStarNamePolicy = struct let anonymous_field_transform index = "_" ^ index - let reserved_words = Hash_set.of_list (module String) ["attributes";"noeq";"unopteq";"and";"assert";"assume";"begin";"by";"calc";"class";"default";"decreases";"effect";"eliminate";"else";"end";"ensures";"exception";"exists";"false";"friend";"forall";"fun";"λ";"function";"if";"in";"include";"inline";"inline_for_extraction";"instance";"introduce";"irreducible";"let";"logic";"match";"returns";"as";"module";"new";"new_effect";"layered_effect";"polymonadic_bind";"polymonadic_subcomp";"noextract";"of";"open";"opaque";"private";"quote";"range_of";"rec";"reifiable";"reify";"reflectable";"requires";"set_range_of";"sub_effect";"synth";"then";"total";"true";"try";"type";"unfold";"unfoldable";"val";"when";"with";"_";"__SOURCE_FILE__";"__LINE__";"match";"if";"let";"and";"string"] + let reserved_words = Hash_set.of_list (module String) ["attributes";"noeq";"unopteq";"and";"assert";"assume";"begin";"by";"calc";"class";"default";"decreases";"b2t";"effect";"eliminate";"else";"end";"ensures";"exception";"exists";"false";"friend";"forall";"fun";"λ";"function";"if";"in";"include";"inline";"inline_for_extraction";"instance";"introduce";"irreducible";"let";"logic";"match";"returns";"as";"module";"new";"new_effect";"layered_effect";"polymonadic_bind";"polymonadic_subcomp";"noextract";"of";"open";"opaque";"private";"quote";"range_of";"rec";"reifiable";"reify";"reflectable";"requires";"set_range_of";"sub_effect";"synth";"then";"total";"true";"try";"type";"unfold";"unfoldable";"val";"when";"with";"_";"__SOURCE_FILE__";"__LINE__";"match";"if";"let";"and";"string"] end module RenderId = Concrete_ident.MakeRenderAPI (FStarNamePolicy) From e8a987f58ac01e02a7d6f50b492c2f7c9c4949e9 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 17 Feb 2025 16:48:54 +0100 Subject: [PATCH 20/36] fix(hax-lib/prop): always use prop, not bool --- hax-lib/macros/src/implementation.rs | 12 ++++++------ hax-lib/macros/src/utils.rs | 15 ++------------- hax-lib/macros/types/src/lib.rs | 2 +- hax-lib/proofs/fstar/extraction/Hax_lib.fst | 13 ++++--------- hax-lib/src/dummy.rs | 4 ++-- hax-lib/src/implementation.rs | 14 +++++++------- 6 files changed, 22 insertions(+), 38 deletions(-) diff --git a/hax-lib/macros/src/implementation.rs b/hax-lib/macros/src/implementation.rs index 2189232c7..8922e2c3b 100644 --- a/hax-lib/macros/src/implementation.rs +++ b/hax-lib/macros/src/implementation.rs @@ -45,7 +45,7 @@ pub fn fstar_options(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenS /// Add an invariant to a loop which deals with an index. The /// invariant cannot refer to any variable introduced within the /// loop. An invariant is a closure that takes one argument, the -/// index, and returns a boolean. +/// index, and returns a proposition. /// /// Note that loop invariants are unstable (this will be handled in a /// better way in the future, see @@ -175,7 +175,7 @@ pub fn modeled_by(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStre */ /// Mark a `Proof<{STATEMENT}>`-returning function as a lemma, where -/// `STATEMENT` is a boolean expression capturing any input +/// `STATEMENT` is a `Prop` expression capturing any input /// variable. /// In the backends, this will generate a lemma with an empty proof. /// @@ -245,7 +245,7 @@ pub fn lemma(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { } { abort!( item.sig.output.span(), - "A lemma is expected to return a `Proof<{STATEMENT}>`, where {STATEMENT} is a boolean expression." + "A lemma is expected to return a `Proof<{STATEMENT}>`, where {STATEMENT} is a `Prop` expression." ); } } @@ -596,7 +596,7 @@ pub fn attributes(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStr const _: () = { #uid_attr #status_attr - fn refinement(#binders) -> bool { #refine } + fn refinement(#binders) -> ::hax_lib::Prop { #refine } }; }) } @@ -865,7 +865,7 @@ 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. /// -/// This macro takes one argument: a boolean predicate that refines +/// This macro takes one argument: a `Prop` proposition that refines /// values of type `SomeType`. /// /// For example, the following type defines bounded `u64` integers. @@ -1015,7 +1015,7 @@ pub fn refinement_type(mut attr: pm::TokenStream, item: pm::TokenStream) -> pm:: fn get_mut(&mut self) -> &mut Self::InnerType { &mut self.0 } - fn invariant(#ret_binder: Self::InnerType) -> bool { + fn invariant(#ret_binder: Self::InnerType) -> ::hax_lib::Prop { #phi } } diff --git a/hax-lib/macros/src/utils.rs b/hax-lib/macros/src/utils.rs index 48fba6aea..f89244dcb 100644 --- a/hax-lib/macros/src/utils.rs +++ b/hax-lib/macros/src/utils.rs @@ -1,23 +1,12 @@ use crate::prelude::*; use crate::rewrite_self::*; -/// `HaxQuantifiers` expands to the definition of the `forall` and `exists` functions +/// `HaxQuantifiers` makes polymorphic expression inlining functions available pub struct HaxQuantifiers; impl ToTokens for HaxQuantifiers { fn to_tokens(&self, tokens: &mut proc_macro2::TokenStream) { let status_attr = &AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true }); quote! { - #AttrHaxLang - #status_attr - fn forall, F: Fn(T) -> U>(f: F) -> hax_lib::Prop { - true.into() - } - #AttrHaxLang - #status_attr - fn exists, F: Fn(T) -> U>(f: F) -> hax_lib::Prop { - true.into() - } - use ::hax_lib::fstar_unsafe_expr as fstar; use ::hax_lib::coq_unsafe_expr as coq; use ::hax_lib::proverif_unsafe_expr as proverif; @@ -279,7 +268,7 @@ pub fn make_fn_decoration( sig.output = if let FnDecorationKind::Decreases = &kind { syn::parse_quote! { -> Box } } else { - syn::parse_quote! { -> impl Into } + syn::parse_quote! { -> impl Into<::hax_lib::Prop> } }; sig }; diff --git a/hax-lib/macros/types/src/lib.rs b/hax-lib/macros/types/src/lib.rs index b342a1355..50b35f8d2 100644 --- a/hax-lib/macros/types/src/lib.rs +++ b/hax-lib/macros/types/src/lib.rs @@ -12,7 +12,7 @@ use serde::{Deserialize, Serialize}; /// in place with a simple reference (the `ItemUid` in stake). /// /// Morally, we expand `struct Foo { #[refine(x > 3)] x: u32 }` to: -/// 1. `#[uuid(A_UNIQUE_ID_123)] fn refinement(x: u32) -> bool {x > 3}`; +/// 1. `#[uuid(A_UNIQUE_ID_123)] fn refinement(x: u32) -> hax_lib::Prop {x > 3}`; /// 2. `struct Foo { #[refined_by(A_UNIQUE_ID_123)] x: u32 }`. #[derive(Debug, Clone, Serialize, Deserialize)] #[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))] diff --git a/hax-lib/proofs/fstar/extraction/Hax_lib.fst b/hax-lib/proofs/fstar/extraction/Hax_lib.fst index 4ef779aa7..640144815 100644 --- a/hax-lib/proofs/fstar/extraction/Hax_lib.fst +++ b/hax-lib/proofs/fstar/extraction/Hax_lib.fst @@ -2,13 +2,8 @@ module Hax_lib #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open FStar.Tactics -val v_assert (p: bool) : Pure unit (requires p) (ensures (fun x -> p)) -let v_assert (v__formula: bool) = () +val v_assert (p: Type0) : Pure unit (requires p) (ensures (fun x -> p)) +let v_assert (v__formula: Type0) = () -val v_assume (p: bool) : Pure unit (requires True) (ensures (fun x -> p)) -let v_assume (v__formula: bool) = assume v__formula - - -unfold let v_exists (v__f: 'a -> t_Prop): t_Prop = exists (x: 'a). v__f x -unfold let v_forall (v__f: 'a -> t_Prop): t_Prop = forall (x: 'a). v__f x -unfold let implies (lhs: t_Prop) (rhs: (x:unit{lhs} -> t_Prop)): t_Prop = (~ lhs) \/ rhs () +val v_assume (p: Type0) : Pure unit (requires True) (ensures (fun x -> p)) +let v_assume (v__formula: Type0) = assume v__formula diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index 66814f64e..5056a87a3 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -39,14 +39,14 @@ pub fn inline_unsafe(_: &str) -> T { } #[doc(hidden)] -pub fn _internal_loop_invariant Prop>(_: P) {} +pub fn _internal_loop_invariant, P: FnOnce(T) -> R>(_: P) {} pub trait Refinement { type InnerType; fn new(x: Self::InnerType) -> Self; fn get(self) -> Self::InnerType; fn get_mut(&mut self) -> &mut Self::InnerType; - fn invariant(value: Self::InnerType) -> bool; + fn invariant(value: Self::InnerType) -> crate::Prop; } pub trait RefineAs { diff --git a/hax-lib/src/implementation.rs b/hax-lib/src/implementation.rs index bccecc947..50c088277 100644 --- a/hax-lib/src/implementation.rs +++ b/hax-lib/src/implementation.rs @@ -54,7 +54,7 @@ macro_rules! debug_assert { /// into a `assert` in the backend. macro_rules! assert { ($($arg:tt)*) => { - $crate::proxy_macro_if_not_hax!(::core::assert, $crate::assert, $($arg)*) + $crate::proxy_macro_if_not_hax!(::core::assert, $crate::assert, $(::hax_lib::Prop::from($arg))*) }; } @@ -63,24 +63,24 @@ macro_rules! assert { /// This function exists only when compiled with `hax`, and is not /// meant to be used directly. It is called by `assert!` only in /// appropriate situations. -pub fn assert>(_formula: T) {} +pub fn assert(_formula: Prop) {} #[doc(hidden)] #[cfg(hax)] /// This function exists only when compiled with `hax`, and is not /// meant to be used directly. It is called by `assume!` only in /// appropriate situations. -pub fn assume>(_formula: T) {} +pub fn assume(_formula: Prop) {} #[cfg(hax)] #[macro_export] macro_rules! assume { ($formula:expr) => { - $crate::assume($formula) + $crate::assume(Prop::from($formula)) }; } -/// Assume a boolean formula holds. In Rust, this is expanded to the +/// Assume a proposition holds. In Rust, this is expanded to the /// expression `()`. While extracted with Hax, this gets expanded to a /// call to an `assume` function. /// @@ -113,7 +113,7 @@ pub fn inline_unsafe(_: &str) -> T { /// A dummy function that holds a loop invariant. #[doc(hidden)] -pub fn _internal_loop_invariant Prop>(_: P) {} +pub fn _internal_loop_invariant, P: FnOnce(T) -> R>(_: P) {} /// A type that implements `Refinement` should be a newtype for a /// type `T`. The field holding the value of type `T` should be @@ -133,7 +133,7 @@ pub trait Refinement { /// Gets a mutable reference to a refinement fn get_mut(&mut self) -> &mut Self::InnerType; /// Tests wether a value satisfies the refinement - fn invariant>(value: Self::InnerType) -> T; + fn invariant>(value: Self::InnerType) -> T; } /// A utilitary trait that provides a `into_checked` method on traits From 1ec966285205e10a4571de44aaf59dfccf884c3f Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 17 Feb 2025 16:50:17 +0100 Subject: [PATCH 21/36] chore(hax-lib/prop): fmt, visibility --- hax-lib/src/dummy.rs | 10 +++++----- hax-lib/src/implementation.rs | 7 +++---- hax-lib/src/prop.rs | 6 +++--- 3 files changed, 11 insertions(+), 12 deletions(-) diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index 5056a87a3..d3c3be2ac 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -1,7 +1,7 @@ mod abstraction; pub use abstraction::*; -mod prop; +pub mod prop; pub use prop::*; pub use int::*; @@ -140,10 +140,10 @@ pub mod int { $(implement_abstraction!($ty);)* }; } - + implement_abstraction!(u8 u16 u32 u64 u128 usize); implement_abstraction!(i8 i16 i32 i64 i128 isize); - + macro_rules! implement_concretize { ($ty:ident $method:ident) => { impl Concretization<$ty> for Int { @@ -163,7 +163,7 @@ pub mod int { }; () => {}; } - + implement_concretize!( u8 to_u8, u16 to_u16, @@ -178,4 +178,4 @@ pub mod int { i128 to_i128, isize to_isize, ); -} \ No newline at end of file +} diff --git a/hax-lib/src/implementation.rs b/hax-lib/src/implementation.rs index 50c088277..34f4beedb 100644 --- a/hax-lib/src/implementation.rs +++ b/hax-lib/src/implementation.rs @@ -1,10 +1,10 @@ mod abstraction; pub use abstraction::*; -mod int; +pub mod int; pub use int::*; -mod prop; +pub mod prop; pub use prop::*; #[cfg(feature = "macros")] @@ -100,7 +100,6 @@ macro_rules! assume { }; } - /// Dummy function that carries a string to be printed as such in the output language #[doc(hidden)] pub fn inline(_: &str) {} @@ -153,4 +152,4 @@ pub trait RefineAs { /// refinement type `RefinedType` with the `refinement_type` macro /// and its `no_debug_runtime_check` option. fn into_checked(self) -> RefinedType; -} \ No newline at end of file +} diff --git a/hax-lib/src/prop.rs b/hax-lib/src/prop.rs index 95a57c333..6361eb2fb 100644 --- a/hax-lib/src/prop.rs +++ b/hax-lib/src/prop.rs @@ -26,14 +26,14 @@ impl From for Prop { } } -impl> BitAnd for Prop { +impl> BitAnd for Prop { type Output = Prop; fn bitand(self, rhs: T) -> Self::Output { Prop(self.0 & rhs.into().0) } } -impl> BitOr for Prop { +impl> BitOr for Prop { type Output = Prop; fn bitor(self, rhs: T) -> Self::Output { Prop(self.0 | rhs.into().0) @@ -43,7 +43,7 @@ impl> BitOr for Prop { impl Not for Prop { type Output = Prop; fn not(self) -> Self::Output { - Prop(! self.0) + Prop(!self.0) } } From edae02e96f05f826bc1595d56721ab9eb0b6cc5d Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 17 Feb 2025 16:51:00 +0100 Subject: [PATCH 22/36] feat(hax-lib/prop): define everything in terms of `hax_lib::prop::constructors` --- hax-lib/src/prop.rs | 83 ++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 74 insertions(+), 9 deletions(-) diff --git a/hax-lib/src/prop.rs b/hax-lib/src/prop.rs index 6361eb2fb..8bb89574c 100644 --- a/hax-lib/src/prop.rs +++ b/hax-lib/src/prop.rs @@ -1,10 +1,72 @@ use crate::abstraction::*; use core::ops::*; +/// Represent a logical proposition, that may be not computable. +#[derive(Clone, Copy, Debug)] pub struct Prop(bool); -pub trait ToProp { - fn to_prop(self) -> Prop; +/// This module provides monomorphic constructors for `Prop`. +/// Hax rewrite more elaborated versions (see `forall` or `AndBit` below) to those monomorphic constructors. +pub mod constructors { + use super::Prop; + pub fn from_bool(b: bool) -> Prop { + Prop(b) + } + pub fn and(lhs: Prop, other: Prop) -> Prop { + Prop(lhs.0 && other.0) + } + pub fn or(lhs: Prop, other: Prop) -> Prop { + Prop(lhs.0 || other.0) + } + pub fn not(lhs: Prop) -> Prop { + Prop(!lhs.0) + } + pub fn eq(lhs: Prop, other: Prop) -> Prop { + Prop(lhs.0 == other.0) + } + pub fn ne(lhs: Prop, other: Prop) -> Prop { + Prop(lhs.0 != other.0) + } + pub fn implies(lhs: Prop, other: Prop) -> Prop { + Prop(lhs.0 || !other.0) + } + pub fn forall Prop>(_pred: F) -> Prop { + Prop(true) + } + pub fn exists Prop>(_pred: F) -> Prop { + Prop(true) + } +} + +impl Prop { + /// Lifts a boolean to a logical proposition. + pub fn from_bool(b: bool) -> Self { + constructors::from_bool(b) + } + /// Conjuction of two propositions. + pub fn and(self, other: impl Into) -> Self { + constructors::and(self, other.into()) + } + /// Disjunction of two propositions. + pub fn or(self, other: impl Into) -> Self { + constructors::or(self, other.into()) + } + /// Negation of a proposition. + pub fn not(self) -> Self { + constructors::not(self) + } + /// Equality between two propositions. + pub fn eq(self, other: impl Into) -> Self { + constructors::eq(self, other.into()) + } + /// Equality between two propositions. + pub fn ne(self, other: impl Into) -> Self { + constructors::ne(self, other.into()) + } + /// Logical implication. + pub fn implies(self, other: impl Into) -> Self { + constructors::implies(self, other.into()) + } } impl Abstraction for bool { @@ -14,6 +76,9 @@ impl Abstraction for bool { } } +pub trait ToProp { + fn to_prop(self) -> Prop; +} impl ToProp for bool { fn to_prop(self) -> Prop { self.lift() @@ -53,8 +118,8 @@ impl Not for Prop { /// # Example: /// /// The Rust expression `forall(|x: T| phi(x))` corresponds to `∀ (x: T), phi(x)`. -pub fn forall>(_f: impl Fn(T) -> U) -> Prop { - Prop(true) +pub fn forall>(f: impl Fn(T) -> U) -> Prop { + constructors::forall(|x| f(x).into()) } /// The existential quantifier. This should be used only for Hax code: in @@ -63,11 +128,11 @@ pub fn forall>(_f: impl Fn(T) -> U) -> Prop { /// # Example: /// /// The Rust expression `exists(|x: T| phi(x))` corresponds to `∃ (x: T), phi(x)`. -pub fn exists>(_f: impl Fn(T) -> U) -> Prop { - Prop(true) +pub fn exists>(f: impl Fn(T) -> U) -> Prop { + constructors::exists(|x| f(x).into()) } /// The logical implication `a ==> b`. -pub fn implies, U:Into>(lhs: T, rhs: impl Fn() -> U) -> Prop { - !lhs.into() | rhs().into() -} \ No newline at end of file +pub fn implies(lhs: impl Into, rhs: impl Into) -> Prop { + constructors::implies(lhs.into(), rhs.into()) +} From 807ed68d9fa5b056632f5ae58e2a90386e1c9d81 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 17 Feb 2025 16:51:28 +0100 Subject: [PATCH 23/36] feat(hax-lib/prop): F*: add `t_Prop` --- hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst diff --git a/hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst b/hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst new file mode 100644 index 000000000..3ccc865fa --- /dev/null +++ b/hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst @@ -0,0 +1,3 @@ +module Hax_lib.Prop + +unfold type t_Prop = Type0 From 62936eaa1f3a8dd2129b8bc22fada4c7d9eeb846 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 17 Feb 2025 16:52:23 +0100 Subject: [PATCH 24/36] fix(backend/F*): no not insert ascriptions on propositions --- engine/lib/ast_utils.ml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml index ef55bf45c..c65d4f68c 100644 --- a/engine/lib/ast_utils.ml +++ b/engine/lib/ast_utils.ml @@ -341,6 +341,14 @@ module Make (F : Features.T) = struct super#visit_expr' ascribe_app e method! visit_expr (ascribe_app : bool) e = + let ascribe_app = + ascribe_app + && not + (match e.typ with + | TApp { ident; _ } -> + Global_ident.eq_name Hax_lib__prop__Prop ident + | _ -> false) + in let e = super#visit_expr ascribe_app e in let ascribe (e : expr) = if [%matches? Ascription _] e.e then e From 326f52073cc6f23127e1952be4a4569e00a9935a Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 17 Feb 2025 16:53:35 +0100 Subject: [PATCH 25/36] fix(engine/specialize): rewrite prop functions --- engine/lib/phases/phase_specialize.ml | 206 +++++++++++++++++++++----- engine/names/src/lib.rs | 28 ++++ 2 files changed, 195 insertions(+), 39 deletions(-) diff --git a/engine/lib/phases/phase_specialize.ml b/engine/lib/phases/phase_specialize.ml index 5916792c2..3d39e6259 100644 --- a/engine/lib/phases/phase_specialize.ml +++ b/engine/lib/phases/phase_specialize.ml @@ -16,9 +16,57 @@ module Make (F : Features.T) = open struct open Concrete_ident_generated + module FnReplace = struct + type t = + span:Span.t -> + typ:ty -> + f:expr -> + args:expr list -> + generic_args:generic_value list -> + bounds_impls:impl_expr list -> + trait:(impl_expr * generic_value list) option -> + expr + + (** Retype a function application: this concretize the types, using concrete types from arguments. *) + let retype (fn : t) : t = + fun ~span ~typ ~f ~args ~generic_args ~bounds_impls ~trait -> + let f = + let typ = + if List.is_empty args then f.typ + else TArrow (List.map ~f:(fun e -> e.typ) args, typ) + in + { f with typ } + in + fn ~span ~typ ~f ~args ~generic_args ~bounds_impls ~trait + + (** Gets rid of trait and impl informations. *) + let remove_traits (fn : t) : t = + fun ~span ~typ ~f ~args ~generic_args:_ ~bounds_impls:_ ~trait:_ -> + fn ~span ~typ ~f ~args ~generic_args:[] ~bounds_impls:[] ~trait:None + + (** Monomorphize a function call: this removes any impl references, and concretize types. *) + let monorphic (fn : t) : t = remove_traits (retype fn) + + let name name : t = + fun ~span ~typ ~f ~args ~generic_args ~bounds_impls ~trait -> + let name = Ast.Global_ident.of_name ~value:true name in + let f = { f with e = GlobalVar name } in + let e = App { args; f; generic_args; bounds_impls; trait } in + { typ; span; e } + + let and_then (f1 : t) (f2 : expr -> expr) : t = + fun ~span ~typ ~f ~args ~generic_args ~bounds_impls ~trait -> + f1 ~span ~typ ~f ~args ~generic_args ~bounds_impls ~trait |> f2 + + let map_args (fn : int -> expr -> expr) : t -> t = + fun g ~span ~typ ~f ~args ~generic_args ~bounds_impls ~trait -> + let args = List.mapi ~f:fn args in + g ~span ~typ ~f ~args ~generic_args ~bounds_impls ~trait + end + type pattern = { fn : t; - fn_replace : t; + fn_replace : FnReplace.t; args : (expr -> bool) list; ret : ty -> bool; } @@ -29,12 +77,16 @@ module Make (F : Features.T) = work with `_ -> _ option` so that we can chain them *) (** Constructs a predicate out of predicates and names *) - let mk (args : ('a, 'b) predicate list) (ret : ('c, 'd) predicate) - (fn : t) (fn_replace : t) : pattern = + let mk' (args : ('a, 'b) predicate list) (ret : ('c, 'd) predicate) + (fn : t) (fn_replace : FnReplace.t) : pattern = let args = List.map ~f:(fun p x -> p x |> Option.is_some) args in let ret t = ret t |> Option.is_some in { fn; fn_replace; args; ret } + let mk (args : ('a, 'b) predicate list) (ret : ('c, 'd) predicate) + (fn : t) (fn_replace : t) : pattern = + mk' args ret fn (FnReplace.name fn_replace |> FnReplace.monorphic) + open struct let etyp (e : expr) : ty = e.typ let tref = function TRef { typ; _ } -> Some typ | _ -> None @@ -56,9 +108,21 @@ module Make (F : Features.T) = let erase : 'a. ('a, unit) predicate = fun _ -> Some () + let ( ||. ) (type a b) (f : (a, b) predicate) (g : (a, b) predicate) : + (a, b) predicate = + fun x -> + match (f x, g x) with Some a, _ | _, Some a -> Some a | _ -> None + let is_int : (ty, unit) predicate = tapp0 >>& eq_global_ident Hax_lib__int__Int >>& erase + let is_prop : (ty, unit) predicate = + tapp0 >>& eq_global_ident Hax_lib__prop__Prop >>& erase + + let is_bool : (ty, unit) predicate = function + | TBool -> Some () + | _ -> None + let any _ = Some () let int_any = mk [ etyp >> is_int ] any let int_int_any = mk [ etyp >> is_int; etyp >> is_int ] any @@ -69,10 +133,24 @@ module Make (F : Features.T) = mk [ etyp >> (tref >>& is_int); etyp >> (tref >>& is_int) ] any let any_rint = mk [ any ] (tref >>& is_int) + let bool_prop = mk [ etyp >> is_bool ] is_prop + let prop_bool = mk [ etyp >> is_prop ] is_bool + + let arrow : (ty, ty list) predicate = function + | TArrow (ts, t) -> Some (ts @ [ t ]) + | _ -> None + + let a_to_b a b : _ predicate = + arrow >> fun x -> + let* t, u = + match x with Some [ a; b ] -> Some (a, b) | _ -> None + in + let* a = a t in + let* b = b u in + Some (a, b) end - (** The list of replacements *) - let patterns = + let int_replacements = [ int_int_any Core__ops__arith__Add__add Rust_primitives__hax__int__add; @@ -94,11 +172,70 @@ module Make (F : Features.T) = Rust_primitives__hax__int__le; rint_rint_any Core__cmp__PartialEq__ne Rust_primitives__hax__int__ne; rint_rint_any Core__cmp__PartialEq__eq Rust_primitives__hax__int__eq; - any_rint Hax_lib__int__Abstraction__lift + any_rint Hax_lib__abstraction__Abstraction__lift Rust_primitives__hax__int__from_machine; - int_any Hax_lib__int__Concretization__concretize + int_any Hax_lib__abstraction__Concretization__concretize Rust_primitives__hax__int__into_machine; ] + + let prop_replacements = + let name_from_bool = Hax_lib__prop__constructors__from_bool in + let prop_type = + let ident = + Ast.Global_ident.of_name ~value:false Hax_lib__prop__Prop + in + TApp { ident; args = [] } + in + let bool_prop__from_bool f = bool_prop f name_from_bool in + let poly n f g = + let args = + let prop_or_bool = is_bool ||. is_prop in + List.init n ~f:(fun _ -> + etyp + >> (prop_or_bool + ||. (a_to_b prop_or_bool prop_or_bool >> erase))) + in + let promote_bool (e : A.expr) = + match e.typ with + | TBool -> U.call name_from_bool [ e ] e.span prop_type + | _ -> e + in + mk' args any f + (FnReplace.map_args + (fun _ e -> + let e = promote_bool e in + match e.e with + | Closure { params; body; captures } -> + let body = promote_bool body in + { e with e = Closure { params; body; captures } } + | _ -> e) + (FnReplace.name g |> FnReplace.monorphic)) + in + [ + bool_prop__from_bool Hax_lib__abstraction__Abstraction__lift; + bool_prop__from_bool Hax_lib__prop__ToProp__to_prop; + bool_prop__from_bool Core__convert__Into__into; + bool_prop__from_bool Core__convert__From__from; + (* Transform inherent methods on Prop *) + poly 2 Hax_lib__prop__Impl__and Hax_lib__prop__constructors__and; + poly 2 Hax_lib__prop__Impl__or Hax_lib__prop__constructors__or; + poly 1 Hax_lib__prop__Impl__not Hax_lib__prop__constructors__not; + poly 2 Hax_lib__prop__Impl__eq Hax_lib__prop__constructors__eq; + poly 2 Hax_lib__prop__Impl__ne Hax_lib__prop__constructors__ne; + poly 2 Hax_lib__prop__Impl__implies + Hax_lib__prop__constructors__implies; + (* Transform standalone functions in `prop` *) + poly 2 Hax_lib__prop__implies Hax_lib__prop__constructors__implies; + poly 1 Hax_lib__prop__forall Hax_lib__prop__constructors__forall; + poly 1 Hax_lib__prop__exists Hax_lib__prop__constructors__exists; + (* Transform core `&`, `|`, `!` on `Prop` *) + poly 2 Core__ops__bit__BitAnd__bitand + Hax_lib__prop__constructors__and; + poly 2 Core__ops__bit__BitOr__bitor Hax_lib__prop__constructors__or; + poly 1 Core__ops__bit__Not__not Hax_lib__prop__constructors__not; + ] + + let replacements = List.concat [ int_replacements; prop_replacements ] end module Error = Phase_utils.MakeError (struct @@ -123,45 +260,31 @@ module Make (F : Features.T) = } -> ( let l = List.map ~f:(self#visit_expr ()) l in let matching = - List.filter patterns ~f:(fun { fn; args; _ } -> + List.filter + (List.mapi ~f:(fun i x -> (i, x)) replacements) + ~f:(fun (_, { fn; args; ret; fn_replace = _ }) -> Ast.Global_ident.eq_name fn f + && ret e.typ && match List.for_all2 args l ~f:apply with | Ok r -> r | _ -> false) in match matching with - | [ { fn_replace; _ } ] -> - let f = Ast.Global_ident.of_name ~value:true fn_replace in - let f = { f' with e = GlobalVar f } in - { - e with - e = - App - { - f; - args = l; - trait = None; - generic_args = []; - bounds_impls = []; - }; - } + | [ (_, { fn_replace; _ }) ] -> + let e = + fn_replace ~args:l ~typ:e.typ ~span:e.span ~generic_args + ~bounds_impls ~trait ~f:f' + in + self#visit_expr () e | [] -> ( (* In this case we need to avoid recursing again through the arguments *) let visited = - super#visit_expr () - { - e with - e = - App - { - f = f'; - args = []; - trait; - generic_args; - bounds_impls; - }; - } + let args = [] in + let e' = + App { f = f'; args; trait; generic_args; bounds_impls } + in + super#visit_expr () { e with e = e' } in match visited.e with | App { f; trait; generic_args; bounds_impls; _ } -> @@ -172,9 +295,14 @@ module Make (F : Features.T) = { f; args = l; trait; generic_args; bounds_impls }; } | _ -> super#visit_expr () e) - | _ -> - Error.assertion_failure e.span - "Found multiple matching patterns") + | r -> + let msg = + "Found multiple matching patterns: " + ^ [%show: int list] (List.map ~f:fst r) + in + Stdio.prerr_endline msg; + U.Debug.expr e; + Error.assertion_failure e.span msg) | _ -> super#visit_expr () e end diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs index f3334d46e..72aabe404 100644 --- a/engine/names/src/lib.rs +++ b/engine/names/src/lib.rs @@ -31,6 +31,34 @@ fn dummy_hax_concrete_ident_wrapper>(x: I, mu hax_lib::assert!(true); hax_lib::_internal_loop_invariant(|_: usize| true); + fn props() { + use hax_lib::prop::*; + let x = Prop::from_bool(true); + constructors::from_bool(true); + constructors::and(x, x); + constructors::or(x, x); + constructors::not(x); + constructors::eq(x, x); + constructors::ne(x, x); + constructors::implies(x, || x); + constructors::forall(|_: ()| x); + constructors::exists(|_: ()| x); + + Prop::from_bool(true); + Prop::and(x, x); + Prop::or(x, x); + Prop::not(x); + Prop::eq(x, x); + Prop::ne(x, x); + Prop::implies(x, x); + + true.to_prop(); + + forall(|_: ()| x); + exists(|_: ()| x); + implies(x, || x); + } + let _ = [()].into_iter(); let _: u16 = 6u8.into(); let _ = 1..2; From 8886c11fba30e3b9d85e14113186611e7f4281cb Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 17 Feb 2025 16:54:24 +0100 Subject: [PATCH 26/36] feat(backend/F*): pretty print prop operators --- engine/backends/fstar/fstar_backend.ml | 55 +++++++++++++++++++++++++- 1 file changed, 54 insertions(+), 1 deletion(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index e07f9bddc..43e13478d 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -89,6 +89,7 @@ module U = Ast_utils.Make (InputLanguage) module Visitors = Ast_visitors.Make (InputLanguage) open AST module F = Fstar_ast +module Destruct = Ast_destruct.Make (InputLanguage) module Context = struct type t = { @@ -317,6 +318,12 @@ struct (c Rust_primitives__hax__int__lt, (2, "<")); (c Rust_primitives__hax__int__ne, (2, "<>")); (c Rust_primitives__hax__int__eq, (2, "=")); + (c Hax_lib__prop__constructors__and, (2, "/\\")); + (c Hax_lib__prop__constructors__or, (2, "\\/")); + (c Hax_lib__prop__constructors__not, (1, "~")); + (c Hax_lib__prop__constructors__eq, (2, "==")); + (c Hax_lib__prop__constructors__ne, (2, "=!=")); + (c Hax_lib__prop__constructors__implies, (2, "==>")); ] |> Map.of_alist_exn (module Global_ident) @@ -511,6 +518,52 @@ struct F.AST.unit_const F.dummyRange | GlobalVar global_ident -> F.term @@ F.AST.Var (pglobal_ident e.span @@ global_ident) + | App { f = { e = GlobalVar f; _ }; args = [ x ] } + when Global_ident.eq_name Hax_lib__prop__constructors__from_bool f -> + let x = pexpr x in + F.mk_e_app (F.term_of_lid [ "b2t" ]) [ x ] + | App + { + f = { e = GlobalVar f; _ }; + args = [ { e = Closure { params = [ x ]; body = phi; _ }; _ } ]; + } + when Global_ident.eq_name Hax_lib__prop__constructors__forall f -> + let phi = pexpr phi in + let binders = + let b = Destruct.pat_PBinding x |> Option.value_exn in + [ + F.AST. + { + b = F.AST.Annotated (plocal_ident b.var, pty x.span b.typ); + brange = F.dummyRange; + blevel = Un; + aqual = None; + battributes = []; + }; + ] + in + F.term @@ F.AST.QForall (binders, ([], []), phi) + | App + { + f = { e = GlobalVar f; _ }; + args = [ { e = Closure { params = [ x ]; body = phi; _ }; _ } ]; + } + when Global_ident.eq_name Hax_lib__prop__constructors__exists f -> + let phi = pexpr phi in + let binders = + let b = Destruct.pat_PBinding x |> Option.value_exn in + [ + F.AST. + { + b = F.AST.Annotated (plocal_ident b.var, pty x.span b.typ); + brange = F.dummyRange; + blevel = Un; + aqual = None; + battributes = []; + }; + ] + in + F.term @@ F.AST.QExists (binders, ([], []), phi) | App { f = { e = GlobalVar (`Projector (`TupleField (n, len))) }; @@ -525,7 +578,7 @@ struct let arity, op = Map.find_exn operators x in if List.length args <> arity then Error.assertion_failure e.span - "pexpr: bad arity for operator application"; + ("pexpr: bad arity for operator application (" ^ op ^ ")"); F.term @@ F.AST.Op (F.Ident.id_of_text op, List.map ~f:pexpr args) | App { From 652cbf4ab4bcb062d9de671ba33053fdccb54be0 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 17 Feb 2025 17:04:56 +0100 Subject: [PATCH 27/36] fix(hax-lib): drop useless variable --- hax-lib/macros/src/utils.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/hax-lib/macros/src/utils.rs b/hax-lib/macros/src/utils.rs index f89244dcb..c421200a2 100644 --- a/hax-lib/macros/src/utils.rs +++ b/hax-lib/macros/src/utils.rs @@ -5,7 +5,6 @@ use crate::rewrite_self::*; pub struct HaxQuantifiers; impl ToTokens for HaxQuantifiers { fn to_tokens(&self, tokens: &mut proc_macro2::TokenStream) { - let status_attr = &AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true }); quote! { use ::hax_lib::fstar_unsafe_expr as fstar; use ::hax_lib::coq_unsafe_expr as coq; From 31297b374389c7e99d806914dccdb4402d8df5f6 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 17 Feb 2025 17:19:03 +0100 Subject: [PATCH 28/36] fix(engine/specialize): fix minor bugs --- engine/lib/phases/phase_specialize.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/engine/lib/phases/phase_specialize.ml b/engine/lib/phases/phase_specialize.ml index 3d39e6259..e3defa774 100644 --- a/engine/lib/phases/phase_specialize.ml +++ b/engine/lib/phases/phase_specialize.ml @@ -172,7 +172,7 @@ module Make (F : Features.T) = Rust_primitives__hax__int__le; rint_rint_any Core__cmp__PartialEq__ne Rust_primitives__hax__int__ne; rint_rint_any Core__cmp__PartialEq__eq Rust_primitives__hax__int__eq; - any_rint Hax_lib__abstraction__Abstraction__lift + any_int Hax_lib__abstraction__Abstraction__lift Rust_primitives__hax__int__from_machine; int_any Hax_lib__abstraction__Concretization__concretize Rust_primitives__hax__int__into_machine; @@ -200,7 +200,7 @@ module Make (F : Features.T) = | TBool -> U.call name_from_bool [ e ] e.span prop_type | _ -> e in - mk' args any f + mk' args is_prop f (FnReplace.map_args (fun _ e -> let e = promote_bool e in From a0d8cb9d756ee1c4ce926170428ec066a6dea895 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 17 Feb 2025 17:19:41 +0100 Subject: [PATCH 29/36] fix(hax-lib): insert `from` calls for refinements --- hax-lib/macros/src/implementation.rs | 4 ++-- hax-lib/src/implementation.rs | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/hax-lib/macros/src/implementation.rs b/hax-lib/macros/src/implementation.rs index 8922e2c3b..fb933f087 100644 --- a/hax-lib/macros/src/implementation.rs +++ b/hax-lib/macros/src/implementation.rs @@ -596,7 +596,7 @@ pub fn attributes(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStr const _: () = { #uid_attr #status_attr - fn refinement(#binders) -> ::hax_lib::Prop { #refine } + fn refinement(#binders) -> ::hax_lib::Prop { ::hax_lib::Prop::from(#refine) } }; }) } @@ -1016,7 +1016,7 @@ pub fn refinement_type(mut attr: pm::TokenStream, item: pm::TokenStream) -> pm:: &mut self.0 } fn invariant(#ret_binder: Self::InnerType) -> ::hax_lib::Prop { - #phi + ::hax_lib::Prop::from(#phi) } } diff --git a/hax-lib/src/implementation.rs b/hax-lib/src/implementation.rs index 34f4beedb..f15d1324c 100644 --- a/hax-lib/src/implementation.rs +++ b/hax-lib/src/implementation.rs @@ -132,7 +132,7 @@ pub trait Refinement { /// Gets a mutable reference to a refinement fn get_mut(&mut self) -> &mut Self::InnerType; /// Tests wether a value satisfies the refinement - fn invariant>(value: Self::InnerType) -> T; + fn invariant(value: Self::InnerType) -> Prop; } /// A utilitary trait that provides a `into_checked` method on traits From 73411b495e0dcfeec40a5a729b4f33ce7cffd89f Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 17 Feb 2025 17:20:23 +0100 Subject: [PATCH 30/36] test(hax-lib/props): add test, fix tests --- .../toolchain__attributes into-fstar.snap | 24 +++++++++++++------ .../toolchain__literals into-coq.snap | 4 ++-- .../toolchain__loops into-fstar.snap | 2 +- tests/attributes/src/lib.rs | 16 ++++++++++--- tests/literals/src/lib.rs | 2 +- 5 files changed, 34 insertions(+), 14 deletions(-) diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap index 2cd940219..aefd0338d 100644 --- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap @@ -144,7 +144,7 @@ open FStar.Mul let v_MAX: usize = mk_usize 10 -type t_SafeIndex = { f_i:f_i: usize{f_i <. v_MAX} } +type t_SafeIndex = { f_i:f_i: usize{b2t (f_i <. v_MAX <: bool)} } let impl_SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex = if i <. v_MAX @@ -237,6 +237,19 @@ let test (x: v_T) : u8 = (f_method #v_T #FStar.Tactics.Typeclasses.solve x (mk_u8 99) <: u8) -! mk_u8 88 ''' +"Attributes.Props.fst" = ''' +module Attributes.Props +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +let f (x: Hax_lib.Prop.t_Prop) (y: bool) : Hax_lib.Prop.t_Prop = + let (xprop: Hax_lib.Prop.t_Prop):Hax_lib.Prop.t_Prop = b2t y in + let p:Hax_lib.Prop.t_Prop = b2t y /\ xprop /\ b2t y /\ b2t y in + ~(p \/ b2t y ==> + (forall (x: u8). b2t (x <=. Core.Num.impl_u8__MAX <: bool)) /\ + (exists (x: u16). b2t (x >. mk_u16 300 <: bool))) +''' "Attributes.Refined_arithmetic.fst" = ''' module Attributes.Refined_arithmetic #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -495,10 +508,7 @@ let add3 (x y z: u32) (ensures fun result -> let result:u32 = result in - Hax_lib.implies true - (fun temp_0_ -> - let _:Prims.unit = temp_0_ in - result >. mk_u32 32 <: bool)) = (x +! y <: u32) +! z + b2t true ==> b2t (result >. mk_u32 32 <: bool)) = (x +! y <: u32) +! z let swap_and_mut_req_ens (x y: u32) : Prims.Pure (u32 & u32 & u32) @@ -529,8 +539,8 @@ let add3_lemma (x: u32) type t_Foo = { f_x:u32; - f_y:f_y: u32{f_y >. mk_u32 3}; - f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. mk_u32 3} + f_y:f_y: u32{b2t (f_y >. mk_u32 3 <: bool)}; + f_z:f_z: u32{b2t (((f_y +! f_x <: u32) +! f_z <: u32) >. mk_u32 3 <: bool)} } let inlined_code__v_V: u8 = mk_u8 12 diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap index 6f95144b9..d2dadf182 100644 --- a/test-harness/src/snapshots/toolchain__literals into-coq.snap +++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap @@ -44,8 +44,8 @@ Import RecordSetNotations. (* NotImplementedYet *) -From Literals Require Import Hax_lib (t_int). -Export Hax_lib (t_int). +From Literals Require Import hax_lib. +Export hax_lib. Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl_Int__e_unsafe_from_str ("0"%string))) (f_lt (x) (impl_Int__e_unsafe_from_str ("16"%string))) = true} : t_u8 := let _ : t_Int := f_lift (3) in diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap index c713c83d4..1fae22223 100644 --- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap @@ -768,7 +768,7 @@ let enumerated_chunked_slice (#v_T: Type0) (slice: t_Slice v_T) : (u64 & Prims.u (fun count i -> let count:u64 = count in let i:usize = i in - i <= Core.Slice.impl__len #v_T slice <: usize) + i <= Core.Slice.impl__len #v_T slice) count (fun count i -> let count:u64 = count in diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs index 9af4f8ae3..589472bed 100644 --- a/tests/attributes/src/lib.rs +++ b/tests/attributes/src/lib.rs @@ -6,7 +6,7 @@ const u32_max: u32 = 90000; /// A doc comment on `add3` #[doc = "another doc comment on add3"] #[hax::requires(x > 10 && y > 10 && z > 10 && x + y + z < u32_max)] -#[hax::ensures(|result| hax_lib::implies(true, || result > 32))] +#[hax::ensures(|result| hax_lib::implies(true, result > 32))] fn add3(x: u32, y: u32, z: u32) -> u32 { x + y + z } @@ -181,7 +181,7 @@ fn some_function() -> String { } mod pre_post_on_traits_and_impls { - use hax_lib::int::*; + use hax_lib::*; #[hax_lib::attributes] trait Operation { @@ -348,7 +348,7 @@ mod verifcation_status { } mod requires_mut { - use hax_lib::int::*; + use hax_lib::*; #[hax_lib::attributes] trait Foo { @@ -397,3 +397,13 @@ mod issue_1266 { fn v(x: &mut Self); } } + +mod props { + use hax_lib::*; + + fn f(x: Prop, y: bool) -> Prop { + let xprop: Prop = y.into(); + let p = y.lift() & xprop & y & y.to_prop(); + !(p | y).implies(forall(|x: u8| x <= u8::MAX) & exists(|x: u16| x > 300)) + } +} diff --git a/tests/literals/src/lib.rs b/tests/literals/src/lib.rs index 7fbc1be70..37fc45d59 100644 --- a/tests/literals/src/lib.rs +++ b/tests/literals/src/lib.rs @@ -1,5 +1,5 @@ #![allow(dead_code)] -use hax_lib::int::*; +use hax_lib::*; #[hax_lib::requires(x > int!(0) && x < int!(16))] fn math_integers(x: Int) -> u8 { From f1e19940703e1681ecebce15a9a1c1a0aa5a04b0 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 17 Feb 2025 17:23:27 +0100 Subject: [PATCH 31/36] fix(name-crate/props): fix implies --- engine/names/src/lib.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs index 72aabe404..88eff705d 100644 --- a/engine/names/src/lib.rs +++ b/engine/names/src/lib.rs @@ -40,7 +40,7 @@ fn dummy_hax_concrete_ident_wrapper>(x: I, mu constructors::not(x); constructors::eq(x, x); constructors::ne(x, x); - constructors::implies(x, || x); + constructors::implies(x, x); constructors::forall(|_: ()| x); constructors::exists(|_: ()| x); @@ -56,7 +56,7 @@ fn dummy_hax_concrete_ident_wrapper>(x: I, mu forall(|_: ()| x); exists(|_: ()| x); - implies(x, || x); + implies(x, x); } let _ = [()].into_iter(); From a4c9c0c796091667af091f70945498517bbd0012 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 18 Feb 2025 08:17:59 +0100 Subject: [PATCH 32/36] fix(hax-lib): add non-computable `assert_prop` --- hax-lib/proofs/fstar/extraction/Hax_lib.fst | 7 ++++-- hax-lib/src/implementation.rs | 25 +++++++++++++++++++-- hax-lib/src/lib.rs | 6 +++-- 3 files changed, 32 insertions(+), 6 deletions(-) diff --git a/hax-lib/proofs/fstar/extraction/Hax_lib.fst b/hax-lib/proofs/fstar/extraction/Hax_lib.fst index 640144815..c1a7ef8e0 100644 --- a/hax-lib/proofs/fstar/extraction/Hax_lib.fst +++ b/hax-lib/proofs/fstar/extraction/Hax_lib.fst @@ -2,8 +2,11 @@ module Hax_lib #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open FStar.Tactics -val v_assert (p: Type0) : Pure unit (requires p) (ensures (fun x -> p)) -let v_assert (v__formula: Type0) = () +val v_assert (p: bool) : Pure unit (requires p) (ensures (fun x -> p)) +let v_assert (v__formula: bool) = () + +val assert_prop (p: Type0) : Pure unit (requires p) (ensures (fun x -> p)) +let assert_prop (v__formula: Type0) = () val v_assume (p: Type0) : Pure unit (requires True) (ensures (fun x -> p)) let v_assume (v__formula: Type0) = assume v__formula diff --git a/hax-lib/src/implementation.rs b/hax-lib/src/implementation.rs index f15d1324c..947390f68 100644 --- a/hax-lib/src/implementation.rs +++ b/hax-lib/src/implementation.rs @@ -54,7 +54,7 @@ macro_rules! debug_assert { /// into a `assert` in the backend. macro_rules! assert { ($($arg:tt)*) => { - $crate::proxy_macro_if_not_hax!(::core::assert, $crate::assert, $(::hax_lib::Prop::from($arg))*) + $crate::proxy_macro_if_not_hax!(::core::assert, $crate::assert, $($arg)*) }; } @@ -63,7 +63,28 @@ macro_rules! assert { /// This function exists only when compiled with `hax`, and is not /// meant to be used directly. It is called by `assert!` only in /// appropriate situations. -pub fn assert(_formula: Prop) {} +pub fn assert(_formula: bool) {} + +#[macro_export] +/// Assert a logical proposition [`Prop`]: this exists only in the backends of +/// hax. In Rust, this macro expands to an empty block `{ }`. +macro_rules! assert_prop { + ($($arg:tt)*) => { + { + #[cfg(hax)] + { + $crate::assert_prop($crate::Prop::from($($arg)*)); + } + } + }; +} + +#[doc(hidden)] +#[cfg(hax)] +/// This function exists only when compiled with `hax`, and is not meant to be +/// used directly. It is called by `assert_prop!` only in appropriate +/// situations. +pub fn assert_prop(_formula: Prop) {} #[doc(hidden)] #[cfg(hax)] diff --git a/hax-lib/src/lib.rs b/hax-lib/src/lib.rs index 304ace616..a481ecdf1 100644 --- a/hax-lib/src/lib.rs +++ b/hax-lib/src/lib.rs @@ -5,10 +5,12 @@ //! # Example: //! //! ```rust +//! use hax_lib::*; //! fn sum(x: Vec, y: Vec) -> Vec { //! hax_lib::assume!(x.len() == y.len()); -//! hax_lib::assert!(hax_lib::forall(|i: usize| hax_lib::implies(i < x.len(), || x[i] < 4242))); -//! hax_lib::debug_assert!(hax_lib::exists(|i: usize| hax_lib::implies(i < x.len(), || x[i] > 123))); +//! hax_lib::assert!(x.len() >= 0); +//! hax_lib::assert_prop!(forall(|i: usize| implies(i < x.len(), x[i] < 4242))); +//! hax_lib::debug_assert!(exists(|i: usize| implies(i < x.len(), x[i] > 123))); //! x.into_iter().zip(y.into_iter()).map(|(x, y)| x + y).collect() //! } //! ``` From e2891825591460499d160a55450a39006dd86140 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 18 Feb 2025 08:20:37 +0100 Subject: [PATCH 33/36] fix(hax-lib): `assert_prop`: define in `dummy` as well --- hax-lib/src/dummy.rs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index d3c3be2ac..72c883346 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -23,6 +23,11 @@ macro_rules! assert { }; } +#[macro_export] +macro_rules! assert_prop { + ($($arg:tt)*) => {{}}; +} + #[macro_export] macro_rules! assume { ($formula:expr) => { From d3e245464a0ce0f77108c0a47a21e49789e57aff Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 18 Feb 2025 08:54:50 +0100 Subject: [PATCH 34/36] fmt --- hax-lib/src/int/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hax-lib/src/int/mod.rs b/hax-lib/src/int/mod.rs index def4fd68b..c09eb448d 100644 --- a/hax-lib/src/int/mod.rs +++ b/hax-lib/src/int/mod.rs @@ -149,4 +149,4 @@ implement_concretize!( i64 to_i64, i128 to_i128, isize to_isize, -); \ No newline at end of file +); From 96967d4c777d9360094dfd56f00d4f8bda88de8d Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Tue, 18 Feb 2025 20:44:41 +0530 Subject: [PATCH 35/36] regen example code --- .../extraction/Chacha20.Hacspec_helper.fst | 174 +++++++------- .../proofs/fstar/extraction/Chacha20.fst | 86 +++---- .../sha256/proofs/fstar/extraction/Sha256.fst | 212 +++++++++--------- 3 files changed, 237 insertions(+), 235 deletions(-) diff --git a/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst b/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst index 21d11370e..40c92fcff 100644 --- a/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst +++ b/examples/chacha20/proofs/fstar/extraction/Chacha20.Hacspec_helper.fst @@ -1,85 +1,24 @@ module Chacha20.Hacspec_helper -#set-options "--fuel 0 --ifuel 1 --z3rlimit 40" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul -let add_state (state other: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_usize 16) = - let state:t_Array u32 (mk_usize 16) = - Rust_primitives.Hax.Folds.fold_range (mk_usize 0) - (mk_usize 16) - (fun state temp_1_ -> - let state:t_Array u32 (mk_usize 16) = state in - let _:usize = temp_1_ in - true) - state - (fun state i -> - let state:t_Array u32 (mk_usize 16) = state in - let i:usize = i in - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state - i - (Core.Num.impl__u32__wrapping_add (state.[ i ] <: u32) (other.[ i ] <: u32) <: u32) - <: - t_Array u32 (mk_usize 16)) - in - state - -let update_array (array: t_Array u8 (mk_usize 64)) (v_val: t_Slice u8) : t_Array u8 (mk_usize 64) = - let _:Prims.unit = - Hax_lib.v_assert (mk_usize 64 >=. (Core.Slice.impl__len #u8 v_val <: usize) <: bool) - in - let array:t_Array u8 (mk_usize 64) = - Rust_primitives.Hax.Folds.fold_range (mk_usize 0) - (Core.Slice.impl__len #u8 v_val <: usize) - (fun array temp_1_ -> - let array:t_Array u8 (mk_usize 64) = array in - let _:usize = temp_1_ in - true) - array - (fun array i -> - let array:t_Array u8 (mk_usize 64) = array in - let i:usize = i in - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize array i (v_val.[ i ] <: u8) - <: - t_Array u8 (mk_usize 64)) - in - array - -let xor_state (state other: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_usize 16) = - let state:t_Array u32 (mk_usize 16) = - Rust_primitives.Hax.Folds.fold_range (mk_usize 0) - (mk_usize 16) - (fun state temp_1_ -> - let state:t_Array u32 (mk_usize 16) = state in - let _:usize = temp_1_ in - true) - state - (fun state i -> - let state:t_Array u32 (mk_usize 16) = state in - let i:usize = i in - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state - i - ((state.[ i ] <: u32) ^. (other.[ i ] <: u32) <: u32) - <: - t_Array u32 (mk_usize 16)) - in - state - -let to_le_u32s_16_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 16) = - let out:t_Array u32 (mk_usize 16) = Rust_primitives.Hax.repeat (mk_u32 0) (mk_usize 16) in - let out:t_Array u32 (mk_usize 16) = +let to_le_u32s_3_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 3) = + let out:t_Array u32 (mk_usize 3) = Rust_primitives.Hax.repeat (mk_u32 0) (mk_usize 3) in + let out:t_Array u32 (mk_usize 3) = Rust_primitives.Hax.Folds.fold_range (mk_usize 0) - (mk_usize 16) + (mk_usize 3) (fun out temp_1_ -> - let out:t_Array u32 (mk_usize 16) = out in + let out:t_Array u32 (mk_usize 3) = out in let _:usize = temp_1_ in true) out (fun out i -> - let out:t_Array u32 (mk_usize 16) = out in + let out:t_Array u32 (mk_usize 3) = out in let i:usize = i in Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out i - (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4)) + (Core.Num.impl_u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4)) #Core.Array.t_TryFromSliceError (Core.Convert.f_try_into #(t_Slice u8) #(t_Array u8 (mk_usize 4)) @@ -101,26 +40,26 @@ let to_le_u32s_16_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 16) = <: u32) <: - t_Array u32 (mk_usize 16)) + t_Array u32 (mk_usize 3)) in out -let to_le_u32s_3_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 3) = - let out:t_Array u32 (mk_usize 3) = Rust_primitives.Hax.repeat (mk_u32 0) (mk_usize 3) in - let out:t_Array u32 (mk_usize 3) = +let to_le_u32s_8_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 8) = + let out:t_Array u32 (mk_usize 8) = Rust_primitives.Hax.repeat (mk_u32 0) (mk_usize 8) in + let out:t_Array u32 (mk_usize 8) = Rust_primitives.Hax.Folds.fold_range (mk_usize 0) - (mk_usize 3) + (mk_usize 8) (fun out temp_1_ -> - let out:t_Array u32 (mk_usize 3) = out in + let out:t_Array u32 (mk_usize 8) = out in let _:usize = temp_1_ in true) out (fun out i -> - let out:t_Array u32 (mk_usize 3) = out in + let out:t_Array u32 (mk_usize 8) = out in let i:usize = i in Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out i - (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4)) + (Core.Num.impl_u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4)) #Core.Array.t_TryFromSliceError (Core.Convert.f_try_into #(t_Slice u8) #(t_Array u8 (mk_usize 4)) @@ -142,26 +81,26 @@ let to_le_u32s_3_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 3) = <: u32) <: - t_Array u32 (mk_usize 3)) + t_Array u32 (mk_usize 8)) in out -let to_le_u32s_8_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 8) = - let out:t_Array u32 (mk_usize 8) = Rust_primitives.Hax.repeat (mk_u32 0) (mk_usize 8) in - let out:t_Array u32 (mk_usize 8) = +let to_le_u32s_16_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 16) = + let out:t_Array u32 (mk_usize 16) = Rust_primitives.Hax.repeat (mk_u32 0) (mk_usize 16) in + let out:t_Array u32 (mk_usize 16) = Rust_primitives.Hax.Folds.fold_range (mk_usize 0) - (mk_usize 8) + (mk_usize 16) (fun out temp_1_ -> - let out:t_Array u32 (mk_usize 8) = out in + let out:t_Array u32 (mk_usize 16) = out in let _:usize = temp_1_ in true) out (fun out i -> - let out:t_Array u32 (mk_usize 8) = out in + let out:t_Array u32 (mk_usize 16) = out in let i:usize = i in Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out i - (Core.Num.impl__u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4)) + (Core.Num.impl_u32__from_le_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4)) #Core.Array.t_TryFromSliceError (Core.Convert.f_try_into #(t_Slice u8) #(t_Array u8 (mk_usize 4)) @@ -183,7 +122,7 @@ let to_le_u32s_8_ (bytes: t_Slice u8) : t_Array u32 (mk_usize 8) = <: u32) <: - t_Array u32 (mk_usize 8)) + t_Array u32 (mk_usize 16)) in out @@ -200,7 +139,7 @@ let u32s_to_le_bytes (state: t_Array u32 (mk_usize 16)) : t_Array u8 (mk_usize 6 (fun out i -> let out:t_Array u8 (mk_usize 64) = out in let i:usize = i in - let tmp:t_Array u8 (mk_usize 4) = Core.Num.impl__u32__to_le_bytes (state.[ i ] <: u32) in + let tmp:t_Array u8 (mk_usize 4) = Core.Num.impl_u32__to_le_bytes (state.[ i ] <: u32) in Rust_primitives.Hax.Folds.fold_range (mk_usize 0) (mk_usize 4) (fun out temp_1_ -> @@ -218,3 +157,64 @@ let u32s_to_le_bytes (state: t_Array u32 (mk_usize 16)) : t_Array u8 (mk_usize 6 t_Array u8 (mk_usize 64))) in out + +let xor_state (state other: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_usize 16) = + let state:t_Array u32 (mk_usize 16) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + (mk_usize 16) + (fun state temp_1_ -> + let state:t_Array u32 (mk_usize 16) = state in + let _:usize = temp_1_ in + true) + state + (fun state i -> + let state:t_Array u32 (mk_usize 16) = state in + let i:usize = i in + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state + i + ((state.[ i ] <: u32) ^. (other.[ i ] <: u32) <: u32) + <: + t_Array u32 (mk_usize 16)) + in + state + +let add_state (state other: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_usize 16) = + let state:t_Array u32 (mk_usize 16) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + (mk_usize 16) + (fun state temp_1_ -> + let state:t_Array u32 (mk_usize 16) = state in + let _:usize = temp_1_ in + true) + state + (fun state i -> + let state:t_Array u32 (mk_usize 16) = state in + let i:usize = i in + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state + i + (Core.Num.impl_u32__wrapping_add (state.[ i ] <: u32) (other.[ i ] <: u32) <: u32) + <: + t_Array u32 (mk_usize 16)) + in + state + +let update_array (array: t_Array u8 (mk_usize 64)) (v_val: t_Slice u8) : t_Array u8 (mk_usize 64) = + let _:Prims.unit = + Hax_lib.v_assert (mk_usize 64 >=. (Core.Slice.impl__len #u8 v_val <: usize) <: bool) + in + let array:t_Array u8 (mk_usize 64) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + (Core.Slice.impl__len #u8 v_val <: usize) + (fun array temp_1_ -> + let array:t_Array u8 (mk_usize 64) = array in + let _:usize = temp_1_ in + true) + array + (fun array i -> + let array:t_Array u8 (mk_usize 64) = array in + let i:usize = i in + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize array i (v_val.[ i ] <: u8) + <: + t_Array u8 (mk_usize 64)) + in + array diff --git a/examples/chacha20/proofs/fstar/extraction/Chacha20.fst b/examples/chacha20/proofs/fstar/extraction/Chacha20.fst index f21b19a52..5526e7bc9 100644 --- a/examples/chacha20/proofs/fstar/extraction/Chacha20.fst +++ b/examples/chacha20/proofs/fstar/extraction/Chacha20.fst @@ -1,5 +1,5 @@ module Chacha20 -#set-options "--fuel 0 --ifuel 1 --z3rlimit 40" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -18,7 +18,7 @@ let chacha20_line let state:t_Array u32 (mk_usize 16) = Rust_primitives.Hax.update_at state a - (Core.Num.impl__u32__wrapping_add (state.[ a ] <: u32) (state.[ b ] <: u32) <: u32) + (Core.Num.impl_u32__wrapping_add (state.[ a ] <: u32) (state.[ b ] <: u32) <: u32) in let state:t_Array u32 (mk_usize 16) = Rust_primitives.Hax.update_at state d ((state.[ d ] <: u32) ^. (state.[ a ] <: u32) <: u32) @@ -26,7 +26,7 @@ let chacha20_line let state:t_Array u32 (mk_usize 16) = Rust_primitives.Hax.update_at state d - (Core.Num.impl__u32__rotate_left (state.[ d ] <: u32) s <: u32) + (Core.Num.impl_u32__rotate_left (state.[ d ] <: u32) s <: u32) in state @@ -121,9 +121,9 @@ let chacha20_rounds (state: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_usize 1 let _:i32 = temp_1_ in true) st - (fun st v__i -> + (fun st e_i -> let st:t_Array u32 (mk_usize 16) = st in - let v__i:i32 = v__i in + let e_i:i32 = e_i in chacha20_double_round st <: t_Array u32 (mk_usize 16)) in st @@ -133,11 +133,39 @@ let chacha20_core (ctr: u32) (st0: t_Array u32 (mk_usize 16)) : t_Array u32 (mk_ let state:t_Array u32 (mk_usize 16) = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state (mk_usize 12) - (Core.Num.impl__u32__wrapping_add (state.[ mk_usize 12 ] <: u32) ctr <: u32) + (Core.Num.impl_u32__wrapping_add (state.[ mk_usize 12 ] <: u32) ctr <: u32) in let k:t_Array u32 (mk_usize 16) = chacha20_rounds state in Chacha20.Hacspec_helper.add_state state k +let chacha20_init (key: t_Array u8 (mk_usize 32)) (iv: t_Array u8 (mk_usize 12)) (ctr: u32) + : t_Array u32 (mk_usize 16) = + let (key_u32: t_Array u32 (mk_usize 8)):t_Array u32 (mk_usize 8) = + Chacha20.Hacspec_helper.to_le_u32s_8_ (key <: t_Slice u8) + in + let (iv_u32: t_Array u32 (mk_usize 3)):t_Array u32 (mk_usize 3) = + Chacha20.Hacspec_helper.to_le_u32s_3_ (iv <: t_Slice u8) + in + let list = + [ + mk_u32 1634760805; mk_u32 857760878; mk_u32 2036477234; mk_u32 1797285236; + key_u32.[ mk_usize 0 ]; key_u32.[ mk_usize 1 ]; key_u32.[ mk_usize 2 ]; key_u32.[ mk_usize 3 ]; + key_u32.[ mk_usize 4 ]; key_u32.[ mk_usize 5 ]; key_u32.[ mk_usize 6 ]; key_u32.[ mk_usize 7 ]; + ctr; iv_u32.[ mk_usize 0 ]; iv_u32.[ mk_usize 1 ]; iv_u32.[ mk_usize 2 ] + ] + in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 16); + Rust_primitives.Hax.array_of_list 16 list + +let chacha20_key_block (state: t_Array u32 (mk_usize 16)) : t_Array u8 (mk_usize 64) = + let state:t_Array u32 (mk_usize 16) = chacha20_core (mk_u32 0) state in + Chacha20.Hacspec_helper.u32s_to_le_bytes state + +let chacha20_key_block0 (key: t_Array u8 (mk_usize 32)) (iv: t_Array u8 (mk_usize 12)) + : t_Array u8 (mk_usize 64) = + let state:t_Array u32 (mk_usize 16) = chacha20_init key iv (mk_u32 0) in + chacha20_key_block state + let chacha20_encrypt_block (st0: t_Array u32 (mk_usize 16)) (ctr: u32) @@ -169,34 +197,6 @@ let chacha20_encrypt_last (st0: t_Array u32 (mk_usize 16)) (ctr: u32) (plain: t_ <: t_Slice u8) -let chacha20_init (key: t_Array u8 (mk_usize 32)) (iv: t_Array u8 (mk_usize 12)) (ctr: u32) - : t_Array u32 (mk_usize 16) = - let (key_u32: t_Array u32 (mk_usize 8)):t_Array u32 (mk_usize 8) = - Chacha20.Hacspec_helper.to_le_u32s_8_ (key <: t_Slice u8) - in - let (iv_u32: t_Array u32 (mk_usize 3)):t_Array u32 (mk_usize 3) = - Chacha20.Hacspec_helper.to_le_u32s_3_ (iv <: t_Slice u8) - in - let list = - [ - mk_u32 1634760805; mk_u32 857760878; mk_u32 2036477234; mk_u32 1797285236; - key_u32.[ mk_usize 0 ]; key_u32.[ mk_usize 1 ]; key_u32.[ mk_usize 2 ]; key_u32.[ mk_usize 3 ]; - key_u32.[ mk_usize 4 ]; key_u32.[ mk_usize 5 ]; key_u32.[ mk_usize 6 ]; key_u32.[ mk_usize 7 ]; - ctr; iv_u32.[ mk_usize 0 ]; iv_u32.[ mk_usize 1 ]; iv_u32.[ mk_usize 2 ] - ] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 16); - Rust_primitives.Hax.array_of_list 16 list - -let chacha20_key_block (state: t_Array u32 (mk_usize 16)) : t_Array u8 (mk_usize 64) = - let state:t_Array u32 (mk_usize 16) = chacha20_core (mk_u32 0) state in - Chacha20.Hacspec_helper.u32s_to_le_bytes state - -let chacha20_key_block0 (key: t_Array u8 (mk_usize 32)) (iv: t_Array u8 (mk_usize 12)) - : t_Array u8 (mk_usize 64) = - let state:t_Array u32 (mk_usize 16) = chacha20_init key iv (mk_u32 0) in - chacha20_key_block state - let chacha20_update (st0: t_Array u32 (mk_usize 16)) (m: t_Slice u8) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in @@ -237,10 +237,11 @@ let chacha20_update (st0: t_Array u32 (mk_usize 16)) (m: t_Slice u8) t_Array u8 (mk_usize 64)) in let _:Prims.unit = - Hax_lib.v_assume ((Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global blocks_out <: usize) =. - (i *! mk_usize 64 <: usize) - <: - bool) + Hax_lib.v_assume (b2t + ((Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global blocks_out <: usize) =. + (i *! mk_usize 64 <: usize) + <: + bool)) in let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl_2__extend_from_slice #u8 @@ -251,10 +252,11 @@ let chacha20_update (st0: t_Array u32 (mk_usize 16)) (m: t_Slice u8) blocks_out) in let _:Prims.unit = - Hax_lib.v_assume ((Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global blocks_out <: usize) =. - (num_blocks *! mk_usize 64 <: usize) - <: - bool) + Hax_lib.v_assume (b2t + ((Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global blocks_out <: usize) =. + (num_blocks *! mk_usize 64 <: usize) + <: + bool)) in let blocks_out:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = if remainder_len <>. mk_usize 0 diff --git a/examples/sha256/proofs/fstar/extraction/Sha256.fst b/examples/sha256/proofs/fstar/extraction/Sha256.fst index 835f8bf68..9dcbcc2b2 100644 --- a/examples/sha256/proofs/fstar/extraction/Sha256.fst +++ b/examples/sha256/proofs/fstar/extraction/Sha256.fst @@ -5,25 +5,25 @@ open FStar.Mul let v_BLOCK_SIZE: usize = mk_usize 64 -let v_HASH_INIT: t_Array u32 (mk_usize 8) = +let v_LEN_SIZE: usize = mk_usize 8 + +let v_K_SIZE: usize = mk_usize 64 + +let v_HASH_SIZE: usize = mk_usize 256 /! mk_usize 8 + +let ch (x y z: u32) : u32 = (x &. y <: u32) ^. ((~.x <: u32) &. z <: u32) + +let maj (x y z: u32) : u32 = (x &. y <: u32) ^. ((x &. z <: u32) ^. (y &. z <: u32) <: u32) + +let v_OP_TABLE: t_Array u8 (mk_usize 12) = let list = [ - mk_u32 1779033703; - mk_u32 3144134277; - mk_u32 1013904242; - mk_u32 2773480762; - mk_u32 1359893119; - mk_u32 2600822924; - mk_u32 528734635; - mk_u32 1541459225 + mk_u8 2; mk_u8 13; mk_u8 22; mk_u8 6; mk_u8 11; mk_u8 25; mk_u8 7; mk_u8 18; mk_u8 3; mk_u8 17; + mk_u8 19; mk_u8 10 ] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 8); - Rust_primitives.Hax.array_of_list 8 list - -let v_HASH_SIZE: usize = mk_usize 256 /! mk_usize 8 - -let v_K_SIZE: usize = mk_usize 64 + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 12); + Rust_primitives.Hax.array_of_list 12 list let v_K_TABLE: t_Array u32 (mk_usize 64) = let list = @@ -46,25 +46,25 @@ let v_K_TABLE: t_Array u32 (mk_usize 64) = FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 64); Rust_primitives.Hax.array_of_list 64 list -let v_LEN_SIZE: usize = mk_usize 8 - -let v_OP_TABLE: t_Array u8 (mk_usize 12) = +let v_HASH_INIT: t_Array u32 (mk_usize 8) = let list = [ - mk_u8 2; mk_u8 13; mk_u8 22; mk_u8 6; mk_u8 11; mk_u8 25; mk_u8 7; mk_u8 18; mk_u8 3; mk_u8 17; - mk_u8 19; mk_u8 10 + mk_u32 1779033703; + mk_u32 3144134277; + mk_u32 1013904242; + mk_u32 2773480762; + mk_u32 1359893119; + mk_u32 2600822924; + mk_u32 528734635; + mk_u32 1541459225 ] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 12); - Rust_primitives.Hax.array_of_list 12 list - -let ch (x y z: u32) : u32 = (x &. y <: u32) ^. ((~.x <: u32) &. z <: u32) - -let maj (x y z: u32) : u32 = (x &. y <: u32) ^. ((x &. z <: u32) ^. (y &. z <: u32) <: u32) + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 8); + Rust_primitives.Hax.array_of_list 8 list let sigma (x: u32) (i op: usize) : Prims.Pure u32 (requires i <. mk_usize 4) (fun _ -> Prims.l_True) = let (tmp: u32):u32 = - Core.Num.impl__u32__rotate_right x + Core.Num.impl_u32__rotate_right x (Core.Convert.f_into #u8 #u32 #FStar.Tactics.Typeclasses.solve @@ -89,84 +89,12 @@ let sigma (x: u32) (i op: usize) : Prims.Pure u32 (requires i <. mk_usize 4) (fu #FStar.Tactics.Typeclasses.solve (v_OP_TABLE.[ (mk_usize 3 *! i <: usize) +! mk_usize 1 <: usize ] <: u8) in - ((Core.Num.impl__u32__rotate_right x rot_val_1_ <: u32) ^. - (Core.Num.impl__u32__rotate_right x rot_val_2_ <: u32) + ((Core.Num.impl_u32__rotate_right x rot_val_1_ <: u32) ^. + (Core.Num.impl_u32__rotate_right x rot_val_2_ <: u32) <: u32) ^. tmp -let shuffle (ws: t_Array u32 (mk_usize 64)) (hashi: t_Array u32 (mk_usize 8)) - : t_Array u32 (mk_usize 8) = - let h:t_Array u32 (mk_usize 8) = hashi in - let h:t_Array u32 (mk_usize 8) = - Rust_primitives.Hax.Folds.fold_range (mk_usize 0) - v_K_SIZE - (fun h temp_1_ -> - let h:t_Array u32 (mk_usize 8) = h in - let _:usize = temp_1_ in - true) - h - (fun h i -> - let h:t_Array u32 (mk_usize 8) = h in - let i:usize = i in - let a0:u32 = h.[ mk_usize 0 ] in - let b0:u32 = h.[ mk_usize 1 ] in - let c0:u32 = h.[ mk_usize 2 ] in - let d0:u32 = h.[ mk_usize 3 ] in - let e0:u32 = h.[ mk_usize 4 ] in - let f0:u32 = h.[ mk_usize 5 ] in - let g0:u32 = h.[ mk_usize 6 ] in - let (h0: u32):u32 = h.[ mk_usize 7 ] in - let t1:u32 = - Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add - (Core.Num.impl__u32__wrapping_add h0 - (sigma e0 (mk_usize 1) (mk_usize 1) <: u32) - <: - u32) - (ch e0 f0 g0 <: u32) - <: - u32) - (v_K_TABLE.[ i ] <: u32) - <: - u32) - (ws.[ i ] <: u32) - in - let t2:u32 = - Core.Num.impl__u32__wrapping_add (sigma a0 (mk_usize 0) (mk_usize 1) <: u32) - (maj a0 b0 c0 <: u32) - in - let h:t_Array u32 (mk_usize 8) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h - (mk_usize 0) - (Core.Num.impl__u32__wrapping_add t1 t2 <: u32) - in - let h:t_Array u32 (mk_usize 8) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 1) a0 - in - let h:t_Array u32 (mk_usize 8) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 2) b0 - in - let h:t_Array u32 (mk_usize 8) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 3) c0 - in - let h:t_Array u32 (mk_usize 8) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h - (mk_usize 4) - (Core.Num.impl__u32__wrapping_add d0 t1 <: u32) - in - let h:t_Array u32 (mk_usize 8) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 5) e0 - in - let h:t_Array u32 (mk_usize 8) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 6) f0 - in - let h:t_Array u32 (mk_usize 8) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 7) g0 - in - h) - in - h - let to_be_u32s (block: t_Array u8 (mk_usize 64)) : Alloc.Vec.t_Vec u32 Alloc.Alloc.t_Global = let out:Alloc.Vec.t_Vec u32 Alloc.Alloc.t_Global = Alloc.Vec.impl__with_capacity #u32 (v_BLOCK_SIZE /! mk_usize 4 <: usize) @@ -185,7 +113,7 @@ let to_be_u32s (block: t_Array u8 (mk_usize 64)) : Alloc.Vec.t_Vec u32 Alloc.All let out:Alloc.Vec.t_Vec u32 Alloc.Alloc.t_Global = out in let block_chunk:t_Slice u8 = block_chunk in let block_chunk_array:u32 = - Core.Num.impl__u32__from_be_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4)) + Core.Num.impl_u32__from_be_bytes (Core.Result.impl__unwrap #(t_Array u8 (mk_usize 4)) #Core.Array.t_TryFromSliceError (Core.Convert.f_try_into #(t_Slice u8) #(t_Array u8 (mk_usize 4)) @@ -233,7 +161,7 @@ let schedule (block: t_Array u8 (mk_usize 64)) : t_Array u32 (mk_usize 64) = let s:t_Array u32 (mk_usize 64) = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize s i - (Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add + (Core.Num.impl_u32__wrapping_add (Core.Num.impl_u32__wrapping_add (Core.Num.impl_u32__wrapping_add s1 t7 <: @@ -249,6 +177,78 @@ let schedule (block: t_Array u8 (mk_usize 64)) : t_Array u32 (mk_usize 64) = in s +let shuffle (ws: t_Array u32 (mk_usize 64)) (hashi: t_Array u32 (mk_usize 8)) + : t_Array u32 (mk_usize 8) = + let h:t_Array u32 (mk_usize 8) = hashi in + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Folds.fold_range (mk_usize 0) + v_K_SIZE + (fun h temp_1_ -> + let h:t_Array u32 (mk_usize 8) = h in + let _:usize = temp_1_ in + true) + h + (fun h i -> + let h:t_Array u32 (mk_usize 8) = h in + let i:usize = i in + let a0:u32 = h.[ mk_usize 0 ] in + let b0:u32 = h.[ mk_usize 1 ] in + let c0:u32 = h.[ mk_usize 2 ] in + let d0:u32 = h.[ mk_usize 3 ] in + let e0:u32 = h.[ mk_usize 4 ] in + let f0:u32 = h.[ mk_usize 5 ] in + let g0:u32 = h.[ mk_usize 6 ] in + let (h0: u32):u32 = h.[ mk_usize 7 ] in + let t1:u32 = + Core.Num.impl_u32__wrapping_add (Core.Num.impl_u32__wrapping_add (Core.Num.impl_u32__wrapping_add + (Core.Num.impl_u32__wrapping_add h0 + (sigma e0 (mk_usize 1) (mk_usize 1) <: u32) + <: + u32) + (ch e0 f0 g0 <: u32) + <: + u32) + (v_K_TABLE.[ i ] <: u32) + <: + u32) + (ws.[ i ] <: u32) + in + let t2:u32 = + Core.Num.impl_u32__wrapping_add (sigma a0 (mk_usize 0) (mk_usize 1) <: u32) + (maj a0 b0 c0 <: u32) + in + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h + (mk_usize 0) + (Core.Num.impl_u32__wrapping_add t1 t2 <: u32) + in + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 1) a0 + in + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 2) b0 + in + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 3) c0 + in + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h + (mk_usize 4) + (Core.Num.impl_u32__wrapping_add d0 t1 <: u32) + in + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 5) e0 + in + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 6) f0 + in + let h:t_Array u32 (mk_usize 8) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h (mk_usize 7) g0 + in + h) + in + h + let compress (block: t_Array u8 (mk_usize 64)) (h_in: t_Array u32 (mk_usize 8)) : t_Array u32 (mk_usize 8) = let s:t_Array u32 (mk_usize 64) = schedule block in @@ -266,7 +266,7 @@ let compress (block: t_Array u8 (mk_usize 64)) (h_in: t_Array u32 (mk_usize 8)) let i:usize = i in Rust_primitives.Hax.Monomorphized_update_at.update_at_usize h i - (Core.Num.impl__u32__wrapping_add (h.[ i ] <: u32) (h_in.[ i ] <: u32) <: u32) + (Core.Num.impl_u32__wrapping_add (h.[ i ] <: u32) (h_in.[ i ] <: u32) <: u32) <: t_Array u32 (mk_usize 8)) in @@ -288,7 +288,7 @@ let u32s_to_be_bytes (state: t_Array u32 (mk_usize 8)) : t_Array u8 (mk_usize 32 let out:t_Array u8 (mk_usize 32) = out in let i:usize = i in let tmp:u32 = state.[ i ] in - let tmp:t_Array u8 (mk_usize 4) = Core.Num.impl__u32__to_be_bytes tmp in + let tmp:t_Array u8 (mk_usize 4) = Core.Num.impl_u32__to_be_bytes tmp in Rust_primitives.Hax.Folds.fold_range (mk_usize 0) (mk_usize 4) (fun out temp_1_ -> @@ -377,7 +377,7 @@ let hash (msg: t_Slice u8) : t_Array u8 (mk_usize 32) = (mk_u8 128) in let len_bist:u64 = cast ((Core.Slice.impl__len #u8 msg <: usize) *! mk_usize 8 <: usize) <: u64 in - let len_bist_bytes:t_Array u8 (mk_usize 8) = Core.Num.impl__u64__to_be_bytes len_bist in + let len_bist_bytes:t_Array u8 (mk_usize 8) = Core.Num.impl_u64__to_be_bytes len_bist in let h, last_block:(t_Array u32 (mk_usize 8) & t_Array u8 (mk_usize 64)) = if last_block_len <. (v_BLOCK_SIZE -! v_LEN_SIZE <: usize) then From 927c221d15b56d65df866453ae5d5c0a9bce2409 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 18 Feb 2025 16:46:41 +0100 Subject: [PATCH 36/36] feat(engine/specialize): monorphize `to_int` into `from_machine` --- engine/lib/phases/phase_specialize.ml | 2 ++ engine/names/src/lib.rs | 1 + 2 files changed, 3 insertions(+) diff --git a/engine/lib/phases/phase_specialize.ml b/engine/lib/phases/phase_specialize.ml index e3defa774..07b0891ab 100644 --- a/engine/lib/phases/phase_specialize.ml +++ b/engine/lib/phases/phase_specialize.ml @@ -174,6 +174,8 @@ module Make (F : Features.T) = rint_rint_any Core__cmp__PartialEq__eq Rust_primitives__hax__int__eq; any_int Hax_lib__abstraction__Abstraction__lift Rust_primitives__hax__int__from_machine; + any_int Hax_lib__int__ToInt__to_int + Rust_primitives__hax__int__from_machine; int_any Hax_lib__abstraction__Concretization__concretize Rust_primitives__hax__int__into_machine; ] diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs index 88eff705d..718c534df 100644 --- a/engine/names/src/lib.rs +++ b/engine/names/src/lib.rs @@ -82,6 +82,7 @@ fn dummy_hax_concrete_ident_wrapper>(x: I, mu { use hax_lib::*; let a: Int = 3u8.lift(); + let _: Int = 3u8.to_int(); let _ = a.clone().pow2(); let _ = Int::_unsafe_from_str("1"); let _: u32 = a.concretize();