Merge remote-tracking branch 'tmp-smol-bir/main'

examples/compute/.gitignore

@@ -0,0 +1,5 @@
+**/.HOLMK
+**/.holobjs
+**/.hollogs
+**/*Theory.sig
+**/*.exe

examples/compute/.holpath

@@ -0,0 +1 @@
+SMOLBIRDIR

examples/compute/Holmakefile

@@ -0,0 +1,11 @@
+CLINE_OPTIONS = -r
+
+INCLUDES = $(SMOLBIRDIR)/src/theory \
+					 $(SMOLBIRDIR)/test \
+					 $(SMOLBIRDIR)/examples \
+					 $(SMOLBIRDIR)/src/shared
+
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
+

examples/compute/README.md

@@ -0,0 +1,48 @@
+# Smol BIR
+
+This repository implements a fragment of the BIR language from [HolBA](https://github.com/kth-step/HolBA) using a evaluation relation in the theorem prover [HOL4](https://github.com/HOL-Theorem-Prover/HOL)
+
+## Overview of the repository's structure
+The structure of this repository is as follows :
+```
+├─ examples/ : Examples on BIR usage
+├─ src/ : source code of main theory
+│   ├─ shared/ : useful libraries regarding BIR (mainly evaluation)
+│   │   ├─ cv/ : Alternative BIR theory that can be used with cv_compute
+│   │   ├─ bir_computeLib.{sml|sig} : Library to compute BIR terms
+│   │   ├─ bir_cv_basicLib.{sml|sig} : Library to translate BIR terms to the cv equivalent theory
+│   │   ├─ bir_cv_envLib.{sml|sig} : Library to translate BIR environments to the cv equivalent theory
+│   │   └─ bir_cv_programLib.{sml|sig} : Library to translate BIR programs to the cv equivalent theory
+│   └─ theory/ : main BIR theories
+│       ├─ bir_basicScript.sml : Basic Datatypes required of BIR expressions
+│       ├─ bir_binexpScript.sml : Binary Expressions evaluation
+│       ├─ bir_binpredScript.sml : Binary Predicate evaluation
+│       ├─ bir_computeScript.sml : Computation function for BIR expressions
+│       ├─ bir_envScript.sml : Variable Environment
+│       ├─ bir_evalScript.sml : Evaluation relation for BIR expressions
+│       ├─ bir_ifthenelseScript.sml : If Then Else evaluation
+│       ├─ bir_memScript.sml : Memory evaluation
+│       ├─ bir_metaScript.sml : Proofs regarding BIR Meta-Theory
+│       ├─ bir_typingScript.sml : Typing system for BIR expressions
+│       └─ bir_unaryexpScript.sml : Unary Expressions evaluation
+└─ test/ : Sanity checks theorems and tests
+```
+
+Additional `README`s are available in other key directories.
+
+
+## Building
+With a valid HOL4 `trindemossen-1` installation, you can run `Holmake` in the root directory of the repository.
+Remark : Not all commits can be built as regular merge was used.
+Tags are usually used to indicate “stable” release that can be built without errors
+
+## Running the examples
+Examples have an executable generated when you run `Holmake` in the root directory. 
+You can run them either by running `Holmake test` in the directory or by executing the binary.
+These executables act as benchmarks. The size of the input is hard-coded in the associated Lib file, usually by a parameter called `n` at the beginning of the `benchmark` function
+
+## Status of code
+Currently, all pieces of code in the repository work. Here are some caveats :
+  - Using `cv_compute` on programs can lead to various speedups, both negative and positive
+  - Only a few operations (like Binary operations) were implemented
+  - Multi-stepping of programs is not implemented

examples/compute/REMARKS.md

@@ -0,0 +1,9 @@
+# Remarks
+
+Here are some various remarks about the project :
+  - The `eval` semantics of program isn’t clean.
+  - The conversions in `shared/bir_cv*Lib.sml` should create a theorem by using the input term. Here, we are creating the output theorem from the right side and rewriting it to make the input term appear (but there is no guarantee).
+  - Implementation in the actual HolBA project can be done in two ways :
+    - You either keep the project structure the same and add support for unimplemented operations in the `bir_cv` representation.
+    The representation of HolBA and the `compute` one here are really similar (to a few differences like enforcing typing in environment manipulation).
+    - The other way would be to change the BIR representation in HolBA and use the `bir_cv` representation instead. This would remove translation cost but a lot more rewriting would be necessary.

examples/compute/TODO.md

@@ -0,0 +1,39 @@
+## General
+- Tidy code 
+    - [x] Change indent to 2 spaces (or less for proofs)
+    - [x] Add semicolons at the end of statements
+    - [x] Clean double asterisks comment
+    - [x] Add a top level comment describing each files / theories
+    - Split into more directories
+        - [x] Create theories directory
+        - [x] Create example directories
+    - [x] Add `.holpath`
+- [ ] Begin presentation
+
+## Expression semantics
+- Add Examples
+
+- Benchmark examples
+    - [ ] `EVAL`
+    - [ ] `cv_eval` with the deep embedding translation
+
+- Tidy files
+    - [ ] Name variables (like in case split)
+
+- Add Memory expressions
+    - [x] Syntax
+    - [x] Semantics
+    - [x] Update proofs
+
+
+## Statements semantics
+- Add statement semantics
+    - [ ] Assign / Jumps
+    - [ ] Rest of the statements
+
+## Future
+- Try lifting
+    - Check `examples/riscv/isqrt` for reference cf `bir_isqrt_prog_def`
+    - Benchmark evaluation on those bigger programs
+- Check Quotation library and apply it to smol-bir
+    - Check `src/shared/bir_quotationLib.sml` and comments in it

examples/compute/examples/Holmakefile

@@ -0,0 +1,10 @@
+CLINE_OPTIONS = -r
+
+INCLUDES = $(SMOLBIRDIR)/examples/increment \
+					 $(SMOLBIRDIR)/examples/and_not \
+  				 $(SMOLBIRDIR)/examples/mem_incr \
+					 $(SMOLBIRDIR)/examples/sum_list \
+					 $(SMOLBIRDIR)/examples/jump_chain
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all

examples/compute/examples/and_not/Holmakefile

@@ -0,0 +1,4 @@
+INCLUDES = $(SMOLBIRDIR)/src/theory
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all

examples/compute/examples/and_not/ex_and_notScript.sml

@@ -0,0 +1,82 @@
+(* ------------------------------------------------------------------------- *)
+(*  Example regarding a function that AND two boolean and returns            *)
+(*  a variable or its negation                                               *)
+(* ------------------------------------------------------------------------- *)
+
+open HolKernel Parse boolLib bossLib ;
+open bir_basicTheory bir_envTheory ;
+open bir_binexpTheory bir_ifthenelseTheory bir_unaryexpTheory ;
+open bir_computeTheory ;
+open wordsLib ;
+
+
+val _ = new_theory "ex_and_not" ;
+
+(* The variables used in the condition. They will be booleans *)
+Definition var_cond1_def:
+  var_cond1 = BVar "r1"
+End
+
+Definition var_cond2_def:
+  var_cond2 = BVar "r2"
+End
+
+(* The variable we should return. Any size is fine *)
+Definition var_ret_def:
+  var_ret = BVar "r3"
+End
+
+(* Creates an environment where r1 is set to w *)
+Definition start_env_def:
+  start_env b1 b2 w = 
+  bir_env_update (bir_env_update 
+      (bir_env_update bir_empty_env var_ret (BVal_Imm (Imm64 w))) 
+    var_cond1 (BVal_Imm (bool2b b1))) var_cond2 (BVal_Imm (bool2b b2))
+End
+
+Definition and_not_exp_def:
+  and_not_exp = 
+      BExp_IfThenElse (BExp_BinExp BIExp_And (BExp_Den var_cond1) (BExp_Den var_cond2)) 
+        (BExp_Den var_ret) (BExp_UnaryExp BIExp_Not (BExp_Den var_ret))
+End
+
+
+(* ------------------------------------------------------------------------- *)
+(* ------------------------------- THEOREMS -------------------------------- *)
+(* ------------------------------------------------------------------------- *)
+
+Theorem lookup_start_env_var_ret:
+  !b1 b2 w. bir_env_lookup (start_env b1 b2 w) var_ret = SOME (BVal_Imm (Imm64 w))
+Proof
+  EVAL_TAC >>
+  METIS_TAC []
+QED
+
+
+Theorem lookup_start_env_var_cond1:
+  !b1 b2 w. bir_env_lookup (start_env b1 b2 w) var_cond1 = SOME (BVal_Imm (bool2b b1))
+Proof
+  EVAL_TAC >>
+  METIS_TAC []
+QED
+
+Theorem lookup_start_env_var_cond2:
+  !b1 b2 w. bir_env_lookup (start_env b1 b2 w) var_cond2 = SOME (BVal_Imm (bool2b b2))
+Proof
+  EVAL_TAC >>
+  METIS_TAC []
+QED
+
+
+Theorem and_not_exp_correct:
+  !b1 b2 w. bir_compute_exp and_not_exp (start_env b1 b2 w) = 
+    SOME (BVal_Imm (Imm64 (if b1 /\ b2 then w else ~w)))
+Proof
+  Cases_on `b1` >> Cases_on `b2` >>
+      EVAL_TAC >>
+      METIS_TAC []
+QED
+
+
+
+val _ = export_theory () ;

examples/compute/examples/increment/Holmakefile

@@ -0,0 +1,14 @@
+INCLUDES = $(SMOLBIRDIR)/src/theory \
+					 $(SMOLBIRDIR)/src/shared
+
+all: $(DEFAULT_TARGETS) test-increment.exe
+.PHONY: all
+
+
+test-increment.exe: test-increment.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test: test-increment.exe
+	./test-increment.exe
+
+EXTRA_CLEANS = test-increment.exe

examples/compute/examples/increment/ex_incrementLib.sig

@@ -0,0 +1,9 @@
+signature ex_incrementLib =
+sig
+
+  include Abbrev ;
+
+  val generate_bigger_inc : term -> int -> term ;
+  val benchmark : unit -> unit ;
+
+end

examples/compute/examples/increment/ex_incrementLib.sml

@@ -0,0 +1,59 @@
+(* ------------------------------------------------------------------------- *)
+(*  Library for benchmarking increment example                               *)
+(* ------------------------------------------------------------------------- *)
+
+structure ex_incrementLib :> ex_incrementLib =
+struct
+
+open HolKernel Parse bossLib boolLib;
+open bir_basicTheory ;
+open ex_incrementTheory ;
+open bir_computeLib ;
+
+
+fun generate_bigger_inc (term:term) (n:int) : term =
+  if n = 0 then term else 
+    generate_bigger_inc ``BExp_BinExp BIExp_Plus (^term) (^term)`` (n-1)
+
+fun power (x : int) (n : int) : int =
+  if n = 0 then 1
+  else 
+    if (n mod 2) = 0 then 
+      let val r = power x (n div 2) in r * r end
+    else
+      let val r = power x (n div 2) in r * r * x end
+
+
+
+fun benchmark () = 
+let
+  (* val n = power 2 4 ; *)
+  val n = 14 ;
+  val _ = print ("***** n : " ^ (Int.toString n) ^ " ***** \n") ;
+  val unamed_term = rhs (concl increment_exp_def) ;
+
+  val _ = print "Generating term...\n" ;
+  val big_term = time (generate_bigger_inc unamed_term) n ;
+  val _ = print "Finished generating !\n" ;
+
+  val _ = print "Creating big_term definition...\n" ;
+  val exp_def = time (xDefine "big_term") `big_term = ^big_term` ;
+  val env = ``start_env 3w`` ;
+
+  val _ = print "Starting measurements...\n" ;
+  val _ = print "EVAL measurement...\n" ;
+  val eval_value = time (compute_exp_EVAL ``big_term``) env ;
+
+  val _ = print "cv measurement...\n" ;
+  val _ = translate_exp_cv exp_def ;
+  val cv_value = time (compute_exp_cv exp_def) env ;
+
+  val _ = assert (fn x => (Term.compare (x, (rhs (concl cv_value))) = EQUAL)) (rhs (concl eval_value ))
+in 
+  ()
+end
+
+
+
+
+end

examples/compute/examples/increment/ex_incrementScript.sml

@@ -0,0 +1,45 @@
+(* ------------------------------------------------------------------------- *)
+(*  Example regarding a function that increments a variable in the env       *)
+(* ------------------------------------------------------------------------- *)
+
+open HolKernel Parse boolLib bossLib ;
+open bir_basicTheory bir_envTheory ;
+open bir_binexpTheory ;
+open bir_computeTheory ;
+
+
+val _ = new_theory "ex_increment";
+
+Definition reg_var_def:
+  reg_var = BVar "r1"
+End
+
+(* Creates an environment where r1 is set to w *)
+Definition start_env_def:
+  start_env w = bir_env_update bir_empty_env reg_var (BVal_Imm (Imm64 w))
+End
+
+Definition increment_exp_def:
+  increment_exp = 
+    BExp_BinExp BIExp_Plus
+      (BExp_Den reg_var)
+      (BExp_Const (Imm64 1w))
+End
+
+
+Theorem increment_exp_correct:
+  !w. bir_compute_exp increment_exp (start_env w) = SOME (BVal_Imm (Imm64 (w + 1w)))
+Proof
+  rw [bir_compute_exp_def, increment_exp_def] >>
+
+  rw [bir_env_lookup_def, start_env_def] >>
+  rw [bir_env_lookup_update] >>
+
+  rw [bir_compute_binexp_def, bir_compute_binexp_imm_def, bir_binexp_get_oper_def] >>
+  rw [val_from_imm_option_def]
+QED 
+
+
+
+
+val _ = export_theory () ;

examples/compute/examples/increment/test-increment.sml

@@ -0,0 +1,3 @@
+open ex_incrementLib ;
+
+val _ = benchmark () ;

examples/compute/examples/jump_chain/Holmakefile

@@ -0,0 +1,14 @@
+INCLUDES = $(SMOLBIRDIR)/src/theory \
+					 $(SMOLBIRDIR)/src/shared
+
+all: $(DEFAULT_TARGETS) test-jump-chain.exe
+.PHONY: all
+
+
+test-jump-chain.exe: test-jump-chain.uo
+	$(HOLMOSMLC) -o $@ $<
+
+test: test-jump-chain.exe
+	./test-jump-chain.exe
+
+EXTRA_CLEANS = test-jump-chain.exe

examples/compute/examples/jump_chain/ex_jump_chainLib.sig

@@ -0,0 +1,6 @@
+signature ex_jump_chainLib = sig
+
+  val  benchmark_one_step : unit -> unit ;
+
+
+end