Cleanup ZVP notebook.

1 files changed, 132 insertions, 264 deletions

diff --git a/re/zvp.ipynb b/re/zvp.ipynb
index 2b8c738..6e81f1c 100644
--- a/re/zvp.ipynb
+++ b/re/zvp.ipynb
@@ -16,7 +16,7 @@
    "outputs": [],
    "source": [
     "import io\n",
-    "import sympy\n",
+    "import numpy as np\n",
     "from sympy import FF, sympify, symbols, Poly, Monomial\n",
     "from collections import Counter\n",
     "import tabulate\n",
@@ -51,8 +51,18 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "# TODO: Maybe combine with EPA?\n",
-    "# TODO: Maybe extend oracle with number or position?"
+    "# TODO: Maybe combine with EPA?"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "faca31e8-fe51-4017-a41d-ba31b15c548d",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "model = ShortWeierstrassModel()\n",
+    "coordsaff = AffineCoordinateModel(model)"
    ]
   },
   {
@@ -71,8 +81,6 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "model = ShortWeierstrassModel()\n",
-    "coordsaff = AffineCoordinateModel(model)\n",
     "which = \"jacobian\"\n",
     "coords = model.coordinates[which]"
    ]
@@ -118,6 +126,14 @@
    ]
   },
   {
+   "cell_type": "markdown",
+   "id": "0bcc8b9e-39ad-4b53-8f45-a7552b05baa2",
+   "metadata": {},
+   "source": [
+    "The result is a Point with coordinates that are polynomials in the input coordinates and curve parameters."
+   ]
+  },
+  {
    "cell_type": "code",
    "execution_count": null,
    "id": "d8ea0c4d-86e1-46af-ac20-569e6ef5439d",
@@ -134,7 +150,7 @@
    "metadata": {},
    "source": [
     "## Reverse-engineering\n",
-    "Now, lets look at using the ZVP attack for reverse-engineering. First pick 10 random curves and one curve with `a = 0`. These curves are not special in any way and just serve to randomize the process, as the existence of ZVP points for a given intermediate value polynomial depends on the curve."
+    "Now, lets look at using the ZVP attack for reverse-engineering. First pick 10 random curves, some with $a \\in \\{0, -1, -3 \\}$. The randomcurves are not special in any way and just serve to randomize the process, as the existence of ZVP points for a given intermediate value polynomial depends on the curve."
    ]
   },
   {
@@ -145,6 +161,7 @@
    "outputs": [],
    "source": [
     "curves = list(map(lambda spec: load_params_ecgen(io.BytesIO(spec.encode()), \"affine\"), [\n",
+    "    # Random (*10)\n",
     "    \"\"\"[{\"field\":{\"p\":\"0xa7ec3617d4166b2d\"},\"a\":\"0x372994d9d680a83b\",\"b\":\"0xa0a2bf719d8e68c5\",\"order\":\"0xa7ec3618be1dab55\",\"subgroups\":[{\"x\":\"0x1ef15756946a5b6d\",\"y\":\"0x2ca9658f7ab9a558\",\"order\":\"0xa7ec3618be1dab55\",\"cofactor\":\"0x1\",\"points\":[{\"x\":\"0x1ef15756946a5b6d\",\"y\":\"0x2ca9658f7ab9a558\",\"order\":\"0xa7ec3618be1dab55\"}]}]}]\"\"\",\n",
     "    \"\"\"[{\"field\":{\"p\":\"0xa42c1467a1ed04f3\"},\"a\":\"0x55d07340a4572f2d\",\"b\":\"0x0a938c37dfb0b6d5\",\"order\":\"0xa42c14689284d3a7\",\"subgroups\":[{\"x\":\"0x8633981c83ed43a2\",\"y\":\"0x7b5374e9d7997199\",\"order\":\"0xa42c14689284d3a7\",\"cofactor\":\"0x1\",\"points\":[{\"x\":\"0x8633981c83ed43a2\",\"y\":\"0x7b5374e9d7997199\",\"order\":\"0xa42c14689284d3a7\"}]}]}]\"\"\",\n",
     "    \"\"\"[{\"field\":{\"p\":\"0xea0d9cead19016ab\"},\"a\":\"0xcbbfe501c4ef6d92\",\"b\":\"0x5762de777a6d9178\",\"order\":\"0xea0d9cea8cd2c857\",\"subgroups\":[{\"x\":\"0xe7daa3e061c3111b\",\"y\":\"0x56ee59a6845c5e93\",\"order\":\"0xea0d9cea8cd2c857\",\"cofactor\":\"0x1\",\"points\":[{\"x\":\"0xe7daa3e061c3111b\",\"y\":\"0x56ee59a6845c5e93\",\"order\":\"0xea0d9cea8cd2c857\"}]}]}]\"\"\",\n",
@@ -155,9 +172,13 @@
     "    \"\"\"[{\"field\":{\"p\":\"0xd47ec1d03a62686d\"},\"a\":\"0xd00a3ee0f5c86b02\",\"b\":\"0x457a5b6c47db38d8\",\"order\":\"0xd47ec1d107db7d6f\",\"subgroups\":[{\"x\":\"0x41ebc3b763f3cd1b\",\"y\":\"0x3d6925f214620e0c\",\"order\":\"0xd47ec1d107db7d6f\",\"cofactor\":\"0x1\",\"points\":[{\"x\":\"0x41ebc3b763f3cd1b\",\"y\":\"0x3d6925f214620e0c\",\"order\":\"0xd47ec1d107db7d6f\"}]}]}]\"\"\",\n",
     "    \"\"\"[{\"field\":{\"p\":\"0xb1c9115c6f40d755\"},\"a\":\"0x79d3ceefafc44ce9\",\"b\":\"0x8316af84264df42b\",\"order\":\"0xb1c9115d17f84a45\",\"subgroups\":[{\"x\":\"0x8b0a274089b53fe5\",\"y\":\"0x3508d33c4beba5ad\",\"order\":\"0xb1c9115d17f84a45\",\"cofactor\":\"0x1\",\"points\":[{\"x\":\"0x8b0a274089b53fe5\",\"y\":\"0x3508d33c4beba5ad\",\"order\":\"0xb1c9115d17f84a45\"}]}]}]\"\"\",\n",
     "    \"\"\"[{\"field\":{\"p\":\"0x8f738fda18cd5dff\"},\"a\":\"0x4747f2f9b8628cbf\",\"b\":\"0x586cdb9378a1389f\",\"order\":\"0x8f738fd8fc7ebed3\",\"subgroups\":[{\"x\":\"0x7ad306c73b64c1b5\",\"y\":\"0x69e3ca555190da4b\",\"order\":\"0x8f738fd8fc7ebed3\",\"cofactor\":\"0x1\",\"points\":[{\"x\":\"0x7ad306c73b64c1b5\",\"y\":\"0x69e3ca555190da4b\",\"order\":\"0x8f738fd8fc7ebed3\"}]}]}]\"\"\",\n",
+    "    # a = -1\n",
     "    \"\"\"[{\"field\":{\"p\":\"0xcfef393139c3007f\"},\"a\":\"0xcfef393139c3007e\",\"b\":\"0x950312812acb155f\",\"order\":\"0xcfef39320179387b\",\"subgroups\":[{\"x\":\"0xae2d2f58ca5b5cf7\",\"y\":\"0xc3a4bf3a1dc10005\",\"order\":\"0xcfef39320179387b\",\"cofactor\":\"0x1\",\"points\":[{\"x\":\"0xae2d2f58ca5b5cf7\",\"y\":\"0xc3a4bf3a1dc10005\",\"order\":\"0xcfef39320179387b\"}]}]}]\"\"\",\n",
+    "    # a = -3\n",
     "    \"\"\"[{\"field\":{\"p\":\"0x8d79ca36cee026a7\"},\"a\":\"0x8d79ca36cee026a4\",\"b\":\"0x0478c1f80ce2c9c6\",\"order\":\"0x8d79ca35a428c76f\",\"subgroups\":[{\"x\":\"0x2e94a3e38f8b345e\",\"y\":\"0x83e6c6f0cb8f69c4\",\"order\":\"0x8d79ca35a428c76f\",\"cofactor\":\"0x1\",\"points\":[{\"x\":\"0x2e94a3e38f8b345e\",\"y\":\"0x83e6c6f0cb8f69c4\",\"order\":\"0x8d79ca35a428c76f\"}]}]}]\"\"\",\n",
+    "    # a = 0\n",
     "    \"\"\"[{\"field\":{\"p\":\"0xceaf446a53f14bc1\"},\"a\":\"0x0000000000000000\",\"b\":\"0x326539376260f173\",\"order\":\"0xceaf446aae275419\",\"subgroups\":[{\"x\":\"0x98fe44948c3f8678\",\"y\":\"0x3d440ee959a912d7\",\"order\":\"0xceaf446aae275419\",\"cofactor\":\"0x1\",\"points\":[{\"x\":\"0x98fe44948c3f8678\",\"y\":\"0x3d440ee959a912d7\",\"order\":\"0xceaf446aae275419\"}]}]}]\"\"\",\n",
+    "    # b = 0 (causes more issues than gain)\n",
     "    #\"\"\"[{\"field\":{\"p\":\"0x9d9119957f02fe3f\"},\"a\":\"0x0106903196d88df9\",\"b\":\"0x0000000000000000\",\"order\":\"0x9d9119957f02fe40\",\"subgroups\":[{\"x\":\"0x191a36b9cd81de96\",\"y\":\"0x10f2c6bded391aa9\",\"order\":\"0x9d9119957f02fe40\",\"cofactor\":\"0x1\",\"points\":[{\"x\":\"0x0000000000000000\",\"y\":\"0x0000000000000000\",\"order\":\"0x2\"},{\"x\":\"0x95913fae9065da0f\",\"y\":\"0x5eeddeee7152d6fb\",\"order\":\"0x276446655fc0bf9\"}]}]}]\"\"\"\n",
     "]))"
    ]
@@ -167,7 +188,7 @@
    "id": "4276de4c-78f4-4cdb-b60e-8c24eabfa00d",
    "metadata": {},
    "source": [
-    "First lets fix a scalar, go over the curves and compute the addition chain to obtain information about which multiples of the input point will go into the formulas."
+    "First lets fix some scalars, go over the curves and compute the addition chain to obtain information about which multiples of the input point will go into the formulas."
    ]
   },
   {
@@ -180,9 +201,11 @@
     "scalars = [123456789, 98765432, 0b10000000, 0b1010101010, 0b1010101, 77777, 66666, 55555, 44444, 33333, 22222, 11111, 0b1111111111]\n",
     "\n",
     "chains = []\n",
+    "scalar_map = {}\n",
     "for i, (scalar, params) in enumerate(zip(scalars, curves)):\n",
     "    chain = addition_chain(scalar, params, LTRMultiplier, lambda add,dbl: LTRMultiplier(add, dbl, None, False, AccumulationOrder.PeqRP, True, True))\n",
-    "    chains.append(chain)"
+    "    chains.append(chain)\n",
+    "    scalar_map[params] = scalar"
    ]
   },
   {
@@ -200,12 +223,14 @@
    "metadata": {},
    "outputs": [],
    "source": [
+    "# bound is the maximal dlog in the hard case of the DCP to be solved\n",
     "bound = 15\n",
-    "chain_bound = 10\n",
+    "# chain_bound is the number of formula applications at the start of the addition chain that is processed\n",
+    "chain_bound = 30\n",
     "\n",
     "formula_classes = [AdditionFormula, DoublingFormula]\n",
     "point_chains = {}\n",
-    "with ProcessPoolExecutor(max_workers=14) as pool:\n",
+    "with ProcessPoolExecutor(max_workers=30) as pool:\n",
     "    futures = []\n",
     "    args = []\n",
     "    for coord_name, coords in model.coordinates.items():\n",
@@ -214,16 +239,15 @@
     "                params = affine_params.to_coords(coords)\n",
     "            except UnsatisfiedAssumptionError:\n",
     "                continue\n",
-    "            formula_groups = [list(filter(lambda formula: isinstance(formula, formula_class), coords.formulas.values())) for formula_class in formula_classes]\n",
+    "            formula_groups = [list(filter(lambda formula: isinstance(formula, formula_class) and (formula.name.startswith(\"add\") or formula.name.startswith(\"dbl\")), coords.formulas.values())) for formula_class in formula_classes]\n",
     "\n",
     "            for formula_group, formula_class in zip(formula_groups, formula_classes):\n",
     "                for formula in formula_group:\n",
-    "                    futures.append(pool.submit(precomp_zvp_points, chain[:chain_bound], {formula_class.shortname: formula}, params, bound))\n",
+    "                    futures.append(pool.submit(precomp_zvp_points, chain[:chain_bound], {formula_class.shortname: formula}, params, bound, filter_nonhomo=False))\n",
     "                    args.append((coords, formula, affine_params))\n",
     "    for future in tqdm(as_completed(futures), desc=\"Compute\", total=len(futures)):\n",
     "        j = futures.index(future)\n",
-    "        point_chains[args[j]] = future.result()\n",
-    "            "
+    "        point_chains[args[j]] = future.result()"
    ]
   },
   {
@@ -253,6 +277,9 @@
     "                    params = affine_params.to_coords(coords)\n",
     "                except UnsatisfiedAssumptionError:\n",
     "                    continue\n",
+    "                if (coords, formula, affine_params) not in point_chains:\n",
+    "                    print(f\"Missing {formula}\")\n",
+    "                    continue\n",
     "                point_chain = point_chains[(coords, formula, affine_params)]\n",
     "                for step in point_chain:\n",
     "                    for poly, poly_points in step.items():\n",
@@ -288,23 +315,39 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "def print_leaf_sizes(tree):\n",
-    "    leaf_sizes = [len(leaf.cfgs) for leaf in tree.leaves]\n",
-    "    print(sorted(leaf_sizes))\n",
+    "def render_tree(tree):\n",
+    "    print(RenderTree(tree).by_attr(lambda n: n.name if n.name is not None else \"\\n\".join((\", \".join(str(formula) for formula in cfg) for cfg in n.cfgs))))\n",
     "\n",
-    "print_leaf_sizes(tree)"
+    "def describe_tree(tree):\n",
+    "    leaf_sizes = [len(leaf.cfgs) for leaf in tree.leaves]\n",
+    "    print(f\"Total cfgs: {len(tree.cfgs)}\")\n",
+    "    print(f\"Depth: {tree.height}\")\n",
+    "    print(f\"Leaf sizes: {sorted(leaf_sizes)}\")\n",
+    "    print(f\"Average leaf size: {np.mean(leaf_sizes):.3}\")\n",
+    "    leafs = sum(([size] * size for size in leaf_sizes), [])\n",
+    "    print(f\"Mean result size: {np.mean(leafs):.3}\")"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
    "id": "ab09b767-71ca-4d28-abf0-532307efefbd",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "describe_tree(tree)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "1a779729-380a-4e41-b35e-4afa0943e550",
    "metadata": {
     "scrolled": true
    },
    "outputs": [],
    "source": [
-    "print(RenderTree(tree).by_attr(lambda n: n.name if n.name is not None else \"\\n\".join((\", \".join(str(formula) for formula in cfg) for cfg in n.cfgs))))"
+    "render_tree(tree)"
    ]
   },
   {
@@ -312,7 +355,11 @@
    "id": "ed2d4b51-573f-4fef-b1a4-d30b3be07423",
    "metadata": {},
    "source": [
-    "Our ZVP points might (due to the bounds above thus the incompleteness of our analysis) lead to more zeros than we attribute to then (in more configurations), thus we perform a remapping step where we execute the scalar multiplication with given points and trace whether they introduce the zeros. This gives us a new distinguishing map `remapped_point_map`, now without \"false negatives\"."
+    "Our ZVP points might (due to the bounds above thus the incompleteness of our analysis) lead to more zeros than we attribute to them (in more configurations), i.e. \"false negatives\". They might also be erroneous and not lead to zeros if the argument `filter_nonhomo` is False, as non-homogenous intermediate polynomials are not filtered out of the analysis. They introduce \"false positives\" but also some true positives.\n",
+    "\n",
+    "Thus we perform a remapping step where we execute the scalar multiplication with given points and trace whether they introduce the zeros. This gives us a new distinguishing map `remapped_hit_point_map`, now without \"false negatives\" or \"false positives\".\n",
+    "\n",
+    "Note that we also construct two additional maps `remapped_count_point_map` and `remapped_position_point_map` which represent the results of remapping using an oracle counting the zeros and an oracle giving the positions of the zeros in the computation, respectively."
    ]
   },
   {
@@ -322,9 +369,12 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "def remap(coords, formulas, points, scalar):\n",
+    "def remap(coords, formulas, points, scalar_map):\n",
     "    mult = LTRMultiplier(*formulas, None, False, AccumulationOrder.PeqRP, True, True)\n",
-    "    new_points = set()\n",
+    "    hit_points = set()\n",
+    "    count_points = set()\n",
+    "    position_points = set()\n",
+    "    \n",
     "    param_map = {}\n",
     "    for point, params in tqdm(points):\n",
     "        if params not in param_map:\n",
@@ -336,6 +386,7 @@
     "        elif param_map[params] is None:\n",
     "            continue\n",
     "        mult.init(param_map[params], point.to_model(param_map[params].curve.coordinate_model, param_map[params].curve))\n",
+    "        scalar = scalar_map[params]\n",
     "        with local(DefaultContext()) as ctx:\n",
     "            try:\n",
     "                mult.multiply(scalar)\n",
@@ -347,28 +398,33 @@
     "                for intermediate in action.op_results:\n",
     "                    trace.append(intermediate.value)\n",
     "        ctx.actions.walk(callback)\n",
-    "        hit_zero = any(int(value) == 0 for value in trace)\n",
-    "        if hit_zero:\n",
-    "            new_points.add((point, params))\n",
-    "    return new_points\n",
+    "        zeros = tuple(map(lambda x: int(x) == 0, trace))\n",
+    "        if any(zeros):\n",
+    "            hit_points.add((point, params))\n",
+    "            count_points.add((point, sum(zeros), params))\n",
+    "            position_points.add((point, zeros, params))\n",
+    "    return hit_points, count_points, position_points\n",
     "\n",
-    "remapped_point_map = {}\n",
-    "with ProcessPoolExecutor(max_workers=12) as pool:\n",
+    "remapped_hit_point_map = {}\n",
+    "remapped_count_point_map = {}\n",
+    "remapped_position_point_map = {}\n",
+    "with ProcessPoolExecutor(max_workers=30) as pool:\n",
     "    futures = []\n",
     "    pairs = []\n",
     "    for coord_name, coords in model.coordinates.items():\n",
     "        formula_groups = [list(filter(lambda formula: isinstance(formula, formula_class) and (formula.name.startswith(\"add\") or formula.name.startswith(\"dbl\")), coords.formulas.values())) for formula_class in formula_classes]\n",
     "        formula_combinations = list(product(*formula_groups))\n",
     "        for formulas in formula_combinations:\n",
-    "            #remap(coords, formulas, all_points, scalar)\n",
-    "            #break\n",
-    "            futures.append(pool.submit(remap, coords, formulas, all_points, scalar))\n",
+    "            futures.append(pool.submit(remap, coords, formulas, all_points, scalar_map))\n",
     "            pairs.append(formulas)\n",
-    "        #break\n",
     "    results = [None for _ in futures]\n",
-    "    for future in tqdm(as_completed(futures), total=len(futures), desc=\"Remap\"):\n",
+    "    for future in tqdm(as_completed(futures), total=len(futures), desc=\"Remapping\"):\n",
     "        j = futures.index(future)\n",
-    "        remapped_point_map[pairs[j]] = future.result()"
+    "        cfg = pairs[j]\n",
+    "        h, c, p = future.result()\n",
+    "        remapped_hit_point_map[cfg] = h \n",
+    "        remapped_count_point_map[cfg] = c\n",
+    "        remapped_position_point_map[cfg] = p"
    ]
   },
   {
@@ -383,21 +439,18 @@
    "cell_type": "code",
    "execution_count": null,
    "id": "cc87dfd1-f058-4338-aaca-fc05105fc9f1",
-   "metadata": {
-    "scrolled": true
-   },
+   "metadata": {},
    "outputs": [],
    "source": [
+    "table = [[\"Add\", \"Dbl\", \"raw\", \"remapped\", \"removed\", \"new\"]]\n",
     "for pair in point_map.keys():\n",
-    "    print(pair[0], pair[1],\n",
+    "    table.append((pair[0], pair[1],\n",
     "          len(point_map[pair]),\n",
-    "          len(remapped_point_map[pair]),\n",
-    "          -len(point_map[pair].difference(remapped_point_map[pair])),\n",
-    "          len(remapped_point_map[pair].difference(point_map[pair])))\n",
-    "    #crvs = set()\n",
-    "    #for point, params in remapped_point_map[pair].difference(point_map[pair]):\n",
-    "    #    crvs.add(params)\n",
-    "    #print(repr(crvs))"
+    "          len(remapped_hit_point_map[pair]),\n",
+    "          -len(point_map[pair].difference(remapped_hit_point_map[pair])),\n",
+    "          len(remapped_hit_point_map[pair].difference(point_map[pair]))))\n",
+    "\n",
+    "display(HTML(tabulate.tabulate(table, tablefmt=\"html\", headers=\"firstrow\")))"
    ]
   },
   {
@@ -415,178 +468,59 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "remapped_tree = build_distinguishing_tree(set(remapped_point_map.keys()), remapped_point_map)\n",
-    "print_leaf_sizes(remapped_tree)"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "5d2bbf5b-76e6-4137-9c32-cbd09a5c3600",
-   "metadata": {
-    "scrolled": true
-   },
-   "outputs": [],
-   "source": [
-    "print(RenderTree(remapped_tree).by_attr(lambda n: n.name if n.name is not None else \"\\n\".join((\", \".join(str(formula) for formula in cfg) for cfg in n.cfgs))))"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "3ea9912e",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "def remap(coords, formulas, points, scalar):\n",
-    "    mult = LTRMultiplier(*formulas, None, False, AccumulationOrder.PeqRP, True, True)\n",
-    "    new_points = set()\n",
-    "    param_map = {}\n",
-    "    for point, params in tqdm(points):\n",
-    "        if params not in param_map:\n",
-    "            try:\n",
-    "                param_map[params] = params.to_coords(coords)\n",
-    "            except UnsatisfiedAssumptionError:\n",
-    "                param_map[params] = None\n",
-    "                continue\n",
-    "        elif param_map[params] is None:\n",
-    "            continue\n",
-    "        mult.init(param_map[params], point.to_model(param_map[params].curve.coordinate_model, param_map[params].curve))\n",
-    "        with local(DefaultContext()) as ctx:\n",
-    "            try:\n",
-    "                mult.multiply(scalar)\n",
-    "            except UnsatisfiedAssumptionError:\n",
-    "                continue\n",
-    "        trace = []\n",
-    "        def callback(action):\n",
-    "            if isinstance(action, FormulaAction):\n",
-    "                for intermediate in action.op_results:\n",
-    "                    trace.append(intermediate.value)\n",
-    "        ctx.actions.walk(callback)\n",
-    "        hit_zero = any(int(value) == 0 for value in trace)\n",
-    "        #if hit_zero:\n",
-    "            #new_points.add((point, params))\n",
-    "        hit_zero = sum(int(value) == 0 for value in trace)\n",
-    "        new_points.add((point, hit_zero, params))\n",
-    "    return new_points\n",
-    "\n",
-    "remapped_point_map_dupl = {}\n",
-    "with ProcessPoolExecutor(max_workers=12) as pool:\n",
-    "    futures = []\n",
-    "    pairs = []\n",
-    "    for coord_name, coords in model.coordinates.items():\n",
-    "        formula_groups = [list(filter(lambda formula: isinstance(formula, formula_class) and (formula.name.startswith(\"add\") or formula.name.startswith(\"dbl\")), coords.formulas.values())) for formula_class in formula_classes]\n",
-    "        formula_combinations = list(product(*formula_groups))\n",
-    "        for formulas in formula_combinations:\n",
-    "            #remap(coords, formulas, all_points, scalar)\n",
-    "            #break\n",
-    "            futures.append(pool.submit(remap, coords, formulas, all_points, scalar))\n",
-    "            pairs.append(formulas)\n",
-    "        #break\n",
-    "    results = [None for _ in futures]\n",
-    "    for future in tqdm(as_completed(futures), total=len(futures), desc=\"Remap\"):\n",
-    "        j = futures.index(future)\n",
-    "        remapped_point_map_dupl[pairs[j]] = future.result()"
+    "remapped_tree = build_distinguishing_tree(set(remapped_hit_point_map.keys()), remapped_hit_point_map)"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
-   "id": "10b5059c",
+   "id": "b921aadd-ccc6-4bc2-9cb0-e3905ff4f6ab",
    "metadata": {},
    "outputs": [],
    "source": [
-    "remapped_tree_dupl = build_distinguishing_tree(remapped_point_map_dupl)\n",
-    "print_leaf_sizes(remapped_tree_dupl)"
+    "describe_tree(remapped_tree)"
    ]
   },
   {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "c5d52e7a",
+   "cell_type": "markdown",
+   "id": "27f4be08-76fd-437a-bde7-8579b38fc686",
    "metadata": {},
-   "outputs": [],
    "source": [
-    "print(RenderTree(remapped_tree_dupl).by_attr(lambda n: n.name if n.name is not None else \"\\n\".join((\", \".join(str(formula) for formula in cfg) for cfg in n.cfgs))))"
+    "We can also investigate the other oracles and the distinguishing trees they can build:"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
-   "id": "47d2056f",
+   "id": "17de9a81-102e-4804-906a-02d2baef42d5",
    "metadata": {},
    "outputs": [],
    "source": [
-    "def remap(coords, formulas, points, scalar):\n",
-    "    mult = LTRMultiplier(*formulas, None, False, AccumulationOrder.PeqRP, True, True)\n",
-    "    new_points = set()\n",
-    "    param_map = {}\n",
-    "    for point, params in tqdm(points):\n",
-    "        if params not in param_map:\n",
-    "            try:\n",
-    "                param_map[params] = params.to_coords(coords)\n",
-    "            except UnsatisfiedAssumptionError:\n",
-    "                param_map[params] = None\n",
-    "                continue\n",
-    "        elif param_map[params] is None:\n",
-    "            continue\n",
-    "        mult.init(param_map[params], point.to_model(param_map[params].curve.coordinate_model, param_map[params].curve))\n",
-    "        with local(DefaultContext()) as ctx:\n",
-    "            try:\n",
-    "                mult.multiply(scalar)\n",
-    "            except UnsatisfiedAssumptionError:\n",
-    "                continue\n",
-    "        trace = []\n",
-    "        def callback(action):\n",
-    "            if isinstance(action, FormulaAction):\n",
-    "                for intermediate in action.op_results:\n",
-    "                    trace.append(intermediate.value)\n",
-    "        ctx.actions.walk(callback)\n",
-    "        #hit_zero = any(int(value) == 0 for value in trace)\n",
-    "        #if hit_zero:\n",
-    "            #new_points.add((point, params))\n",
-    "        hit_zero = tuple(map(lambda x: int(x) == 0,trace))\n",
-    "        new_points.add((point, hit_zero, params))\n",
-    "    return new_points\n",
-    "\n",
-    "remapped_point_map_loc = {}\n",
-    "with ProcessPoolExecutor(max_workers=12) as pool:\n",
-    "    futures = []\n",
-    "    pairs = []\n",
-    "    for coord_name, coords in model.coordinates.items():\n",
-    "        formula_groups = [list(filter(lambda formula: isinstance(formula, formula_class) and (formula.name.startswith(\"add\") or formula.name.startswith(\"dbl\")), coords.formulas.values())) for formula_class in formula_classes]\n",
-    "        formula_combinations = list(product(*formula_groups))\n",
-    "        for formulas in formula_combinations:\n",
-    "            #remap(coords, formulas, all_points, scalar)\n",
-    "            #break\n",
-    "            futures.append(pool.submit(remap, coords, formulas, all_points, scalar))\n",
-    "            pairs.append(formulas)\n",
-    "        #break\n",
-    "    results = [None for _ in futures]\n",
-    "    for future in tqdm(as_completed(futures), total=len(futures), desc=\"Remap\"):\n",
-    "        j = futures.index(future)\n",
-    "        remapped_point_map_loc[pairs[j]] = future.result()"
+    "remapped_count_tree = build_distinguishing_tree(set(remapped_count_point_map.keys()), remapped_count_point_map)\n",
+    "remapped_position_tree = build_distinguishing_tree(set(remapped_position_point_map.keys()), remapped_position_point_map)"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
-   "id": "c3a632fb",
+   "id": "b81d013a-7ff0-4b02-8c89-d6748d42874b",
    "metadata": {},
    "outputs": [],
    "source": [
-    "remapped_tree_loc = build_distinguishing_tree(remapped_point_map_loc)\n",
-    "print_leaf_sizes(remapped_tree_loc)"
+    "print(\"Zero hit\")\n",
+    "describe_tree(remapped_tree)\n",
+    "print(\"\\nZero count\")\n",
+    "describe_tree(remapped_count_tree)\n",
+    "print(\"\\nZero position\")\n",
+    "describe_tree(remapped_position_tree)"
    ]
   },
   {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "cf37df73",
+   "cell_type": "markdown",
+   "id": "e50daa23-25b8-4970-a69b-e31d8b000204",
    "metadata": {},
-   "outputs": [],
    "source": [
-    "print(RenderTree(remapped_tree_loc).by_attr(lambda n: n.name if n.name is not None else \"\\n\".join((\", \".join(str(formula) for formula in cfg) for cfg in n.cfgs))))"
+    "Now, lets examine the representation of factor sets and the distinguishing trees they can build."
    ]
   },
   {
@@ -597,19 +531,24 @@
    "outputs": [],
    "source": [
     "fset_map = {}\n",
+    "fset_nonhomo_map = {}\n",
     "for coord_name, coords in model.coordinates.items():\n",
     "    formula_groups = [list(filter(lambda formula: isinstance(formula, formula_class) and (formula.name.startswith(\"add\") or formula.name.startswith(\"dbl\")), coords.formulas.values())) for formula_class in formula_classes]\n",
     "    factor_sets = {}\n",
+    "    factor_sets_nonhomo = {}\n",
     "    for formula_group in formula_groups:\n",
     "        for formula in formula_group:\n",
-    "            fset = compute_factor_set(formula)\n",
-    "            factor_sets[formula] = fset\n",
+    "            factor_sets[formula] = compute_factor_set(formula)\n",
+    "            factor_sets_nonhomo[formula] = compute_factor_set(formula, filter_nonhomo=False)\n",
     "    formula_combinations = list(product(*formula_groups))\n",
     "    for formulas in formula_combinations:\n",
     "        fset = set()\n",
+    "        fset_nonhomo = set()\n",
     "        for formula in formulas:\n",
     "            fset.update(factor_sets[formula])\n",
-    "        fset_map[formulas] = fset"
+    "            fset_nonhomo.update(factor_sets_nonhomo[formula])\n",
+    "        fset_map[formulas] = fset\n",
+    "        fset_nonhomo_map[formulas] = fset_nonhomo"
    ]
   },
   {
@@ -620,91 +559,20 @@
    "outputs": [],
    "source": [
     "fset_tree = build_distinguishing_tree(set(fset_map.keys()), fset_map)\n",
-    "print_leaf_sizes(fset_tree)"
+    "fset_nonhomo_tree = build_distinguishing_tree(set(fset_nonhomo_map.keys()), fset_nonhomo_map)"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": null,
-   "id": "9f0dc435-e08a-45d0-846d-ee865d6a4b7c",
-   "metadata": {
-    "scrolled": true
-   },
-   "outputs": [],
-   "source": [
-    "print(RenderTree(fset_tree).by_attr(lambda n: n.name if n.name is not None else \"\\n\".join((\", \".join(str(formula) for formula in cfg) for cfg in n.cfgs))))"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "24c98d6a-fc16-495a-bd70-35cb022b7b17",
-   "metadata": {
-    "scrolled": true
-   },
-   "outputs": [],
-   "source": [
-    "expanded = expand_tree(remapped_tree, fset_map)\n",
-    "print(RenderTree(expanded).by_attr(lambda n: n.name if n.name is not None else \"\\n\".join((\", \".join(str(formula) for formula in cfg) for cfg in n.cfgs))))"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "1066e690-d036-47b6-995f-c54c412595f9",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "polys = set()\n",
-    "for node in PreOrderIter(expanded):\n",
-    "    if not node.name:\n",
-    "        continue\n",
-    "    _, elem = node.name\n",
-    "    if isinstance(elem, Poly):\n",
-    "        polys.add(elem)\n",
-    "for poly in polys:\n",
-    "    print(poly)"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "4a4de408-84b7-4559-92a5-94563ba1c1bf",
+   "id": "b47a3a13-1067-4901-9441-7160130fef1c",
    "metadata": {},
    "outputs": [],
    "source": [
-    "print_leaf_sizes(tree)\n",
-    "print_leaf_sizes(fset_tree)\n",
-    "print_leaf_sizes(expanded)"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "42b5f4cc-c327-4f6c-9d41-357593ef1799",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "def simulated_oracle(scalar, affine_point, real_coord_name=\"projective\", real_add_name=\"add-2007-bl\", real_dbl_name=\"dbl-2007-bl\"):\n",
-    "    real_coords = model.coordinates[real_coord_name]\n",
-    "    real_add = real_coords.formulas[real_add_name]\n",
-    "    real_dbl = real_coords.formulas[real_dbl_name]\n",
-    "    real_mult = LTRMultiplier(real_add, real_dbl, None, False, AccumulationOrder.PeqRP, True, True)\n",
-    "    point = affine_point.to_model(params.curve.coordinate_model, params.curve)\n",
-    "    with local(DefaultContext()) as ctx:\n",
-    "        real_mult.init(params, point)\n",
-    "        real_mult.multiply(scalar)\n",
-    "\n",
-    "    result = {\"result\": False}\n",
-    "\n",
-    "    def callback(action):\n",
-    "        if isinstance(action, FormulaAction):\n",
-    "            for intermediate in action.op_results:\n",
-    "                if int(value) == 0:\n",
-    "                    result[\"result\"] = True\n",
-    "                trace.append(intermediate.value)\n",
-    "    ctx.actions.walk(callback)\n",
-    "    return result[\"result\"]"
+    "print(\"Factor sets\")\n",
+    "describe_tree(fset_tree)\n",
+    "print(\"\\nFactor sets (nonhomogenous)\")\n",
+    "describe_tree(fset_nonhomo_tree)"
    ]
   }
  ],
@@ -724,7 +592,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.11.5"
+   "version": "3.11.4"
   }
  },
  "nbformat": 4,