Xavier Denis

I've written a document here: https://hackmd.io/CuEgMe-oSau4oj2UwNSx4g .

Is it not translated to `absurd`? It should be. By the way I believe rust has a `assume` intrinsic which you could use here.

Yea, this wouldn't be documented in `creusot-contracts` as the intrinsic will get lowered to a specific MIR construct, not a function call.

``` pub fn uint_to_int(uty: &UintTy) -> Exp { match uty { UintTy::Usize => Exp::impure_qvar(QName::from_string("UIntSize.to_int").unwrap()), UintTy::U8 => unimplemented!(), UintTy::U16 => unimplemented!(), UintTy::U32 => Exp::impure_qvar(QName::from_string("UInt32.to_int").unwrap()), UintTy::U64 => Exp::impure_qvar(QName::from_string("UInt64.to_int").unwrap()), UintTy::U128 => unimplemented!(), }...

that'll be a trivial fix

> Now that https://github.com/xldenis/creusot/pull/488 has been merged this seems to have become a soundness issue. Yea, the example given above demonstrates that. Allowing access to prophetic information in ghost code...

> Currently, there doesn't seem to be much difference between predicates and logic functions (that return bool), so I wonder if it would work to forbid calling predicates in logic...

Does `rustc` ignore unknown cfgs ? If so I'll see how we can add this

Great, I'll work on setting up Creusot to set this cfg then

Additionally, it would be good to have a systematic way to validate external specifications... I know they are trusted and thus fundamentally axioms, but in some cases they can be...