From 5e1842f150a6f63b110b0a3ff7e7db293436e256 Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Thu, 5 Mar 2026 22:19:58 -0800 Subject: [PATCH 1/6] Support IEEE floating point SMT theory --- source/air/src/ast.rs | 44 +++ source/air/src/closure.rs | 34 ++- source/air/src/parser.rs | 120 +++++++- source/air/src/printer.rs | 97 +++++- source/air/src/tests.rs | 28 +- source/air/src/typecheck.rs | 186 +++++++++++- source/builtin/src/lib.rs | 324 +++++++++++++++++++++ source/builtin_macros/src/syntax_trait.rs | 4 +- source/rust_verify/src/fn_call_to_vir.rs | 118 +++++++- source/rust_verify/src/rust_to_vir_base.rs | 17 ++ source/rust_verify/src/verus_items.rs | 59 ++++ source/rust_verify_test/tests/float.rs | 89 ++++++ source/rust_verify_test/tests/real.rs | 2 +- source/vir/src/ast.rs | 37 +++ source/vir/src/ast_simplify.rs | 15 +- source/vir/src/ast_util.rs | 14 +- source/vir/src/bitvector_to_air.rs | 142 ++++++++- source/vir/src/datatype_to_air.rs | 11 + source/vir/src/def.rs | 26 ++ source/vir/src/heuristics.rs | 4 +- source/vir/src/interpreter.rs | 14 +- source/vir/src/poly.rs | 4 +- source/vir/src/prelude.rs | 57 ++++ source/vir/src/printer.rs | 1 + source/vir/src/prune.rs | 7 + source/vir/src/sst_to_air.rs | 61 +++- source/vir/src/sst_util.rs | 11 +- source/vir/src/triggers.rs | 11 +- source/vir/src/triggers_auto.rs | 5 +- source/vstd/contrib/mod.rs | 1 + source/vstd/float.rs | 2 +- 31 files changed, 1489 insertions(+), 56 deletions(-) diff --git a/source/air/src/ast.rs b/source/air/src/ast.rs index 783b92ec59..1a22ba8149 100644 --- a/source/air/src/ast.rs +++ b/source/air/src/ast.rs @@ -22,7 +22,13 @@ pub enum TypX { // Fun deliberately omits argument, return types to make box/unbox for generics easier Fun, Named(Ident), + // Bit vector; the u32 is the number of bits (e.g. (_ BitVec 64) is BitVec(64)) BitVec(u32), + // IEEE floating point type with exp_bits exponent bits and sig_bits significand bits, + // counting the implicit leading 1 bit in the significand + // (e.g. f32 is Float { exp_bits: 8, sig_bits: 24 }) + // See https://smt-lib.org/theories-FloatingPoint.shtml + Float { exp_bits: u32, sig_bits: u32 }, } #[derive(Clone, PartialEq, Eq, Hash)] // for Debug, see ast_util @@ -35,6 +41,20 @@ pub enum Constant { BitVec(Arc, u32), } +#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)] +pub enum RoundingMode { + // roundNearestTiesToEven + RNE, + // roundNearestTiesToAway + RNA, + // roundTowardPositive + RTP, + // roundTowardNegative + RTN, + // roundTowardZero + RTZ, +} + #[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)] pub enum UnaryOp { Not, @@ -43,6 +63,19 @@ pub enum UnaryOp { BitExtract(u32, u32), BitZeroExtend(u32), BitSignExtend(u32), + FloatNeg, + FloatRoundToInt(RoundingMode), + FloatIsNormal, + FloatIsSubnormal, + FloatIsZero, + FloatIsInfinite, + FloatIsNaN, + FloatIsNegative, + FloatIsPositive, + FloatFromIeeeBits { exp_bits: u32, sig_bits: u32 }, + FloatFrom { exp_bits: u32, sig_bits: u32, signed: bool, round: RoundingMode }, + FloatToBitVec { bits: u32, signed: bool, round: RoundingMode }, + FloatToReal, ToReal, RealToInt, } @@ -102,6 +135,15 @@ pub enum BinaryOp { LShr, Shl, BitConcat, + FloatAdd(RoundingMode), + FloatSub(RoundingMode), + FloatMul(RoundingMode), + FloatDiv(RoundingMode), + FloatEq, + FloatLt, + FloatGt, + FloatLe, + FloatGe, FieldUpdate(Ident), } @@ -114,6 +156,8 @@ pub enum MultiOp { Sub, Mul, Distinct, + // (fp sign exp sig) constructor, taking bit vectors as arguments and returning a Float + Float, } pub type Binder = Arc>; diff --git a/source/air/src/closure.rs b/source/air/src/closure.rs index 22f4692571..a3b6a3e8f6 100644 --- a/source/air/src/closure.rs +++ b/source/air/src/closure.rs @@ -551,6 +551,23 @@ fn simplify_expr(ctxt: &mut Context, state: &mut State, expr: &Expr) -> (Typ, Ex TypX::BitVec(n) => Arc::new(TypX::BitVec(n + w)), _ => panic!("internal error during processing bit extend"), }, + UnaryOp::FloatNeg => ts[0].0.clone(), + UnaryOp::FloatRoundToInt(_) => ts[0].0.clone(), + UnaryOp::FloatIsNormal => Arc::new(TypX::Bool), + UnaryOp::FloatIsSubnormal => Arc::new(TypX::Bool), + UnaryOp::FloatIsZero => Arc::new(TypX::Bool), + UnaryOp::FloatIsInfinite => Arc::new(TypX::Bool), + UnaryOp::FloatIsNaN => Arc::new(TypX::Bool), + UnaryOp::FloatIsNegative => Arc::new(TypX::Bool), + UnaryOp::FloatIsPositive => Arc::new(TypX::Bool), + UnaryOp::FloatFromIeeeBits { exp_bits, sig_bits } => { + Arc::new(TypX::Float { exp_bits: *exp_bits, sig_bits: *sig_bits }) + } + UnaryOp::FloatFrom { exp_bits, sig_bits, signed: _, round: _ } => { + Arc::new(TypX::Float { exp_bits: *exp_bits, sig_bits: *sig_bits }) + } + UnaryOp::FloatToBitVec { bits, .. } => Arc::new(TypX::BitVec(*bits)), + UnaryOp::FloatToReal => Arc::new(TypX::Real), UnaryOp::ToReal => Arc::new(TypX::Real), UnaryOp::RealToInt => Arc::new(TypX::Int), }; @@ -570,6 +587,11 @@ fn simplify_expr(ctxt: &mut Context, state: &mut State, expr: &Expr) -> (Typ, Ex BinaryOp::BitSGt | BinaryOp::BitSLt | BinaryOp::BitSGe | BinaryOp::BitSLe => { Arc::new(TypX::Bool) } + BinaryOp::FloatEq + | BinaryOp::FloatLt + | BinaryOp::FloatGt + | BinaryOp::FloatLe + | BinaryOp::FloatGe => Arc::new(TypX::Bool), BinaryOp::BitXor | BinaryOp::BitAnd | BinaryOp::BitOr @@ -582,7 +604,11 @@ fn simplify_expr(ctxt: &mut Context, state: &mut State, expr: &Expr) -> (Typ, Ex | BinaryOp::LShr | BinaryOp::AShr | BinaryOp::Shl - | BinaryOp::BitURem => { + | BinaryOp::BitURem + | BinaryOp::FloatAdd(_) + | BinaryOp::FloatSub(_) + | BinaryOp::FloatMul(_) + | BinaryOp::FloatDiv(_) => { assert!(typ_eq(&(ts[0].0), &(ts[1].0))); ts[0].0.clone() } @@ -607,6 +633,12 @@ fn simplify_expr(ctxt: &mut Context, state: &mut State, expr: &Expr) -> (Typ, Ex } } MultiOp::Distinct => Arc::new(TypX::Bool), + MultiOp::Float => match (&*ts[0].0, &*ts[1].0, &*ts[2].0) { + (TypX::BitVec(1), TypX::BitVec(exp_bits), TypX::BitVec(sig1_bits)) => { + Arc::new(TypX::Float { exp_bits: *exp_bits, sig_bits: *sig1_bits + 1 }) + } + _ => panic!("internal error during processing float"), + }, }; let (es, t) = enclose(state, App::Multi(*op), es, ts); (typ, Arc::new(ExprX::Multi(*op, Arc::new(es))), t) diff --git a/source/air/src/parser.rs b/source/air/src/parser.rs index 4d855056a2..671d52c91a 100644 --- a/source/air/src/parser.rs +++ b/source/air/src/parser.rs @@ -1,7 +1,7 @@ use crate::ast::{ Axiom, BinaryOp, BindX, Binder, BinderX, Binders, Command, CommandX, Commands, Constant, Decl, - DeclX, Decls, Expr, ExprX, Exprs, Ident, MultiOp, Qid, Quant, QueryX, Relation, Stmt, StmtX, - Stmts, Trigger, Triggers, Typ, TypX, UnaryOp, + DeclX, Decls, Expr, ExprX, Exprs, Ident, MultiOp, Qid, Quant, QueryX, Relation, RoundingMode, + Stmt, StmtX, Stmts, Trigger, Triggers, Typ, TypX, UnaryOp, }; use crate::def::mk_skolem_id; use crate::messages::ArcDynMessageLabel; @@ -35,6 +35,23 @@ fn is_bitvec(nodes: &Vec) -> Option { None } +fn is_float_type(nodes: &Vec) -> Option { + if nodes[0] == Node::Atom("_".to_string()) + && nodes[1] == Node::Atom("FloatingPoint".to_string()) + && nodes.len() == 4 + { + if let (Node::Atom(s2), Node::Atom(s3)) = (&nodes[2], &nodes[3]) { + match (s2.parse::(), s3.parse::()) { + (Ok(exp_bits), Ok(sig_bits)) => { + return Some(Arc::new(TypX::Float { exp_bits, sig_bits })); + } + _ => return None, + } + } + } + None +} + fn underscore_atom_atom_expr(s1: &str, s2: &str) -> Option { let value = s1.strip_prefix("bv")?; let width = s2.parse::().ok()?; @@ -116,10 +133,25 @@ impl Parser { Node::Atom(s) if s == "Int" => Ok(Arc::new(TypX::Int)), Node::Atom(s) if s == "Real" => Ok(Arc::new(TypX::Real)), Node::Atom(s) if s == "Fun" => Ok(Arc::new(TypX::Fun)), + Node::Atom(s) if s == "Float16" => { + Ok(Arc::new(TypX::Float { exp_bits: 5, sig_bits: 11 })) + } + Node::Atom(s) if s == "Float32" => { + Ok(Arc::new(TypX::Float { exp_bits: 8, sig_bits: 24 })) + } + Node::Atom(s) if s == "Float64" => { + Ok(Arc::new(TypX::Float { exp_bits: 11, sig_bits: 53 })) + } + Node::Atom(s) if s == "Float128" => { + Ok(Arc::new(TypX::Float { exp_bits: 15, sig_bits: 113 })) + } Node::Atom(s) if is_symbol(s) => Ok(Arc::new(TypX::Named(Arc::new(s.clone())))), Node::List(nodes) if is_bitvec(nodes).is_some() => { Ok(Arc::new(TypX::BitVec(is_bitvec(nodes).unwrap()))) } + Node::List(nodes) if is_float_type(nodes).is_some() => { + Ok(is_float_type(nodes).unwrap()) + } _ => Err(format!("expected type, found: {}", node_to_string(node))), } } @@ -234,10 +266,82 @@ impl Parser { } _ => {} } - let args = self.nodes_to_exprs(&nodes[1..])?; + let round = |args: &mut Exprs| { + Arc::make_mut(args).remove(0); + match nodes.get(1) { + Some(Node::Atom(s)) => match s.as_str() { + "RNE" | "roundNearestTiesToEven" => Ok(RoundingMode::RNE), + "RNA" | "roundNearestTiesToAway" => Ok(RoundingMode::RNA), + "RTP" | "roundTowardPositive" => Ok(RoundingMode::RTP), + "RTN" | "roundTowardNegative" => Ok(RoundingMode::RTN), + "RTZ" | "roundTowardZero" => Ok(RoundingMode::RTZ), + _ => Err("expected rounding mode in fp operation"), + }, + _ => Err("expected rounding mode in fp operation"), + } + }; + let mut args = self.nodes_to_exprs(&nodes[1..])?; let uop = match &nodes[0] { Node::Atom(s) if s == "not" => Some(UnaryOp::Not), Node::Atom(s) if s == "bvnot" => Some(UnaryOp::BitNot), + Node::Atom(s) if s == "bvneg" => Some(UnaryOp::BitNeg), + Node::Atom(s) if s == "fp.neg" => Some(UnaryOp::FloatNeg), + Node::Atom(s) if s == "fp.roundToIntegral" => { + Some(UnaryOp::FloatRoundToInt(round(&mut args)?)) + } + Node::Atom(s) if s == "fp.isNormal" => Some(UnaryOp::FloatIsNormal), + Node::Atom(s) if s == "fp.isSubnormal" => Some(UnaryOp::FloatIsSubnormal), + Node::Atom(s) if s == "fp.isZero" => Some(UnaryOp::FloatIsZero), + Node::Atom(s) if s == "fp.isInfinite" => Some(UnaryOp::FloatIsInfinite), + Node::Atom(s) if s == "fp.isNaN" => Some(UnaryOp::FloatIsNaN), + Node::Atom(s) if s == "fp.isNegative" => Some(UnaryOp::FloatIsNegative), + Node::Atom(s) if s == "fp.isPositive" => Some(UnaryOp::FloatIsPositive), + Node::List(nodes) + if nodes.len() == 4 + && nodes[0] == Node::Atom("_".to_string()) + && (nodes[1] == Node::Atom("to_fp".to_string()) + || nodes[1] == Node::Atom("to_fp_unsigned".to_string())) => + { + let signed = nodes[1] == Node::Atom("to_fp".to_string()); + let exp_sig_bits = match (&nodes[2], &nodes[3]) { + (Node::Atom(s2), Node::Atom(s3)) => { + match (s2.parse::(), s3.parse::()) { + (Ok(exp_bits), Ok(sig_bits)) => Some((exp_bits, sig_bits)), + _ => None, + } + } + _ => None, + }; + if let Some((exp_bits, sig_bits)) = exp_sig_bits { + if args.len() <= 1 && signed { + Some(UnaryOp::FloatFromIeeeBits { exp_bits, sig_bits }) + } else if args.len() > 1 { + let round = round(&mut args)?; + Some(UnaryOp::FloatFrom { exp_bits, sig_bits, signed, round }) + } else { + None + } + } else { + None + } + } + Node::List(nodes) + if nodes.len() == 3 + && nodes[0] == Node::Atom("_".to_string()) + && (nodes[1] == Node::Atom("fp.to_ubv".to_string()) + || nodes[1] == Node::Atom("fp.to_sbv".to_string())) => + { + let signed = nodes[1] == Node::Atom("fp.to_sbv".to_string()); + let round = round(&mut args)?; + match &nodes[2] { + Node::Atom(s2) => match s2.parse::() { + Ok(bits) => Some(UnaryOp::FloatToBitVec { bits, signed, round }), + _ => None, + }, + _ => None, + } + } + Node::Atom(s) if s == "fp.to_real" => Some(UnaryOp::FloatToReal), Node::Atom(s) if s == "to_real" => Some(UnaryOp::ToReal), Node::Atom(s) if s == "to_int" => Some(UnaryOp::RealToInt), Node::List(nodes) @@ -302,6 +406,15 @@ impl Parser { Node::Atom(s) if s == "bvlshr" => Some(BinaryOp::LShr), Node::Atom(s) if s == "bvshl" => Some(BinaryOp::Shl), Node::Atom(s) if s == "concat" => Some(BinaryOp::BitConcat), + Node::Atom(s) if s == "fp.add" => Some(BinaryOp::FloatAdd(round(&mut args)?)), + Node::Atom(s) if s == "fp.sub" => Some(BinaryOp::FloatSub(round(&mut args)?)), + Node::Atom(s) if s == "fp.mul" => Some(BinaryOp::FloatMul(round(&mut args)?)), + Node::Atom(s) if s == "fp.div" => Some(BinaryOp::FloatDiv(round(&mut args)?)), + Node::Atom(s) if s == "fp.eq" => Some(BinaryOp::FloatEq), + Node::Atom(s) if s == "fp.lt" => Some(BinaryOp::FloatLt), + Node::Atom(s) if s == "fp.gt" => Some(BinaryOp::FloatGt), + Node::Atom(s) if s == "fp.leq" => Some(BinaryOp::FloatLe), + Node::Atom(s) if s == "fp.geq" => Some(BinaryOp::FloatGe), Node::List(nodes) if nodes.len() == 3 && nodes[0] == Node::Atom("_".to_string()) @@ -326,6 +439,7 @@ impl Parser { Node::Atom(s) if s == "-" => Some(MultiOp::Sub), Node::Atom(s) if s == "*" => Some(MultiOp::Mul), Node::Atom(s) if s == "distinct" => Some(MultiOp::Distinct), + Node::Atom(s) if s == "fp" => Some(MultiOp::Float), _ => None, }; let ite = match &nodes[0] { diff --git a/source/air/src/printer.rs b/source/air/src/printer.rs index f41cbb81a3..cc88fc06ca 100644 --- a/source/air/src/printer.rs +++ b/source/air/src/printer.rs @@ -1,6 +1,7 @@ use crate::ast::{ Axiom, BinaryOp, BindX, Binder, Binders, Constant, Datatypes, Decl, DeclX, Expr, ExprX, Exprs, - Ident, MultiOp, Qid, Quant, Query, QueryX, Stmt, StmtX, Triggers, Typ, TypX, Typs, UnaryOp, + Ident, MultiOp, Qid, Quant, Query, QueryX, RoundingMode, Stmt, StmtX, Triggers, Typ, TypX, + Typs, UnaryOp, }; use crate::context::SmtSolver; use crate::def::mk_skolem_id; @@ -103,6 +104,16 @@ impl Printer { str_to_node("BitVec"), str_to_node(&size.to_string()), ]), + TypX::Float { exp_bits: 5, sig_bits: 11 } => str_to_node("Float16"), + TypX::Float { exp_bits: 8, sig_bits: 24 } => str_to_node("Float32"), + TypX::Float { exp_bits: 11, sig_bits: 53 } => str_to_node("Float64"), + TypX::Float { exp_bits: 15, sig_bits: 113 } => str_to_node("Float128"), + TypX::Float { exp_bits, sig_bits } => Node::List(vec![ + str_to_node("_"), + str_to_node("FloatingPoint"), + str_to_node(&exp_bits.to_string()), + str_to_node(&sig_bits.to_string()), + ]), } } @@ -120,6 +131,16 @@ impl Printer { if let Some(filter) = filter { nodes!({ str_to_node(filter) }) } else { Node::List(vec![]) } } + fn rounding_mode_to_node(&self, r: &RoundingMode) -> Node { + match r { + RoundingMode::RNE => str_to_node("RNE"), + RoundingMode::RNA => str_to_node("RNA"), + RoundingMode::RTP => str_to_node("RTP"), + RoundingMode::RTN => str_to_node("RTN"), + RoundingMode::RTZ => str_to_node("RTZ"), + } + } + pub fn expr_to_node(&self, expr: &Expr) -> Node { match &**expr { ExprX::Const(Constant::Bool(b)) => Node::Atom(b.to_string()), @@ -148,6 +169,10 @@ impl Printer { } Node::List(nodes) } + ExprX::Unary(UnaryOp::FloatRoundToInt(r), expr) => { + let r = self.rounding_mode_to_node(r); + Node::List(vec![str_to_node("fp.roundToIntegral"), r, self.expr_to_node(expr)]) + } ExprX::Unary(op, expr) => { let sop = match op { UnaryOp::Not => "not", @@ -156,6 +181,21 @@ impl Printer { UnaryOp::BitExtract(_, _) => "extract", UnaryOp::BitZeroExtend(_) => "zero_extend", UnaryOp::BitSignExtend(_) => "sign_extend", + UnaryOp::FloatNeg => "fp.neg", + UnaryOp::FloatRoundToInt(_) => unreachable!(), + UnaryOp::FloatIsNormal => "fp.isNormal", + UnaryOp::FloatIsSubnormal => "fp.isSubnormal", + UnaryOp::FloatIsZero => "fp.isZero", + UnaryOp::FloatIsInfinite => "fp.isInfinite", + UnaryOp::FloatIsNaN => "fp.isNaN", + UnaryOp::FloatIsNegative => "fp.isNegative", + UnaryOp::FloatIsPositive => "fp.isPositive", + UnaryOp::FloatFromIeeeBits { .. } => "to_fp", + UnaryOp::FloatFrom { signed: false, .. } => "to_fp_unsigned", + UnaryOp::FloatFrom { signed: true, .. } => "to_fp", + UnaryOp::FloatToBitVec { signed: false, .. } => "fp.to_ubv", + UnaryOp::FloatToBitVec { signed: true, .. } => "fp.to_sbv", + UnaryOp::FloatToReal => "fp.to_real", UnaryOp::ToReal => "to_real", UnaryOp::RealToInt => "to_int", }; @@ -178,6 +218,37 @@ impl Printer { let nodes = vec![Node::List(nodes_in), self.expr_to_node(expr)]; Node::List(nodes) } + UnaryOp::FloatFromIeeeBits { exp_bits, sig_bits } => { + let nodes_in = vec![ + str_to_node("_"), + str_to_node(sop), + str_to_node(&exp_bits.to_string()), + str_to_node(&sig_bits.to_string()), + ]; + let nodes = vec![Node::List(nodes_in), self.expr_to_node(expr)]; + Node::List(nodes) + } + UnaryOp::FloatFrom { exp_bits, sig_bits, signed: _, round } => { + let nodes_in = vec![ + str_to_node("_"), + str_to_node(sop), + str_to_node(&exp_bits.to_string()), + str_to_node(&sig_bits.to_string()), + ]; + let r = self.rounding_mode_to_node(round); + let nodes = vec![Node::List(nodes_in), r, self.expr_to_node(expr)]; + Node::List(nodes) + } + UnaryOp::FloatToBitVec { bits, signed: _, round } => { + let nodes_in = vec![ + str_to_node("_"), + str_to_node(sop), + str_to_node(&bits.to_string()), + ]; + let r = self.rounding_mode_to_node(round); + let nodes = vec![Node::List(nodes_in), r, self.expr_to_node(expr)]; + Node::List(nodes) + } _ => Node::List(vec![str_to_node(sop), self.expr_to_node(expr)]), } } @@ -227,13 +298,34 @@ impl Printer { BinaryOp::AShr => str_to_node("bvashr"), BinaryOp::Shl => str_to_node("bvshl"), BinaryOp::BitConcat => str_to_node("concat"), + BinaryOp::FloatAdd(_) => str_to_node("fp.add"), + BinaryOp::FloatSub(_) => str_to_node("fp.sub"), + BinaryOp::FloatMul(_) => str_to_node("fp.mul"), + BinaryOp::FloatDiv(_) => str_to_node("fp.div"), + BinaryOp::FloatEq => str_to_node("fp.eq"), + BinaryOp::FloatLt => str_to_node("fp.lt"), + BinaryOp::FloatGt => str_to_node("fp.gt"), + BinaryOp::FloatLe => str_to_node("fp.leq"), + BinaryOp::FloatGe => str_to_node("fp.geq"), BinaryOp::FieldUpdate(field_ident) => Node::List(vec![ str_to_node("_"), str_to_node("update-field"), str_to_node(&**field_ident), ]), }; - Node::List(vec![sop, self.expr_to_node(lhs), self.expr_to_node(rhs)]) + let round = match op { + BinaryOp::FloatAdd(r) + | BinaryOp::FloatSub(r) + | BinaryOp::FloatMul(r) + | BinaryOp::FloatDiv(r) => Some(self.rounding_mode_to_node(r)), + _ => None, + }; + match round { + None => Node::List(vec![sop, self.expr_to_node(lhs), self.expr_to_node(rhs)]), + Some(r) => { + Node::List(vec![sop, r, self.expr_to_node(lhs), self.expr_to_node(rhs)]) + } + } } ExprX::Multi(op, exprs) => { let sop = match op { @@ -244,6 +336,7 @@ impl Printer { MultiOp::Sub => "-", MultiOp::Mul => "*", MultiOp::Distinct => "distinct", + MultiOp::Float => "fp", }; let mut nodes: Vec = Vec::new(); nodes.push(str_to_node(sop)); diff --git a/source/air/src/tests.rs b/source/air/src/tests.rs index aa4913ee71..b94cfacaff 100644 --- a/source/air/src/tests.rs +++ b/source/air/src/tests.rs @@ -4,7 +4,7 @@ use crate::messages::Reporter; #[allow(unused_imports)] use crate::parser::Parser; #[allow(unused_imports)] -use crate::printer::macro_push_node; +use crate::printer::{macro_push_node, str_to_node}; #[allow(unused_imports)] use sise::Node; @@ -186,6 +186,32 @@ fn no_int_axiom() { ); } +#[test] +fn yes_float() { + yes!( + (check-valid + (declare-const x (_ FloatingPoint 2 3)) + (declare-const y (_ FloatingPoint 2 3)) + (assert + (= ({str_to_node("fp.add")} RNE x y) ({str_to_node("fp.add")} RNE y x)) + ) + ) + ); +} + +#[test] +fn no_float() { + no!( + (check-valid + (declare-const x (_ FloatingPoint 2 3)) + (declare-const y (_ FloatingPoint 2 3)) + (assert + (= ({str_to_node("fp.add")} RNE x y) (fp (_ bv0 1) (_ bv2 2) (_ bv2 2))) + ) + ) + ); +} + #[test] fn yes_test_block() { yes!( diff --git a/source/air/src/typecheck.rs b/source/air/src/typecheck.rs index c0a106aca3..f2779c31d8 100644 --- a/source/air/src/typecheck.rs +++ b/source/air/src/typecheck.rs @@ -64,6 +64,7 @@ fn typ_name(typ: &Typ) -> String { TypX::Fun => "Fun".to_string(), TypX::Named(x) => x.to_string(), TypX::BitVec(n) => format!("BitVec{}", n), + TypX::Float { exp_bits, sig_bits } => format!("Float{exp_bits}_{sig_bits}"), } } @@ -86,6 +87,15 @@ fn check_typ(typing: &Typing, typ: &Typ) -> Result<(), TypeError> { _ => Err(format!("use of undeclared type {}", x)), }, TypX::BitVec(_) => Ok(()), + TypX::Float { exp_bits, sig_bits } => { + if *exp_bits <= 1 || *sig_bits <= 1 { + Err(format!( + "unsupported floating point type (_ FloatingPoint {exp_bits} {sig_bits})" + )) + } else { + Ok(()) + } + } } } @@ -235,6 +245,69 @@ fn check_bv_exprs( } } +fn check_float_unary_exprs( + typing: &mut Typing, + op: UnaryOp, + f_name: &str, + expr: &Expr, +) -> Result { + let t0 = check_expr(typing, expr)?; + match &*t0 { + TypX::Float { .. } => match op { + UnaryOp::FloatNeg => Ok(t0.clone()), + UnaryOp::FloatRoundToInt(_) => Ok(t0.clone()), + UnaryOp::FloatIsNormal + | UnaryOp::FloatIsSubnormal + | UnaryOp::FloatIsZero + | UnaryOp::FloatIsInfinite + | UnaryOp::FloatIsNaN + | UnaryOp::FloatIsNegative + | UnaryOp::FloatIsPositive => Ok(bt()), + UnaryOp::FloatToBitVec { bits, .. } => Ok(Arc::new(TypX::BitVec(bits))), + UnaryOp::FloatToReal => Ok(rt()), + _ => unreachable!(), + }, + _ => Err(format!( + "in call to {}, expected a floating point argument, but got {}", + f_name, + typ_name(&t0), + )), + } +} + +fn check_float_exprs( + typing: &mut Typing, + bop: BinaryOp, + f_name: &str, + exprs: &[Expr], +) -> Result { + let t0 = check_expr(typing, &exprs[0])?; + let t1 = check_expr(typing, &exprs[1])?; + match (&*t0, &*t1) { + ( + TypX::Float { exp_bits: exp_bits0, sig_bits: sig_bits0 }, + TypX::Float { exp_bits: exp_bits1, sig_bits: sig_bits1 }, + ) if exp_bits0 == exp_bits1 && sig_bits0 == sig_bits1 => match bop { + BinaryOp::FloatEq + | BinaryOp::FloatLt + | BinaryOp::FloatGt + | BinaryOp::FloatLe + | BinaryOp::FloatGe => Ok(bt()), + BinaryOp::FloatAdd(_) + | BinaryOp::FloatSub(_) + | BinaryOp::FloatMul(_) + | BinaryOp::FloatDiv(_) => Ok(t0.clone()), + _ => unreachable!(), + }, + _ => Err(format!( + "in call to {}, expected both arguments to have the same floating point type, but got {} and {}", + f_name, + typ_name(&t0), + typ_name(&t1) + )), + } +} + fn check_expr(typing: &mut Typing, expr: &Expr) -> Result { let result = match &**expr { ExprX::Const(Constant::Bool(_)) => Ok(Arc::new(TypX::Bool)), @@ -286,6 +359,65 @@ fn check_expr(typing: &mut Typing, expr: &Expr) -> Result { ExprX::Unary(UnaryOp::BitSignExtend(n), e1) => { check_bv_unary_exprs(typing, UnaryOp::BitSignExtend(*n), "sign_extend", &e1.clone()) } + ExprX::Unary(op @ UnaryOp::FloatNeg, e1) => { + check_float_unary_exprs(typing, op.clone(), "float_neg", &e1.clone()) + } + ExprX::Unary(op @ UnaryOp::FloatRoundToInt(_), e1) => { + check_float_unary_exprs(typing, op.clone(), "float_round_to_int", &e1.clone()) + } + ExprX::Unary(op @ UnaryOp::FloatIsNormal, e1) => { + check_float_unary_exprs(typing, op.clone(), "float_is_normal", &e1.clone()) + } + ExprX::Unary(op @ UnaryOp::FloatIsSubnormal, e1) => { + check_float_unary_exprs(typing, op.clone(), "float_is_subnormal", &e1.clone()) + } + ExprX::Unary(op @ UnaryOp::FloatIsZero, e1) => { + check_float_unary_exprs(typing, op.clone(), "float_is_zero", &e1.clone()) + } + ExprX::Unary(op @ UnaryOp::FloatIsInfinite, e1) => { + check_float_unary_exprs(typing, op.clone(), "float_is_infinite", &e1.clone()) + } + ExprX::Unary(op @ UnaryOp::FloatIsNaN, e1) => { + check_float_unary_exprs(typing, op.clone(), "float_is_nan", &e1.clone()) + } + ExprX::Unary(op @ UnaryOp::FloatIsNegative, e1) => { + check_float_unary_exprs(typing, op.clone(), "float_is_negative", &e1.clone()) + } + ExprX::Unary(op @ UnaryOp::FloatIsPositive, e1) => { + check_float_unary_exprs(typing, op.clone(), "float_is_positive", &e1.clone()) + } + ExprX::Unary(UnaryOp::FloatFromIeeeBits { exp_bits, sig_bits }, e1) => { + let t1 = check_expr(typing, e1)?; + match &*t1 { + TypX::BitVec(n) if *n == exp_bits + sig_bits => { + Ok(Arc::new(TypX::Float { exp_bits: *exp_bits, sig_bits: *sig_bits })) + } + _ => Err(format!( + "in float_from_ieee_bits, expected argument of type (_ BitVec {}) but found {}", + exp_bits + sig_bits, + typ_name(&t1) + )), + } + } + ExprX::Unary(UnaryOp::FloatFrom { exp_bits, sig_bits, signed, round: _ }, e1) => { + let t1 = check_expr(typing, e1)?; + let tf = Arc::new(TypX::Float { exp_bits: *exp_bits, sig_bits: *sig_bits }); + match (&*t1, signed) { + (TypX::Real, true) => Ok(tf), + (TypX::Float { .. }, true) => Ok(tf), + (TypX::BitVec(_), _) => Ok(tf), + _ => Err(format!( + "in float_from, expected argument of type Real or BitVec but found {}", + typ_name(&t1) + )), + } + } + ExprX::Unary(op @ UnaryOp::FloatToBitVec { .. }, e1) => { + check_float_unary_exprs(typing, op.clone(), "float_to_bitvec", &e1.clone()) + } + ExprX::Unary(UnaryOp::FloatToReal, e1) => { + check_float_unary_exprs(typing, UnaryOp::FloatToReal, "float_to_real", &e1.clone()) + } ExprX::Unary(UnaryOp::ToReal, e1) => { check_exprs(typing, "to_real", &[it()], &rt(), std::slice::from_ref(e1)) } @@ -435,7 +567,58 @@ fn check_expr(typing: &mut Typing, expr: &Expr) -> Result { ExprX::Binary(BinaryOp::BitConcat, e1, e2) => { check_bv_exprs(typing, BinaryOp::BitConcat, "concat", &[e1.clone(), e2.clone()]) } - + ExprX::Binary(op @ BinaryOp::FloatAdd(_), e1, e2) => { + check_float_exprs(typing, op.clone(), "float_add", &[e1.clone(), e2.clone()]) + } + ExprX::Binary(op @ BinaryOp::FloatSub(_), e1, e2) => { + check_float_exprs(typing, op.clone(), "float_sub", &[e1.clone(), e2.clone()]) + } + ExprX::Binary(op @ BinaryOp::FloatMul(_), e1, e2) => { + check_float_exprs(typing, op.clone(), "float_mul", &[e1.clone(), e2.clone()]) + } + ExprX::Binary(op @ BinaryOp::FloatDiv(_), e1, e2) => { + check_float_exprs(typing, op.clone(), "float_div", &[e1.clone(), e2.clone()]) + } + ExprX::Binary(BinaryOp::FloatEq, e1, e2) => { + check_float_exprs(typing, BinaryOp::FloatEq, "float_eq", &[e1.clone(), e2.clone()]) + } + ExprX::Binary(BinaryOp::FloatLt, e1, e2) => { + check_float_exprs(typing, BinaryOp::FloatLt, "float_lt", &[e1.clone(), e2.clone()]) + } + ExprX::Binary(BinaryOp::FloatLe, e1, e2) => { + check_float_exprs(typing, BinaryOp::FloatLe, "float_le", &[e1.clone(), e2.clone()]) + } + ExprX::Binary(BinaryOp::FloatGt, e1, e2) => { + check_float_exprs(typing, BinaryOp::FloatGt, "float_gt", &[e1.clone(), e2.clone()]) + } + ExprX::Binary(BinaryOp::FloatGe, e1, e2) => { + check_float_exprs(typing, BinaryOp::FloatGe, "float_ge", &[e1.clone(), e2.clone()]) + } + ExprX::Multi(MultiOp::Float, exprs) => { + if exprs.len() != 3 { + Err(format!( + "floating point constructor expects 3 arguments, found {}", + exprs.len(), + )) + } else { + let sign = check_expr(typing, &exprs[0])?; + let exp = check_expr(typing, &exprs[1])?; + let sig = check_expr(typing, &exprs[2])?; + match (&*sign, &*exp, &*sig) { + (TypX::BitVec(1), TypX::BitVec(exp_bits), TypX::BitVec(sig1_bits)) + if *exp_bits > 1 && *sig1_bits > 0 => + { + Ok(Arc::new(TypX::Float { exp_bits: *exp_bits, sig_bits: *sig1_bits + 1 })) + } + _ => Err(format!( + "in floating point constructor, expected arguments of type (BitVec 1), (BitVec exp_bits), (BitVec sig1_bits) with exp_bits > 1 and sig1_bits > 0, but found {}, {}, {}", + typ_name(&sign), + typ_name(&exp), + typ_name(&sig) + )), + } + } + } ExprX::Multi(op, exprs) => { let (x, t) = match op { MultiOp::And => ("and", bt()), @@ -445,6 +628,7 @@ fn check_expr(typing: &mut Typing, expr: &Expr) -> Result { MultiOp::Sub => ("-", it()), MultiOp::Mul => ("*", it()), MultiOp::Distinct => ("distinct", it()), + MultiOp::Float => unreachable!(), }; match op { MultiOp::Distinct => { diff --git a/source/builtin/src/lib.rs b/source/builtin/src/lib.rs index 9d977f09fa..810a69adf9 100644 --- a/source/builtin/src/lib.rs +++ b/source/builtin/src/lib.rs @@ -1012,6 +1012,8 @@ unsafe impl Decimal for f64 { pub unsafe trait Chainable: Copy {} unsafe impl Chainable for T {} unsafe impl Chainable for real {} +unsafe impl Chainable for f32 {} +unsafe impl Chainable for f64 {} // spec literals of the form "33", which could have any Integer type #[cfg(verus_keep_ghost)] @@ -1414,6 +1416,8 @@ impl_ord!([ ]); impl_ord_self_rhs!([real]); +impl_ord_self_rhs!([f32]); +impl_ord_self_rhs!([f64]); impl_unary_op!(SpecNeg, spec_neg, int, [ int nat @@ -1422,6 +1426,8 @@ impl_unary_op!(SpecNeg, spec_neg, int, [ ]); impl_unary_op!(SpecNeg, spec_neg, real, [real]); +impl_unary_op!(SpecNeg, spec_neg, f32, [f32]); +impl_unary_op!(SpecNeg, spec_neg, f64, [f64]); impl_binary_op!(SpecAdd, spec_add, int, [ int @@ -1477,6 +1483,16 @@ impl_binary_op_rhs!(SpecSub, spec_sub, Self, Self, [real]); impl_binary_op_rhs!(SpecMul, spec_mul, Self, Self, [real]); impl_binary_op_rhs!(SpecEuclideanOrRealDiv, spec_euclidean_or_real_div, Self, Self, [real]); +impl_binary_op_rhs!(SpecAdd, spec_add, Self, Self, [f32]); +impl_binary_op_rhs!(SpecSub, spec_sub, Self, Self, [f32]); +impl_binary_op_rhs!(SpecMul, spec_mul, Self, Self, [f32]); +impl_binary_op_rhs!(SpecEuclideanOrRealDiv, spec_euclidean_or_real_div, Self, Self, [f32]); + +impl_binary_op_rhs!(SpecAdd, spec_add, Self, Self, [f64]); +impl_binary_op_rhs!(SpecSub, spec_sub, Self, Self, [f64]); +impl_binary_op_rhs!(SpecMul, spec_mul, Self, Self, [f64]); +impl_binary_op_rhs!(SpecEuclideanOrRealDiv, spec_euclidean_or_real_div, Self, Self, [f64]); + impl_binary_op_rhs!(SpecBitAnd, spec_bitand, Self, Self, [ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 @@ -1503,6 +1519,314 @@ impl_binary_op!(SpecShr, spec_shr, Self, [ isize i8 i16 i32 i64 i128 ]); +// +// IEEE floats ( https://smt-lib.org/theories-FloatingPoint.shtml ) +// Note that for float types, spec-level +, -, *, /, <=, >=, <, > are synonyms for ieee_add, etc. +// + +// rounding modes: RNE unless otherwise specified +#[cfg_attr(verus_keep_ghost, verifier::sealed)] +pub trait IeeeFloat { + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_add"] + #[verifier::spec] + fn ieee_add(self, rhs: Self) -> Self; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_sub"] + #[verifier::spec] + fn ieee_sub(self, rhs: Self) -> Self; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_mul"] + #[verifier::spec] + fn ieee_mul(self, rhs: Self) -> Self; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_div"] + #[verifier::spec] + fn ieee_div(self, rhs: Self) -> Self; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_eq"] + #[verifier::spec] + fn ieee_eq(self, rhs: Self) -> bool; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_le"] + #[verifier::spec] + fn ieee_le(self, rhs: Self) -> bool; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_ge"] + #[verifier::spec] + fn ieee_ge(self, rhs: Self) -> bool; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_lt"] + #[verifier::spec] + fn ieee_lt(self, rhs: Self) -> bool; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_gt"] + #[verifier::spec] + fn ieee_gt(self, rhs: Self) -> bool; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_neg"] + #[verifier::spec] + fn ieee_neg(self) -> Self; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_floor"] + #[verifier::spec] + fn ieee_floor(self) -> Self; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_ceil"] + #[verifier::spec] + fn ieee_ceil(self) -> Self; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_round"] + #[verifier::spec] + fn ieee_round(self) -> Self; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_round_ties_even"] + #[verifier::spec] + fn ieee_round_ties_even(self) -> Self; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_trunc"] + #[verifier::spec] + fn ieee_trunc(self) -> Self; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_is_normal"] + #[verifier::spec] + fn ieee_is_normal(self) -> bool; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_is_subnormal"] + #[verifier::spec] + fn ieee_is_subnormal(self) -> bool; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_is_zero"] + #[verifier::spec] + fn ieee_is_zero(self) -> bool; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_is_infinite"] + #[verifier::spec] + fn ieee_is_infinite(self) -> bool; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_is_nan"] + #[verifier::spec] + fn ieee_is_nan(self) -> bool; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_is_negative"] + #[verifier::spec] + fn ieee_is_negative(self) -> bool; + + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloat::ieee_is_positive"] + #[verifier::spec] + fn ieee_is_positive(self) -> bool; +} + +#[cfg_attr(verus_keep_ghost, verifier::sealed)] +pub trait IeeeFloatCast { + // rounding modes: + // - to integer: RTZ + // - to float: RNE + // - to real: no rounding + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::IeeeFloatCast::ieee_cast"] + #[verifier::spec] + fn ieee_cast(self) -> To; +} + +macro_rules! impl_ieee_float { + ([$($t:ty)*]) => { + $( + impl IeeeFloat for $t { + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_add(self, _rhs : Self) -> Self { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_sub(self, _rhs : Self) -> Self { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_mul(self, _rhs : Self) -> Self { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_div(self, _rhs : Self) -> Self { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_eq(self, _rhs : Self) -> bool { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_le(self, _rhs : Self) -> bool { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_ge(self, _rhs : Self) -> bool { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_lt(self, _rhs : Self) -> bool { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_gt(self, _rhs : Self) -> bool { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_neg(self) -> Self { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_floor(self) -> Self { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_ceil(self) -> Self { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_round(self) -> Self { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_round_ties_even(self) -> Self { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_trunc(self) -> Self { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_is_normal(self) -> bool { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_is_subnormal(self) -> bool { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_is_zero(self) -> bool { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_is_infinite(self) -> bool { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_is_nan(self) -> bool { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_is_negative(self) -> bool { + unimplemented!() + } + + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_is_positive(self) -> bool { + unimplemented!() + } + } + )* + } +} + +macro_rules! impl_ieee_float_cast { + ($from:ty, [$($to:ty)*]) => { + $( + impl IeeeFloatCast<$to> for $from { + #[cfg(verus_keep_ghost)] + #[verifier::spec] + fn ieee_cast(self) -> $to { + unimplemented!() + } + } + )* + } +} + +impl_ieee_float!([f32 f64]); +impl_ieee_float_cast!(f32, [real f64]); +impl_ieee_float_cast!(f64, [real f32]); +impl_ieee_float_cast!(real, [f32 f64]); +impl_ieee_float_cast!(u8, [f32 f64]); +impl_ieee_float_cast!(u16, [f32 f64]); +impl_ieee_float_cast!(u32, [f32 f64]); +impl_ieee_float_cast!(u64, [f32 f64]); +impl_ieee_float_cast!(u128, [f32 f64]); +impl_ieee_float_cast!(i8, [f32 f64]); +impl_ieee_float_cast!(i16, [f32 f64]); +impl_ieee_float_cast!(i32, [f32 f64]); +impl_ieee_float_cast!(i64, [f32 f64]); +impl_ieee_float_cast!(i128, [f32 f64]); +impl_ieee_float_cast!(f32, [u8 u16 u32 u64 u128]); +impl_ieee_float_cast!(f32, [i8 i16 i32 i64 i128]); +impl_ieee_float_cast!(f64, [u8 u16 u32 u64 u128]); +impl_ieee_float_cast!(f64, [i8 i16 i32 i64 i128]); + +// +// +// + #[cfg(verus_keep_ghost)] #[verifier::spec] #[rustc_diagnostic_item = "verus::verus_builtin::f32_to_bits"] diff --git a/source/builtin_macros/src/syntax_trait.rs b/source/builtin_macros/src/syntax_trait.rs index 2828834122..25d11b4973 100644 --- a/source/builtin_macros/src/syntax_trait.rs +++ b/source/builtin_macros/src/syntax_trait.rs @@ -179,7 +179,9 @@ fn expand_extension_trait<'tcx>( let blanket_bound: TypeParamBound = { tr.supertraits.iter().find(|tpb| is_sizedness_bound(tpb)).cloned().unwrap_or_else(|| { let span = tr.generics.span(); - parse_quote_spanned!(span => core::marker::MetaSized) + // eventually TODO? MetaSized currently breaks stable rust when compiling to executable code + // parse_quote_spanned!(span => core::marker::MetaSized) + parse_quote_spanned!(span => ?Sized) }) }; blanket_impl.generics.params.push(parse_quote_spanned!(span => #self_x: #t + #blanket_bound)); diff --git a/source/rust_verify/src/fn_call_to_vir.rs b/source/rust_verify/src/fn_call_to_vir.rs index d1950f587b..28c21c5254 100644 --- a/source/rust_verify/src/fn_call_to_vir.rs +++ b/source/rust_verify/src/fn_call_to_vir.rs @@ -1496,8 +1496,11 @@ fn verus_item_to_vir<'tcx, 'a>( varg, )) } + TypX::Float(_) => { + mk_expr(ExprX::Unary(UnaryOp::IeeeFloat(vir::ast::IeeeFloatUnaryOp::Neg), varg)) + } _ => { - return err_span(expr.span, "spec_neg expected int or real type"); + return err_span(expr.span, "spec_neg expected int or real or float type"); } } } @@ -1508,9 +1511,12 @@ fn verus_item_to_vir<'tcx, 'a>( ChainedItem::Value => { unsupported_err_unless!(args_len == 1, expr.span, "spec_chained_value", &args); unsupported_err_unless!( - matches!(*undecorate_typ(&vir_args[0].typ), TypX::Int(_) | TypX::Real), + matches!( + *undecorate_typ(&vir_args[0].typ), + TypX::Int(_) | TypX::Real | TypX::Float(_), + ), expr.span, - "chained inequalities require integer or real types", + "chained inequalities require integer or real or float types", &args ); let exprx = ExprX::Multi( @@ -1536,9 +1542,12 @@ fn verus_item_to_vir<'tcx, 'a>( &args ); unsupported_err_unless!( - matches!(*undecorate_typ(&vir_args[1].typ), TypX::Int(_) | TypX::Real), + matches!( + *undecorate_typ(&vir_args[1].typ), + TypX::Int(_) | TypX::Real | TypX::Float(_), + ), expr.span, - "chained inequalities require integer or real types", + "chained inequalities require integer or real or float types", &args ); if let ExprX::Multi(MultiOp::Chained(_), es) = &vir_args[0].x { @@ -1548,12 +1557,13 @@ fn verus_item_to_vir<'tcx, 'a>( let types_match = match (&*first_typ, &*new_typ) { (TypX::Int(_), TypX::Int(_)) => true, (TypX::Real, TypX::Real) => true, + (TypX::Float(f1), TypX::Float(f2)) => f1 == f2, _ => false, }; unsupported_err_unless!( types_match, expr.span, - "chained inequalities require all elements to have the same type (all integers or all reals)" + "chained inequalities require all elements to have the same type (all integers or all reals or all floats)" ); } } @@ -1806,15 +1816,74 @@ fn verus_item_to_vir<'tcx, 'a>( let vop = BinaryOp::Implies; mk_expr(ExprX::Binary(vop, lhs, rhs)) } + VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(fop)) => { + use crate::verus_items::IeeeFloatUnaryItem; + use vir::ast::IeeeFloatUnaryOp; + record_spec_fn(bctx, expr); + let varg = mk_one_vir_arg(bctx, expr.span, &args)?; + let vop = match fop { + IeeeFloatUnaryItem::Cast => UnaryOp::IeeeFloat(IeeeFloatUnaryOp::Cast), + IeeeFloatUnaryItem::Neg => UnaryOp::IeeeFloat(IeeeFloatUnaryOp::Neg), + IeeeFloatUnaryItem::Floor => UnaryOp::IeeeFloat(IeeeFloatUnaryOp::Floor), + IeeeFloatUnaryItem::Ceil => UnaryOp::IeeeFloat(IeeeFloatUnaryOp::Ceil), + IeeeFloatUnaryItem::Round => UnaryOp::IeeeFloat(IeeeFloatUnaryOp::Round), + IeeeFloatUnaryItem::RoundTiesEven => { + UnaryOp::IeeeFloat(IeeeFloatUnaryOp::RoundTiesEven) + } + IeeeFloatUnaryItem::Trunc => UnaryOp::IeeeFloat(IeeeFloatUnaryOp::Trunc), + IeeeFloatUnaryItem::IsNormal => UnaryOp::IeeeFloat(IeeeFloatUnaryOp::IsNormal), + IeeeFloatUnaryItem::IsSubnormal => { + UnaryOp::IeeeFloat(IeeeFloatUnaryOp::IsSubnormal) + } + IeeeFloatUnaryItem::IsZero => UnaryOp::IeeeFloat(IeeeFloatUnaryOp::IsZero), + IeeeFloatUnaryItem::IsInfinite => UnaryOp::IeeeFloat(IeeeFloatUnaryOp::IsInfinite), + IeeeFloatUnaryItem::IsNaN => UnaryOp::IeeeFloat(IeeeFloatUnaryOp::IsNaN), + IeeeFloatUnaryItem::IsNegative => UnaryOp::IeeeFloat(IeeeFloatUnaryOp::IsNegative), + IeeeFloatUnaryItem::IsPositive => UnaryOp::IeeeFloat(IeeeFloatUnaryOp::IsPositive), + }; + mk_expr(ExprX::Unary(vop, varg)) + } + VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(fop)) => { + use crate::verus_items::IeeeFloatBinaryItem; + use vir::ast::IeeeFloatBinaryOp; + record_spec_fn(bctx, expr); + let (lhs, rhs) = mk_two_vir_args(bctx, expr.span, &args)?; + let vop = match fop { + IeeeFloatBinaryItem::Add => BinaryOp::IeeeFloat(IeeeFloatBinaryOp::Add), + IeeeFloatBinaryItem::Sub => BinaryOp::IeeeFloat(IeeeFloatBinaryOp::Sub), + IeeeFloatBinaryItem::Mul => BinaryOp::IeeeFloat(IeeeFloatBinaryOp::Mul), + IeeeFloatBinaryItem::Div => BinaryOp::IeeeFloat(IeeeFloatBinaryOp::Div), + IeeeFloatBinaryItem::Eq => BinaryOp::IeeeFloat(IeeeFloatBinaryOp::Eq), + IeeeFloatBinaryItem::Le => { + BinaryOp::IeeeFloat(IeeeFloatBinaryOp::InEq(InequalityOp::Le)) + } + IeeeFloatBinaryItem::Ge => { + BinaryOp::IeeeFloat(IeeeFloatBinaryOp::InEq(InequalityOp::Ge)) + } + IeeeFloatBinaryItem::Lt => { + BinaryOp::IeeeFloat(IeeeFloatBinaryOp::InEq(InequalityOp::Lt)) + } + IeeeFloatBinaryItem::Gt => { + BinaryOp::IeeeFloat(IeeeFloatBinaryOp::InEq(InequalityOp::Gt)) + } + }; + mk_expr(ExprX::Binary(vop, lhs, rhs)) + } VerusItem::BinaryOp( BinaryOpItem::Arith(_) | BinaryOpItem::SpecArith(_) | BinaryOpItem::SpecBitwise(_) | BinaryOpItem::SpecOrd(_), ) => { + use crate::rust_to_vir_base::is_float_arith; + record_spec_fn(bctx, expr); - if !is_smt_arith(bctx, args[0].span, args[1].span, &args[0].hir_id, &args[1].hir_id)? { + let is_smt = + is_smt_arith(bctx, args[0].span, args[1].span, &args[0].hir_id, &args[1].hir_id)?; + let is_float = + is_float_arith(bctx, args[0].span, args[1].span, &args[0].hir_id, &args[1].hir_id)?; + if !is_smt && !is_float { let t1 = bctx.types.expr_ty_adjusted(&args[0]); let t2 = bctx.types.expr_ty_adjusted(&args[1]); return err_span( @@ -1829,6 +1898,25 @@ fn verus_item_to_vir<'tcx, 'a>( let (lhs, rhs) = mk_two_vir_args(bctx, expr.span, &args)?; let vop = match verus_item { + VerusItem::BinaryOp(BinaryOpItem::SpecOrd(spec_ord_item)) + if matches!(&*undecorate_typ(&lhs.typ), TypX::Float(_)) => + { + use vir::ast::IeeeFloatBinaryOp; + match spec_ord_item { + SpecOrdItem::Le => { + BinaryOp::IeeeFloat(IeeeFloatBinaryOp::InEq(InequalityOp::Le)) + } + SpecOrdItem::Ge => { + BinaryOp::IeeeFloat(IeeeFloatBinaryOp::InEq(InequalityOp::Ge)) + } + SpecOrdItem::Lt => { + BinaryOp::IeeeFloat(IeeeFloatBinaryOp::InEq(InequalityOp::Lt)) + } + SpecOrdItem::Gt => { + BinaryOp::IeeeFloat(IeeeFloatBinaryOp::InEq(InequalityOp::Gt)) + } + } + } VerusItem::BinaryOp(BinaryOpItem::SpecOrd(spec_ord_item)) => match spec_ord_item { SpecOrdItem::Le => BinaryOp::Inequality(InequalityOp::Le), SpecOrdItem::Ge => BinaryOp::Inequality(InequalityOp::Ge), @@ -1862,6 +1950,22 @@ fn verus_item_to_vir<'tcx, 'a>( } } } + VerusItem::BinaryOp(BinaryOpItem::SpecArith(spec_arith_item)) + if matches!(&*undecorate_typ(&expr_typ()?), TypX::Float(_)) => + { + use vir::ast::IeeeFloatBinaryOp; + match spec_arith_item { + SpecArithItem::Add => BinaryOp::IeeeFloat(IeeeFloatBinaryOp::Add), + SpecArithItem::Sub => BinaryOp::IeeeFloat(IeeeFloatBinaryOp::Sub), + SpecArithItem::Mul => BinaryOp::IeeeFloat(IeeeFloatBinaryOp::Mul), + SpecArithItem::EuclideanOrRealDiv => { + BinaryOp::IeeeFloat(IeeeFloatBinaryOp::Div) + } + SpecArithItem::EuclideanMod => { + unreachable!("spec mod operation cannot have floating point type") + } + } + } VerusItem::BinaryOp(BinaryOpItem::SpecArith(spec_arith_item)) => { let range = crate::rust_to_vir_base::get_range(&expr_typ()?); match spec_arith_item { diff --git a/source/rust_verify/src/rust_to_vir_base.rs b/source/rust_verify/src/rust_to_vir_base.rs index 50994c11a7..39e72009a4 100644 --- a/source/rust_verify/src/rust_to_vir_base.rs +++ b/source/rust_verify/src/rust_to_vir_base.rs @@ -1643,6 +1643,23 @@ pub(crate) fn is_smt_arith<'tcx>( } } +pub(crate) fn is_float_arith<'tcx>( + bctx: &BodyCtxt<'tcx>, + span1: Span, + span2: Span, + id1: &HirId, + id2: &HirId, +) -> Result { + let (t1, t2) = ( + typ_of_expr_adjusted(bctx, span1, id1, false)?, + typ_of_expr_adjusted(bctx, span2, id2, false)?, + ); + match (&*undecorate_typ(&t1), &*undecorate_typ(&t2)) { + (TypX::Float(_), TypX::Float(_)) => Ok(true), + _ => Ok(false), + } +} + fn get_proof_fn_one_mode<'tcx>( ctxt: &Context<'tcx>, span: Span, diff --git a/source/rust_verify/src/verus_items.rs b/source/rust_verify/src/verus_items.rs index fd28abcf17..d83015e474 100644 --- a/source/rust_verify/src/verus_items.rs +++ b/source/rust_verify/src/verus_items.rs @@ -217,6 +217,37 @@ pub(crate) enum SpecBitwiseItem { Shr, } +#[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] +pub(crate) enum IeeeFloatUnaryItem { + Cast, + Neg, + Floor, + Ceil, + Round, + RoundTiesEven, + Trunc, + IsNormal, + IsSubnormal, + IsZero, + IsInfinite, + IsNaN, + IsNegative, + IsPositive, +} + +#[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] +pub(crate) enum IeeeFloatBinaryItem { + Add, + Sub, + Mul, + Div, + Eq, + Le, + Ge, + Lt, + Gt, +} + #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] pub(crate) enum BinaryOpItem { Arith(ArithItem), @@ -224,6 +255,7 @@ pub(crate) enum BinaryOpItem { SpecOrd(SpecOrdItem), SpecArith(SpecArithItem), SpecBitwise(SpecBitwiseItem), + IeeeFloat(IeeeFloatBinaryItem), } #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] @@ -273,6 +305,7 @@ pub(crate) enum UnaryOpItem { SpecCastReal, RealFloor, SpecGhostTracked(SpecGhostTrackedItem), + IeeeFloat(IeeeFloatUnaryItem), } #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] @@ -518,6 +551,16 @@ fn verus_items_map() -> Vec<(&'static str, VerusItem)> { ("verus::verus_builtin::SpecShl::spec_shl", VerusItem::BinaryOp(BinaryOpItem::SpecBitwise(SpecBitwiseItem::Shl))), ("verus::verus_builtin::SpecShr::spec_shr", VerusItem::BinaryOp(BinaryOpItem::SpecBitwise(SpecBitwiseItem::Shr))), + ("verus::verus_builtin::IeeeFloat::ieee_add", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Add))), + ("verus::verus_builtin::IeeeFloat::ieee_sub", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Sub))), + ("verus::verus_builtin::IeeeFloat::ieee_mul", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Mul))), + ("verus::verus_builtin::IeeeFloat::ieee_div", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Div))), + ("verus::verus_builtin::IeeeFloat::ieee_eq", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Eq))), + ("verus::verus_builtin::IeeeFloat::ieee_le", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Le))), + ("verus::verus_builtin::IeeeFloat::ieee_ge", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Ge))), + ("verus::verus_builtin::IeeeFloat::ieee_lt", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Lt))), + ("verus::verus_builtin::IeeeFloat::ieee_gt", VerusItem::BinaryOp(BinaryOpItem::IeeeFloat(IeeeFloatBinaryItem::Gt))), + ("verus::verus_builtin::spec_chained_value", VerusItem::Chained(ChainedItem::Value)), ("verus::verus_builtin::spec_chained_le", VerusItem::Chained(ChainedItem::Le)), ("verus::verus_builtin::spec_chained_lt", VerusItem::Chained(ChainedItem::Lt)), @@ -551,6 +594,22 @@ fn verus_items_map() -> Vec<(&'static str, VerusItem)> { ("verus::verus_builtin::Ghost::borrow_mut", VerusItem::UnaryOp(UnaryOpItem::SpecGhostTracked(SpecGhostTrackedItem::GhostBorrowMut))), ("verus::verus_builtin::Tracked::view", VerusItem::UnaryOp(UnaryOpItem::SpecGhostTracked(SpecGhostTrackedItem::TrackedView))), + ("verus::verus_builtin::IeeeFloat::ieee_neg", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::Neg))), + ("verus::verus_builtin::IeeeFloat::ieee_floor", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::Floor))), + ("verus::verus_builtin::IeeeFloat::ieee_ceil", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::Ceil))), + ("verus::verus_builtin::IeeeFloat::ieee_round", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::Round))), + ("verus::verus_builtin::IeeeFloat::ieee_round_ties_even", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::RoundTiesEven))), + ("verus::verus_builtin::IeeeFloat::ieee_trunc", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::Trunc))), + ("verus::verus_builtin::IeeeFloat::ieee_is_normal", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::IsNormal))), + ("verus::verus_builtin::IeeeFloat::ieee_is_subnormal", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::IsSubnormal))), + ("verus::verus_builtin::IeeeFloat::ieee_is_zero", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::IsZero))), + ("verus::verus_builtin::IeeeFloat::ieee_is_infinite", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::IsInfinite))), + ("verus::verus_builtin::IeeeFloat::ieee_is_nan", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::IsNaN))), + ("verus::verus_builtin::IeeeFloat::ieee_is_negative", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::IsNegative))), + ("verus::verus_builtin::IeeeFloat::ieee_is_positive", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::IsPositive))), + ("verus::verus_builtin::IeeeFloat::ieee_is_positive", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::IsPositive))), + ("verus::verus_builtin::IeeeFloatCast::ieee_cast", VerusItem::UnaryOp(UnaryOpItem::IeeeFloat(IeeeFloatUnaryItem::Cast))), + ("verus::verus_builtin::erased_ghost_value", VerusItem::ErasedGhostValue), ("verus::verus_builtin::mutable_reference_tie", VerusItem::MutableReferenceTie), ("verus::verus_builtin::DummyCapture", VerusItem::DummyCapture(DummyCaptureItem::Struct)), diff --git a/source/rust_verify_test/tests/float.rs b/source/rust_verify_test/tests/float.rs index 27ce779d50..7bca34ad32 100644 --- a/source/rust_verify_test/tests/float.rs +++ b/source/rust_verify_test/tests/float.rs @@ -49,3 +49,92 @@ test_verify_one_file! { } } => Err(err) => assert_one_fails(err) } + +test_verify_one_file! { + #[test] f32_ieee verus_code! { + fn test1(x: f32, y: f32) { + assert(2.0f32 <= x <= 5.0f32 ==> x + x <= 10.0f32) by(bit_vector); + assert(2.0f32 <= x <= 5.0f32 && 2.0f32 <= y <= 5.0f32 ==> x + y == y + x) by(bit_vector); + assert(0.5f32.ieee_cast() === 0.5real) by(bit_vector); + assert(0.5f32 === 0.5real.ieee_cast()) by(bit_vector); + assert(4f32.ieee_cast() === 4u8) by(bit_vector); + assert(4f32 === 4u8.ieee_cast()) by(bit_vector); + assert(4f32 === 4f64.ieee_cast()) by(bit_vector); + assert(4f32.ieee_cast() === 4f64) by(bit_vector); + } + fn test2(x: f32, y: f32) { + assert(2.0f32 <= x <= 7.0f32 ==> x + x <= 10.0f32) by(bit_vector); // FAILS + } + fn test3(x: f32, y: f32) { + assert(2.0f32 <= x <= 5.0f32 && 2.0f32 <= y <= 5.0f32 ==> x + y == x + x) by(bit_vector); // FAILS + } + fn test4(x: f32, y: f32) { + assert(0.5f32.ieee_cast() === 0.6real) by(bit_vector); // FAILS + } + fn test5(x: f32, y: f32) { + assert(0.5f32 === 0.6real.ieee_cast()) by(bit_vector); // FAILS + } + fn test6(x: f32, y: f32) { + assert(4f32.ieee_cast() === 5u8) by(bit_vector); // FAILS + } + fn test7(x: f32, y: f32) { + assert(4f32 === 5u8.ieee_cast()) by(bit_vector); // FAILS + } + fn test8(x: f32, y: f32) { + assert(4f32 === 5f64.ieee_cast()) by(bit_vector); // FAILS + } + fn test9(x: f32, y: f32) { + assert(4f32.ieee_cast() === 5f64) by(bit_vector); // FAILS + } + } => Err(err) => assert_fails(err, 8) +} + +test_verify_one_file! { + #[test] f32_assume_ieee verus_code! { + use vstd::std_specs::cmp::{PartialEqSpec, PartialOrdSpec, PartialOrdIs}; + + fn test1(x: f32, y: f32) -> (z: f32) + requires + 1.0f32.is_le(&x), + x.is_le(&2.0), + 4.0f32.is_le(&y), + y.is_le(&8.0), + ensures + 5.0f32.is_le(&z), + z.is_le(&10.0), + { + broadcast use vstd::contrib::assume_ieee_float::assume_ieee_float; + + let z = x + y; + assert(5.0f32.ieee_le(x.ieee_add(y)) && x.ieee_add(y).ieee_le(10.0)) by(bit_vector) + requires + 1.0f32.ieee_le(x), + x.ieee_le(2.0), + 4.0f32.ieee_le(y), + y.ieee_le(8.0); + z + } + + fn test2(x: f32, y: f32) -> (z: f32) + requires + 1.0f32.is_le(&x), + x.is_le(&2.0), + 4.0f32.is_le(&y), + y.is_le(&8.0), + ensures + 5.0f32.is_le(&z), + z.is_lt(&10.0), + { + broadcast use vstd::contrib::assume_ieee_float::assume_ieee_float; + + let z = x + y; + assert(5.0f32.ieee_le(x.ieee_add(y)) && x.ieee_add(y).ieee_lt(10.0)) by(bit_vector) // FAILS + requires + 1.0f32.ieee_le(x), + x.ieee_le(2.0), + 4.0f32.ieee_le(y), + y.ieee_le(8.0); + z + } + } => Err(err) => assert_one_fails(err) +} diff --git a/source/rust_verify_test/tests/real.rs b/source/rust_verify_test/tests/real.rs index f0085e9960..38f1502a85 100644 --- a/source/rust_verify_test/tests/real.rs +++ b/source/rust_verify_test/tests/real.rs @@ -70,5 +70,5 @@ test_verify_one_file! { proof fn test() { assert(0real <= 1int <= 2real); } - } => Err(err) => assert_vir_error_msg(err, "The verifier does not yet support the following Rust feature: chained inequalities require all elements to have the same type (all integers or all reals)") + } => Err(err) => assert_vir_error_msg(err, "The verifier does not yet support the following Rust feature: chained inequalities require all elements to have the same type") } diff --git a/source/vir/src/ast.rs b/source/vir/src/ast.rs index b9be4c0982..920bb547f9 100644 --- a/source/vir/src/ast.rs +++ b/source/vir/src/ast.rs @@ -373,6 +373,28 @@ pub enum ArrayKind { Slice, } +/// IEEE floating point unary ops +#[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq, Hash, ToDebugSNode)] +pub enum IeeeFloatUnaryOp { + /// Cast to integer: rounding mode RTZ + /// Cast to float: rounding mode RNE + /// Cast to real: no rounding + Cast, + Neg, + Floor, + Ceil, + Round, + RoundTiesEven, + Trunc, + IsNormal, + IsSubnormal, + IsZero, + IsInfinite, + IsNaN, + IsNegative, + IsPositive, +} + /// Primitive unary operations /// (not arbitrary user-defined functions -- these are represented by ExprX::Call) #[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq, Hash, ToDebugSNode)] @@ -402,6 +424,8 @@ pub enum UnaryOp { RealToInt, /// Return raw bits of a float as an int FloatToBits, + /// IEEE unary floating point ops + IeeeFloat(IeeeFloatUnaryOp), /// Operations that coerce from/to verus_builtin::Ghost or verus_builtin::Tracked CoerceMode { op_mode: Mode, @@ -629,6 +653,17 @@ pub enum ChainedOp { MultiEq, } +/// IEEE floating point binary ops (rounding mode RNE) +#[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq, Hash, ToDebugSNode)] +pub enum IeeeFloatBinaryOp { + Add, + Sub, + Mul, + Div, + Eq, + InEq(InequalityOp), +} + /// Primitive binary operations /// (not arbitrary user-defined functions -- these are represented by ExprX::Call) /// Note that all integer operations are on mathematic integers (IntRange::Int), @@ -660,6 +695,8 @@ pub enum BinaryOp { RealArith(RealArithOp), /// Bit Vector Operators Bitwise(BitwiseOp, BitshiftBehavior), + /// IEEE floating point binary ops (rounding mode RNE) + IeeeFloat(IeeeFloatBinaryOp), /// Used only for handling verus_builtin::strslice_get_char StrGetChar, /// Index into an array or slice, no bounds-checking. diff --git a/source/vir/src/ast_simplify.rs b/source/vir/src/ast_simplify.rs index 8403d424cf..6a7cbf97a2 100644 --- a/source/vir/src/ast_simplify.rs +++ b/source/vir/src/ast_simplify.rs @@ -586,20 +586,29 @@ fn simplify_one_expr( } ExprX::Unary(UnaryOp::CoerceMode { .. }, expr0) => Ok(expr0.clone()), ExprX::Multi(MultiOp::Chained(ops), args) => { + use crate::ast::IeeeFloatBinaryOp; assert!(args.len() == ops.len() + 1); let mut stmts: Vec = Vec::new(); let mut es: Vec = Vec::new(); + let mut is_float = false; // Execute each argument in order; no short-circuiting for i in 0..args.len() { + let t = crate::ast_util::undecorate_typ(&args[i].typ); + if matches!(*t, TypX::Float(_)) { + is_float = true; + } let (decl, e) = temp_expr(state, &args[i]); stmts.push(decl); es.push(e); } let mut conjunction: Expr = es[0].clone(); for i in 0..ops.len() { - let op = match ops[i] { - ChainedOp::Inequality(a) => BinaryOp::Inequality(a), - ChainedOp::MultiEq => BinaryOp::Eq(Mode::Spec), + let op = match (is_float, ops[i]) { + (false, ChainedOp::Inequality(a)) => BinaryOp::Inequality(a), + (true, ChainedOp::Inequality(a)) => { + BinaryOp::IeeeFloat(IeeeFloatBinaryOp::InEq(a)) + } + (_, ChainedOp::MultiEq) => BinaryOp::Eq(Mode::Spec), }; let left = es[i].clone(); let right = es[i + 1].clone(); diff --git a/source/vir/src/ast_util.rs b/source/vir/src/ast_util.rs index 6b362a0103..705a007af4 100644 --- a/source/vir/src/ast_util.rs +++ b/source/vir/src/ast_util.rs @@ -287,12 +287,15 @@ pub fn undecorate_typ(typ: &Typ) -> Typ { if let TypX::Decorate(_, _, t) = &**typ { undecorate_typ(t) } else { typ.clone() } } -pub fn allowed_bitvector_type(typ: &Typ) -> bool { - match &*undecorate_typ(typ) { - TypX::Bool => true, - TypX::Int(IntRange::U(_) | IntRange::I(_) | IntRange::USize | IntRange::ISize) => true, +pub fn allowed_bitvector_type(typ: &Typ) -> Option { + let u = undecorate_typ(typ); + match &*u { + TypX::Bool => Some(u), + TypX::Int(IntRange::U(_) | IntRange::I(_) | IntRange::USize | IntRange::ISize) => Some(u), + TypX::Float { .. } => Some(u), + TypX::Real => Some(u), TypX::Boxed(typ) => allowed_bitvector_type(typ), - _ => false, + _ => None, } } @@ -1459,6 +1462,7 @@ impl BinaryOp { | BinaryOp::Arith(_) | BinaryOp::RealArith(_) | BinaryOp::Bitwise(..) + | BinaryOp::IeeeFloat(_) | BinaryOp::StrGetChar | BinaryOp::Index(..) => false, } diff --git a/source/vir/src/bitvector_to_air.rs b/source/vir/src/bitvector_to_air.rs index f535fa954a..3a2f27226a 100644 --- a/source/vir/src/bitvector_to_air.rs +++ b/source/vir/src/bitvector_to_air.rs @@ -250,6 +250,8 @@ enum Extend { enum BvTyp { Bool, Bv(u32, Extend), + Float { exp_bits: u32, sig_bits: u32 }, + Real, } #[derive(Debug, Clone)] @@ -258,6 +260,14 @@ struct BvExpr { bv_typ: BvTyp, } +fn f32_typ() -> BvTyp { + BvTyp::Float { exp_bits: 8, sig_bits: 24 } +} + +fn f64_typ() -> BvTyp { + BvTyp::Float { exp_bits: 11, sig_bits: 53 } +} + fn bv_exp_to_expr(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result { match &exp.x { ExpX::Const(crate::ast::Constant::Int(i)) => { @@ -271,6 +281,19 @@ fn bv_exp_to_expr(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result { Ok(BvExpr { expr: Arc::new(ExprX::Const(Constant::Bool(*b))), bv_typ: BvTyp::Bool }) } + ExpX::Const(crate::ast::Constant::Float32(i)) => { + let e_i = Arc::new(ExprX::Const(Constant::BitVec(Arc::new(i.to_string()), 32))); + let op = air::ast::UnaryOp::FloatFromIeeeBits { exp_bits: 8, sig_bits: 24 }; + Ok(BvExpr { expr: Arc::new(ExprX::Unary(op, e_i)), bv_typ: f32_typ() }) + } + ExpX::Const(crate::ast::Constant::Float64(i)) => { + let e_i = Arc::new(ExprX::Const(Constant::BitVec(Arc::new(i.to_string()), 64))); + let op = air::ast::UnaryOp::FloatFromIeeeBits { exp_bits: 11, sig_bits: 53 }; + Ok(BvExpr { expr: Arc::new(ExprX::Unary(op, e_i)), bv_typ: f64_typ() }) + } + ExpX::Const(crate::ast::Constant::Real(r)) => { + Ok(BvExpr { expr: air::ast_util::mk_real(r), bv_typ: BvTyp::Real }) + } ExpX::Var(x) => { let id = suffix_local_unique_id(x); @@ -340,9 +363,65 @@ fn bv_exp_to_expr(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result panic!("internal error: unexpected float to bits coercion"), + UnaryOp::IeeeFloat(crate::ast::IeeeFloatUnaryOp::Cast) => { + use air::ast::RoundingMode; + let BvExpr { expr: e_from, bv_typ: t_from } = bv_exp_to_expr(ctx, state, arg)?; + let t_to = bv_typ_for_vir_typ(state, &exp.span, &exp.typ)?; + let op = match (t_from, t_to) { + (_, BvTyp::Float { exp_bits, sig_bits }) => { + let signed = !is_integer_type(&arg.typ) || is_integer_type_signed(&arg.typ); + air::ast::UnaryOp::FloatFrom { + exp_bits, + sig_bits, + signed, + round: RoundingMode::RNE, + } + } + (BvTyp::Float { .. }, BvTyp::Real) => air::ast::UnaryOp::FloatToReal, + (BvTyp::Float { .. }, _) => { + assert!(is_integer_type(&exp.typ)); + let signed = is_integer_type_signed(&exp.typ); + let w = bitwidth_from_type(&exp.typ).expect("is_integer_type"); + let IntegerTypeBitwidth::Width(bits) = w else { + panic!("internal error: unexpected usize/isize") + }; + air::ast::UnaryOp::FloatToBitVec { bits, signed, round: RoundingMode::RTZ } + } + _ => { + panic!("internal error: unexpected cast from {:?} to {:?}", t_from, t_to) + } + }; + Ok(BvExpr { expr: Arc::new(ExprX::Unary(op, e_from)), bv_typ: t_to }) + } + UnaryOp::IeeeFloat(fop) => { + use crate::ast::IeeeFloatUnaryOp; + use air::ast::RoundingMode; + let BvExpr { expr, bv_typ } = bv_exp_to_expr(ctx, state, arg)?; + assert!(matches!(bv_typ, BvTyp::Float { .. })); + let round = |r: RoundingMode| (false, air::ast::UnaryOp::FloatRoundToInt(r)); + let (is_bool, op) = match fop { + IeeeFloatUnaryOp::Cast => unreachable!(), + IeeeFloatUnaryOp::Neg => (false, air::ast::UnaryOp::FloatNeg), + IeeeFloatUnaryOp::Floor => round(RoundingMode::RTN), + IeeeFloatUnaryOp::Ceil => round(RoundingMode::RTP), + IeeeFloatUnaryOp::Round => round(RoundingMode::RNA), + IeeeFloatUnaryOp::RoundTiesEven => round(RoundingMode::RNE), + IeeeFloatUnaryOp::Trunc => round(RoundingMode::RTZ), + IeeeFloatUnaryOp::IsNormal => (true, air::ast::UnaryOp::FloatIsNormal), + IeeeFloatUnaryOp::IsSubnormal => (true, air::ast::UnaryOp::FloatIsSubnormal), + IeeeFloatUnaryOp::IsZero => (true, air::ast::UnaryOp::FloatIsZero), + IeeeFloatUnaryOp::IsInfinite => (true, air::ast::UnaryOp::FloatIsInfinite), + IeeeFloatUnaryOp::IsNaN => (true, air::ast::UnaryOp::FloatIsNaN), + IeeeFloatUnaryOp::IsNegative => (true, air::ast::UnaryOp::FloatIsNegative), + IeeeFloatUnaryOp::IsPositive => (true, air::ast::UnaryOp::FloatIsPositive), + }; + + let bv_typ = if is_bool { BvTyp::Bool } else { bv_typ }; + Ok(BvExpr { expr: Arc::new(ExprX::Unary(op, expr)), bv_typ }) + } UnaryOp::IntToReal => panic!("internal error: unexpected int to real coercion"), UnaryOp::RealToInt => panic!("internal error: unexpected real to int coercion"), + UnaryOp::FloatToBits => panic!("internal error: unexpected float to bits coercion"), UnaryOp::HeightTrigger => panic!("internal error: unexpected HeightTrigger"), UnaryOp::Trigger(_) => bv_exp_to_expr(ctx, state, arg), UnaryOp::CoerceMode { .. } => { @@ -532,6 +611,29 @@ fn bv_exp_to_expr(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result { + use crate::ast::IeeeFloatBinaryOp; + use air::ast::RoundingMode; + let lhs = bv_exp_to_expr(ctx, state, lhs)?; + let rhs = bv_exp_to_expr(ctx, state, rhs)?; + assert!(matches!((lhs.bv_typ, rhs.bv_typ), (BvTyp::Float { .. }, BvTyp::Float { .. }))); + + let round = RoundingMode::RNE; + let (is_bool, op) = match fop { + IeeeFloatBinaryOp::Add => (false, air::ast::BinaryOp::FloatAdd(round)), + IeeeFloatBinaryOp::Sub => (false, air::ast::BinaryOp::FloatSub(round)), + IeeeFloatBinaryOp::Mul => (false, air::ast::BinaryOp::FloatMul(round)), + IeeeFloatBinaryOp::Div => (false, air::ast::BinaryOp::FloatDiv(round)), + IeeeFloatBinaryOp::Eq => (true, air::ast::BinaryOp::FloatEq), + IeeeFloatBinaryOp::InEq(InequalityOp::Le) => (true, air::ast::BinaryOp::FloatLe), + IeeeFloatBinaryOp::InEq(InequalityOp::Ge) => (true, air::ast::BinaryOp::FloatGe), + IeeeFloatBinaryOp::InEq(InequalityOp::Lt) => (true, air::ast::BinaryOp::FloatLt), + IeeeFloatBinaryOp::InEq(InequalityOp::Gt) => (true, air::ast::BinaryOp::FloatGt), + }; + + let bv_typ = if is_bool { BvTyp::Bool } else { lhs.bv_typ }; + Ok(BvExpr { expr: Arc::new(ExprX::Binary(op, lhs.expr, rhs.expr)), bv_typ }) + } ExpX::Binary(BinaryOp::Arith(arith_op), lhs, rhs) => { return do_arith_then_clip(ctx, state, &exp.span, arith_op, lhs, rhs, None); } @@ -759,6 +861,12 @@ fn make_same_bv_typ(span: &Span, lhs: BvExpr, rhs: BvExpr) -> Result<(BvExpr, Bv if lhs.bv_typ == BvTyp::Bool && rhs.bv_typ == BvTyp::Bool { return Ok((lhs, rhs)); } + if lhs.bv_typ == BvTyp::Real && rhs.bv_typ == BvTyp::Real { + return Ok((lhs, rhs)); + } + if matches!((lhs.bv_typ, rhs.bv_typ), (BvTyp::Float { .. }, BvTyp::Float { .. })) { + return Ok((lhs, rhs)); + } // Compute the minimum extension satisfying both constraints: // - We need to extend both to be the same width @@ -813,9 +921,13 @@ impl BvTyp { } fn to_air_typ(&self) -> air::ast::Typ { - match self { - BvTyp::Bv(w, _) => air::ast_util::bv_typ(*w), + match *self { + BvTyp::Bv(w, _) => air::ast_util::bv_typ(w), BvTyp::Bool => bool_typ(), + BvTyp::Float { exp_bits, sig_bits } => { + Arc::new(air::ast::TypX::Float { exp_bits, sig_bits }) + } + BvTyp::Real => Arc::new(air::ast::TypX::Real), } } } @@ -865,17 +977,21 @@ fn bv_typ_for_vir_typ(state: &mut State, span: &Span, typ: &Typ) -> Result Ok(BvTyp::Bool), + TypX::Float(32) => Ok(f32_typ()), + TypX::Float(64) => Ok(f64_typ()), + TypX::Real => Ok(BvTyp::Real), + _ => unreachable!(), } + } else { + Err(error( + span, + format!( + "error: bit_vector prover cannot handle this type (bit_vector can only handle variables of type `bool` or of fixed-width integers)" + ), + )) } } diff --git a/source/vir/src/datatype_to_air.rs b/source/vir/src/datatype_to_air.rs index 8d9e0a33fe..b324b469e8 100644 --- a/source/vir/src/datatype_to_air.rs +++ b/source/vir/src/datatype_to_air.rs @@ -822,6 +822,16 @@ pub fn datatypes_and_primitives_to_air(ctx: &Ctx, datatypes: &crate::ast::Dataty vec![] }; + let ieee_float_commands = if ctx.used_builtins.uses_ieee_float { + let nodes = crate::prelude::ieee_float_prelude(); + let cmds = air::parser::Parser::new(Arc::new(crate::messages::VirMessageInterface {})) + .nodes_to_commands(&nodes) + .expect("internal error: malformed IEEE float axioms"); + (*cmds).clone() + } else { + vec![] + }; + let pointee_metadata_commands = if ctx.used_builtins.uses_pointee_metadata { let nodes = crate::prelude::pointee_metadata_prelude(); let cmds = air::parser::Parser::new(Arc::new(crate::messages::VirMessageInterface {})) @@ -846,6 +856,7 @@ pub fn datatypes_and_primitives_to_air(ctx: &Ctx, datatypes: &crate::ast::Dataty commands.append(&mut axiom_commands); commands.extend(array_commands); commands.extend(strslice_commands); + commands.extend(ieee_float_commands); commands.extend(resolve_axiom_commands); Arc::new(commands) } diff --git a/source/vir/src/def.rs b/source/vir/src/def.rs index 6f966d849d..1a08b46786 100644 --- a/source/vir/src/def.rs +++ b/source/vir/src/def.rs @@ -251,6 +251,32 @@ pub const STRSLICE_NEW_STRLIT: &str = "str%new_strlit"; // only used to prove that new_strlit is injective pub const STRSLICE_FROM_STRLIT: &str = "str%from_strlit"; +pub const IEEE_FLOAT_CAST: &str = "ieee_float_cast"; +pub const IEEE_FLOAT_CAST_FROM_REAL: &str = "ieee_float_cast_from_real"; +pub const IEEE_FLOAT_CAST_TO_REAL: &str = "ieee_float_cast_to_real"; +pub const IEEE_FLOAT_NEG: &str = "ieee_float_neg"; +pub const IEEE_FLOAT_FLOOR: &str = "ieee_float_floor"; +pub const IEEE_FLOAT_CEIL: &str = "ieee_float_ceil"; +pub const IEEE_FLOAT_ROUND: &str = "ieee_float_round"; +pub const IEEE_FLOAT_ROUND_TIES_EVEN: &str = "ieee_float_round_ties_even"; +pub const IEEE_FLOAT_TRUNC: &str = "ieee_float_trunc"; +pub const IEEE_FLOAT_IS_NORMAL: &str = "ieee_float_is_normal"; +pub const IEEE_FLOAT_IS_SUBNORMAL: &str = "ieee_float_is_subnormal"; +pub const IEEE_FLOAT_IS_ZERO: &str = "ieee_float_is_zero"; +pub const IEEE_FLOAT_IS_INFINITE: &str = "ieee_float_is_infinite"; +pub const IEEE_FLOAT_IS_NAN: &str = "ieee_float_is_nan"; +pub const IEEE_FLOAT_IS_NEGATIVE: &str = "ieee_float_is_negative"; +pub const IEEE_FLOAT_IS_POSITIVE: &str = "ieee_float_is_positive"; +pub const IEEE_FLOAT_ADD: &str = "ieee_float_add"; +pub const IEEE_FLOAT_SUB: &str = "ieee_float_sub"; +pub const IEEE_FLOAT_MUL: &str = "ieee_float_mul"; +pub const IEEE_FLOAT_DIV: &str = "ieee_float_div"; +pub const IEEE_FLOAT_EQ: &str = "ieee_float_eq"; +pub const IEEE_FLOAT_LE: &str = "ieee_float_le"; +pub const IEEE_FLOAT_GE: &str = "ieee_float_ge"; +pub const IEEE_FLOAT_LT: &str = "ieee_float_lt"; +pub const IEEE_FLOAT_GT: &str = "ieee_float_gt"; + pub const VERUSLIB: &str = "vstd"; pub const VERUSLIB_PREFIX: &str = "vstd::"; pub const PERVASIVE_PREFIX: &str = "pervasive::"; diff --git a/source/vir/src/heuristics.rs b/source/vir/src/heuristics.rs index a264cff7aa..28c6a16de6 100644 --- a/source/vir/src/heuristics.rs +++ b/source/vir/src/heuristics.rs @@ -53,9 +53,10 @@ fn insert_auto_ext_equal(ctx: &Ctx, exp: &Exp) -> Exp { match &exp.x { ExpX::Unary(op, e) => match op { UnaryOp::Not | UnaryOp::BitNot(_) | UnaryOp::Clip { .. } => exp.clone(), - UnaryOp::FloatToBits => exp.clone(), UnaryOp::IntToReal => exp.clone(), UnaryOp::RealToInt => exp.clone(), + UnaryOp::FloatToBits => exp.clone(), + UnaryOp::IeeeFloat(_) => exp.clone(), UnaryOp::StrLen | UnaryOp::StrIsAscii | UnaryOp::Length(_) => exp.clone(), UnaryOp::InferSpecForLoopIter { .. } => exp.clone(), UnaryOp::Trigger(_) @@ -103,6 +104,7 @@ fn insert_auto_ext_equal(ctx: &Ctx, exp: &Exp) -> Exp { | BinaryOp::Arith(..) | BinaryOp::RealArith(..) | BinaryOp::Bitwise(..) + | BinaryOp::IeeeFloat(_) | BinaryOp::StrGetChar | BinaryOp::Index(..) => exp.clone(), }, diff --git a/source/vir/src/interpreter.rs b/source/vir/src/interpreter.rs index 42500b2ff0..6b46ceaa56 100644 --- a/source/vir/src/interpreter.rs +++ b/source/vir/src/interpreter.rs @@ -1170,9 +1170,10 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result bool_new(!b), BitNot(..) | Clip { .. } - | FloatToBits | IntToReal | RealToInt + | FloatToBits + | IeeeFloat(_) | HeightTrigger | Trigger(_) | CoerceMode { .. } @@ -1292,9 +1293,10 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result Result { - ok_e2(e2.clone()) - } + Index(ArrayKind::Slice, _) + | HeightCompare { .. } + | StrGetChar + | RealArith(..) + | IeeeFloat(_) => ok_e2(eval_expr_internal(ctx, state, e2)?), } } BinaryOpr(op, e1, e2) => { diff --git a/source/vir/src/poly.rs b/source/vir/src/poly.rs index ad8a40e0c6..a90de33f64 100644 --- a/source/vir/src/poly.rs +++ b/source/vir/src/poly.rs @@ -560,9 +560,10 @@ fn visit_exp(ctx: &Ctx, state: &mut State, exp: &Exp) -> Exp { match op { UnaryOp::Not | UnaryOp::Clip { .. } - | UnaryOp::FloatToBits | UnaryOp::IntToReal | UnaryOp::RealToInt + | UnaryOp::FloatToBits + | UnaryOp::IeeeFloat(..) | UnaryOp::BitNot(_) | UnaryOp::StrLen | UnaryOp::StrIsAscii => { @@ -670,6 +671,7 @@ fn visit_exp(ctx: &Ctx, state: &mut State, exp: &Exp) -> Exp { BinaryOp::RealArith(..) => (true, false), BinaryOp::Eq(_) | BinaryOp::Ne => (false, false), BinaryOp::Bitwise(..) => (true, false), + BinaryOp::IeeeFloat(..) => (true, false), BinaryOp::StrGetChar { .. } => (true, false), BinaryOp::Index(..) => unreachable!("Index"), }; diff --git a/source/vir/src/prelude.rs b/source/vir/src/prelude.rs index c6c4d46069..b194ad5bc0 100644 --- a/source/vir/src/prelude.rs +++ b/source/vir/src/prelude.rs @@ -1221,6 +1221,63 @@ pub(crate) fn pointee_metadata_prelude() -> Vec { ) } +pub(crate) fn ieee_float_prelude() -> Vec { + let typ = str_to_node(TYPE); + let ieee_float_cast = str_to_node(IEEE_FLOAT_CAST); + let ieee_float_cast_from_real = str_to_node(IEEE_FLOAT_CAST_FROM_REAL); + let ieee_float_cast_to_real = str_to_node(IEEE_FLOAT_CAST_TO_REAL); + let ieee_float_neg = str_to_node(IEEE_FLOAT_NEG); + let ieee_float_floor = str_to_node(IEEE_FLOAT_FLOOR); + let ieee_float_ceil = str_to_node(IEEE_FLOAT_CEIL); + let ieee_float_round = str_to_node(IEEE_FLOAT_ROUND); + let ieee_float_round_ties_even = str_to_node(IEEE_FLOAT_ROUND_TIES_EVEN); + let ieee_float_trunc = str_to_node(IEEE_FLOAT_TRUNC); + let ieee_float_is_normal = str_to_node(IEEE_FLOAT_IS_NORMAL); + let ieee_float_is_subnormal = str_to_node(IEEE_FLOAT_IS_SUBNORMAL); + let ieee_float_is_zero = str_to_node(IEEE_FLOAT_IS_ZERO); + let ieee_float_is_infinite = str_to_node(IEEE_FLOAT_IS_INFINITE); + let ieee_float_is_nan = str_to_node(IEEE_FLOAT_IS_NAN); + let ieee_float_is_negative = str_to_node(IEEE_FLOAT_IS_NEGATIVE); + let ieee_float_is_positive = str_to_node(IEEE_FLOAT_IS_POSITIVE); + let ieee_float_add = str_to_node(IEEE_FLOAT_ADD); + let ieee_float_sub = str_to_node(IEEE_FLOAT_SUB); + let ieee_float_mul = str_to_node(IEEE_FLOAT_MUL); + let ieee_float_div = str_to_node(IEEE_FLOAT_DIV); + let ieee_float_eq = str_to_node(IEEE_FLOAT_EQ); + let ieee_float_le = str_to_node(IEEE_FLOAT_LE); + let ieee_float_ge = str_to_node(IEEE_FLOAT_GE); + let ieee_float_lt = str_to_node(IEEE_FLOAT_LT); + let ieee_float_gt = str_to_node(IEEE_FLOAT_GT); + + nodes_vec!( + (declare-fun [ieee_float_cast] ([typ] [typ] Int) Int) + (declare-fun [ieee_float_cast_from_real] ([typ] Real) Int) + (declare-fun [ieee_float_cast_to_real] ([typ] Int) Real) + (declare-fun [ieee_float_neg] (Int) Int) + (declare-fun [ieee_float_floor] (Int) Int) + (declare-fun [ieee_float_ceil] (Int) Int) + (declare-fun [ieee_float_round] (Int) Int) + (declare-fun [ieee_float_round_ties_even] (Int) Int) + (declare-fun [ieee_float_trunc] (Int) Int) + (declare-fun [ieee_float_is_normal] (Int) Bool) + (declare-fun [ieee_float_is_subnormal] (Int) Bool) + (declare-fun [ieee_float_is_zero] (Int) Bool) + (declare-fun [ieee_float_is_infinite] (Int) Bool) + (declare-fun [ieee_float_is_nan] (Int) Bool) + (declare-fun [ieee_float_is_negative] (Int) Bool) + (declare-fun [ieee_float_is_positive] (Int) Bool) + (declare-fun [ieee_float_add] (Int Int) Int) + (declare-fun [ieee_float_sub] (Int Int) Int) + (declare-fun [ieee_float_mul] (Int Int) Int) + (declare-fun [ieee_float_div] (Int Int) Int) + (declare-fun [ieee_float_eq] (Int Int) Bool) + (declare-fun [ieee_float_le] (Int Int) Bool) + (declare-fun [ieee_float_ge] (Int Int) Bool) + (declare-fun [ieee_float_lt] (Int Int) Bool) + (declare-fun [ieee_float_gt] (Int Int) Bool) + ) +} + fn datatype_height_axiom( typ_name1: &Path, typ_name2: &Option, diff --git a/source/vir/src/printer.rs b/source/vir/src/printer.rs index f5318a001c..830446057b 100644 --- a/source/vir/src/printer.rs +++ b/source/vir/src/printer.rs @@ -236,6 +236,7 @@ impl ToDebugSNode for air::ast::TypX { TypX::BitVec(size) => { Node::List(vec![Node::Atom("BitVec".to_string()), size.to_node(opts)]) } + TypX::Float { exp_bits, sig_bits } => Node::Atom(format!("Float{exp_bits}_{sig_bits}")), } } } diff --git a/source/vir/src/prune.rs b/source/vir/src/prune.rs index 232282ddf0..e86592d050 100644 --- a/source/vir/src/prune.rs +++ b/source/vir/src/prune.rs @@ -113,6 +113,7 @@ struct State { dyn_traits: HashSet, uses_array: bool, uses_pointee_metadata: bool, + uses_ieee_float: bool, fndef_types: HashSet, // broadcast functions that are also defined or called normally // (not just used for the broadcast) @@ -520,6 +521,10 @@ fn traverse_reachable(ctxt: &Ctxt, state: &mut State) { reach_function(ctxt, state, &fn_slice_len(&ctxt.vstd_crate_name)); } } + ExprX::Unary(UnaryOp::IeeeFloat(_), _) + | ExprX::Binary(BinaryOp::IeeeFloat(_), _, _) => { + state.uses_ieee_float = true; + } _ => {} } Ok(e.clone()) @@ -801,6 +806,7 @@ fn collect_broadcast_triggers(f: &Function) -> Vec<(Vec, Vec)> pub struct UsedBuiltins { pub uses_array: bool, pub uses_pointee_metadata: bool, + pub uses_ieee_float: bool, } // - module is none: prune to keep what's reachable from current_crate @@ -1282,6 +1288,7 @@ pub fn prune_krate_for_module_or_krate( let used_builtins = UsedBuiltins { uses_array: state.uses_array, uses_pointee_metadata: state.uses_pointee_metadata, + uses_ieee_float: state.uses_ieee_float, }; let prune_info = PruneInfo { mono_abstract_datatypes, diff --git a/source/vir/src/sst_to_air.rs b/source/vir/src/sst_to_air.rs index 13874375ee..8aa8e074ae 100644 --- a/source/vir/src/sst_to_air.rs +++ b/source/vir/src/sst_to_air.rs @@ -1059,7 +1059,6 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp, expr_ctxt: &ExprCtxt) -> Result< }; apply_range_fun(&f_name, &range, vec![expr]) } - UnaryOp::FloatToBits => exp_to_expr(ctx, e, expr_ctxt)?, UnaryOp::IntToReal => { let expr = exp_to_expr(ctx, e, expr_ctxt)?; Arc::new(ExprX::Unary(air::ast::UnaryOp::ToReal, expr)) @@ -1068,6 +1067,50 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp, expr_ctxt: &ExprCtxt) -> Result< let expr = exp_to_expr(ctx, e, expr_ctxt)?; Arc::new(ExprX::Unary(air::ast::UnaryOp::RealToInt, expr)) } + UnaryOp::FloatToBits => exp_to_expr(ctx, e, expr_ctxt)?, + UnaryOp::IeeeFloat(crate::ast::IeeeFloatUnaryOp::Cast) => { + let t_from = undecorate_typ(&e.typ); + let t_to = undecorate_typ(&exp.typ); + let mut args: Vec = Vec::new(); + let fname = match (&*t_from, &*t_to) { + (TypX::Real, _) => { + args.push(typ_to_id(ctx, &t_to)); + crate::def::IEEE_FLOAT_CAST_FROM_REAL + } + (_, TypX::Real) => { + args.push(typ_to_id(ctx, &t_from)); + crate::def::IEEE_FLOAT_CAST_TO_REAL + } + _ => { + args.push(typ_to_id(ctx, &t_from)); + args.push(typ_to_id(ctx, &t_to)); + crate::def::IEEE_FLOAT_CAST + } + }; + args.push(exp_to_expr(ctx, e, expr_ctxt)?); + Arc::new(ExprX::Apply(Arc::new(fname.to_string()), Arc::new(args))) + } + UnaryOp::IeeeFloat(fop) => { + use crate::ast::IeeeFloatUnaryOp; + let expr = exp_to_expr(ctx, e, expr_ctxt)?; + let fname = match fop { + IeeeFloatUnaryOp::Cast => unreachable!(), + IeeeFloatUnaryOp::Neg => crate::def::IEEE_FLOAT_NEG, + IeeeFloatUnaryOp::Floor => crate::def::IEEE_FLOAT_FLOOR, + IeeeFloatUnaryOp::Ceil => crate::def::IEEE_FLOAT_CEIL, + IeeeFloatUnaryOp::Round => crate::def::IEEE_FLOAT_ROUND, + IeeeFloatUnaryOp::RoundTiesEven => crate::def::IEEE_FLOAT_ROUND_TIES_EVEN, + IeeeFloatUnaryOp::Trunc => crate::def::IEEE_FLOAT_TRUNC, + IeeeFloatUnaryOp::IsNormal => crate::def::IEEE_FLOAT_IS_NORMAL, + IeeeFloatUnaryOp::IsSubnormal => crate::def::IEEE_FLOAT_IS_SUBNORMAL, + IeeeFloatUnaryOp::IsZero => crate::def::IEEE_FLOAT_IS_ZERO, + IeeeFloatUnaryOp::IsInfinite => crate::def::IEEE_FLOAT_IS_INFINITE, + IeeeFloatUnaryOp::IsNaN => crate::def::IEEE_FLOAT_IS_NAN, + IeeeFloatUnaryOp::IsNegative => crate::def::IEEE_FLOAT_IS_NEGATIVE, + IeeeFloatUnaryOp::IsPositive => crate::def::IEEE_FLOAT_IS_POSITIVE, + }; + Arc::new(ExprX::Apply(Arc::new(fname.to_string()), Arc::new(vec![expr]))) + } UnaryOp::CoerceMode { .. } => { panic!("internal error: CoerceMode should have been removed before here") } @@ -1370,6 +1413,21 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp, expr_ctxt: &ExprCtxt) -> Result< return clip_bitwise_result(bit_expr, exp); } + BinaryOp::IeeeFloat(fop) => { + use crate::ast::IeeeFloatBinaryOp; + let fname = match fop { + IeeeFloatBinaryOp::Add => crate::def::IEEE_FLOAT_ADD, + IeeeFloatBinaryOp::Sub => crate::def::IEEE_FLOAT_SUB, + IeeeFloatBinaryOp::Mul => crate::def::IEEE_FLOAT_MUL, + IeeeFloatBinaryOp::Div => crate::def::IEEE_FLOAT_DIV, + IeeeFloatBinaryOp::Eq => crate::def::IEEE_FLOAT_EQ, + IeeeFloatBinaryOp::InEq(InequalityOp::Le) => crate::def::IEEE_FLOAT_LE, + IeeeFloatBinaryOp::InEq(InequalityOp::Ge) => crate::def::IEEE_FLOAT_GE, + IeeeFloatBinaryOp::InEq(InequalityOp::Lt) => crate::def::IEEE_FLOAT_LT, + IeeeFloatBinaryOp::InEq(InequalityOp::Gt) => crate::def::IEEE_FLOAT_GT, + }; + ExprX::Apply(Arc::new(fname.to_string()), Arc::new(vec![lh, rh])) + } _ => { let aop = match op { BinaryOp::And => unreachable!(), @@ -1394,6 +1452,7 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp, expr_ctxt: &ExprCtxt) -> Result< } BinaryOp::RealArith(..) => unreachable!(), BinaryOp::Bitwise(..) => unreachable!(), + BinaryOp::IeeeFloat(_) => unreachable!(), BinaryOp::StrGetChar => unreachable!(), BinaryOp::Index(..) => unreachable!(), }; diff --git a/source/vir/src/sst_util.rs b/source/vir/src/sst_util.rs index ff7edad5b2..7c24d30f0d 100644 --- a/source/vir/src/sst_util.rs +++ b/source/vir/src/sst_util.rs @@ -353,6 +353,7 @@ impl BinaryOp { BitOr => (20, 20, 21), Shr(..) | Shl(..) => (26, 26, 27), }, + IeeeFloat(_) => (5, 90, 90), StrGetChar => (90, 90, 90), Index(_, _) => (90, 90, 90), } @@ -446,15 +447,18 @@ impl ExpX { ), 99, ), - UnaryOp::FloatToBits => { - (format!("float_to_bits({})", exp.x.to_user_string(global)), 99) - } UnaryOp::IntToReal => { (format!("int_to_real({})", exp.x.to_user_string(global)), 99) } UnaryOp::RealToInt => { (format!("real_to_int({})", exp.x.to_user_string(global)), 99) } + UnaryOp::FloatToBits => { + (format!("float_to_bits({})", exp.x.to_user_string(global)), 99) + } + UnaryOp::IeeeFloat(_) => { + (format!("ieee_float({})", exp.x.to_user_string(global)), 99) + } UnaryOp::HeightTrigger => { (format!("height_trigger({})", exp.x.to_user_string(global)), 99) } @@ -565,6 +569,7 @@ impl ExpX { Shr(..) => ">>", Shl(..) => "<<", }, + IeeeFloat(_) => "ieee_float", StrGetChar => "ignored", // This is a non-infix BinaryOp, so it needs special handling below Index(..) => "ignored", // This is a non-infix BinaryOp, so it needs special handling below }; diff --git a/source/vir/src/triggers.rs b/source/vir/src/triggers.rs index 27455a99de..25cdf12591 100644 --- a/source/vir/src/triggers.rs +++ b/source/vir/src/triggers.rs @@ -121,9 +121,10 @@ fn check_trigger_expr_arg(state: &mut State, arg: &Exp) { } UnaryOp::Not | UnaryOp::Clip { .. } - | UnaryOp::FloatToBits | UnaryOp::IntToReal | UnaryOp::RealToInt + | UnaryOp::FloatToBits + | UnaryOp::IeeeFloat(_) | UnaryOp::BitNot(_) | UnaryOp::StrLen | UnaryOp::StrIsAscii @@ -199,6 +200,7 @@ fn check_trigger_expr( ExpX::Unary(UnaryOp::BitNot(_), _) => {} ExpX::BinaryOpr(crate::ast::BinaryOpr::ExtEq(..), _, _) => {} ExpX::Unary(UnaryOp::Clip { .. }, _) | ExpX::Binary(BinaryOp::Arith(..), _, _) => {} + ExpX::Unary(UnaryOp::IeeeFloat(_), _) | ExpX::Binary(BinaryOp::IeeeFloat(_), _, _) => {} ExpX::UnaryOpr(UnaryOpr::HasResolved(_), _) => {} _ => { return Err(error( @@ -269,9 +271,10 @@ fn check_trigger_expr( Ok(()) } UnaryOp::Clip { .. } - | UnaryOp::FloatToBits | UnaryOp::IntToReal - | UnaryOp::RealToInt => { + | UnaryOp::RealToInt + | UnaryOp::FloatToBits + | UnaryOp::IeeeFloat(_) => { check_trigger_expr_arg(state, arg); Ok(()) } @@ -327,7 +330,7 @@ fn check_trigger_expr( check_trigger_expr_arg(state, arg2); Ok(()) } - Arith(..) | RealArith(..) => { + Arith(..) | RealArith(..) | IeeeFloat(..) => { check_trigger_expr_arg(state, arg1); check_trigger_expr_arg(state, arg2); Ok(()) diff --git a/source/vir/src/triggers_auto.rs b/source/vir/src/triggers_auto.rs index d2794723d0..3ffcc0c8d3 100644 --- a/source/vir/src/triggers_auto.rs +++ b/source/vir/src/triggers_auto.rs @@ -411,9 +411,10 @@ fn gather_terms(ctxt: &mut Ctxt, ctx: &Ctx, exp: &Exp, depth: u64) -> (bool, Ter | UnaryOp::Length(_) => 0, UnaryOp::HeightTrigger => 1, UnaryOp::Trigger(_) | UnaryOp::Clip { .. } | UnaryOp::BitNot(_) => 1, - UnaryOp::FloatToBits => 1, UnaryOp::IntToReal => 1, UnaryOp::RealToInt => 1, + UnaryOp::FloatToBits => 1, + UnaryOp::IeeeFloat(_) => 1, UnaryOp::InferSpecForLoopIter { .. } => 1, UnaryOp::StrIsAscii | UnaryOp::StrLen => fail_on_strop(), UnaryOp::MutRefFinal(_) => 1, @@ -468,7 +469,7 @@ fn gather_terms(ctxt: &mut Ctxt, ctx: &Ctx, exp: &Exp, depth: u64) -> (bool, Ter let depth = match op { And | Or | Xor | Implies | Eq(_) => 0, HeightCompare { .. } => 1, - Ne | Inequality(_) | Arith(..) | RealArith(..) => 1, + Ne | Inequality(_) | Arith(..) | RealArith(..) | IeeeFloat(..) => 1, Bitwise(..) => 1, StrGetChar => fail_on_strop(), Index(..) => 1, diff --git a/source/vstd/contrib/mod.rs b/source/vstd/contrib/mod.rs index e292439809..515a6c6a00 100644 --- a/source/vstd/contrib/mod.rs +++ b/source/vstd/contrib/mod.rs @@ -1,4 +1,5 @@ pub use verus_builtin_macros::auto_spec; pub use verus_builtin_macros::{make_spec_type, self_view}; pub use verus_builtin_macros::{set_build, set_build_debug}; +pub mod assume_ieee_float; pub mod exec_spec; diff --git a/source/vstd/float.rs b/source/vstd/float.rs index af9d6d1243..626cac6a94 100644 --- a/source/vstd/float.rs +++ b/source/vstd/float.rs @@ -20,7 +20,7 @@ pub trait FloatBitsProperties { // Positive or negative infinity (not zero, not subnormal, not normal, not NaN) spec fn is_infinite_spec(&self) -> bool; - // A NaN value (not zero, not subnormal, not normal, not NaN) + // A NaN value (not zero, not subnormal, not normal, not infinity) spec fn is_nan_spec(&self) -> bool; } From 5ce68c9494cc5fa3ed959e97ea11d587cbf1fabb Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Thu, 5 Mar 2026 23:10:45 -0800 Subject: [PATCH 2/6] Add assume_ieee_float.rs --- source/vstd/contrib/assume_ieee_float.rs | 289 +++++++++++++++++++++++ 1 file changed, 289 insertions(+) create mode 100644 source/vstd/contrib/assume_ieee_float.rs diff --git a/source/vstd/contrib/assume_ieee_float.rs b/source/vstd/contrib/assume_ieee_float.rs new file mode 100644 index 0000000000..a6589b13f0 --- /dev/null +++ b/source/vstd/contrib/assume_ieee_float.rs @@ -0,0 +1,289 @@ +use super::super::prelude::*; + +/* +Verus deliberately omits axioms about floating point from vstd, +because the desired set of useful and sound axioms may vary by project and platform. +(See https://github.com/rust-lang/rfcs/blob/master/text/3514-float-semantics.md for details +about why Rust floating point semantics are complex, may be non-deterministic, and may fall short +of desired behavior on some platforms.) + +Some platforms may strictly obey IEEE 754 semantics. +For such platforms, you can "broadcast use assume_ieee_float" from this module +to connect the Rust floating point semantics to the IEEE semantics +as defined in SMT solvers according to https://smt-lib.org/theories-FloatingPoint.shtml . +This allows proofs using assert-by-bit_vector, which calls into the SMT solver's bit vector +and floating point theories to prove properties of ieee_add, ieee_eq, ieee_le, etc. +(note that <=, +, etc. in specs are equivalent to ieee_le, ieee_add, etc.): + +``` +use vstd::std_specs::cmp::{PartialEqSpec, PartialOrdSpec, PartialOrdIs}; + +fn test(x: f32, y: f32) -> (z: f32) + requires + 1.0f32 <= x <= 2.0f32, + 4.0f32 <= y <= 8.0f32, + ensures + 5.0f32 <= z <= 10f32, +{ + broadcast use vstd::contrib::assume_ieee_float::assume_ieee_float; + + let z = x + y; + assert(5.0f32 <= x + y <= 10.0f32) by(bit_vector) + requires + 1.0f32 <= x <= 2.0f32, + 4.0f32 <= y <= 8.0f32; + z +} +``` +*/ + +verus! { + +#[cfg(verus_keep_ghost)] +use super::super::std_specs::cmp::{PartialEqSpec, PartialOrdSpec, PartialOrdIs}; + +#[cfg(verus_keep_ghost)] +use super::super::std_specs::ops::{NegSpec, AddSpec, SubSpec, MulSpec, DivSpec}; + +use super::super::float::FloatBitsProperties; + +// ieee_is_nan picks one particular NaN value, while is_nan_spec covers all possible NaN values +// (i.e. x.ieee_is_nan() && y.ieee_is_nan() ==> x == y, whereas this is not true for is_nan_spec) +pub broadcast axiom fn assume_ieee_f32_is_nan(x: f32) + ensures + #![trigger x.is_nan_spec()] + #![trigger x.ieee_is_nan()] + x.ieee_is_nan() ==> x.is_nan_spec(), +; + +pub broadcast axiom fn assume_ieee_f32_is_infinite(x: f32) + ensures + #![trigger x.is_infinite_spec()] + #![trigger x.ieee_is_infinite()] + x.is_infinite_spec() == x.ieee_is_infinite(), +; + +pub broadcast axiom fn assume_ieee_f32_neg(x: f32) + ensures + #![trigger x.neg_req()] + #![trigger x.neg_spec()] + #![trigger x.ieee_neg()] + ::obeys_neg_spec(), + x.neg_req(), + x.neg_spec() == x.ieee_neg(), +; + +pub broadcast axiom fn assume_ieee_f32_add(x: f32, y: f32) + ensures + #![trigger x.add_req(y)] + #![trigger x.add_spec(y)] + #![trigger x.ieee_add(y)] + ::obeys_add_spec(), + x.add_req(y), + x.add_spec(y) == x.ieee_add(y), +; + +pub broadcast axiom fn assume_ieee_f32_sub(x: f32, y: f32) + ensures + #![trigger x.sub_req(y)] + #![trigger x.sub_spec(y)] + #![trigger x.ieee_sub(y)] + ::obeys_sub_spec(), + x.sub_req(y), + x.sub_spec(y) == x.ieee_sub(y), +; + +pub broadcast axiom fn assume_ieee_f32_mul(x: f32, y: f32) + ensures + #![trigger x.mul_req(y)] + #![trigger x.mul_spec(y)] + #![trigger x.ieee_mul(y)] + ::obeys_mul_spec(), + x.mul_req(y), + x.mul_spec(y) == x.ieee_mul(y), +; + +pub broadcast axiom fn assume_ieee_f32_div(x: f32, y: f32) + ensures + #![trigger x.div_req(y)] + #![trigger x.div_spec(y)] + #![trigger x.ieee_div(y)] + ::obeys_div_spec(), + x.div_req(y), + x.div_spec(y) == x.ieee_div(y), +; + +pub broadcast axiom fn assume_ieee_f32_eq(x: f32, y: f32) + ensures + #![trigger x.eq_spec(&y)] + #![trigger x.ieee_eq(y)] + ::obeys_eq_spec(), + x.eq_spec(&y) == x.ieee_eq(y), +; + +pub broadcast axiom fn assume_ieee_f32_le(x: f32, y: f32) + ensures + #![trigger x.partial_cmp_spec(&y)] + #![trigger x.ieee_le(y)] + ::obeys_partial_cmp_spec(), + x.is_le(&y) == x.ieee_le(y), +; + +pub broadcast axiom fn assume_ieee_f32_ge(x: f32, y: f32) + ensures + #![trigger x.partial_cmp_spec(&y)] + #![trigger x.ieee_ge(y)] + ::obeys_partial_cmp_spec(), + x.is_ge(&y) == x.ieee_ge(y), +; + +pub broadcast axiom fn assume_ieee_f32_lt(x: f32, y: f32) + ensures + #![trigger x.partial_cmp_spec(&y)] + #![trigger x.ieee_lt(y)] + ::obeys_partial_cmp_spec(), + x.is_lt(&y) == x.ieee_lt(y), +; + +pub broadcast axiom fn assume_ieee_f32_gt(x: f32, y: f32) + ensures + #![trigger x.partial_cmp_spec(&y)] + #![trigger x.ieee_gt(y)] + ::obeys_partial_cmp_spec(), + x.is_gt(&y) == x.ieee_gt(y), +; + +// ieee_is_nan picks one particular NaN value, while is_nan_spec covers all possible NaN values +// (i.e. x.ieee_is_nan() && y.ieee_is_nan() ==> x == y, whereas this is not true for is_nan_spec) +pub broadcast axiom fn assume_ieee_f64_is_nan(x: f64) + ensures + #![trigger x.is_nan_spec()] + #![trigger x.ieee_is_nan()] + x.ieee_is_nan() ==> x.is_nan_spec(), +; + +pub broadcast axiom fn assume_ieee_f64_is_infinite(x: f64) + ensures + #![trigger x.is_infinite_spec()] + #![trigger x.ieee_is_infinite()] + x.is_infinite_spec() == x.ieee_is_infinite(), +; + +pub broadcast axiom fn assume_ieee_f64_neg(x: f64) + ensures + #![trigger x.neg_req()] + #![trigger x.neg_spec()] + #![trigger x.ieee_neg()] + ::obeys_neg_spec(), + x.neg_req(), + x.neg_spec() == x.ieee_neg(), +; + +pub broadcast axiom fn assume_ieee_f64_add(x: f64, y: f64) + ensures + #![trigger x.add_req(y)] + #![trigger x.add_spec(y)] + #![trigger x.ieee_add(y)] + ::obeys_add_spec(), + x.add_req(y), + x.add_spec(y) == x.ieee_add(y), +; + +pub broadcast axiom fn assume_ieee_f64_sub(x: f64, y: f64) + ensures + #![trigger x.sub_req(y)] + #![trigger x.sub_spec(y)] + #![trigger x.ieee_sub(y)] + ::obeys_sub_spec(), + x.sub_req(y), + x.sub_spec(y) == x.ieee_sub(y), +; + +pub broadcast axiom fn assume_ieee_f64_mul(x: f64, y: f64) + ensures + #![trigger x.mul_req(y)] + #![trigger x.mul_spec(y)] + #![trigger x.ieee_mul(y)] + ::obeys_mul_spec(), + x.mul_req(y), + x.mul_spec(y) == x.ieee_mul(y), +; + +pub broadcast axiom fn assume_ieee_f64_div(x: f64, y: f64) + ensures + #![trigger x.div_req(y)] + #![trigger x.div_spec(y)] + #![trigger x.ieee_div(y)] + ::obeys_div_spec(), + x.div_req(y), + x.div_spec(y) == x.ieee_div(y), +; + +pub broadcast axiom fn assume_ieee_f64_eq(x: f64, y: f64) + ensures + #![trigger x.eq_spec(&y)] + #![trigger x.ieee_eq(y)] + ::obeys_eq_spec(), + x.eq_spec(&y) == x.ieee_eq(y), +; + +pub broadcast axiom fn assume_ieee_f64_le(x: f64, y: f64) + ensures + #![trigger x.partial_cmp_spec(&y)] + #![trigger x.ieee_le(y)] + ::obeys_partial_cmp_spec(), + x.is_le(&y) == x.ieee_le(y), +; + +pub broadcast axiom fn assume_ieee_f64_ge(x: f64, y: f64) + ensures + #![trigger x.partial_cmp_spec(&y)] + #![trigger x.ieee_ge(y)] + ::obeys_partial_cmp_spec(), + x.is_ge(&y) == x.ieee_ge(y), +; + +pub broadcast axiom fn assume_ieee_f64_lt(x: f64, y: f64) + ensures + #![trigger x.partial_cmp_spec(&y)] + #![trigger x.ieee_lt(y)] + ::obeys_partial_cmp_spec(), + x.is_lt(&y) == x.ieee_lt(y), +; + +pub broadcast axiom fn assume_ieee_f64_gt(x: f64, y: f64) + ensures + #![trigger x.partial_cmp_spec(&y)] + #![trigger x.ieee_gt(y)] + ::obeys_partial_cmp_spec(), + x.is_gt(&y) == x.ieee_gt(y), +; + +pub broadcast group assume_ieee_float { + assume_ieee_f32_is_nan, + assume_ieee_f32_is_infinite, + assume_ieee_f32_neg, + assume_ieee_f32_add, + assume_ieee_f32_sub, + assume_ieee_f32_mul, + assume_ieee_f32_div, + assume_ieee_f32_eq, + assume_ieee_f32_le, + assume_ieee_f32_ge, + assume_ieee_f32_lt, + assume_ieee_f32_gt, + assume_ieee_f64_is_nan, + assume_ieee_f64_is_infinite, + assume_ieee_f64_neg, + assume_ieee_f64_add, + assume_ieee_f64_sub, + assume_ieee_f64_mul, + assume_ieee_f64_div, + assume_ieee_f64_eq, + assume_ieee_f64_le, + assume_ieee_f64_ge, + assume_ieee_f64_lt, + assume_ieee_f64_gt, +} + +} // verus! From 4cf145f5ab7cd2622cb7d41ac039503fae65e494 Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Thu, 5 Mar 2026 23:18:20 -0800 Subject: [PATCH 3/6] vargo fmt --- source/vstd/contrib/assume_ieee_float.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/source/vstd/contrib/assume_ieee_float.rs b/source/vstd/contrib/assume_ieee_float.rs index a6589b13f0..45d45a2793 100644 --- a/source/vstd/contrib/assume_ieee_float.rs +++ b/source/vstd/contrib/assume_ieee_float.rs @@ -41,10 +41,8 @@ verus! { #[cfg(verus_keep_ghost)] use super::super::std_specs::cmp::{PartialEqSpec, PartialOrdSpec, PartialOrdIs}; - #[cfg(verus_keep_ghost)] use super::super::std_specs::ops::{NegSpec, AddSpec, SubSpec, MulSpec, DivSpec}; - use super::super::float::FloatBitsProperties; // ieee_is_nan picks one particular NaN value, while is_nan_spec covers all possible NaN values From 893e3404dba5bf03bc3c033d4592697bf5ad8040 Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Fri, 6 Mar 2026 16:27:03 -0800 Subject: [PATCH 4/6] Split assume_ieee_float off into a separate pull request --- source/rust_verify_test/tests/float.rs | 50 ---- source/vstd/contrib/assume_ieee_float.rs | 287 ----------------------- source/vstd/contrib/mod.rs | 1 - 3 files changed, 338 deletions(-) delete mode 100644 source/vstd/contrib/assume_ieee_float.rs diff --git a/source/rust_verify_test/tests/float.rs b/source/rust_verify_test/tests/float.rs index 7bca34ad32..848a9b0a6e 100644 --- a/source/rust_verify_test/tests/float.rs +++ b/source/rust_verify_test/tests/float.rs @@ -88,53 +88,3 @@ test_verify_one_file! { } } => Err(err) => assert_fails(err, 8) } - -test_verify_one_file! { - #[test] f32_assume_ieee verus_code! { - use vstd::std_specs::cmp::{PartialEqSpec, PartialOrdSpec, PartialOrdIs}; - - fn test1(x: f32, y: f32) -> (z: f32) - requires - 1.0f32.is_le(&x), - x.is_le(&2.0), - 4.0f32.is_le(&y), - y.is_le(&8.0), - ensures - 5.0f32.is_le(&z), - z.is_le(&10.0), - { - broadcast use vstd::contrib::assume_ieee_float::assume_ieee_float; - - let z = x + y; - assert(5.0f32.ieee_le(x.ieee_add(y)) && x.ieee_add(y).ieee_le(10.0)) by(bit_vector) - requires - 1.0f32.ieee_le(x), - x.ieee_le(2.0), - 4.0f32.ieee_le(y), - y.ieee_le(8.0); - z - } - - fn test2(x: f32, y: f32) -> (z: f32) - requires - 1.0f32.is_le(&x), - x.is_le(&2.0), - 4.0f32.is_le(&y), - y.is_le(&8.0), - ensures - 5.0f32.is_le(&z), - z.is_lt(&10.0), - { - broadcast use vstd::contrib::assume_ieee_float::assume_ieee_float; - - let z = x + y; - assert(5.0f32.ieee_le(x.ieee_add(y)) && x.ieee_add(y).ieee_lt(10.0)) by(bit_vector) // FAILS - requires - 1.0f32.ieee_le(x), - x.ieee_le(2.0), - 4.0f32.ieee_le(y), - y.ieee_le(8.0); - z - } - } => Err(err) => assert_one_fails(err) -} diff --git a/source/vstd/contrib/assume_ieee_float.rs b/source/vstd/contrib/assume_ieee_float.rs deleted file mode 100644 index 45d45a2793..0000000000 --- a/source/vstd/contrib/assume_ieee_float.rs +++ /dev/null @@ -1,287 +0,0 @@ -use super::super::prelude::*; - -/* -Verus deliberately omits axioms about floating point from vstd, -because the desired set of useful and sound axioms may vary by project and platform. -(See https://github.com/rust-lang/rfcs/blob/master/text/3514-float-semantics.md for details -about why Rust floating point semantics are complex, may be non-deterministic, and may fall short -of desired behavior on some platforms.) - -Some platforms may strictly obey IEEE 754 semantics. -For such platforms, you can "broadcast use assume_ieee_float" from this module -to connect the Rust floating point semantics to the IEEE semantics -as defined in SMT solvers according to https://smt-lib.org/theories-FloatingPoint.shtml . -This allows proofs using assert-by-bit_vector, which calls into the SMT solver's bit vector -and floating point theories to prove properties of ieee_add, ieee_eq, ieee_le, etc. -(note that <=, +, etc. in specs are equivalent to ieee_le, ieee_add, etc.): - -``` -use vstd::std_specs::cmp::{PartialEqSpec, PartialOrdSpec, PartialOrdIs}; - -fn test(x: f32, y: f32) -> (z: f32) - requires - 1.0f32 <= x <= 2.0f32, - 4.0f32 <= y <= 8.0f32, - ensures - 5.0f32 <= z <= 10f32, -{ - broadcast use vstd::contrib::assume_ieee_float::assume_ieee_float; - - let z = x + y; - assert(5.0f32 <= x + y <= 10.0f32) by(bit_vector) - requires - 1.0f32 <= x <= 2.0f32, - 4.0f32 <= y <= 8.0f32; - z -} -``` -*/ - -verus! { - -#[cfg(verus_keep_ghost)] -use super::super::std_specs::cmp::{PartialEqSpec, PartialOrdSpec, PartialOrdIs}; -#[cfg(verus_keep_ghost)] -use super::super::std_specs::ops::{NegSpec, AddSpec, SubSpec, MulSpec, DivSpec}; -use super::super::float::FloatBitsProperties; - -// ieee_is_nan picks one particular NaN value, while is_nan_spec covers all possible NaN values -// (i.e. x.ieee_is_nan() && y.ieee_is_nan() ==> x == y, whereas this is not true for is_nan_spec) -pub broadcast axiom fn assume_ieee_f32_is_nan(x: f32) - ensures - #![trigger x.is_nan_spec()] - #![trigger x.ieee_is_nan()] - x.ieee_is_nan() ==> x.is_nan_spec(), -; - -pub broadcast axiom fn assume_ieee_f32_is_infinite(x: f32) - ensures - #![trigger x.is_infinite_spec()] - #![trigger x.ieee_is_infinite()] - x.is_infinite_spec() == x.ieee_is_infinite(), -; - -pub broadcast axiom fn assume_ieee_f32_neg(x: f32) - ensures - #![trigger x.neg_req()] - #![trigger x.neg_spec()] - #![trigger x.ieee_neg()] - ::obeys_neg_spec(), - x.neg_req(), - x.neg_spec() == x.ieee_neg(), -; - -pub broadcast axiom fn assume_ieee_f32_add(x: f32, y: f32) - ensures - #![trigger x.add_req(y)] - #![trigger x.add_spec(y)] - #![trigger x.ieee_add(y)] - ::obeys_add_spec(), - x.add_req(y), - x.add_spec(y) == x.ieee_add(y), -; - -pub broadcast axiom fn assume_ieee_f32_sub(x: f32, y: f32) - ensures - #![trigger x.sub_req(y)] - #![trigger x.sub_spec(y)] - #![trigger x.ieee_sub(y)] - ::obeys_sub_spec(), - x.sub_req(y), - x.sub_spec(y) == x.ieee_sub(y), -; - -pub broadcast axiom fn assume_ieee_f32_mul(x: f32, y: f32) - ensures - #![trigger x.mul_req(y)] - #![trigger x.mul_spec(y)] - #![trigger x.ieee_mul(y)] - ::obeys_mul_spec(), - x.mul_req(y), - x.mul_spec(y) == x.ieee_mul(y), -; - -pub broadcast axiom fn assume_ieee_f32_div(x: f32, y: f32) - ensures - #![trigger x.div_req(y)] - #![trigger x.div_spec(y)] - #![trigger x.ieee_div(y)] - ::obeys_div_spec(), - x.div_req(y), - x.div_spec(y) == x.ieee_div(y), -; - -pub broadcast axiom fn assume_ieee_f32_eq(x: f32, y: f32) - ensures - #![trigger x.eq_spec(&y)] - #![trigger x.ieee_eq(y)] - ::obeys_eq_spec(), - x.eq_spec(&y) == x.ieee_eq(y), -; - -pub broadcast axiom fn assume_ieee_f32_le(x: f32, y: f32) - ensures - #![trigger x.partial_cmp_spec(&y)] - #![trigger x.ieee_le(y)] - ::obeys_partial_cmp_spec(), - x.is_le(&y) == x.ieee_le(y), -; - -pub broadcast axiom fn assume_ieee_f32_ge(x: f32, y: f32) - ensures - #![trigger x.partial_cmp_spec(&y)] - #![trigger x.ieee_ge(y)] - ::obeys_partial_cmp_spec(), - x.is_ge(&y) == x.ieee_ge(y), -; - -pub broadcast axiom fn assume_ieee_f32_lt(x: f32, y: f32) - ensures - #![trigger x.partial_cmp_spec(&y)] - #![trigger x.ieee_lt(y)] - ::obeys_partial_cmp_spec(), - x.is_lt(&y) == x.ieee_lt(y), -; - -pub broadcast axiom fn assume_ieee_f32_gt(x: f32, y: f32) - ensures - #![trigger x.partial_cmp_spec(&y)] - #![trigger x.ieee_gt(y)] - ::obeys_partial_cmp_spec(), - x.is_gt(&y) == x.ieee_gt(y), -; - -// ieee_is_nan picks one particular NaN value, while is_nan_spec covers all possible NaN values -// (i.e. x.ieee_is_nan() && y.ieee_is_nan() ==> x == y, whereas this is not true for is_nan_spec) -pub broadcast axiom fn assume_ieee_f64_is_nan(x: f64) - ensures - #![trigger x.is_nan_spec()] - #![trigger x.ieee_is_nan()] - x.ieee_is_nan() ==> x.is_nan_spec(), -; - -pub broadcast axiom fn assume_ieee_f64_is_infinite(x: f64) - ensures - #![trigger x.is_infinite_spec()] - #![trigger x.ieee_is_infinite()] - x.is_infinite_spec() == x.ieee_is_infinite(), -; - -pub broadcast axiom fn assume_ieee_f64_neg(x: f64) - ensures - #![trigger x.neg_req()] - #![trigger x.neg_spec()] - #![trigger x.ieee_neg()] - ::obeys_neg_spec(), - x.neg_req(), - x.neg_spec() == x.ieee_neg(), -; - -pub broadcast axiom fn assume_ieee_f64_add(x: f64, y: f64) - ensures - #![trigger x.add_req(y)] - #![trigger x.add_spec(y)] - #![trigger x.ieee_add(y)] - ::obeys_add_spec(), - x.add_req(y), - x.add_spec(y) == x.ieee_add(y), -; - -pub broadcast axiom fn assume_ieee_f64_sub(x: f64, y: f64) - ensures - #![trigger x.sub_req(y)] - #![trigger x.sub_spec(y)] - #![trigger x.ieee_sub(y)] - ::obeys_sub_spec(), - x.sub_req(y), - x.sub_spec(y) == x.ieee_sub(y), -; - -pub broadcast axiom fn assume_ieee_f64_mul(x: f64, y: f64) - ensures - #![trigger x.mul_req(y)] - #![trigger x.mul_spec(y)] - #![trigger x.ieee_mul(y)] - ::obeys_mul_spec(), - x.mul_req(y), - x.mul_spec(y) == x.ieee_mul(y), -; - -pub broadcast axiom fn assume_ieee_f64_div(x: f64, y: f64) - ensures - #![trigger x.div_req(y)] - #![trigger x.div_spec(y)] - #![trigger x.ieee_div(y)] - ::obeys_div_spec(), - x.div_req(y), - x.div_spec(y) == x.ieee_div(y), -; - -pub broadcast axiom fn assume_ieee_f64_eq(x: f64, y: f64) - ensures - #![trigger x.eq_spec(&y)] - #![trigger x.ieee_eq(y)] - ::obeys_eq_spec(), - x.eq_spec(&y) == x.ieee_eq(y), -; - -pub broadcast axiom fn assume_ieee_f64_le(x: f64, y: f64) - ensures - #![trigger x.partial_cmp_spec(&y)] - #![trigger x.ieee_le(y)] - ::obeys_partial_cmp_spec(), - x.is_le(&y) == x.ieee_le(y), -; - -pub broadcast axiom fn assume_ieee_f64_ge(x: f64, y: f64) - ensures - #![trigger x.partial_cmp_spec(&y)] - #![trigger x.ieee_ge(y)] - ::obeys_partial_cmp_spec(), - x.is_ge(&y) == x.ieee_ge(y), -; - -pub broadcast axiom fn assume_ieee_f64_lt(x: f64, y: f64) - ensures - #![trigger x.partial_cmp_spec(&y)] - #![trigger x.ieee_lt(y)] - ::obeys_partial_cmp_spec(), - x.is_lt(&y) == x.ieee_lt(y), -; - -pub broadcast axiom fn assume_ieee_f64_gt(x: f64, y: f64) - ensures - #![trigger x.partial_cmp_spec(&y)] - #![trigger x.ieee_gt(y)] - ::obeys_partial_cmp_spec(), - x.is_gt(&y) == x.ieee_gt(y), -; - -pub broadcast group assume_ieee_float { - assume_ieee_f32_is_nan, - assume_ieee_f32_is_infinite, - assume_ieee_f32_neg, - assume_ieee_f32_add, - assume_ieee_f32_sub, - assume_ieee_f32_mul, - assume_ieee_f32_div, - assume_ieee_f32_eq, - assume_ieee_f32_le, - assume_ieee_f32_ge, - assume_ieee_f32_lt, - assume_ieee_f32_gt, - assume_ieee_f64_is_nan, - assume_ieee_f64_is_infinite, - assume_ieee_f64_neg, - assume_ieee_f64_add, - assume_ieee_f64_sub, - assume_ieee_f64_mul, - assume_ieee_f64_div, - assume_ieee_f64_eq, - assume_ieee_f64_le, - assume_ieee_f64_ge, - assume_ieee_f64_lt, - assume_ieee_f64_gt, -} - -} // verus! diff --git a/source/vstd/contrib/mod.rs b/source/vstd/contrib/mod.rs index 515a6c6a00..e292439809 100644 --- a/source/vstd/contrib/mod.rs +++ b/source/vstd/contrib/mod.rs @@ -1,5 +1,4 @@ pub use verus_builtin_macros::auto_spec; pub use verus_builtin_macros::{make_spec_type, self_view}; pub use verus_builtin_macros::{set_build, set_build_debug}; -pub mod assume_ieee_float; pub mod exec_spec; From c81de7af7c07670ab6c2bfa44be7a1f65163de62 Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Mon, 9 Mar 2026 14:51:01 -0700 Subject: [PATCH 5/6] Address comments --- source/air/src/typecheck.rs | 2 ++ source/rust_verify_test/tests/float.rs | 2 ++ source/vir/src/bitvector_to_air.rs | 2 +- source/vir/src/sst_to_air.rs | 3 +++ 4 files changed, 8 insertions(+), 1 deletion(-) diff --git a/source/air/src/typecheck.rs b/source/air/src/typecheck.rs index f2779c31d8..392888a674 100644 --- a/source/air/src/typecheck.rs +++ b/source/air/src/typecheck.rs @@ -252,6 +252,7 @@ fn check_float_unary_exprs( expr: &Expr, ) -> Result { let t0 = check_expr(typing, expr)?; + // See https://smt-lib.org/theories-FloatingPoint.shtml for types of each operation match &*t0 { TypX::Float { .. } => match op { UnaryOp::FloatNeg => Ok(t0.clone()), @@ -283,6 +284,7 @@ fn check_float_exprs( ) -> Result { let t0 = check_expr(typing, &exprs[0])?; let t1 = check_expr(typing, &exprs[1])?; + // See https://smt-lib.org/theories-FloatingPoint.shtml for types of each operation match (&*t0, &*t1) { ( TypX::Float { exp_bits: exp_bits0, sig_bits: sig_bits0 }, diff --git a/source/rust_verify_test/tests/float.rs b/source/rust_verify_test/tests/float.rs index 848a9b0a6e..50485b2c82 100644 --- a/source/rust_verify_test/tests/float.rs +++ b/source/rust_verify_test/tests/float.rs @@ -52,6 +52,8 @@ test_verify_one_file! { test_verify_one_file! { #[test] f32_ieee verus_code! { + // TODO: replace explicit calls to ieee_cast with "as" when support for "as" is added + // (and use this to replace === with ==) fn test1(x: f32, y: f32) { assert(2.0f32 <= x <= 5.0f32 ==> x + x <= 10.0f32) by(bit_vector); assert(2.0f32 <= x <= 5.0f32 && 2.0f32 <= y <= 5.0f32 ==> x + y == y + x) by(bit_vector); diff --git a/source/vir/src/bitvector_to_air.rs b/source/vir/src/bitvector_to_air.rs index 3a2f27226a..5207b9631c 100644 --- a/source/vir/src/bitvector_to_air.rs +++ b/source/vir/src/bitvector_to_air.rs @@ -989,7 +989,7 @@ fn bv_typ_for_vir_typ(state: &mut State, span: &Span, typ: &Typ) -> Result Result< let t_from = undecorate_typ(&e.typ); let t_to = undecorate_typ(&exp.typ); let mut args: Vec = Vec::new(); + // translate to uninterpreted function ieee_float_cast + // (except for cast to/from real, which needs a separate uninterpreted function + // because real has a different SMT type) let fname = match (&*t_from, &*t_to) { (TypX::Real, _) => { args.push(typ_to_id(ctx, &t_to)); From caf6b707fed54238024a29a2a75e58b42df5cfb1 Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Mon, 9 Mar 2026 14:54:38 -0700 Subject: [PATCH 6/6] Explicitly mark real->real case as unreachable --- source/vir/src/sst_to_air.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/source/vir/src/sst_to_air.rs b/source/vir/src/sst_to_air.rs index 520ce8bff7..20bc5557e8 100644 --- a/source/vir/src/sst_to_air.rs +++ b/source/vir/src/sst_to_air.rs @@ -1076,6 +1076,7 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp, expr_ctxt: &ExprCtxt) -> Result< // (except for cast to/from real, which needs a separate uninterpreted function // because real has a different SMT type) let fname = match (&*t_from, &*t_to) { + (TypX::Real, TypX::Real) => unreachable!("no real->real cast in IeeeFloatCast"), (TypX::Real, _) => { args.push(typ_to_id(ctx, &t_to)); crate::def::IEEE_FLOAT_CAST_FROM_REAL