Add attributes #[skip] and refinement attributes

[W95Psp]

Example:

use hax_lib_macros::*;

#[skip]
pub fn skip_me() {}

#[hax]
pub struct Hello {
    pub x: u32,
    #[refine(y > 3)]
    pub y: u32,
    #[refine(y + x + z > 3)]
    pub z: u32,
}

Translates into the following F*:

module Attributes
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core

let v___: Prims.unit = ()

let refinement_under___ (x y: u32) : bool = y >. 3ul

let v___1: Prims.unit = ()

let refinement_under___1 (x y z: u32) : bool = ((y +. x <: u32) +. z <: u32) >. 3ul

type t_Hello = {
  f_x:u32;
  f_y:f_y: u32{f_y >. 3ul};
  f_z:f_z: u32{((f_y +. f_x <: u32) +. f_z <: u32) >. 3ul}
}

I need to add more attributes and clean up the refinement_under__* things

TODO (follow up PRs):

• a #[hax::late_skip] (internal thing: translate to the backend, but don't print)
• refinements on functions inputs & outputs (follow up PR)
• pre/post on functions, contract style
• #[refine(...)] on enum fields
• #[hax::lemma] for marking a function and express that this function is a lemma statement we want to prove on the proof assistant side
• please comment if other ideas

[franziskuskiefer]

Thanks, I think there's enough good stuff in here to get it in.

Did you remove the hax attribute again? We should have it at some point. But skip is more important for now I think.

[W95Psp]

I just renamed that hax attribute to hax_attributes: when an item is marked with this attribute, anything below it can use the refine attribute (where it's allowed --for now only on struct fields).

[franziskuskiefer]

I just renamed that hax attribute to hax_attributes: when an item is marked with this attribute, anything below it can use the refine attribute (where it's allowed --for now only on struct fields).

Right, but we want a hax attribute that disables everything in a crate except for the annotated functions to extract code from large crates. But that's not urgent yet. Can you file a follow up for it?

[W95Psp]

Oh, right! Sure, filed #223 :)

[franziskuskiefer]

@W95Psp this needs manual conflict resolution