New lemmas for stdlib

[namasikanam]

This is the first part of the auxiliary lemmas used in the oram proofs. My current plan is to create 5 PRs (~2k LoC) in total.

I will make sure all the proofs are either written by human, or first generated by LLM and then carefully edited step by step by myself.

[oskgo]

It seems like applying some_not_none is going to be no more helpful than destructuring the argument.

Some of the proofs for the option lemmas can also be significantly simplified by destructuring. omap_some_oget can be proven with just by case x.

[namasikanam]

It seems like applying some_not_none is going to be no more helpful than destructuring the argument.

Some of the proofs for the option lemmas can also be significantly simplified by destructuring. omap_some_oget can be proven with just by case x.

Thanks. This makes lots of sense. I feel that I learned the proper way of handling option. I removed the all lemmas related to option except the following one, which I feel useful and I hope it's also useful for others.

lemma oget_ext ['a] (x y : 'a option) :
     x <> None
  => y <> None
  => oget x = oget y
  => x = y.
proof. by case x; case y. qed.

[oskgo]

Had a look at the rest now.

[namasikanam]

@oskgo Thanks for your review. They make lots of sense to me and I learned something. I've resolved all your comments and updated my PR.

[namasikanam]

Hmmm...as now we strengthened two lemmas in stdlib, an external project (xmss) is broken. Shall I keep the original lemmas, rexpr_hmono_ltr and rexpr_hmono, or updated external projects which depend on these two lemmas?

[oskgo]

@namasikanam The external projects should be updated. I think @fdupress maintains xmss.

[fdupress]

I don't, but I keep it up to date.
I don't see the failure, though.

[namasikanam]

I don't, but I keep it up to date. I don't see the failure, though.

@fdupress You can see the failure through CI now.
https://github.com/EasyCrypt/easycrypt/actions/runs/27955903321/job/82726110975?pr=1053

I can also create a PR to XMSS by myself if you want.

[fdupress]

I don't, but I keep it up to date. I don't see the failure, though.

@fdupress You can see the failure through CI now. https://github.com/EasyCrypt/easycrypt/actions/runs/27955903321/job/82726110975?pr=1053

I can also create a PR to XMSS by myself if you want.

This is done. External CI works, but we'll need to synchronise the merging across the repos.

[fdupress]

Which we can't do because the local CI setup for the XMSS repo is still not fixed for compatibility with the external CI on breaking changes.

I'll reprioritise sorting this out.

[oskgo]

PR is good. Squash your commits and we'll be ready to merge once the CI issues with XMSS are sorted out.

[namasikanam]

PR is good. Squash your commits and we'll be ready to merge once the CI issues with XMSS are sorted out.

@oskgo Thanks. I separate commits intentionally so that the change of different theory falls into different commit. Can we keep the clean commits as they currently are?

[fdupress]

Do they pass CI individually? (Ignoring external CI, which shouldn't run in bisection anyway; and also obviously the single commit enforcement job.)

[namasikanam]

Do they pass CI individually? (Ignoring external CI, which shouldn't run in bisection anyway.)

Yes, they do. @fdupress

[fdupress]

Then I'll bypass the requirements when the time comes to merge. Make one PR per file in he future, so we don't need to make exceptions. Document dependencies between PRs by making sure they are made against the PR branch they need to follow.

[strub]

Then I'll bypass the requirements when the time comes to merge. Make one PR per file in he future, so we don't need to make exceptions. Document dependencies between PRs by making sure they are made against the PR branch they need to follow.

I'll change the CI so that a label triggers all PR commits check. Meanwhile, this PR is put on hold.