fix and opt backend and revise netfactory.

.codecov.yml

@@ -44,9 +44,10 @@ ignore:
   - "act/pipeline/fuzzing/trace_reader.py"
   - "act/front_end/vnnlib_loader/cli.py"
   - "act/pipeline/verification/llm_probe.py"
-  - "act/back_end/cli.py"
-  - "act/front_end/cli.py"
-  - "act/pipeline/cli.py"
+  - "act/config/backend_cli.py"
+  - "act/config/frontend_cli.py"
+  - "act/config/pipeline_cli.py"
+  - "act/config/check_parity.py"
   - "act/front_end/torchvision_loader/cli.py"
   - "act/back_end/serialization/test_serialization.py"
   - "vnncomp/"

.coveragerc

@@ -40,6 +40,7 @@ omit =
     */__main__.py
     act/pipeline/verification/llm_probe.py
     act/wrapper_exts/ext_runner.py
+    act/config/check_parity.py
 
 precision = 2
 show_missing = True

.github/workflows/act-bab.yml

@@ -57,7 +57,7 @@ jobs:
         uses: actions/cache@v4
         with:
           path: act/back_end/examples/nets
-          key: act-nets-${{ hashFiles('act/back_end/examples/config_gen_act_net.yaml', 'act/back_end/net_factory.py', 'act/back_end/config.yaml') }}
+          key: act-nets-${{ hashFiles('act/config/gen_act_net.yaml', 'act/back_end/net_factory.py', 'act/config/backend.yaml') }}
           restore-keys: |
             act-nets-
 

.github/workflows/act.config.yml

@@ -0,0 +1,43 @@
+name: ACT Config Parity
+
+# Enforce CLI <-> YAML <-> dataclass consistency for the three config tiers, so
+# an option added on one surface can never be silently missed by the others.
+on:
+  push:
+    branches: [ main ]
+    paths:
+      - 'act/config/**'
+      - 'act/pipeline/fuzzing/actfuzzer.py'
+      - '.github/workflows/act.config.yml'
+  pull_request:
+    branches: [ main ]
+    paths:
+      - 'act/config/**'
+      - 'act/pipeline/fuzzing/actfuzzer.py'
+      - '.github/workflows/act.config.yml'
+  workflow_dispatch:
+
+env:
+  PYTHONPATH: ${{ github.workspace }}
+
+jobs:
+  config-parity:
+    name: CLI <-> YAML parity
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+
+      - name: Install dependencies
+        run: |
+          python -m pip install --upgrade pip
+          pip install torch torchvision --index-url https://download.pytorch.org/whl/cpu
+          pip install -r modules/setup/main_requirements.txt
+
+      - name: Check CLI <-> YAML <-> dataclass parity
+        run: python -m act.config.check_parity

act/README.md

@@ -33,8 +33,17 @@ This directory contains the core verification framework for the Abstract Constra
 act/
 ├── __init__.py                     # Package initialization
 │
+├── config/                         # Centralized Configuration
+│   ├── config.py                   # Global configuration dataclasses
+│   ├── backend.yaml         # Back-end specific scalar configuration
+│   ├── gen_act_net.yaml      # NetFactory architecture-sampling DSL
+│   ├── pipeline.yaml        # Pipeline specific configuration
+│   ├── frontend.yaml        # Front-end specific configuration
+│   ├── backend_cli.py              # Back-end CLI implementation
+│   ├── pipeline_cli.py             # Pipeline CLI implementation
+│   └── frontend_cli.py             # Front-end CLI implementation
+│
 ├── front_end/                      # Front-End: User-facing data processing
-│   ├── cli.py                      # Main front-end CLI with unified device/dtype args
 │   ├── torchvision_loader/         # TorchVision integration
 │   │   ├── cli.py                  # TorchVision-specific CLI
 │   │   ├── create_specs.py         # TorchVisionSpecCreator for dataset-model pairs
