protection-hooks

(in-package "ACL2S-HOOKS")

(include-book "canonical-print")

(include-book "categorize-input")

(include-book "hacking/hacker" :dir :system)

(include-book "hacking/defcode" :dir :system :ttags ((defcode)))

(include-book "hacking/redefun" :dir :system)

(include-book "hacking/rewrite-code" :dir :system)

(include-book "super-history" :ttags ((:acl2s-super-history) (defcode)))

(include-book "hacking/raw" :dir :system)

(program)

(set-state-ok t)

(defun acl2s-password-hash
  (password)
  (let ((n (+ 4984190985322139823307306678324857897
         (acl2-count password))))
    (mod (* n n)
      1976322537236016347623339359149920390129)))

(defun acl2s-passwordp
  (password state)
  (equal (acl2s-password-hash password)
    (@ acl2s-password)))

(defun acl2s-protection-begin
  (password state)
  (if (boundp-global 'acl2s-password
      state)
    (er soft
      'set-acl2s-password
      "Password already assigned.")
    (er-progn (assign acl2s-password
        (acl2s-password-hash password))
      (value :invisible))))

(defun clear-acl2s-password
  (password state)
  (if (boundp-global 'acl2s-password
      state)
    (if (acl2s-passwordp password
        state)
      (pprogn (makunbound-global 'acl2s-password
          state)
        (value :invisible))
      (er soft
        'clear-acl2s-password
        "Bad password given."))
    (value :invisible)))

(push-untouchable acl2s-password
  nil)

(defun acl2s-protected-modep
  (state)
  (boundp-global 'acl2s-password
    state))

(defun user-revert-super-history
  (n password state)
  (cond ((not (acl2s-passwordp password
         state)) (er soft
        'revert-super-history
        "Not authorized."))
    (t (revert-super-history n
        state))))

(push-untouchable (update-super-history restore-current-super-history
    revert-super-history)
  t)

(defttag :acl2s-protection)

(progn+touchable :all (redefun+rewrite chk-acceptable-ld-fn1-pair
    (:carpat (and (symbolp %val%)
        (open-input-channel-p %val%
          :object state) . %cdr%)
      :vars (%val% %cdr%)
      :mult 2
      :repl (and (symbolp %val%)
        (open-input-channel-p %val%
          :object state)
        (or (not (acl2s-protected-modep state))
          (<= (@ ld-level) 2)
          (not (eq %val% *standard-oi*))) . %cdr%)))
  (redefun+rewrite ld-read-eval-print
    (:carpat (prog2$ (and (equal (standard-oi state)
            *standard-oi*)
          (good-bye))
        state)
      :mult 1
      :repl (if (equal (standard-oi state)
          *standard-oi*)
        (pprogn (makunbound-global 'acl2s-password
            state)
          (prog2$ (good-bye)
            state))
        state))))

(defttag nil)