Can this extern definition be used to prove False?

Stream: lean4

[François G. Dorais]

I'm currently using this definition in some personal projects but I always mark it unsafe (which is fine for my purposes) but I realized I could make it into a plain safe definition with no harm to my code. Is there potential harm in marking it safe?

/-- Returns the first input but forces the compiler to evaluate the second input. -/
@[never_extract, extern c inline "#3"]
def withEffects {α : Type _} {β : Type _} (a : α) (b : @& β) : α := a

theorem withEffects_def {α : Type _} {β : Type _} (a : α) (b : β) :
  withEffects a b = a := by rfl

The idea is that withEffects forces the compiler to evaluate b and then returns a unchanged, this is because the compiler doesn't know b isn't used because of the extern so it thinks a might be changed. (This is true if evaluating b has effects on a, as is possible in unsafe code.) When pressed, the kernel doesn't care much, it thinks that withEffects a is just a. The weird thing is that the kernel is correct: withEffects a is really just a!

Can withEffects be used in nefarious ways to make the kernel prove False?

[François G. Dorais]

Part of me says no because, in a safe context, b is pure and can't actually have effects so forcing evaluation is meaningless. But I'm still skeptical...

[Jason Rute]

When you talk about the kernel being able to prove False, do you mean using native_decide or similar? Because if you mean with just the usual three axioms, that would be really bad, right?

[Jason Rute]

And hence seems very doubtful this would be a soundness issue, right?

[François G. Dorais]

Using native_decide or similar would be necessary here since it's about an extern definition. These are invisible to the kernel without such trickery.

[Jason Rute]

I'm probably misunderstanding, but if this is external, doesn't that already allow it to prove False (again, using native_decide which we already know is unsound)? Just give an external implementation which doesn't match the Lean definition, right?

[Jason Rute]

Oh I see. extern c inline "#3" doesn't associate this function with another (arbitrary) external function, but somehow converts it into an external C function.

[François G. Dorais]

Yes, the extern c inline "#3" just makes the compiler spit out a but the compiler can't inspect this extern so it assumes that b (the effect) is actually used even though the result is just a.

[Robin Arnez]

I'm pretty sure your definition is effectively equivalent to the following:

@[never_extract, noinline]
def withEffects {α : Type _} {β : Type _} (a : α) (b : @& β) : α :=
  destruct (a, b)
where
  @[noinline]
  destruct (x : α × β) : α := x.1

theorem withEffects_def {α : Type _} {β : Type _} (a : α) (b : β) :
  withEffects a b = a := by rfl

A regular non-unsafe definition shouldn't have any soundness concerns so anything equivalent to it should not be much different.