coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A question regarding Coq rational arithmetic

From: Milad Ketabii <ketabii.math AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] A question regarding Coq rational arithmetic
Date: Thu, 23 Mar 2017 11:04:38 +1100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ketabii.math AT gmail.com; spf=Pass smtp.mailfrom=ketabii.math AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f44.google.com
Ironport-phdr: 9a23:Nb2v8haQQwOcNec/iOOSj/r/LSx+4OfEezUN459isYplN5qZpsu+bnLW6fgltlLVR4KTs6sC0LuL9f+6EjdaqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2a3IyL0LW5/ISWaAFVjhK8Z6lzJVO4t1b/rM4T1K5jLq89gjjEvnJCeuUekWBlOVuZnhe6486s/LZs9i1Rv7Qq8MsWAvayRLgxUbENVGduCGsy/sC+7RQ=

Good Day

We're using coq libraries for rational arithmetic to formalize some electronic voting schemes, and then extract in Haskell to actually do the counting for a real election. Our extracted code in Haskell works fine for up tp 68 number of votes. However, when we go for 69 (or above) the program does not terminate!

When we do profiling, there is nothing strange with respect to memory consumption or time for numbers below 69. However, there is a function "add" from library "BinPos" for adding two Positives, which takes up to 70% of the memory. It seems this function is the culprit, but such behaviour is weird. Has anyone ever encountered something similar with Coq rational arithmetic before? Any suggestion is welcome.

Best

Milad

[Coq-Club] A question regarding Coq rational arithmetic, Milad Ketabii, 03/23/2017
- Re: [Coq-Club] A question regarding Coq rational arithmetic, Abhishek Anand, 03/23/2017
- Re: [Coq-Club] A question regarding Coq rational arithmetic, Laurent Thery, 03/23/2017