Revert "using Prop for propositions, revealing more Int"

This reverts commit 6bd3e9b.

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 ()

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<T>(_f: impl Fn(T) -> bool) -> bool {
+    true
+}
+
+pub fn exists<T>(_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<u8>) -> Self {
@@ -67,31 +76,31 @@ pub mod int {
         type Output = Self;
 
         fn add(self, other: Self) -> Self::Output {
-            Int(self.0 + other.0)
+            Int(0)
         }
     }
 
     impl Sub for Int {
         type Output = Self;
 
         fn sub(self, other: Self) -> Self::Output {
-            Int(self.0 - other.0)
+            Int(0)
         }
     }
 
     impl Mul for Int {
         type Output = Self;
 
         fn mul(self, other: Self) -> Self::Output {
-            Int(self.0 * other.0)
+            Int(0)
         }
     }
 
     impl Div for 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<u32> 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,
-    );
 }

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<T>(_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<T>(_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<T>(_: &str) -> T {
 
 /// A dummy function that holds a loop invariant.
 #[doc(hidden)]
-pub fn _internal_loop_invariant<T, P: FnOnce(T) -> Prop>(_: P) {}
+pub fn _internal_loop_invariant<T, P: FnOnce(T) -> 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

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<T> {
+    /// 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);)*