exception Invalid_argument("List.map2: list lengths differ")

[alberdingk-thijm]

Managed to trigger an interesting error with a more complicated assert function that I was testing for partitioning. I'll see about coming up with a minimal working example, but here is the complete code.

include "utils.nv"

(* Each node keeps track of who its next hop is to and how long the total route is. *)
type route = { len: int; nexthop: tnode }
type attribute = option[route]

(* --- Predicates ----------------------------------------------------------------- *)

(* predicate that a route r exactly has length l and nexthop n *)
let exact_route r l n = match r with
  | Some r -> r.len = l && r.nexthop = n
  | None -> false

(* predicate that a route r has length at least l and exactly nexthop n *)
let min_len_route r l n = match r with
  | Some r -> r.len >= l && r.nexthop = n
  | None -> false

(* --- Hypotheses ----------------------------------------------------------------- *)

(* chosen destination *)
let dest = 9n

(* node hypotheses *)
(* h_i_j is the hypothesis on j's input that represents a message coming from i *)
symbolic h_0_2 : option[route]
symbolic h_2_0 : option[route]
symbolic h_0_6 : option[route]
symbolic h_6_0 : option[route]
symbolic h_1_3 : option[route]
symbolic h_3_1 : option[route]
symbolic h_1_7 : option[route]
symbolic h_7_1 : option[route]

(* requirements on the hypotheses *)
(* as the destination is 9n, hypotheses entering 9's pod do not need to be exact *)
require (exact_route h_0_2 3 0n)
require (min_len_route h_2_0 4 2n)
require (min_len_route h_0_6 3 0n)
require (exact_route h_6_0 2 6n)
require (exact_route h_1_3 3 1n)
require (min_len_route h_3_1 4 3n)
require (min_len_route h_1_7 3 1n)
require (exact_route h_7_1 2 7n)

(* --- Topology ------------------------------------------------------------------ *)
(* 10 node fattree, partitioned along the 4 bidirectional spine-pod edges *)

(* base_nodes = 10 + input_nodes = 8 + output_nodes = 8 *)
let nodes = 26

(*
  Edge arrangement:
  0 to 2 and 6
  1 to 3 and 7

   0  1
  | \/ \
  | /\  \
  2 3 6 7
  |X| |X|
  6 7 8 9

*)
let edges = {
  (* cut 0=2 edge *)
  0-10;
  11-2;
  2-12;
  13-0;
  (* cut 0=6 edge *)
  0-14;
  15-6;
  6-16;
  17-0;
  (* cut 1=3 edge *)
  1-18;
  19-3;
  3-20;
  21-1;
  (* cut 1=7 edge *)
  1-22;
  23-7;
  7-24;
  25-1;
  (* uncut pod edges: left pod *)
  2=4;
  2=5;
  3=4;
  3=5;
  (* uncut pod edges: right pod *)
  6=8;
  6=9;
  7=8;
  7=9;
}

(* --- Policy Definition --------------------------------------------------------- *)

(* -------- Merge ---------------------------------------------------------------- *)
(* between two routes, pick the shorter one;
 * if the routes have the same length, pick the one with the lower node number
 *)
let compare_routes r1 r2 =
  if (r1.len < r2.len) then r1 else 
  if (r1.len = r2.len && r1.nexthop <n r2.nexthop) then r1 else r2

(* merge compares two routes and selects the best *)
let merge node x y = mapbetter compare_routes x y
(* NOTE: this definition shows that the SMT encoding of the output's solution
 * is the same as setting the output's solution to trans(L(base)),
 * because the base node is the output's only choice and its initial value is None
 *)

(* -------- Transfer ------------------------------------------------------------- *)
(* update a route to increase len by one and give this node as the next hop *)
let update_route node r =
  let new_len = r.len + 1 in
  { len = new_len; nexthop = node }

(* update the route if it exists, using the source node and ignoring the sink *)
let transfer_route src snk x = mapo (fun r -> update_route src r) x

(* the final trans function in the partitioned SRP uses the original trans for all non-input edges
 * and the identity function for the others *)
let trans edge x = match edge with
  (* use identity for all input~base edges *)
  | 11~2 -> x
  | 13~0 -> x
  | 15~6 -> x
  | 17~0 -> x
  | 19~3 -> x
  | 21~1 -> x
  | 23~7 -> x
  | 25~1 -> x
  (* use original edge transfer for base~output edges *)
  | 0~10 -> transfer_route 0n 2n x
  | 2~12 -> transfer_route 2n 0n x
  | 0~14 -> transfer_route 0n 6n x
  | 6~16 -> transfer_route 6n 0n x
  | 1~18 -> transfer_route 1n 3n x
  | 3~20 -> transfer_route 3n 1n x
  | 1~22 -> transfer_route 1n 7n x
  | 7~24 -> transfer_route 7n 1n x
  (* otherwise use original transfer *)
  | src~snk -> transfer_route src snk x

(* -------- Init ----------------------------------------------------------------- *)
let init node = if node = dest then
  Some { len = 0; nexthop = node } else 
  match node with
  | 11n -> h_0_2
  | 13n -> h_2_0
  | 15n -> h_0_6
  | 17n -> h_6_0
  | 19n -> h_1_3
  | 21n -> h_3_1
  | 23n -> h_1_7
  | 25n -> h_7_1
  | _ -> None

(* -------- Assert --------------------------------------------------------------- *)
symbolic a : option[route]
let assert node x = 
  match node with
  (* Check that the outputs satisfy the inputs *)
  | 10n -> mapbetter compare_routes h_0_2 a = mapbetter compare_routes x a
  | 12n -> mapbetter compare_routes h_2_0 a = mapbetter compare_routes x a
  | 14n -> mapbetter compare_routes h_0_6 a = mapbetter compare_routes x a
  | 16n -> mapbetter compare_routes h_6_0 a = mapbetter compare_routes x a
  | 18n -> mapbetter compare_routes h_1_3 a = mapbetter compare_routes x a
  | 20n -> mapbetter compare_routes h_3_1 a = mapbetter compare_routes x a
  | 22n -> mapbetter compare_routes h_1_7 a = mapbetter compare_routes x a
  | 24n -> mapbetter compare_routes h_7_1 a = mapbetter compare_routes x a
  (* Check that everyone can reach the destination *)
  | _ -> isSome x

The error appears to be triggered by the assert function. The stack trace is (using master):

Processing examples/fattree-10.nv
Processing examples/utils.nv
Inlining took: 0.000538 secs to complete
Map unrolling took: 0.000760 secs to complete
Inlining took: 0.000166 secs to complete
Unbox options took: 0.000478 secs to complete
Flattening Tuples took: 0.002041 secs to complete
Partially Evaluating Network took: 0.000144 secs to complete
Fatal error: exception Invalid_argument("List.map2: list lengths differ")
Raised at file "pervasives.ml", line 33, characters 20-45
Called from file "src/batList.mlv", line 599, characters 2-18
Called from file "src/lib/smt/SmtClassicEncoding.ml", line 147, characters 17-127
Called from file "src/lib/smt/SmtClassicEncoding.ml", line 261, characters 12-68
Called from file "src/lib/smt/Smt.ml", line 142, characters 29-42
Called from file "src/lib/utils/Profile.ml", line 10, characters 12-16
Called from file "src/lib/smt/Smt.ml", line 141, characters 6-204
Called from file "src/lib/smt/Smt.ml", line 179, characters 12-24
Called from file "src/lib/Main_defs.ml", line 94, characters 10-60
Called from file "src/lib/utils/Profile.ml", line 10, characters 12-16
Called from file "src/lib/Main_defs.ml", line 136, characters 8-161
Called from file "src/exe/Main.ml", line 22, characters 12-37
Called from file "src/lib/utils/Profile.ml", line 10, characters 12-16
Called from file "src/exe/Main.ml", line 32, characters 2-67

This points to something going wrong when calling lift2 within encode_exp_z3_assert.

[DKLoehr]

This is possibly related to #31, although it's a different symptom. It looks like a problem with the unboxed encoding not properly encoding tuple comparisons. I came up with the following minimal example (only the last few lines are relevant):

type attribute = bool
let nodes = 1
let edges = {}
let trans e x = x
let merge n x y = x
let assert n x = x

symbolic foo : bool
let init n =
 (if foo then (1,2) else (3,4)) =
 (if foo then (1,2) else (3,4))

The symbolic variable and if statement are just there so we can't statically do the comparison during partial evaluation.