Skip to content

Conversation

@mbbarbosa
Copy link
Contributor

Removed everything that depends on cost analysis.
This means that the theorem statements don't look so nice, because now one cannot use existential quantification over modules and all simulators are concrete.
Still, it is an interesting example of how UC execution model can look in EC.

I also touched the theories/algebra/DynMatrix.eca file due to smt instability.

@mbbarbosa
Copy link
Contributor Author

Can't replicate that smt failure for theories/algebra/DynMatrix.eca in my machine.

@fdupress
Copy link
Member

Are you running with z3 4.8 and cvc5 whatever version is in the docker container?

@alleystoughton
Copy link
Member

Looks good to me, Manuel. I didn't run into the SMT issue on my machine, either. Was there anything in particular you wanted my input on?

@alleystoughton
Copy link
Member

Looks good to me, Manuel. I didn't run into the SMT issue on my machine, either. Was there anything in particular you wanted my input on?

$ z3 --version
Z3 version 4.15.3 - 64 bit
$ alt-ergo --version
v2.6.2
$ cvc5 --version
This is cvc5 version 1.3.0 [git tag 1.3.0 branch HEAD]
compiled with GCC version Apple LLVM 15.0.0 (clang-1500.3.9.4)
on Jun 19 2025 00:32:01

@mbbarbosa
Copy link
Contributor Author

Looks good to me, Manuel. I didn't run into the SMT issue on my machine, either. Was there anything in particular you wanted my input on?

@alleystoughton thanks. I tagged you just to give you a thumbs up that I am starting again to think about this.
Also, at some point I'll probably take a look at EasyUC again to see how you state the various results looking for some inspiration.

@alleystoughton
Copy link
Member

Looks good to me, Manuel. I didn't run into the SMT issue on my machine, either. Was there anything in particular you wanted my input on?

@alleystoughton thanks. I tagged you just to give you a thumbs up that I am starting again to think about this. Also, at some point I'll probably take a look at EasyUC again to see how you state the various results looking for some inspiration.

We finally have proofs in EasyUC of both the UC composition and dummy adversary theorems (originally, we just had an instance of composition), our translator from the UC DSL into EC is complete, and we're just finishing the SMC example in this new form. Once we get things cleaned up and all on the main branch, I'll ping you.

Copy link
Member

@strub strub left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the example is recovered, it should be added to the CI.

@fdupress
Copy link
Member

If the example is recovered, it should be added to the CI.

It is in the standard examples run. See here, for example.

@strub
Copy link
Member

strub commented Oct 28, 2025

If the example is recovered, it should be added to the CI.

It is in the standard examples run. See here, for example.

Indeed. But note that we have a lot of disabled examples in examples/ 😄

@fdupress
Copy link
Member

fdupress commented Nov 4, 2025

@mbbarbosa Do you need one of us to split out the DynMatrix changes into their own PR?

@mbbarbosa
Copy link
Contributor Author

It is on my stack, but if you would like to pursue it independently, then I would appreciate the help.

@fdupress
Copy link
Member

fdupress commented Nov 5, 2025

It is on my stack, but if you would like to pursue it independently, then I would appreciate the help.

Cool. Let's communicate to avoid doing the work twice. I'll take the token for today. (But consider it released if nothing is pushed here by midnight.)

@fdupress
Copy link
Member

fdupress commented Nov 5, 2025

I managed to fat-finger my way through this on my phone on the way in. Let's let CI run, but this is ready to merge as soon as that succeeds. I'll change my review to an accept.

@fdupress fdupress self-requested a review November 5, 2025 09:30
@mbbarbosa
Copy link
Contributor Author

Thank you François

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants