Implement entities database and auditor

GNUmakefile

@@ -47,25 +47,27 @@ DafnyPipeline = $(dafny_Source)/Dafny/DafnyPipeline
 DafnyAST = $(dafny_Source)/Dafny/AST/DafnyAst
 DafnyRuntime := $(dafny_Source)/DafnyRuntime/DafnyRuntime.cs
 
-dafny := dotnet run --project $(DafnyDriver).csproj $(DAFNY_DOTNET_RUN_FLAGS) --
-dafny_codegen := $(dafny) -spillTargetCode:3 -compile:0 -noVerify -useRuntimeLib
-dafny_typecheck := $(dafny) -dafnyVerify:0
-dafny_verify := $(dafny) -compile:0  -trace -verifyAllModules -showSnippets:1 -vcsCores:8
+DAFNY ?= dotnet run --project $(DafnyDriver).csproj $(DAFNY_DOTNET_RUN_FLAGS) --
+dafny_codegen := $(DAFNY) -spillTargetCode:3 -compile:0 -noVerify -useRuntimeLib
+dafny_typecheck := $(DAFNY) -dafnyVerify:0
+dafny_verify := $(DAFNY) -compile:0  -trace -verifyAllModules -showSnippets:1 -vcsCores:8
 
 # Project files
 # =============
 
 # Subprojects
 csharp := src/Backends/CSharp
 repl := src/REPL
+auditor := src/Tools/Auditor
 
 # Binaries
 plugin_dll := $(csharp)/bin/Debug/net6.0/CSharpCompiler.dll
 repl_dll := $(repl)/bin/Release/net6.0/REPL.dll
-dlls := $(plugin_dll) $(repl_dll)
+auditor_dll := $(auditor)/bin/Debug/net6.0/DafnyAuditor.dll
+dlls := $(plugin_dll) $(repl_dll) $(auditor_dll)
 
 # Entry points
-dfy_entry_points := $(repl)/Repl.dfy $(csharp)/Compiler.dfy
+dfy_entry_points := $(repl)/Repl.dfy $(csharp)/Compiler.dfy $(auditor)/Auditor.dfy
 cs_entry_points := $(dfy_entry_points:.dfy=.cs)
 cs_roots := $(dir $(cs_entry_points))
 cs_objs := $(cs_roots:=bin) $(cs_roots:=obj)
@@ -103,10 +105,18 @@ $(csharp)/Compiler.cs: $(csharp)/Compiler.dfy $(dfy_models) $(dfy_interop) $(Daf
 	sed -i.bak -e 's/__AUTOGEN__//g' "$@"
 	rm "[email protected]" # https://stackoverflow.com/questions/4247068/
 
+$(auditor)/Auditor.cs: $(auditor)/Auditor.dfy $(dfy_models) $(dfy_interop) $(DafnyRuntime)
+	$(dafny_codegen) $< || true
+	sed -i.bak -e 's/__AUTOGEN__//g' "$@"
+	rm "[email protected]" # https://stackoverflow.com/questions/4247068/
+
 # Compile the resulting C# code
 $(plugin_dll): $(csharp)/Compiler.cs $(cs_interop)
 	dotnet build $(csharp)/CSharpCompiler.csproj
 
+$(auditor_dll): $(auditor)/Auditor.cs $(auditor)/EntryPoint.cs $(cs_interop)
+	dotnet build $(auditor)/DafnyAuditor.csproj
+
 # Run it on tests
 test/%.cs: test/%.dfy $(plugin_dll) $(DafnyRuntime)
 	$(dafny_codegen) -plugin:$(plugin_dll) -compileTarget:cs "$<"
@@ -129,6 +139,8 @@ tests: $(cs_tests)
 repl: $(repl_dll) FORCE
 	dotnet exec $<
 
+auditor: $(auditor_dll) FORCE
+
 typecheck:
 	$(dafny_typecheck) $(dfy_entry_points)