Integrate Coq fixes

cmd/vplogic/coq.go

@@ -48,7 +48,7 @@ func coqModel(m Model, valKnowledgeMap *KnowledgeMap) (string, error) {
 		blocksByPhase[block.Phase.Number] = append(blocksByPhase[block.Phase.Number], block)
 	}
 	for i, phase := range blocksByPhase {
-		output = append(output, fmt.Sprintf("Definition phase_%d := [", i))
+		output = append(output, fmt.Sprintf("Definition phase_%d : list block := [", i))
 		output, err = coqBlockByPhase(valKnowledgeMap, phase, output)
 		if err != nil {
 			return "", err
@@ -144,6 +144,7 @@ func coqPrincipal(block Block, valKnowledgeMap *KnowledgeMap) (string, error) {
 			default:
 				for _, c := range expression.Constants {
 					var crc string
+					expressions = append(expressions, fmt.Sprintf("(* knows %s *)", c.Name))
 					crc, err = coqResolveConstant(c, valKnowledgeMap)
 					switch expression.Qualifier {
 					case typesEnumPrivate:
@@ -164,6 +165,7 @@ func coqPrincipal(block Block, valKnowledgeMap *KnowledgeMap) (string, error) {
 		case typesEnumGenerates:
 			for _, c := range expression.Constants {
 				var crv string
+				expressions = append(expressions, fmt.Sprintf("(* generates %s *)", c.Name))
 				crv, err = coqResolveConstant(c, valKnowledgeMap)
 				expressions = append(expressions, fmt.Sprintf(
 					"EXP generation private %s unleaked;", crv,
@@ -172,13 +174,17 @@ func coqPrincipal(block Block, valKnowledgeMap *KnowledgeMap) (string, error) {
 		case typesEnumLeaks:
 			for _, c := range expression.Constants {
 				var crc string
+				expressions = append(expressions, fmt.Sprintf("(* leaks %s *)", c.Name))
 				crc, err = coqResolveConstant(c, valKnowledgeMap)
 				expressions = append(expressions, fmt.Sprintf(
-					"EXP knows public %s leaked;", crc,
+					"EXP knowledge public %s leaked;", crc,
 				))
 			}
 		case typesEnumAssignment:
 			var cae []string
+			for _, c := range expression.Constants {
+				expressions = append(expressions, fmt.Sprintf("(* assigns to %s *)", c.Name))
+			}
 			cae, err = coqAssignmentExpression(expression, valKnowledgeMap)
 			expressions = append(expressions, cae...)
 		}

cmd/vplogic/libcoq.go

@@ -503,17 +503,17 @@ var libcoq = strings.Join([]string{
 	"      end",
 	"  end.",
 	"",
-	"Fixpoint absorb_principal (p: principal) : list value :=",
+	"Definition absorb_principal (p: principal) : list value :=",
 	"  match p with",
 	"  | PRINCIPAL _ pk => merge_lists (absorb_expression pk) (absorb_passwords_expression pk)",
 	"end.",
 	"",
-	"Fixpoint absorb_message (m: message) : value :=",
+	"Definition absorb_message (m: message) : value :=",
 	"  match m with",
 	"  | MSG _ val => val",
 	"end.",
 	"",
-	"Fixpoint absorb_block (b: block) : list value :=",
+	"Definition absorb_block (b: block) : list value :=",
 	"  match b with",
 	"    | pblock p => absorb_principal p",
 	"    | mblock m => [absorb_message m]",
@@ -1662,7 +1662,7 @@ var libcoq = strings.Join([]string{
 	"    | confidentiality v => shallow_search l v",
 	"  end.",
 	"",
-	"Fixpoint recompose (l: list value) (v: value) : list value :=",
+	"Definition recompose (l: list value) (v: value) : list value :=",
 	"  match ((shallow_search l (prim(SHAMIR_SPLIT1 v)) && shallow_search l (prim(SHAMIR_SPLIT2 v)))",
 	"    || (shallow_search l (prim(SHAMIR_SPLIT1 v)) && shallow_search l (prim(SHAMIR_SPLIT3 v)))",
 	"    || (shallow_search l (prim(SHAMIR_SPLIT2 v)) && shallow_search l (prim(SHAMIR_SPLIT3 v))) ",

internal/libcoq/libcoqtemplate.v

@@ -494,17 +494,17 @@ Fixpoint absorb_passwords_expression (l: list expression) : list value :=
       end
   end.
 
-Fixpoint absorb_principal (p: principal) : list value :=
+Definition absorb_principal (p: principal) : list value :=
   match p with
   | PRINCIPAL _ pk => merge_lists (absorb_expression pk) (absorb_passwords_expression pk)
 end.
 
-Fixpoint absorb_message (m: message) : value :=
+Definition absorb_message (m: message) : value :=
   match m with
   | MSG _ val => val
 end.
 
-Fixpoint absorb_block (b: block) : list value :=
+Definition absorb_block (b: block) : list value :=
   match b with
     | pblock p => absorb_principal p
     | mblock m => [absorb_message m]
@@ -1653,7 +1653,7 @@ Definition resolve_query (q: query) (l: list value) : bool :=
     | confidentiality v => shallow_search l v
   end.
 
-Fixpoint recompose (l: list value) (v: value) : list value :=
+Definition recompose (l: list value) (v: value) : list value :=
   match ((shallow_search l (prim(SHAMIR_SPLIT1 v)) && shallow_search l (prim(SHAMIR_SPLIT2 v)))
     || (shallow_search l (prim(SHAMIR_SPLIT1 v)) && shallow_search l (prim(SHAMIR_SPLIT3 v)))
     || (shallow_search l (prim(SHAMIR_SPLIT2 v)) && shallow_search l (prim(SHAMIR_SPLIT3 v)))