@@ -51,7 +60,6 @@ act/
 │   └── README.md                   # Front-end documentation
 │
 ├── back_end/                       # Back-End: Core verification engine
-│   ├── cli.py                      # Back-end CLI (generate, verify, info, test)
 │   ├── __main__.py                 # Entry point for python -m act.back_end
 │   ├── core.py                     # Net, Layer, Bounds, Con, ConSet data structures
 │   ├── verifier.py                 # Spec-free verification: verify_once(), verify_lp_batched()
@@ -90,13 +98,11 @@ act/
 │   │   ├── serialization.py        # NetSerializer with tensor encoding
 │   │   └── test_serialization.py   # Serialization correctness tests
 │   ├── examples/                   # Example networks and configurations
-│   │   ├── config_gen_act_net.yaml # YAML network definitions
 │   │   ├── nets/                   # Generated ACT Net JSON files
 │   │   └── README.md               # Examples documentation
 │   └── README.md                   # Back-end documentation
 │
 ├── pipeline/                       # Pipeline: Testing framework and integration
-│   ├── cli.py                      # Pipeline CLI with unified device/dtype args
 │   ├── verification/               # Verification utilities submodule
 │   │   ├── __init__.py             # Verification module initialization
 │   │   ├── torch2act.py            # Automatic PyTorch→ACT Net conversion
@@ -124,7 +130,7 @@ act/
 All ACT modules now have unified CLI architecture with consistent device/dtype handling:
 
 #### **Front-End CLIs**
-- **`front_end/cli.py`**: Main front-end CLI
+- **`act/config/frontend_cli.py`**: Main front-end CLI
   - Commands: `--list`, `--synthesis`, `--list-creators`
   - Unified device/dtype arguments via `cli_utils`
   - Usage: `python -m act.front_end [options]`
@@ -138,15 +144,15 @@ All ACT modules now have unified CLI architecture with consistent device/dtype h
   - Usage: `python -m act.front_end.vnnlib_loader [options]`
 
 #### **Pipeline CLI**
-- **`pipeline/cli.py`**: Pipeline testing and integration CLI
+- **`act/config/pipeline_cli.py`**: Pipeline testing and integration CLI
   - Commands: Testing, validation, regression, reporting
   - Unified device/dtype arguments via `cli_utils`
   - Usage: `python -m act.pipeline [options]`
 
 #### **Back-End CLI**
-- **`back_end/cli.py`**: Comprehensive back-end verification CLI
+- **`act/config/backend_cli.py`**: Comprehensive back-end verification CLI
   - Commands:
-    - `--generate`: Generate example networks from YAML config
+    - `--generate`: Generate example networks from YAML config (default: `backend.yaml`)
     - `--list-examples`: List all available example networks
     - `--info`: Display network structure and details
     - `--verify`: Run verification (single-shot or branch-and-bound)
@@ -241,8 +247,8 @@ All ACT modules now have unified CLI architecture with consistent device/dtype h
   - **`test_serialization.py`**: Serialization correctness validation
 
 - **`examples/`**: Example networks and test cases
-  - **`config_gen_act_net.yaml`**: YAML definitions for example networks
-  - **`nets/`**: Generated ACT Net JSON files (MNIST, CIFAR, control, reachability)
+- **`../config/gen_act_net.yaml`**: network-generation DSL for example networks
+- **`nets/`**: Generated ACT Net JSON files (MNIST, CIFAR, control, reachability)
   - Networks include embedded INPUT_SPEC and ASSERT layers for spec-free verification
 
 ### **`pipeline/` - Testing Framework and Integration**
@@ -263,7 +269,7 @@ All ACT modules now have unified CLI architecture with consistent device/dtype h
   - PyTorch model generation from ACT Nets
   - Integration with VerifiableModel wrapper layers
 
