Skip to content

Commit 49b9726

Browse files
jameyhicksjameyhicks
committed
proved a theorem about a BSV function.
1 parent f687e60 commit 49b9726

File tree

7 files changed

+85
-43
lines changed

7 files changed

+85
-43
lines changed

Diff for: ‎java/BSVToKami.java

+35-23
Original file line numberDiff line numberDiff line change
@@ -124,14 +124,16 @@ public class BSVToKami extends BSVBaseVisitor<Void>
124124
public Void visitPackagedef(BSVParser.PackagedefContext ctx) {
125125
logger.fine("Package " + pkgName);
126126

127-
printstream.println("Require Import Bool String List.");
127+
printstream.println("Require Import Bool String List Arith.");
128128
printstream.println("Require Import Kami.");
129129
printstream.println("Require Import Lib.Indexer.");
130+
printstream.println("Require Import Bsvtokami.");
130131
printstream.println("");
131132
printstream.println("Require Import FunctionalExtensionality.");
132133
printstream.println("");
133134
printstream.println("Set Implicit Arguments.");
134135
printstream.println("");
136+
printstream.println();
135137

136138
scope = scopes.pushScope(ctx);
137139

@@ -337,36 +339,38 @@ BSVParser.CallexprContext getCall(ParserRuleContext ctx) {
337339
@Override public Void visitFunctiondef(BSVParser.FunctiondefContext ctx) {
338340
scope = scopes.pushScope(ctx);
339341
BSVParser.FunctionprotoContext functionproto = ctx.functionproto();
340-
printstream.print(String.format("Definition %s (", functionproto.name.getText()));
342+
printstream.print(String.format("Definition %s", functionproto.name.getText()));
341343
if (functionproto.methodprotoformals() != null) {
342-
String sep = "";
343344
for (BSVParser.MethodprotoformalContext formal: functionproto.methodprotoformals().methodprotoformal()) {
344345
BSVParser.BsvtypeContext bsvtype = formal.bsvtype();
345346
String varName = formal.name.getText();
346-
printstream.print(sep + varName + ": " + bsvTypeToKami(bsvtype));
347-
sep = ", ";
347+
printstream.print(String.format(" (%s: %s)", varName, bsvTypeToKami(bsvtype)));
348348
}
349349
}
350350
String returntype = (functionproto.bsvtype() != null) ? bsvTypeToKami(functionproto.bsvtype()) : "";
351-
printstream.println(String.format(") : %s := ", returntype));
351+
printstream.println(String.format(": %s := ", returntype));
352352

353353
RegReadVisitor regReadVisitor = new RegReadVisitor(scope);
354-
for (BSVParser.StmtContext stmt: ctx.stmt())
355-
regReadVisitor.visit(stmt);
356-
if (ctx.expression() != null)
354+
if (ctx.expression() != null) {
355+
printstream.print(" ");
357356
regReadVisitor.visit(ctx.expression());
358357

359-
for (Map.Entry<String,BSVType> entry: regReadVisitor.regs.entrySet()) {
360-
String regName = entry.getKey();
361-
printstream.println(" Read " + regName + "_v : " + bsvTypeToKami(entry.getValue()) + " <- \"" + regName + "\";");
362-
}
363-
for (BSVParser.StmtContext stmt: ctx.stmt())
364-
visit(stmt);
365358
if (ctx.expression() != null)
366359
visit(ctx.expression());
360+
} else {
367361

368-
if (returntype.equals("Action") || returntype.equals("Void"))
369-
printstream.println(" Retv");
362+
for (Map.Entry<String,BSVType> entry: regReadVisitor.regs.entrySet()) {
363+
String regName = entry.getKey();
364+
printstream.println(" Read " + regName + "_v : " + bsvTypeToKami(entry.getValue()) + " <- \"" + regName + "\";");
365+
}
366+
for (BSVParser.StmtContext stmt: ctx.stmt())
367+
regReadVisitor.visit(stmt);
368+
for (BSVParser.StmtContext stmt: ctx.stmt())
369+
visit(stmt);
370+
371+
if (returntype.equals("Action") || returntype.equals("Void"))
372+
printstream.println(" Retv");
373+
}
370374
printstream.println(".");
371375
printstream.println("");
372376
scope = scopes.popScope();
@@ -475,12 +479,16 @@ public Void visitPattern(BSVParser.PatternContext ctx) {
475479
@Override public Void visitBinopexpr(BSVParser.BinopexprContext expr) {
476480
if (expr.right != null) {
477481
printstream.print("(");
478-
if (expr.left != null)
479-
visit(expr.left);
480482
if (expr.op != null) {
481-
printstream.print(" " + expr.op.getText() + " ");
483+
String op = expr.op.getText();
484+
if (op.equals("<"))
485+
op = "bitlt";
486+
printstream.print(op);
482487
}
483-
488+
printstream.print(" ");
489+
if (expr.left != null)
490+
visit(expr.left);
491+
printstream.print(" ");
484492
visit(expr.right);
485493
printstream.print(")");
486494
} else {
@@ -601,11 +609,15 @@ public String bsvTypeToKami(BSVParser.BsvtypeContext t, int level) {
601609
return "<nulltype>";
602610
if (t.typeide() != null) {
603611
String kamitype = t.typeide().getText();
604-
if (kamitype.equals("Action"))
612+
if (kamitype.equals("Bit"))
613+
kamitype = "word";
614+
else if (kamitype.equals("Bool"))
615+
kamitype = "bool";
616+
else if (kamitype.equals("Action"))
605617
kamitype = "Void";
606618
for (BSVParser.BsvtypeContext p: t.bsvtype())
607619
kamitype += " " + bsvTypeToKami(p, 1);
608-
if (level > 0)
620+
if (t.bsvtype().size() > 0)
609621
kamitype = String.format("(%s)", kamitype);
610622
return kamitype;
611623
} else if (t.typenat() != null) {

Diff for: ‎prooftests/Bsvtokami.v

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
Require Import Bool Arith.
2+
3+
Definition bitlt (x : nat) (y: nat): bool := (Nat.ltb x y).

Diff for: ‎prooftests/Makefile

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
2+
KAMIDIR=../../kami
3+
4+
all: $(patsubst %.bsv, %.stamp, $(wildcard *.bsv))
5+
6+
%.stamp: %.bsv Bsvtokami.vo
7+
../bsvtokami $(*).bsv
8+
make $(*).vo
9+
make $(*)_proofs.vo
10+
touch .$(*).stamp
11+
12+
%.vo: %.v
13+
coqc -R $(KAMIDIR)/Kami Kami $<
14+
15+
16+
clean:
17+
rm -f .*.stamp *.vo *.glob *.pp .*.aux imports.dot

Diff for: ‎tests/lessthan.bsv renamed to ‎prooftests/lessthan.bsv

File renamed without changes.

Diff for: ‎tests/lessthan.v renamed to ‎prooftests/lessthan.v

+2-1
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,13 @@
11
Require Import Bool String List Arith.
22
Require Import Kami.
33
Require Import Lib.Indexer.
4+
Require Import Bsvtokami.
45

56
Require Import FunctionalExtensionality.
67

78
Set Implicit Arguments.
89

9-
Definition bitlt (x : nat) (y: nat): bool := (Nat.ltb x y).
10+
1011
Definition test_lt (a: (word 32)) (b: (word 32)): bool :=
1112
(bitlt #a #b).
1213

Diff for: ‎tests/lessthan_proofs.v renamed to ‎prooftests/lessthan_proofs.v

File renamed without changes.

Diff for: ‎tests/gcd.v

+28-19
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,21 @@
1-
Require Import Bool String List.
2-
Require Import Lib.CommonTactics Lib.ilist Lib.Word.
3-
Require Import Lib.Struct Lib.FMap Lib.StringEq Lib.Indexer.
4-
5-
Require Import Kami.Syntax Kami.Notations Kami.Semantics Kami.Wf.
6-
Require Import Kami.Inline Kami.InlineFacts.
7-
Require Import Kami.RefinementFacts Kami.Decomposition.
8-
Require Import Kami.Tactics.
1+
Require Import Bool String List Arith.
2+
Require Import Kami.
3+
Require Import Lib.Indexer.
4+
Require Import Bsvtokami.
95

106
Require Import FunctionalExtensionality.
117

128
Set Implicit Arguments.
139

10+
11+
Definition \$methodready (m: (word 1)): (word 0) :=
12+
Ret $1
13+
.
14+
15+
Definition \$finish: (word 0) :=
16+
Ret $1
17+
.
18+
1419
Section GCD.
1520
Variable moduleName: string.
1621
Local Notation "^ s" := (moduleName -- s) (at level 0).
@@ -21,27 +26,27 @@ Section GCD.
2126
with Rule ^"swap" :=
2227
Read m_v : Bit 32 <- ^"m";
2328
Read n_v : Bit 32 <- ^"n";
24-
Assert(((#n_v > #m_v) && (#m_v != $0)));
29+
Assert((&& (> #n_v #m_v) (!= #m_v $0)));
2530
Write ^"n" : Bit 32 <- #m_v;
2631
Write ^"m" : Bit 32 <- #n_v;
2732
Retv (* rule swap *)
2833

2934
with Rule ^"sub" :=
3035
Read m_v : Bit 32 <- ^"m";
3136
Read n_v : Bit 32 <- ^"n";
32-
Assert(((#n_v <= #m_v) && (#m_v != $0)));
33-
Write ^"m" : Bit 32 <- (#m_v - #n_v);
37+
Assert((&& (<= #n_v #m_v) (!= #m_v $0)));
38+
Write ^"m" : Bit 32 <- (- #m_v #n_v);
3439
Retv (* rule sub *)
3540

36-
with Method ^"set_n" (in_n: Bit 32) : Void :=
41+
with Method ^"set_n" (in_n: (word 32)) : Void :=
3742
Write ^"n" : Bit 32 <- #in_n;
3843
Retv
3944

40-
with Method ^"set_m" (in_m: Bit 32) : Void :=
45+
with Method ^"set_m" (in_m: (word 32)) : Void :=
4146
Write ^"m" : Bit 32 <- #in_m;
4247
Retv
4348

44-
with Method ^"result" () : Bit 32 :=
49+
with Method ^"result" () : (word 32) :=
4550
Read n_v : Bit 32 <- "n";
4651
Ret #n_v
4752

@@ -57,24 +62,28 @@ Section Main.
5762
Definition gcdset_n := MethodSig (^"gcd"--"set_n") () : Void.
5863
Definition mkMainModule := MODULE {
5964

60-
(* instantiate gcd *)
61-
Register ^"started" : Bit 1 <- $0
65+
Call gcd <- mkGCD(); (* method call 1 *)
66+
with Register ^"started" : Bit 1 <- $0
6267
with Register ^"dv" : Bit 32 <- $0
6368
with Rule ^"rl_start" :=
6469
Read started_v : Bit 1 <- ^"started";
65-
Assert((#started_v == $0));
70+
Assert((&& (&& (== #started_v $0) Call $methodready(#gcd); (* method call expr *)
71+
) Call $methodready(#gcd); (* method call expr *)
72+
));
6673
Call gcdset_n($100); (* method call expr *)
6774
Call gcdset_m($20); (* method call expr *)
6875
Write ^"started" : Bit 1 <- $1;
6976
Retv (* rule rl_start *)
7077

7178
with Rule ^"rl_display" :=
79+
Assert( Call $methodready(#gcd); (* method call expr *)
80+
);
7281
Write ^"dv" : Bit 32 <- Call gcdresult(); (* method call expr *)
7382
;
83+
Call $finish(); (* method call expr *)
7484
Retv (* rule rl_display *)
7585

7686
}. (*mkMain *)
7787

78-
Definition mkMainInstances := (mkGCD("gcd"))%kami.
79-
Definition mkMain := (mkMainInstances ++ mkMainModule)%kami.
88+
Definition mkMain := (mkMainModule)%kami.
8089
End Main.

0 commit comments

Comments
 (0)