From 6edfd782802bb2f458a8e00cc6bafffa23e0248e Mon Sep 17 00:00:00 2001 From: engboris Date: Sun, 1 May 2022 17:14:58 +0200 Subject: [PATCH 1/2] Add circuits and automata --- ocaml/Circuits.ml | 93 ++++++++++++++++++++++------------------ ocaml/Resolution.ml | 7 ++- ocaml/StellarCircuits.ml | 56 ++++++++++++++++++++++++ ocaml/StellarFSA.ml | 15 +++++++ 4 files changed, 127 insertions(+), 44 deletions(-) create mode 100644 ocaml/StellarCircuits.ml create mode 100644 ocaml/StellarFSA.ml diff --git a/ocaml/Circuits.ml b/ocaml/Circuits.ml index e81403e..519a58a 100644 --- a/ocaml/Circuits.ml +++ b/ocaml/Circuits.ml @@ -12,27 +12,31 @@ type op = | CAnd | COr | CNeg type input = id -type gate = input list * op * id +type output = id +type gate = input list * op * output list type circuit = gate list (* _________ Getters _________ *) -let get_node_info circ node = - let (ins, op, i) = - List.hd (List.filter (fun (_, _, i) -> i = node) circ) - in (ins, op) +let get_node_info circ target = + let (ins, op, outs) = + List.hd (List.filter (fun (_, _, outs) -> List.mem target outs) circ) + in (ins, op, outs) let get_inputs circ node = - let (ins, _) = get_node_info circ node in ins + let (ins, _, _) = get_node_info circ node in ins + +let get_outputs circ node = + let (_, _, outs) = get_node_info circ node in outs let get_op circ node = - let (_, op) = get_node_info circ node in op + let (_, op, _) = get_node_info circ node in op (* extracts the two first inputs in a list of inputs *) -let extract_bin_ins = function +let twinhd = function | [] -> failwith "Error extract_bin_ins: no input." | h1::h2::t -> (h1, h2) - | _ -> failwith "Error extract_bin_ins: inputs do not match." + | _ -> failwith "Error extract_bin_ins: inputs do not match." (* _________ Evaluation _________ *) @@ -41,58 +45,63 @@ let rec value circ concl = match get_op circ concl with | CIn i -> i | CShare | COut -> - let x = List.hd (get_inputs circ concl) in - value circ x + let x = List.hd (get_inputs circ concl) in + value circ x | CAnd -> - let (x, y) = extract_bin_ins (get_inputs circ concl) in - let vx = value circ x in - let vy = value circ y in - min vx vy + let (x, y) = twinhd (get_inputs circ concl) in + let vx = value circ x in + let vy = value circ y in + min vx vy | COr -> - let (x, y) = extract_bin_ins (get_inputs circ concl) in - let vx = value circ x in - let vy = value circ y in - max vx vy + let (x, y) = twinhd (get_inputs circ concl) in + let vx = value circ x in + let vy = value circ y in + max vx vy | CNeg -> - let x = List.hd (get_inputs circ concl) in - let vx = value circ x in - 1 - vx + let x = List.hd (get_inputs circ concl) in + let vx = value circ x in + 1 - vx let rec eval (circ : circuit) : int = let (_, _, concl) = List.hd (List.filter (fun (_, o, _) -> o = COut) circ) - in value circ concl + in value circ (List.hd concl) (* _________ Examples _________ *) -let make_gate ins op id : gate = (ins, op, id) -let make_input value id : gate = ([], CIn value, id) +let make_gate ins op outs : gate = (ins, op, outs) +let make_input value outs : gate = ([], CIn value, outs) let make_and_circ x y : circuit = [ - make_input x 0; - make_input y 1; - make_gate [0;1] CAnd 2; - make_gate [2] COut 3 + make_input x [0]; + make_input y [1]; + make_gate [0;1] CAnd [2]; + make_gate [2] COut [3] ] let make_or_circ x y : circuit = [ - make_input x 0; - make_input y 1; - make_gate [0;1] COr 2; - make_gate [2] COut 3 + make_input x [0]; + make_input y [1]; + make_gate [0;1] COr [2]; + make_gate [2] COut [3] ] let make_neg_circ x : circuit = [ - make_input x 0; - make_gate [0] CNeg 1; - make_gate [1] COut 2 + make_input x [0]; + make_gate [0] CNeg [1]; + make_gate [1] COut [2] ] (* corresponds to the excluded middle x v ~x *) let make_em_circ x : circuit = [ - make_input x 0; - make_gate [0] CShare 1; - make_gate [1] CNeg 2; - make_gate [1;2] COr 3; - make_gate [3] COut 4 -] \ No newline at end of file + make_input x [0]; + make_gate [0] CShare [1;2]; + make_gate [1] CNeg [3]; + make_gate [3;2] COr [4]; + make_gate [4] COut [5] +] + +let c1 = List.map eval [make_and_circ 0 0; make_and_circ 0 1; make_and_circ 1 0; make_and_circ 1 1] +let c2 = List.map eval [make_or_circ 0 0; make_or_circ 0 1; make_or_circ 1 0; make_or_circ 1 1] +let c3 = List.map eval [make_neg_circ 0; make_neg_circ 1] +let c4 = List.map eval [make_em_circ 0; make_em_circ 1] \ No newline at end of file diff --git a/ocaml/Resolution.ml b/ocaml/Resolution.ml index 01b1065..1fffd97 100644 --- a/ocaml/Resolution.ml +++ b/ocaml/Resolution.ml @@ -107,17 +107,20 @@ let print_dgraph dg = in print_string (aux dg);; (* _________ Examples _________ *) +let make_const_pol pol c = Func (c, pol, []) +let make_const c = make_const_pol Npol c + let y = Var("y") let x = Var("x") let z = Var("z") let r = Var("r") -let zero = Func("0", Npol, []) +let zero = make_const "0" let s x = Func("s", Npol, [x]) let add p x y z = Func("add", p, [x;y;z]) (* Convert int to term *) let rec enat i = - if i = 0 then Func("0", Npol, []) else s (enat (i-1)) + if i = 0 then zero else s (enat (i-1)) (* makes the constellation corresponding to an addition *) let make_const_add n m = diff --git a/ocaml/StellarCircuits.ml b/ocaml/StellarCircuits.ml new file mode 100644 index 0000000..92ca0e9 --- /dev/null +++ b/ocaml/StellarCircuits.ml @@ -0,0 +1,56 @@ +open Circuits +open Resolution + +(* ============================================ + Stellar Circuits + ============================================ *) + +let port pol i v = Func ("c"^(string_of_int i), pol, v) +let inport i x = port Neg i [Var x] +let outport i x = port Pos i [Var x] + +let call_cneg pol arg res = Func ("neg", pol, [arg; res]) +let call_cand pol arg1 arg2 res = Func ("and", pol, [arg1; arg2; res]) +let call_cor pol arg1 arg2 res = Func ("or", pol, [arg1; arg2; res]) + +let star_of_gate circ (ins, op, outs) = + match op with + | CIn i -> [port Neg (List.hd outs) [make_const (string_of_int i)]] + | COut -> [outport (List.hd ins) "r"; Var "r"] + | CShare -> + let (o1, o2) = twinhd outs in + [inport (List.hd ins) "x"; outport o1 "x"; outport o2 "x"] + | CNeg -> [ + inport (List.hd ins) "x"; + call_cneg Neg (Var "x") (Var "r"); + outport (List.hd outs) "r" + ] + | CAnd -> + let (i1, i2) = twinhd ins in [ + inport i1 "x"; + inport i2 "y"; + call_cand Neg (Var "x") (Var "y") (Var "r"); + outport (List.hd outs) "r" + ] + | COr -> + let (i1, i2) = twinhd ins in [ + inport i1 "x"; + inport i2 "y"; + call_cor Neg (Var "x") (Var "y") (Var "r"); + outport (List.hd outs) "r" + ] + +let const_of_circuit (circ : circuit) = List.map (star_of_gate circ) circ + +let prop_logic : constellation = [ + [call_cneg Pos (make_const "0") (make_const "1")]; + [call_cneg Pos (make_const "1") (make_const "0")]; + [call_cand Pos (make_const "0") (make_const "0") (make_const "0")]; + [call_cand Pos (make_const "0") (make_const "1") (make_const "0")]; + [call_cand Pos (make_const "1") (make_const "0") (make_const "0")]; + [call_cand Pos (make_const "1") (make_const "1") (make_const "1")]; + [call_cor Pos (make_const "0") (make_const "0") (make_const "0")]; + [call_cor Pos (make_const "0") (make_const "1") (make_const "1")]; + [call_cor Pos (make_const "1") (make_const "0") (make_const "1")]; + [call_cor Pos (make_const "1") (make_const "1") (make_const "1")] +] \ No newline at end of file diff --git a/ocaml/StellarFSA.ml b/ocaml/StellarFSA.ml new file mode 100644 index 0000000..9954635 --- /dev/null +++ b/ocaml/StellarFSA.ml @@ -0,0 +1,15 @@ +open Resolution +open FSA + +(* ============================================ + Stellar Automata + ============================================ *) + +let dot x y = Func ("ยท", Npol, [x; y]) + +let const_of_word (w : char list) = + let rec aux = function + | [] -> Func ("", Npol, []) + | c::w -> + dot (Func (String.make 1 c, Npol, [])) (aux w) + in [Func ("i", Pos, [aux w])] \ No newline at end of file From 8db9e5a201189965ad176b6f6196f28fddd766fe Mon Sep 17 00:00:00 2001 From: engboris Date: Sun, 1 May 2022 17:21:13 +0200 Subject: [PATCH 2/2] Fix polarities in StellarCircuits --- ocaml/StellarCircuits.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ocaml/StellarCircuits.ml b/ocaml/StellarCircuits.ml index 92ca0e9..4717ebb 100644 --- a/ocaml/StellarCircuits.ml +++ b/ocaml/StellarCircuits.ml @@ -15,8 +15,8 @@ let call_cor pol arg1 arg2 res = Func ("or", pol, [arg1; arg2; res]) let star_of_gate circ (ins, op, outs) = match op with - | CIn i -> [port Neg (List.hd outs) [make_const (string_of_int i)]] - | COut -> [outport (List.hd ins) "r"; Var "r"] + | CIn i -> [port Pos (List.hd outs) [make_const (string_of_int i)]] + | COut -> [inport (List.hd ins) "r"; Var "r"] | CShare -> let (o1, o2) = twinhd outs in [inport (List.hd ins) "x"; outport o1 "x"; outport o2 "x"]