Add Circuit model and examples

Author: Shreyas4991

Cslib.lean

@@ -9,6 +9,7 @@ public import Cslib.AlgorithmsTheory.Lean.TimeM
 public import Cslib.AlgorithmsTheory.LowerBounds.ComparisonSort
 public import Cslib.AlgorithmsTheory.Models.ListComparisonSearch
 public import Cslib.AlgorithmsTheory.Models.ListComparisonSort
+public import Cslib.AlgorithmsTheory.Models.NCCircuits
 public import Cslib.AlgorithmsTheory.QueryModel
 public import Cslib.Computability.Automata.Acceptors.Acceptor
 public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor

Cslib/AlgorithmsTheory/Algorithms/SingletapeTMAlgorithms/Basics.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026 Shreyas Srinivas. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Shreyas Srinivas, Eric WIeser
+Authors: Shreyas Srinivas, Alex Meiburg
 -/
 
 module

Cslib/AlgorithmsTheory/Models/NCCircuits.lean

@@ -11,6 +11,7 @@ public import CslibTests.HasFresh
 public import CslibTests.ImportWithMathlib
 public import CslibTests.LTS
 public import CslibTests.LambdaCalculus
+public import CslibTests.QueryModel.CircuitExamples
 public import CslibTests.QueryModel.ProgExamples
 public import CslibTests.QueryModel.QueryExamples
 public import CslibTests.Reduction

CslibTests.lean

@@ -14,7 +14,7 @@ public import Mathlib
 /-!
 # Examples of Progs for Circuits
 
-This file contains examples and tests of circuits written in the Prog Model
+This file contains examples and tests of fan-in 2 circuits written in the Prog Model
 -/
 namespace CslibTests
 
@@ -28,17 +28,17 @@ def exCircuit1 : Prog (Circuit Bool) Bool := do
   let w := mul 3 x y
   add 4 z w
 
-/--
-info: true
--/
-#guard_msgs in
-#eval exCircuit1.eval circModel
+-- /--
+-- info: true
+-- -/
+-- #guard_msgs in
+-- #eval exCircuit1.eval circModel
 
-/--
-info: { depth := 2, size := 5 }
--/
-#guard_msgs in
-#eval exCircuit1.time circModel
+-- /--
+-- info: { depth := 2, size := 5 }
+-- -/
+-- #guard_msgs in
+-- #eval exCircuit1.time circModel
 
 open Circuit in
 def exCircuit2 : Prog (Circuit ℚ) ℚ := do
@@ -47,35 +47,35 @@ def exCircuit2 : Prog (Circuit ℚ) ℚ := do
   let z := add 2 x y
   mul 4 z z
 
-/--
-info: 9
--/
-#guard_msgs in
-#eval exCircuit2.eval circModel
+-- /--
+-- info: 9
+-- -/
+-- #guard_msgs in
+-- #eval exCircuit2.eval circModel
 
-/--
-info: true
--/
-#guard_msgs in
-#eval exCircuit2.time circModel == ⟨2,4⟩
+-- /--
+-- info: true
+-- -/
+-- #guard_msgs in
+-- #eval exCircuit2.time circModel == ⟨2,4⟩
 
 open Circuit in
 def exCircuit3 (x y : Circuit ℚ ℚ) : Prog (Circuit ℚ) ℚ := do
   let z := add 2 x y
   let w := mul 3 x y
   mul 4 z w
 
-/--
-info: true
--/
-#guard_msgs in
-#eval (exCircuit3 (.const 0 (1 : ℚ)) (.const 1 (21 : ℚ))).eval circModel == 462
+-- /--
+-- info: true
+-- -/
+-- #guard_msgs in
+-- #eval (exCircuit3 (.const 0 (1 : ℚ)) (.const 1 (21 : ℚ))).eval circModel == 462
 
-/--
-info: true
--/
-#guard_msgs in
-#eval (exCircuit3 (.const 0 (1 : ℚ)) (.const 1 (21 : ℚ))).time circModel == ⟨2,5⟩
+-- /--
+-- info: true
+-- -/
+-- #guard_msgs in
+-- #eval (exCircuit3 (.const 0 (1 : ℚ)) (.const 1 (21 : ℚ))).time circModel == ⟨2,5⟩
 
 
 open Circuit in
@@ -90,17 +90,17 @@ def CircAnd (n : ℕ) (x : Fin n → Circuit Bool Bool) : Circuit Bool Bool :=
 def execCircAnd (x : Fin n → Circuit Bool Bool) : Prog (Circuit Bool) Bool := do
   CircAnd n x
 
-/--
-info: true
--/
-#guard_msgs in
-#eval (execCircAnd ![.const 0 true, .const 1 true, .const 2 true]).eval circModel == true
-
-/--
-info: true
--/
-#guard_msgs in
-#eval (execCircAnd ![.const 0 true, .const 1 true, .const 2 true]).time circModel == ⟨3,5⟩
+-- /--
+-- info: true
+-- -/
+-- #guard_msgs in
+-- #eval (execCircAnd ![.const 0 true, .const 1 true, .const 2 true]).eval circModel == true
+
+-- /--
+-- info: true
+-- -/
+-- #guard_msgs in
+-- #eval (execCircAnd ![.const 0 true, .const 1 true, .const 2 true]).time circModel == ⟨3,5⟩
 
 
 end CslibTests