forge/domains/abac updates, fix import namespace clash, misc improvem…

…ents (#291) (#292)

* Refactor ABAC language to use a .frg domain model that can be extended into an assignment
none inferred multiplicity is no longer set
* Somewhat improved Froglet errors in narrow cases, re-enabled corresponding test cases
* Fix issue recently introduced where using a Forge internal ID as a sig, field, etc. name would cause an error, but only if the file making the definition was imported into another.
* Minor fixes (e.g., License registration for Racket package server)

forge/breaks.rkt

@@ -9,7 +9,8 @@
                          set-subtract! set-map list->mutable-set set-remove! append* set-member?
                          set-empty? set-union! drop-right take-right for/set for*/set filter-not
                          second set-add match identity)
-         racket/contract)
+         racket/contract
+         racket/hash)
 (require (only-in forge/shared get-verbosity VERBOSITY_HIGH))
 
 (provide constrain-bounds (rename-out [break-rel break]) break-bound break-formulas)
@@ -204,7 +205,7 @@
         (define break-key
             (cond [(symbol? break) break]
                   [(@node/breaking/break? break) (@node/breaking/break-break break)]
-                  [else (raise-user-error (format "Not a valid break name: ~a~n" break))]))
+                  [else (@raise-forge-error #:msg (format "Not a valid break name: ~a~n" break) #:context #f)]))
         (unless (hash-has-key? strategies break-key)
                 (error (format "break not implemented among ~a" strategies) break-key))
         (hash-add! rel-breaks rel break)
@@ -254,7 +255,7 @@
 
     (for ([bound total-bounds])
         ; get declared breaks for the relation associated with this bound        
-        (define rel (bound-relation bound))
+        (define rel (bound-relation bound))        
         (define breaks (hash-ref rel-breaks rel (set)))        
         (define break-pris (hash-ref rel-break-pri rel (make-hash)))
         ; compose breaks
@@ -264,6 +265,9 @@
         (cond [(set-empty? breaks)
             (unless defined (cons! new-total-bounds bound))
         ][else
+            (unless (hash-has-key? relations-store rel)
+              (@raise-forge-error #:msg (format "Attempted to set or modify bounds of ~a, but the annotation given was of the wrong form (sig vs. field).~n" rel)
+                                 #:context #f))
             (define rel-list (hash-ref relations-store rel))
             (define atom-lists (map (λ (b) (hash-ref bounds-store b)) rel-list))
 
@@ -272,8 +276,8 @@
                 (define break-sym
                     (cond [(symbol? break) break]
                           [(@node/breaking/break? break) (@node/breaking/break-break break)]
-                          [else (raise-user-error (format "constrain-bounds: not a valid break name: ~a~n"
-                                                          break))]))
+                          [else (@raise-forge-error #:msg (format "constrain-bounds: not a valid break name: ~a~n" break)
+                                                   #:context #f)]))
                 (define loc (if (@node? break) 
                                 (@nodeinfo-loc (@node-info break)) 
                                 #f))

forge/domains/abac/abac.frg

@@ -0,0 +1,90 @@
+#lang forge/froglet 
+
+/*
+    Domain model for attribute-based access control, specialized to the setting of the 
+    Logic for systems ABAC homework. This file is imported by the runner for the 
+    #lang forge/domains/abac DSL. 
+*/
+
+///////////////////////
+// Datatype definitions 
+///////////////////////
+
+// We'll model booleans as presence/non-presence of an entry in a partial function.
+one sig True {}
+// Notice that there's no "one sig False {}". One reason is that it's not necessary. 
+// But a better reason is that if we have False we'd need _total_, not partial, functions,
+// which would make writing concrete examples more verbose. 
+
+// Components of requests (S, A, R)
+sig Subject, Action, Resource {}
+
+// Subjects: the entity requesting access
+sig Customer extends Subject {}
+sig Employee extends Subject {
+  // Notice we don't say "one Boolean" here.
+  // We *could*, but in *this* specific example it might make testing more elaborate. 
+  training: lone True 
+}
+sig Accountant, Admin extends Employee {}
+
+// Actions: the nature of the access
+sig Read, Write extends Action {}
+
+// Resources: the target of the requested access
+sig File extends Resource {
+    // Every File is owned by some entity. Note that we don't allow shared ownership.
+    owner: one Subject,
+    // Every file is under audit or not. Again, notice that we don't say "one Boolean".
+    audit: lone True
+}
+
+// This model works with a single request at a time
+one sig Request {
+    // Every request has a single subject, action, and resource.
+    reqS: one Subject,
+    reqA: one Action,
+    reqR: one Resource
+}
+
+///////////////////////
+// Policy predicates
+///////////////////////
+
+// These are currently all done in the parser/expander for #lang forge/domains/abac
+// But let's try to approximate them in Froglet! Here are two very basic policies:
+
+/*
+policy original
+  permit if: s is admin, a is read, r is file.
+end;
+
+policy modified
+  permit if: s is admin, a is read, r is file.
+  deny if: s is accountant, a is write.
+  permit if: s is accountant, a is read, r is under-audit.
+end;
+*/
+
+pred original_permits_request {
+  // TASK: write a constraint that evaluates to true exactly when the 'original'
+  // policy would permit the request.
+
+  // FILL
+}
+
+pred modified_permits_request {
+  // TASK: write a constraint that evaluates to true exactly when the 'modified'
+  // policy would permit the request.
+
+  // FILL
+}
+
+// This won't run when the file is imported by the abac language. It will only 
+// run (and load the visualizer) if the Forge file is run directly.
+difference_original_modified: run {
+  // TASK: write a constraint that evaluates to true exactly when the two policies
+  // disagree on permitting some request. 
+
+  // FILL
+}

forge/domains/abac/helpers.rkt

@@ -2,7 +2,18 @@
 
 (require (only-in racket remove-duplicates flatten last))
 (require forge/domains/abac/lexparse) 
-(provide (all-defined-out))
+
+; Import the domain model. This contains sig and field definitions.
+(require "abac.frg")
+
+(provide build-rule-matches
+         build-condition
+         apply-quantifiers
+         condition->atomic-fmla
+         rel->unary 
+         list->product
+         (struct-out atomic-fmla)
+         (all-from-out "abac.frg"))
 
 ; Build a formula that is true IFF this rule matches
 (define (build-rule-matches r request-vars relations var->maybe-skolem)
@@ -12,7 +23,7 @@
                                          (append (extract-atomic-formulas-rule r))))))
   (define to-quantify (filter (lambda (v) (equal? #f (member v request-vars))) vars-used))
   ;(printf "to quantify: ~a~n" to-quantify)
-  (define basef (&& (map (lambda (rc) (build-condition rc relations var->maybe-skolem)) (rule-conditions r))))
+  (define basef (&& (map (lambda (rc) (build-condition relations var->maybe-skolem rc)) (rule-conditions r))))
   (apply-quantifiers to-quantify basef))
 
 ; Datatype to represent an atomic formula
@@ -29,12 +40,15 @@
                               (policy-rules pol))))
 
 ; Build a formula (Forge AST) for a specific rule condition given by the parser
-(define (build-condition c relations var->maybe-skolem)
+(define (build-condition relations var->maybe-skolem c)
+  (define args (condition-args c))
   (cond [(condition-sign c)
-         (in (list->product (map var->maybe-skolem (condition-args c)))
+         ; Build positive Forge literal formula 
+         (in (list->product (map var->maybe-skolem args))
              (rel->unary (hash-ref relations (string-titlecase (symbol->string (condition-pred c))))))]
         [else
-         (! (build-condition (condition #t (condition-pred c) (condition-args c)) relations var->maybe-skolem))]))
+         ; Build negative Forge literal formula
+         (! (build-condition relations var->maybe-skolem (condition #t (condition-pred c) args)))]))
 
 (define (apply-quantifiers todo f)
   (if (empty? todo)
@@ -46,15 +60,12 @@
 (define (list->product l)
   (foldl (lambda (i acc) (-> acc i)) (first l) (rest l)))
 
-; Mechanism for building subsets of a sig (which might overlap) in forge/core
-(sig True #:one)
-
 ; Replace a 2+-ary relation that has a "fake" column on True with (join R True)
 (define (rel->unary r)
   (define types ((relation-typelist-thunk r)))
   (cond [(and (node/expr/relation? r) 
               (> (node/expr-arity r) 1)
               (equal? "True" (last types)))
-              (join r True)]
+         (join r True)]
         [else r]))
 

forge/domains/abac/lexparse.rkt

@@ -157,7 +157,7 @@
 (define allowed-relations-lc
   '("admin" "accountant" "customer"
             "read" "write" "file" "under-audit"
-            "owner-of" "in-training"))
+            "owned-by" "in-training"))
 
 (define (command-parser source-name)
 

forge/domains/abac/pretty-formatting.rkt

@@ -49,7 +49,12 @@
          (when msg
            (printf "~a~n" msg))
          ]
-        [else (printf "-----------------------------------~nNo scenario existed matching those conditions.~n")]))
+        [else 
+          (define sol (tree:get-value (forge:Run-result run)))
+
+          (when (and (Unsat? sol) (Unsat-core sol)) 
+                (printf "The solver had core-extraction enabled; printing core information.~n~a~n" sol (Unsat-core sol)))
+          (printf "-----------------------------------~nNo scenario existed matching those conditions.~n")]))
 
 (define (pretty-format-condition c)
   (define signis (cond [(condition-sign c) "is"]