为何data_at_conflict需相同share？指针冲突证明与restrict规范疑问

当前证明上下文 #

...
  * data_at sha (tarray tulong 5) (map (fun x : Z => Vlong (Int64.repr x)) arra) a
  * data_at shb (tarray tulong 5) (map (fun x : Z => Vlong (Int64.repr x)) arrb) b
|-- !! (a <> b)

尝试的策略及报错 #

我使用了以下策略：

destruct (Val.eq a b) as [->|Hneq];[|entailer!].
data_at_conflict b.

但data_at_conflict b执行失败，报错：

Unable to unify "shb" with "sha".

疑问 #

• 为何证明别名指针指向分离块的矛盾需要share统一？
• 我是否误解了share的工作机制？
• 通常我会给每个只读指针分配独立的readable_share，同一内存块的不相交share是否会被视为分离？
• 为带有const和restrict参数的函数编写规范时，是否应该使用相同的share？

内容的提问来源于stack exchange，提问作者Russell O'Connor