GV124 assurance

GV124 closes the semantic-only learning counterexample without pretending that Agda can prove a human mental state. The compiler proves the structural review boundary: every current lesson carries a non-empty review surface plus semantic, code, and assurance probes; evidence is current only when both the learning requirement and the exact rendered review contract match; and the new review-surface lesson remains represented in carried debt until human evidence closes it.

Which code is semantically load-bearing, whether the probes are pedagogically adequate, and whether a human response demonstrates sufficient understanding remain Protocol and human-review judgment. Independent catch-up testing exposed that the first purpose review surface was too small for its own probes; that observation is preserved as a second counterexample, and the old contract is now machine-checkably stale under the corrected lesson.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV124 where

open import Agda.Builtin.Bool using (true; false)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.List using ([]; _∷_)
open import Govenv.Assurance.GV124.Counterexample.SemanticOnlyProgress using
  (semanticOnlyEvidence; contractMatchedEvidence)
open import Govenv.Assurance.GV124.Counterexample.InsufficientPurposeReviewSurface using
  (evidenceUnderInsufficientContract)
open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Learning using
  ( allLearningPrompts; allLessonsReviewable; carriedDebt; containsRequirement
  ; lessonEvidenced; purposeLesson; reviewSurfaceRequirement )

record Proposition : Set where
  constructor satisfied
  field
    everyCurrentLessonHasReviewContract :
      allLessonsReviewable allLearningPrompts ≡ true
    reviewSurfaceRequirementRemainsCarried :
      containsRequirement reviewSurfaceRequirement carriedDebt ≡ true
    semanticOnlyEvidenceIsRejected :
      lessonEvidenced purposeLesson (semanticOnlyEvidence ∷ []) ≡ false
    exactCurrentContractIsAccepted :
      lessonEvidenced purposeLesson (contractMatchedEvidence ∷ []) ≡ true
    insufficientObservedContractIsStale :
      lessonEvidenced purposeLesson (evidenceUnderInsufficientContract ∷ []) ≡ false

proof : Proposition
proof = satisfied refl refl refl refl refl

evidence : StaticEvidence 
evidence = staticEvidence Proposition proof