[clementblaudeau]

Overview

This PR extends the support for rust written specs (via hax_lib annotations) by adding trait-level specs. On the lean side, traits definitions (represented as structures) get a companion "lawful" structure that states the properties. Downstream, callers rely on Lawful as an assumption, and each impl proves its own Lawful theorem.

Example

  #[hax_lib::attributes]
  trait Counter {
      #[requires(n < 100)]
      #[ensures(|res| res > n)]
      fn next(&self, n: u32) -> u32;
  }
 
  struct One;
 
  impl Counter for One {
      fn next(&self, n: u32) -> u32 {
          n + 1
      }
  }

  #[requires(n < 100)]
  #[ensures(|res| res > n)]
  fn step<C: Counter>(c: &C, n: u32) -> u32 {
      c.next(n)
  }

Trait contract (Specs.lean): the conditions become pre/post functions, and the Lawful structure says that every implementation satisfies them.

  -- Specs.lean
  @[reducible]
  def Counter.next.pre {Self_ : Type} (CounterInst : Counter Self_) (self_ : Self_) (n : Std.U32) : RustM Bool := do
    ok (n < 100#u32)

  @[reducible]
  def Counter.next.post {Self_ : Type} (CounterInst : Counter Self_) (self_ : Self_) (n : Std.U32) (res : Std.U32) : RustM Bool := do
    ok (res > n)

  structure Counter.Lawful (Self : Type) (CounterInst : Counter Self) : Prop where
    next_spec (self_ : Self) (n : Std.U32) :
      (Counter.next.pre CounterInst self_ n).holds →
      ⦃ ⌜ True ⌝ ⦄
      CounterInst.next self_ n
      ⦃ ⇓ res => ⌜ (Counter.next.post CounterInst self_ n res).holds ⌝ ⦄

  def step.spec {C : Type} (CounterInst : Counter C) (c : C) (n : Std.U32)
    (CounterInstLawful : Counter.Lawful C CounterInst) : Prop :=
    (step.pre CounterInst c n).holds →
    ⦃ ⌜ True ⌝ ⦄
    step CounterInst c n
    ⦃ ⇓ res => ⌜ (step.post CounterInst c n res).holds ⌝ ⦄

  -- Proof obligations 
  theorem One.Insts.Hax_testsSpecsTraitsDoc_exampleCounter.Lawful :
    Counter.Lawful One One.Insts.Hax_testsSpecsTraitsDoc_exampleCounter
    := by sorry
  
  theorem step.spec.proof {C : Type} (CounterInst : Counter C) (c : C) (n : Std.U32)
    (CounterInstLawful : Counter.Lawful C CounterInst) :
    step.spec CounterInst c n CounterInstLawful
    := by sorry

Review

The detailed documentation is in documentation/hax-specs.md. A large chunk of the diff comes from test files and lean output. The changes to the ml engine are somewhat small and contained.