Open TWal opened 5 days ago
Currently, some amount of boilerplate is needed to merge local predicates, and prove that the global predicate contains all local predicates:
https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/297eeb761f0c070064092f58bd5e34595f6fb72d/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst#L110-L123
The boilerplate is linear in the number of local predicates, there is no reason that this shouldn't be doable in constant size? For example using a meta-program?
Currently, some amount of boilerplate is needed to merge local predicates, and prove that the global predicate contains all local predicates:
https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/297eeb761f0c070064092f58bd5e34595f6fb72d/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst#L110-L123
The boilerplate is linear in the number of local predicates, there is no reason that this shouldn't be doable in constant size? For example using a meta-program?