We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 3b74196 commit bea7f9cCopy full SHA for bea7f9c
examples/MEE-CBC/RCPA_CMA.ec
@@ -336,7 +336,7 @@ theory EtM.
336
type leaks <- leaks,
337
op leak <- leak,
338
op dC (l:leaks) <- (dC l) `*` (MUnit.dunit witness<:tag>)
339
- proof * by smt.
+ proof * by smt(dC_ll dprod_ll dunit_ll).
340
341
(** The black-box construction is as follows **)
342
module EtM(E:SKEa.Enc_Scheme, M:MACa.MAC_Scheme): Enc_Scheme = {
0 commit comments