Track vertex constraints.

src/foil/circuit.rs

@@ -1,9 +1,11 @@
 //! This module provides a general mechanism for converting a minimized Foil instance.
 
+use std::collections::HashSet;
+
 use bellperson::{gadgets::num::AllocatedNum, Circuit, ConstraintSystem, SynthesisError};
 
 use crate::field::LurkField;
-use crate::foil::{Foil, MetaData};
+use crate::foil::{Foil, Id, MetaData};
 
 // This is an incomplete schematic sketch of what synthesis should entail. NOTE: the simplicity and uniformity of this
 // last-mile conversion to a circuit. Most circuit-specific heavy lifting will be concentrated in the individual
@@ -26,37 +28,86 @@ impl<T: PartialEq + Clone, F: LurkField, M: MetaData> Circuit<F> for Foil<T, M>
             .map(|(i, vertex)| {
                 Ok(AllocatedNum::alloc(
                     &mut cs.namespace(|| format!("allocated-{i}-{vertex}")),
-                    || todo!("get from witness or calculate..."),
+                    || todo!("get from witness, calculate, or get as constant..."),
                 )?)
             })
             .collect::<Result<Vec<_>, SynthesisError>>()?;
 
+        let mut constrained: HashSet<Id> = Default::default();
+        for constructor in self.schema.constructors.iter() {
+            let projectors = constructor.projectors();
+            todo!();
+        }
+
         for (i, (representative_id, _)) in partition.classes.iter().enumerate() {
             let vertex = self.graph.vertex(*representative_id);
             let allocated_head = allocated[i].clone();
-            let allocated_successors = vertex
-                .successors()
-                .borrow()
-                .iter()
-                .map(|successor_id| allocated[*successor_id].clone())
-                .collect::<Vec<_>>();
-            let relation: Rel = {
-                let arity = allocated_successors.len();
-                let label = vertex.label();
-                let metadata = vertex.metadata();
-
-                todo!(
+
+            if todo!("determine whether this vertex requires allocation") {
+                // For example, projectors do not require allocation given that they will be constrained by their
+                // corresponding constructor. This *could* be handled at the `Relation` level, however, in general this
+                // decision may require more global context -- so for now, consider that it should be made in the
+                // top-level `synthesize` method.
+
+                // Currently, so-called `Bindings` (equivalences specified through the graph) become trivial after
+                // finalization. There is no reason to allocate variables for them or add any related constraints. The
+                // right answer is probably that minimization should remove them -- along with any other superfluous
+                // nodes of the graph.
+                //
+                // The point is that some parts of the decision (whether a given vertex needs constraints of its own)
+                // should probably be handled upstream. What is important is that we clearly understand the separation
+                // of concerns -- so decisions at each stage do not rely on invalid assumptions about the
+                // responsibilities of others. Some redundancy may therefore be appropriate.
+                //
+                // For example, in the case of bindings, all of the above could be implemented:
+                //
+                // - A full 'minimization' can remove them (with a check to ensure they were indeed enforced -- which
+                // means their successors have been made equivalent). This implies that the bindings themselves will not
+                // be seen here.
+
+                // - If they do appear here, we can detect that and not allocate or constrain them. However, note that
+                // maybe this is the wrong approach -- since it will require increasing knowledge of semantics here. Not
+                // special-casing would be simplest. One answer is to ensure that `Func`s can be defined in such a way
+                // as to provide hints here. Designation of `Bindings` (in the constructors example) as `equivalences`
+                // is effectively such an annotation, but it may be useful to provide a more general (probably
+                // trait-based) mechanism.
+                //
+                // - If we do reach the point of constraining such nodes, their defined `Relation::synthesize` method
+                // can be a no-op.
+
+                constrained.insert(*representative_id);
+
+                let allocated_successors = vertex
+                    .successors()
+                    .borrow()
+                    .iter()
+                    .map(|successor_id| {
+                        constrained.insert(*successor_id);
+                        allocated[*successor_id].clone()
+                    })
+                    .collect::<Vec<_>>();
+
+                let relation: Rel = {
+                    let arity = allocated_successors.len();
+                    let label = vertex.label();
+                    let metadata = vertex.metadata();
+
+                    todo!(
                     "recover source intent from the above -- possibly enhancing Foil to simplify"
                 );
-            };
+                };
 
-            relation.synthesize(
-                &mut cs.namespace(|| format!("relation-{}", i)),
-                allocated_head,
-                allocated_successors,
-            )?;
+                relation.synthesize(
+                    &mut cs.namespace(|| format!("relation-{}", i)),
+                    allocated_head,
+                    allocated_successors,
+                )?;
+            }
         }
 
+        // Every allocation has been constrained.
+        assert_eq!(constrained.len(), partition.size());
+
         Ok(())
     }
 }