Replace the two-bank machine with a K-bank ring, prove its reproduction in Rocq, and revise the paper
a9ea017 | (* writes the netlist defined in Phys.v, extracted by Extract.v, in the layout of the netlist file of | |
| src/twohead.py, for a window of 2^AL cells, K banks of S slots and K tapes of L cells: dump AL K S L PATH *) | |
| let () = | |
| let arg i = int_of_string Sys.argv.(i) in | |
| let al = arg 1 and k = arg 2 and s = arg 3 and l = arg 4 in | |
| let us = Physnet.phys_units al k s l and nx = Physnet.phys_next al k s l in | |
| let oc = open_out_bin Sys.argv.(5) in | |
| let put x = (* little-endian int32 *) | |
| let b = Bytes.create 4 in | |
| Bytes.set_int32_le b 0 (Int32.of_int x); output_bytes oc b in | |
| let edges = List.fold_left (fun a (u : Physnet.tu) -> a + List.length u.tin) 0 us in | |
| put (Physnet.nst al k s l); put (List.length us); put edges; | |
| List.iter (fun (u : Physnet.tu) -> put u.tb) us; | |
| List.iter (fun (u : Physnet.tu) -> put (List.length u.tin)) us; | |
| List.iter (fun (u : Physnet.tu) -> List.iter (fun (s, wt) -> put (wt * (s + 1))) u.tin) us; | |
| List.iter put nx; | |
| close_out oc | |