Search results

Port src/Bluebell/Logic/Ownership.lean to IndexedPSpPmRat

Status: Open.

#255 In Verified-zkEVM/iris-lean;

· pirapira opened on Dec 25, 2025

Port src/Bluebell/Logic/JointCondition.lean to IndexedPSpPmRat

Status: Open.

#254 In Verified-zkEVM/iris-lean;

· pirapira opened on Dec 25, 2025

Proof obligation for <code>wp_comp</code> in <code>src/Bluebell/Logic/WeakestPre.lean</code>

proof wanted

Status: Open.

#208 In Verified-zkEVM/iris-lean;

· alexanderlhicks opened on Sep 14, 2025

Proof obligation for <code>sep_of_and_assertTrue</code> in <code>src/Bluebell/Logic/Ownership.lean</code>

proof wanted

Status: Open.

#207 In Verified-zkEVM/iris-lean;

· alexanderlhicks opened on Sep 14, 2025

Proof obligation for <code>sampledFrom_prod</code> in <code>src/Bluebell/Logic/Ownership.lean</code>

proof wanted

Status: Open.

#206 In Verified-zkEVM/iris-lean;

· alexanderlhicks opened on Sep 14, 2025

Proof obligation for <code>sep_assertTrue_iff</code> in <code>src/Bluebell/Logic/Ownership.lean</code>

proof wanted

Status: Open.

#205 In Verified-zkEVM/iris-lean;

· alexanderlhicks opened on Sep 14, 2025

Proof obligation for <code>C_unit_left</code> in <code>src/Bluebell/Logic/JointCondition.lean</code>

proof wanted

Status: Open.

#204 In Verified-zkEVM/iris-lean;

· alexanderlhicks opened on Sep 14, 2025

Proof obligation for <code>C_wp_swap</code> in <code>src/Bluebell/Logic/WeakestPre.lean</code>

proof wanted

Status: Open.

#203 In Verified-zkEVM/iris-lean;

· alexanderlhicks opened on Sep 14, 2025

Proof obligation for <code>wp_conj</code> in <code>src/Bluebell/Logic/WeakestPre.lean</code>

proof wanted

Status: Open.

#202 In Verified-zkEVM/iris-lean;

· alexanderlhicks opened on Sep 14, 2025

Proof obligation for <code>C_and</code> in <code>src/Bluebell/Logic/JointCondition.lean</code>

proof wanted

Status: Open.

#200 In Verified-zkEVM/iris-lean;

· alexanderlhicks opened on Sep 14, 2025

Proof obligation for <code>sampledFrom_inj</code> in <code>src/Bluebell/Logic/Ownership.lean</code>

proof wanted

Status: Open.

#199 In Verified-zkEVM/iris-lean;

· alexanderlhicks opened on Sep 14, 2025

Proof obligation for <code>C_sep_assertTrue</code> in <code>src/Bluebell/Logic/JointCondition.lean</code>

proof wanted

Status: Open.

#198 In Verified-zkEVM/iris-lean;

· alexanderlhicks opened on Sep 14, 2025