Automatically modeling swap participation

aterga · July 16, 2024, 4:31pm

While thinking about how to generate optimal testing scenarios for SNS swaps, I wrote a little SMT model that seems to work quite well with the Z3 SMT solver. It allows automatically generating participations that satisfy a bunch of constraints.

Sharing the model in case it might be useful for others.

gist.github.com

https://gist.github.com/aterga/be7e3a81004b452cf09a7c3b2c1e0d76

model-sns-swap-participations.smt2

(define-fun e8s ((x Int)) Int (* x 100000000))

; Example values based on parameterf from here:
; https://nns.ic0.app/proposal/?u=qoctq-giaaa-aaaaa-aaaea-cai&proposal=131075
(define-const minimum_participants Int 50)
(define-const minimum_direct_participation_icp Int (e8s 50000))
(define-const maximum_direct_participation_icp Int (e8s 250000))
(define-const minimum_participant_icp Int (e8s 10))
(define-const maximum_participant_icp Int (e8s 50000))

This file has been truncated. show original

Questions and suggestion are welcome!

Topic		Replies	Views
Swaps to allow at most 100K SNS neurons for direct participants Developers sns	0	115	July 15, 2024
Questions about SNS SNS Project Governance	6	242	April 30, 2024
Restriction for SNS swap participation - Design Governance sns	10	1292	July 4, 2023
SNS.yaml: invalid minimim and maximum ICP fields naming? SNS Project Governance	3	95	July 8, 2024
SNS Swap "Aborted" locally SNS Project Governance	7	46	July 15, 2024

Automatically modeling swap participation

Related Topics