-- **`cli.py`**: Main pipeline CLI (`python -m act.pipeline`)
+- **`act/config/pipeline_cli.py`**: Main pipeline CLI (`python -m act.pipeline`)
 - **`verification/`**: Conversion + validation utilities — `torch2act.py`, `act2torch.py`, `validate_verifier.py`, `model_factory.py`, `per_neuron_bounds.py`, `utils.py` (performance profiling), `llm_probe.py`
 - **`fuzzing/`**: Whitebox fuzzing framework — `actfuzzer.py`, `tracer.py`, `trace_storage.py`, `trace_reader.py`, `coverage.py`, `mutations.py`, `checker.py`, `corpus.py`
 - **`log/`**: Centralized execution logs (`act_debug_tf.log`, validation/test output)
@@ -283,6 +289,13 @@ All ACT modules now have unified CLI architecture with consistent device/dtype h
   - `initialize_device(device_str, dtype_str)`: Main initialization function
 
 - **`path_config.py`**: Project path configuration and management
+- **`config/`**: Centralized configuration and CLIs
+  - **`config.py`**: PerformanceOptions, BackendConfig, TorchLPConfig, etc.
+  - **`backend.yaml`**: Back-end runtime and generation scalar defaults
+  - **`gen_act_net.yaml`**: NetFactory architecture-sampling DSL
+  - **`pipeline.yaml`**: Pipeline testing and fuzzing defaults
+  - **`frontend.yaml`**: Loader and spec creation defaults
+  - **`backend_cli.py`**, **`pipeline_cli.py`**, **`frontend_cli.py`**: Implementation of tier CLIs
   - `get_project_root()`, `get_data_root()`, `get_config_root()`
   - `get_pipeline_log_dir()`: Returns absolute path to `act/pipeline/log/`
   - `ensure_gurobi_license()`: Automatic Gurobi license detection
@@ -426,15 +439,16 @@ python -m act.back_end --test-serialization --device cpu --dtype float64
 
 ## Examples and Network Generation
 Example ACT networks are stored as JSON under `act/back_end/examples/nets/`.
-These files are generated from the YAML configuration `act/back_end/examples/config_gen_act_net.yaml`
-using the YAML-driven network factory. The test suite and serializer load networks
-from the `examples/nets` directory. When authoring new example networks prefer the
+These files are generated from the architecture-sampling DSL in `act/config/gen_act_net.yaml`
+using the YAML-driven network factory; scalar generation knobs remain in
+`act/config/backend.yaml`. The test suite and serializer load networks from the
+`examples/nets` directory. When authoring new example networks prefer the
 YAML configuration and the factory rather than hand-editing the JSON files.
 
 ### Using the Back-End CLI for Network Generation
 The back-end CLI provides comprehensive tools for working with ACT networks:
 
-1. **Generate Networks**: `--generate` creates all networks defined in `config_gen_act_net.yaml`
+1. **Generate Networks**: `--generate` creates all networks defined in `gen_act_net.yaml`
 2. **List Networks**: `--list-examples` shows all available networks organized by category
 3. **Inspect Networks**: `--info` displays structure, use `--verbose` for detailed layer information
 4. **Verify Networks**: `--verify` runs verification with optional `--bab` for branch-and-bound

act/back_end/README.md

@@ -286,7 +286,7 @@ Config (`BaBConfig`) / CLI flags:
 | `llm_probe_model` | `--bab-llm-probe-model` | `""` |
 | `llm_probe_base_url` | `--bab-llm-probe-base-url` | `""` |
 | `llm_probe_cadence` | `--bab-llm-probe-cadence` | `1` |
