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
Reduce number of participants when testing SNS in local testing environment SNS Project Governance nns , sns	5	54	November 2, 2024
Swaps to allow at most 100K SNS neurons for direct participants Developers sns	1	209	September 28, 2024
Questions about SNS SNS Project Governance	6	242	April 30, 2024
Restriction for SNS swap participation - Design Governance sns	10	1305	July 4, 2023
SNS.yaml: invalid minimim and maximum ICP fields naming? SNS Project Governance	3	97	July 8, 2024

Automatically modeling swap participation

Related topics