Merge pull request #1997 from AleoHQ/example-twoadicity

[examples] twoadicity: number of factors of two in field value

.circleci/test-examples.sh

@@ -66,4 +66,10 @@
 
   # Run the transfer program.
   $LEO run transfer
+)
+
+# Build and run the two-adicity program.
+(
+  cd ./project/examples/twoadicity || exit
+  $LEO run main
 )

examples/twoadicity/.gitignore

@@ -0,0 +1,2 @@
+outputs/
+build/

examples/twoadicity/README.md

@@ -0,0 +1,8 @@
+# src/twoadicity.leo
+
+## Build Guide
+
+To compile and run this Leo program, run:
+```bash
+leo run
+```

examples/twoadicity/inputs/twoadicity.in

@@ -0,0 +1,11 @@
+// The program input for twoadicity/src/main.leo
+[main]
+// Here is a made-up example.
+// public a: field = 391995973843653359517682711560178397928211734490775552field;
+// (comes from: 2field.pow(41) * 178259130663561045147472537592047227885001field)
+
+// This example is (maxfield - 1).
+// The output for this can be seen in the Pratt certificate
+// for bls12-377-scalar-field-prime
+// as the number of factors of 2 in (bls12-377-scalar-field-prime - 1).
+public a: field = 8444461749428370424248824938781546531375899335154063827935233455917409239040field;

examples/twoadicity/program.json

@@ -0,0 +1,10 @@
+{
+    "program": "twoadicity.aleo",
+    "version": "0.0.0",
+    "description": "",
+    "development": {
+        "private_key": "APrivateKey1zkp3JKK9YGWZYbPUVShFurexLMqRp1JHuvub9fnZwNW7XsW",
+        "address": "aleo1cagy225kufzj3fs2jvf8mk84dvx7umq53u4rana2ukp5d68kjy8s0t24sh"
+    },
+    "license": "MIT"
+}

examples/twoadicity/src/main.leo

@@ -0,0 +1,26 @@
+// The 'twoadicity' main function.
+@program
+function main(public n: field) -> u8 {
+  let remaining_n: field = n;
+  let powers_of_two: u8 = 0u8;
+  // Since field ints are 253 bits or fewer,
+  // any number in the field will have at most 252 powers of two in its prime factoring.
+  for i:u8 in 0u8..252u8 {
+    if is_even_and_nonzero(remaining_n) {
+      remaining_n = remaining_n / 2field;
+      powers_of_two = powers_of_two + 1u8;
+      }
+  }
+  return powers_of_two;
+}
+
+/* We define the is_even predicate on fields as follows.
+   If n is even and nonzero, clearly n/2 < n.
+   If n is odd, n-p is a field-equivalent negative number that is even,
+   and (n-p)/2 is a field-equivalent negative number closer to 0, greater than n-p.
+   If we add p to both of these negative numbers, we have
+   n/2 = (n-p)/2 + p = (n+p)/2 is greater than n and still less than p.
+*/
+function is_even_and_nonzero (n: field) -> bool {
+ return n / 2field < n;
+}