-| `llm_probe_decisions` (e.g. `split,frontier,refine,neuron`) / `llm_probe_max_candidates_total` / `llm_probe_api_key_env` / `_temperature` / `_max_candidates` / `_history` / `_max_failures` / `_log` | (config/YAML only) | see `config.py` |
+| `llm_probe_decisions` (e.g. `split,frontier,refine,neuron`) / `llm_probe_max_candidates_total` / `llm_probe_api_key_env` / `_temperature` / `_max_candidates` / `_history` / `_max_failures` / `_log` | (config/YAML only) | see `act/config/config.py` |
 
 Implementation lives in `act/pipeline/verification/llm_probe.py`. That file has two independent
 sections: the legacy TinyLlama input/output probe (Section A) and this BaB controller (Section B);

act/back_end/__main__.py

@@ -10,7 +10,7 @@
 
 import sys
 
-from act.back_end.cli import main
+from act.config.backend_cli import main
 
 if __name__ == "__main__":
     sys.exit(main())

act/back_end/analyze.py

@@ -26,9 +26,9 @@
 )
 
 # Initialize default transfer function mode
-def initialize_tf_mode(mode: str = "interval"):
+def initialize_tf_mode(mode: str = "interval", tf_config=None):
     """Initialize transfer function mode. Call this before using analyze()."""
-    set_transfer_function_mode(mode)
+    set_transfer_function_mode(mode, tf_config)
 
 
 @dataclass

act/back_end/bab/__init__.py

@@ -6,7 +6,7 @@
 # Distributed without any warranty; see <http://www.gnu.org/licenses/>.
 # ===---------------------------------------------------------------------====#
 
-from act.back_end.config import BaBConfig
+from act.config.config import BaBConfig
 from act.back_end.bab.bab import verify_bab, verify_bab_batched
 from act.back_end.bab.node import BabNode, SubproblemBatch, split_subproblems
 from act.back_end.bab.branching.branching import BranchingStrategy

act/back_end/bab/bab.py

@@ -26,7 +26,7 @@
 
 import torch
 
