From 0b22be4786d263959d7ad262ea961ff255597906 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Sun, 9 Feb 2025 09:24:50 +0100 Subject: [PATCH] Revert "using Prop for propositions, revealing more Int" This reverts commit 6bd3e9bd3789033b0a8b6012db86b44b85fc4bd2. --- hax-lib/proofs/fstar/extraction/Hax_lib.fst | 4 +- hax-lib/src/dummy.rs | 100 +++++++------------- hax-lib/src/implementation.rs | 41 +++++--- hax-lib/src/int/mod.rs | 27 ++++-- 4 files changed, 81 insertions(+), 91 deletions(-) diff --git a/hax-lib/proofs/fstar/extraction/Hax_lib.fst b/hax-lib/proofs/fstar/extraction/Hax_lib.fst index f28018ec2..377b36f5d 100644 --- a/hax-lib/proofs/fstar/extraction/Hax_lib.fst +++ b/hax-lib/proofs/fstar/extraction/Hax_lib.fst @@ -2,8 +2,6 @@ module Hax_lib #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open FStar.Tactics -type t_Prop = Type0 - val v_assert (p: bool) : Pure unit (requires p) (ensures (fun x -> p)) let v_assert (v__formula: bool) = () @@ -13,4 +11,4 @@ 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 implies (lhs: bool) (rhs: (x:unit{lhs} -> bool)): bool = (not lhs) || rhs () diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs index 4dc21c877..891187753 100644 --- a/hax-lib/src/dummy.rs +++ b/hax-lib/src/dummy.rs @@ -1,6 +1,3 @@ -mod prop; -use prop::*; - #[cfg(feature = "macros")] pub use crate::proc_macros::*; @@ -25,6 +22,18 @@ 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) {} @@ -52,7 +61,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 { @@ -67,7 +76,7 @@ pub mod int { type Output = Self; fn add(self, other: Self) -> Self::Output { - Int(self.0 + other.0) + Int(0) } } @@ -75,7 +84,7 @@ pub mod int { type Output = Self; fn sub(self, other: Self) -> Self::Output { - Int(self.0 - other.0) + Int(0) } } @@ -83,7 +92,7 @@ pub mod int { type Output = Self; fn mul(self, other: Self) -> Self::Output { - Int(self.0 * other.0) + Int(0) } } @@ -91,7 +100,7 @@ pub mod int { type Output = Self; fn div(self, other: Self) -> Self::Output { - Int(self.0 / other.0) + Int(0) } } @@ -104,10 +113,6 @@ pub mod int { } } - pub trait ToInt { - fn to_int(self) -> Int; - } - pub trait Abstraction { type AbstractType; fn lift(self) -> Self::AbstractType; @@ -117,60 +122,23 @@ pub mod int { fn concretize(self) -> T; } - 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);)* - }; + impl Abstraction for u8 { + type AbstractType = Int; + fn lift(self) -> Self::AbstractType { + Int(0) + } + } + + impl Abstraction for i32 { + type AbstractType = Int; + fn lift(self) -> Self::AbstractType { + Int(0) + } } - - 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 { - fn concretize(self) -> $ty { - self.0 as $ty; - } - } - impl Int { - pub fn $method(self) -> $ty { - self.concretize() - } - } - }; - ($ty:ident $method:ident, $($tt:tt)*) => { - implement_concretize!($ty $method); - implement_concretize!($($tt)*); - }; - () => {}; + + impl Concretization for Int { + fn concretize(self) -> u32 { + 0 + } } - - 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, - ); } diff --git a/hax-lib/src/implementation.rs b/hax-lib/src/implementation.rs index ef8fea13f..8afd9eca7 100644 --- a/hax-lib/src/implementation.rs +++ b/hax-lib/src/implementation.rs @@ -1,11 +1,4 @@ -mod abstraction; -pub use abstraction::*; - -mod int; -pub use int::*; - -mod prop; -pub use prop::*; +pub mod int; #[cfg(feature = "macros")] pub use crate::proc_macros::*; @@ -63,14 +56,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: bool) {} #[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: bool) {} #[cfg(hax)] #[macro_export] @@ -100,6 +93,30 @@ 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)] @@ -113,7 +130,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 bool>(_: 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 +150,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) -> bool; } /// A utilitary trait that provides a `into_checked` method on traits diff --git a/hax-lib/src/int/mod.rs b/hax-lib/src/int/mod.rs index c09eb448d..25e0939a0 100644 --- a/hax-lib/src/int/mod.rs +++ b/hax-lib/src/int/mod.rs @@ -4,8 +4,6 @@ use num_traits::cast::ToPrimitive; mod bigint; use bigint::*; -use super::abstraction::*; - #[cfg(feature = "macros")] pub use hax_lib_macros::int; @@ -72,9 +70,23 @@ impl Int { } } -#[cfg(feature = "macros")] -pub trait ToInt { - fn to_int(self) -> 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; } /// Instead of defining one overloaded instance, which relies @@ -100,11 +112,6 @@ 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);)*