Prove allocator axioms (dlmalloc, Vec::new, dealloc)

[Isabelle9999]

Three axioms in the merge-sort proof #157 follow the standard convention of axiomatizing unverified C library code (same pattern as Iris-MSWasm's wp_segalloc, CompCert's malloc spec):

• dlmalloc_alloc_spec — malloc wrapper
• func2_vec_init — Vec::new (calls malloc internally)
• func4_dealloc — free/dealloc

These are currently in codelib/CodeLib/SepLogic/AllocSpec.lean.

Eventually these should be replaced with theorems that verify
the actual dlmalloc implementation. This requires stepping through
the compiled C allocator code .

[alexoltean61]

Hi, I got here through the hiring page. Interesting project!

I'd love to contribute to this issue, but it seems to me that dlmalloc_alloc_spec is unsound as stated. It is universally over modules, yet it assumes the existence of a function at index 5. As is, this assumption can be easily falsified, leading to to a Lean proof of False (which is not great 😅).

I'd be inclined to assume the universally quantified m : Module was a typo, and it should instead have referred to the «module» declaration in MergeSort/Program.lean. Is this correct?

Proof of False is below (you will need to import Aesop).

theorem dlmalloc_unsound : False := by
  let env : HostEnv Unit := {}
  let m : Module := { funcs := [] }
  let st : Store Unit :=
    { globals := { }, mem := { pages := 17, bytes := fun _ => 0 }, host := () }
  obtain ⟨N, alloc_spec⟩ := dlmalloc_alloc_spec env m st 0 (by aesop) (by aesop)
  specialize alloc_spec (N+1) (by aesop)
  obtain ⟨vs, st', alloc_spec⟩ := alloc_spec
  simp [run, m] at alloc_spec

[Isabelle9999]

Hi, I got here through the hiring page. Interesting project!

I'd love to contribute to this issue, but it seems to me that dlmalloc_alloc_spec is unsound as stated. It is universally over modules, yet it assumes the existence of a function at index 5. As is, this assumption can be easily falsified, leading to to a Lean proof of False (which is not great 😅).

I'd be inclined to assume the universally quantified m : Module was a typo, and it should instead have referred to the «module» declaration in MergeSort/Program.lean. Is this correct?

Proof of False is below (you will need to import Aesop).

theorem dlmalloc_unsound : False := by
let env : HostEnv Unit := {}
let m : Module := { funcs := [] }
let st : Store Unit :=
{ globals := { }, mem := { pages := 17, bytes := fun _ => 0 }, host := () }
obtain ⟨N, alloc_spec⟩ := dlmalloc_alloc_spec env m st 0 (by aesop) (by aesop)
specialize alloc_spec (N+1) (by aesop)
obtain ⟨vs, st', alloc_spec⟩ := alloc_spec
simp [run, m] at alloc_spec

Yes you're right thanks for catching this, I fixed it by replacing m : Module with the concrete «module»

[mfornet]

Hi @alexoltean61 thanks for the interest of the project, I'm on the process of rewriting large part of the interpreter to use iris-lean instead. We will need a similar proof once that landed, my main concern is that if you start working on this now, we will end up discarding most of your work once the new system is in place.

[mfornet]

@Isabelle9999 thinking about the creation of this axiom: rather than creating a new axiom we can put this as a hypothesis in the spec, and any dependant on this spec will need to have a similar hypothesis. This gives you similar flexibility but avoids having this axiom global wide in the project.

[Isabelle9999]

that's much more clean, I converted all axioms to hypothesis, func2_vec_init (Vec::with_capacity) and func4_dealloc (Vec dealloc) are now Func2VecInitSpec and Func4DeallocSpec as prop defs.

Traced all dependents: func1_terminates calls both, merge_sort_correct calls func1_terminates. Both now take (hvec_init : Func2VecInitSpec) (hdealloc : Func4DeallocSpec) as parameters, with call sites updated accordingly. Also moved AllocSpec.lean from codelib to the MergeSort since it references the concrete module.

(run_env_indep axiom is kept temporarily until it's rebased onto main, was proved and merged)