-from act.back_end.config import BaBConfig, VALID_SOLVER_TIERS
+from act.config.config import BaBConfig, DualConfig, VALID_SOLVER_TIERS
 from act.back_end.bab.node import (
     BabNode,
     SubproblemBatch,
@@ -258,6 +258,7 @@ def _gain_tested_decision(
     net: Net,
     assert_layer: Layer,
     config: BaBConfig,
+    dual_config: DualConfig,
     keep_rows: Optional[torch.Tensor],
     root_bounds_dict: Optional[Dict[int, Bounds]],
     bounds_dict: Optional[Dict[int, Bounds]],
@@ -335,6 +336,7 @@ def _rep_state(state):
         k_actual=n_probe,
         batch=probe,
         config=config,
+        dual_config=dual_config,
         optimize=False,
         keep_rows=keep_rows,
         root_bounds_dict=root_bounds_dict,
@@ -799,8 +801,14 @@ def _check_input_specs_batched(x_batch: torch.Tensor, spec_layers: List[Layer])
         else:
             result &= torch.zeros_like(result)
             continue
+        positions_raw = layer.params.get("perturbed_positions")
+        positions = (
+            positions_raw
+            if positions_raw is None or isinstance(positions_raw, (torch.Tensor, list, tuple))
+            else None
+        )
         mask = normalize_position_mask(
-            layer.params.get("perturbed_positions"),
+            positions,
             int(center_t.shape[-2]),
             batch_shape=tuple(center_t.shape[:-2]),
             device=x_batch.device,
@@ -892,6 +900,7 @@ def _dispatch_dual_solve(
     k_actual: int,
     batch: SubproblemBatch,
     config: BaBConfig,
+    dual_config: DualConfig,
     optimize: bool,
     keep_rows: Optional[torch.Tensor] = None,
     root_bounds_dict: Optional[Dict[int, Bounds]] = None,
@@ -1014,22 +1023,22 @@ def _dispatch_dual_solve(
                 getattr(config, "eta_only_children", False) and is_child_batch
             ),
             refresh_forward=root_bounds_dict is None,
-            n_iters=config.dual_n_iters,
-            lr_alpha=config.lr_alpha,
-            lr_beta=config.lr_beta,
-            lr_decay=config.lr_decay,
+            n_iters=dual_config.n_iters,
+            lr_alpha=dual_config.lr_alpha,
+            lr_beta=dual_config.lr_beta,
+            lr_decay=dual_config.lr_decay,
             eta=batch.incremental_eta if solver_tier == "dual_alpha_eta" else None,
-            incremental_alphas=batch.incremental_alpha if getattr(config, "incremental_start_enabled", True) else None,
+            incremental_alphas=batch.incremental_alpha if dual_config.incremental_start_enabled else None,
             incremental_etas=(
                 batch.incremental_eta
                 if solver_tier == "dual_alpha_eta"
-                and getattr(config, "incremental_start_enabled", True)
+                and dual_config.incremental_start_enabled
                 else None
             ),
             split_signs=batch.split_signs if solver_tier == "dual_alpha_eta" else None,
             return_optimized=True,
             return_sce=True,
-            per_class_alpha=config.per_class_alpha,
+            per_class_alpha=dual_config.per_class_alpha,
             **({"return_nu_per_layer": True} if return_nu and supports_return_nu else {}),
         )
         margins_flat = dual_result.margins
@@ -1128,7 +1137,7 @@ def _dispatch_dual_solve(
             split_signs=(
                 batch.split_signs if solver_tier == "dual_alpha_eta" else None
             ),
-            per_class_alpha=config.per_class_alpha,
+            per_class_alpha=dual_config.per_class_alpha,
         )
     try:
         return DualSolveResult(
@@ -1250,6 +1259,7 @@ def verify_bab_batched(
     *,
     max_batch_size: Optional[Union[int, str]] = None,
     time_budget_s: Optional[float] = None,
+    dual_config: Optional[DualConfig] = None,
     verbose: bool = False,
     _k_log: Optional[List[int]] = None,
 ) -> VerifyResult:
@@ -1287,6 +1297,8 @@ def verify_bab_batched(
     """
     if config is None:
         config = BaBConfig()
+    if dual_config is None:
+        dual_config = DualConfig()
     auto_batch = isinstance(max_batch_size, str) and max_batch_size == "auto"
     if auto_batch:
         effective_batch = (
@@ -1407,6 +1419,7 @@ def verify_bab_batched(
             k_actual=root_batch.batch_size,
             batch=root_batch,
             config=config,
+            dual_config=dual_config,
             optimize=presolve_tier in ("dual_alpha", "dual_alpha_eta"),
             root_bounds_dict=root_fwd,
         )
@@ -1518,6 +1531,7 @@ def verify_bab_batched(
                 k_actual=k_actual,
                 batch=batch,
                 config=config,
+                dual_config=dual_config,
                 optimize=False,
                 keep_rows=spec_keep_rows,
                 root_bounds_dict=node_root_fwd,
@@ -1532,6 +1546,7 @@ def verify_bab_batched(
                 k_actual=k_actual,
                 batch=batch,
                 config=config,
+                dual_config=dual_config,
                 optimize=True,
                 keep_rows=spec_keep_rows,
                 root_bounds_dict=node_root_fwd,
@@ -1738,6 +1753,7 @@ def _select_incremental_state(
                                 net,
                                 assert_layer,
                                 config,
+                                dual_config,
                                 spec_keep_rows,
                                 node_root_fwd,
                                 bd_branch,
@@ -1890,6 +1906,7 @@ def verify_bab(
     time_budget_s: Optional[float] = None,
     timelimit: Optional[float] = None,
     verbose: bool = False,
+    dual_config: Optional[DualConfig] = None,
 ) -> VerifyResult:
     """Single-solver Branch-and-Bound entry: one subproblem per iteration.
 
@@ -1920,6 +1937,7 @@ def verify_bab(
         max_batch_size=1,
         time_budget_s=budget,
         verbose=verbose,
+        dual_config=dual_config,
     )