github-ui.ts

// @ts-nocheck
const { Octokit } = require("@octokit/rest");

export class GitHubUI {
  constructor() {
    this.octokit = null;
    this.webhookSecret = process.env.WEBHOOK_SECRET;
  }

  /**
   * Initialize GitHub client
   * @param {string} token - GitHub token
   */
  initialize(token) {
    this.octokit = new Octokit({ auth: token });
  }

  /**
   * Enhanced Prompt 1.1 — Suggested Spec Comments (LLM-generated)
   * Goal: Auto-insert spec suggestions as native review comments on new/updated PRs.
   * Inputs: PR diff, surrounding code, existing tests.
   * Explicit Outputs: One GitHub review comment per suggestion, formatted with confidence and rationale
   */
  async createSpecComment(context, specSuggestion) {
    const { payload } = context;
    const { pull_request, repository } = payload;

    const commentBody = this.formatSpecComment(specSuggestion);

    // Create review comment anchored to specific line
    const reviewComment = await this.octokit.pulls.createReviewComment({
      owner: repository.owner.login,
      repo: repository.name,
      pull_number: pull_request.number,
      commit_id: pull_request.head.sha,
      path: specSuggestion.filePath,
      line: specSuggestion.lineNumber,
      body: commentBody,
    });

    return reviewComment;
  }

  /**
   * Enhanced format spec comment with confidence transparency and action buttons
   * @param {Object} specSuggestion - Spec suggestion object
   * @returns {string} Formatted comment body
   */
  formatSpecComment(specSuggestion) {
    const { functionName, preconditions, postconditions, invariants, confidence, reasoning } =
      specSuggestion;

    // Confidence transparency (Prompt 5.2)
    const confidenceEmoji = confidence >= 0.8 ? "🟢" : confidence >= 0.6 ? "🟡" : "🔴";
    const confidenceText = confidence >= 0.8 ? "High" : confidence >= 0.6 ? "Medium" : "Low";

    return `## 🤖 SpecSync: Specification for \`${functionName}\`

**File:** \`${specSuggestion.filePath}\` (line ${specSuggestion.lineNumber})
**Confidence:** ${confidenceEmoji} ${confidenceText} (${Math.round(confidence * 100)}%)

### 📋 Preconditions
${preconditions.map((pre) => `- ${pre}`).join("\n")}

### ✅ Postconditions
${postconditions.map((post) => `- ${post}`).join("\n")}

### 🔒 Invariants
${invariants.map((inv) => `- ${inv}`).join("\n")}

### 💭 Reasoning
${reasoning}

---

**Actions:**
- ✅ \`/specsync accept\` - Accept this specification
- ✏️ \`/specsync edit\` - Edit the specification
- ❌ \`/specsync ignore\` - Ignore this suggestion
- 🔍 \`/specsync review\` - Request manual review

*Generated by SpecSync AI*`;
  }

  /**
   * Enhanced Prompt 1.2 — Inline Spec Coverage Tags
   * Goal: Show real-time spec status beside every changed function in PR view.
   * Inputs: Proof status JSON produced by CI.
   * Explicit Outputs: Inline badge with tooltip and linked Lean theorem
   */
  async createCoverageCheck(context, proofStatus) {
    const { payload } = context;
    const { pull_request, repository } = payload;

    const checkRun = await this.octokit.checks.create({
      owner: repository.owner.login,
      repo: repository.name,
      name: "SpecSync Coverage",
      head_sha: pull_request.head.sha,
      status: "completed",
      conclusion: proofStatus.coverage >= 70 ? "success" : "failure",
      output: {
        title: `Spec Coverage: ${proofStatus.coverage}%`,
        summary: this.generateCoverageSummary(proofStatus),
        text: this.generateCoverageDetails(proofStatus),
      },
      annotations: this.generateCoverageAnnotations(proofStatus),
    });

    return checkRun;
  }

  /**
   * Enhanced generate coverage annotations with tooltips and links
   * @param {Object} proofStatus - Proof status object
   * @returns {Array} Annotations array
   */
  generateCoverageAnnotations(proofStatus) {
    const annotations = [];

    proofStatus.functions.forEach((func) => {
      const statusEmoji = func.hasProof ? "🟢" : "🔴";
      const statusText = func.hasProof ? "Spec verified" : "Missing spec";

      annotations.push({
        path: func.filePath,
        start_line: func.line,
        end_line: func.line,
        annotation_level: func.hasProof ? "notice" : "failure",
        message: `${statusEmoji} ${statusText}`,
        title: func.hasProof ? "Spec Verified" : "Missing Spec",
        raw_details: this.generateTooltipContent(func),
      });
    });

    return annotations;
  }

  /**
   * Generate tooltip content for coverage badges
   * @param {Object} func - Function object
   * @returns {string} Tooltip content
   */
  generateTooltipContent(func) {
    if (func.hasProof) {
      return `**Verified Specification**
- Theorem: ${func.theorem || "N/A"}
- Last verified: ${func.lastVerified || "Unknown"}
- [View Proof](${this.generateProofUrl(func)})`;
    } else {
      return `**Missing Specification**
- No formal specification found
- [Add Specification](${this.generateAddSpecUrl(func)})`;
    }
  }

  /**
   * Generate proof URL for tooltip
   * @param {Object} func - Function object
   * @returns {string} Proof URL
   */
  generateProofUrl(func) {
    return `${process.env.DASHBOARD_URL}/audit/${func.name}`;
  }

  /**
   * Generate add spec URL for tooltip
   * @param {Object} func - Function object
   * @returns {string} Add spec URL
   */
  generateAddSpecUrl(func) {
    return `${process.env.DASHBOARD_URL}/specs/add?function=${func.name}&file=${func.filePath}&line=${func.line}`;
  }

  /**
   * Enhanced Prompt 1.3 — ProofCheck Sidebar Panel
   * Goal: One expandable sidebar tab summarizing all proof results for this PR.
   * Inputs: Proof results, drift report.
   * Explicit Outputs: List of touched functions with status and "Prove Now" button
   */
  async createProofCheckComment(context, proofResults) {
    const { payload } = context;
    const { pull_request, repository } = payload;

    const commentBody = this.formatProofCheckComment(proofResults);

    const comment = await this.octokit.issues.createComment({
      owner: repository.owner.login,
      repo: repository.name,
      issue_number: pull_request.number,
      body: commentBody,
    });

    return comment;
  }

  /**
   * Enhanced format proof check comment with expandable sections and action buttons
   * @param {Object} proofResults - Proof results object
   * @returns {string} Formatted comment body
   */
  formatProofCheckComment(proofResults) {
    const { functions, drift, coverage } = proofResults;

    let comment = `## 🔍 ProofCheck Results

<details>
<summary>📊 Coverage Summary (${coverage}%)</summary>

| Function | Status | Proof | Drift |
|----------|--------|-------|-------|
`;

    functions.forEach((func) => {
      const status = func.proofValid ? "✅" : "❌";
      const driftStatus = func.hasDrift ? "⚠️" : "✅";
      comment += `| \`${func.name}\` | ${status} | ${func.theorem || "N/A"} | ${driftStatus} |\n`;
    });

    comment += `\n</details>\n\n`;

    if (drift.length > 0) {
      comment += `<details>
<summary>⚠️ Drift Detection (${drift.length} functions)</summary>

`;
      drift.forEach((d) => {
        comment += `### \`${d.functionName}\`
**Reason:** ${d.reason}
**Previous:** ${d.previousSpec}
**Current:** ${d.currentImplementation}

`;
      });
      comment += `</details>\n\n`;
    }

    comment += `**Actions:**
- 🔄 [Prove Now](${this.generateProveNowUrl(proofResults)}) - Re-run Lean proofs
- 📊 [View Dashboard](${this.generateDashboardUrl(proofResults)}) - Detailed analysis
- 📋 [Export Report](${this.generateExportUrl(proofResults)}) - Download proof artifacts

*Generated by SpecSync ProofCheck*`;

    return comment;
  }

  /**
   * Generate coverage summary for check run
   * @param {Object} proofStatus - Proof status object
   * @returns {string} Summary text
   */
  generateCoverageSummary(proofStatus) {
    const { coverage, totalFunctions, coveredFunctions, failedProofs } = proofStatus;

    return `## SpecSync Coverage Report

- **Coverage:** ${coverage}%
- **Functions:** ${coveredFunctions}/${totalFunctions} covered
- **Failed Proofs:** ${failedProofs}

${coverage >= 70 ? "✅ Coverage threshold met" : "❌ Coverage below threshold"}`;
  }

  /**
   * Generate detailed coverage report
   * @param {Object} proofStatus - Proof status object
   * @returns {string} Detailed report
   */
  generateCoverageDetails(proofStatus) {
    const { functions, proofs } = proofStatus;

    let details = "## Function Coverage\n\n";

    functions.forEach((func) => {
      const status = func.hasProof ? "🟢" : "🔴";
      details += `${status} \`${func.name}\` - ${func.filePath}:${func.line}\n`;
    });

    if (proofs.length > 0) {
      details += "\n## Proof Status\n\n";
      proofs.forEach((proof) => {
        const status = proof.valid ? "✅" : "❌";
        details += `${status} \`${proof.theorem}\` - ${proof.file}\n`;
      });
    }

    return details;
  }

  /**
   * Generate URL for re-running proofs
   * @param {Object} proofResults - Proof results object
   * @returns {string} URL
   */
  generateProveNowUrl(proofResults) {
    // This would trigger a GitHub Action dispatch
    return `https://github.com/${proofResults.repository}/actions/workflows/lean4-ci.yml`;
  }

  /**
   * Generate dashboard URL
   * @param {Object} proofResults - Proof results object
   * @returns {string} URL
   */
  generateDashboardUrl(proofResults) {
    return `${process.env.DASHBOARD_URL}/repo/${proofResults.repository}/pr/${proofResults.prNumber}`;
  }

  /**
   * Generate export URL
   * @param {Object} proofResults - Proof results object
   * @returns {string} URL
   */
  generateExportUrl(proofResults) {
    return `${process.env.DASHBOARD_URL}/export/${proofResults.repository}/${proofResults.prNumber}`;
  }

  /**
   * Handle spec comment actions
   * @param {Object} context - GitHub context
   * @param {Object} comment - Comment object
   */
  async handleSpecCommentAction(context, comment) {
    const { payload } = context;
    const { repository } = payload;

    if (comment.body.includes("/specsync accept")) {
      await this.handleAcceptAction(context, comment);
    } else if (comment.body.includes("/specsync edit")) {
      await this.handleEditAction(context, comment);
    } else if (comment.body.includes("/specsync ignore")) {
      await this.handleIgnoreAction(context, comment);
    } else if (comment.body.includes("/specsync review")) {
      await this.handleReviewAction(context, comment);
    }
  }

  /**
   * Handle accept action
   * @param {Object} context - GitHub context
   * @param {Object} comment - Comment object
   */
  async handleAcceptAction(context, comment) {
    const { payload } = context;
    const { repository } = payload;

    // Extract spec from comment and store it
    const spec = this.extractSpecFromComment(comment.body);

    // Store the accepted spec
    await this.storeAcceptedSpec(spec, context);

    // Hide the comment by marking as resolved
    await this.octokit.pulls.dismissReview({
      owner: repository.owner.login,
      repo: repository.name,
      pull_number: payload.pull_request.number,
      review_id: comment.pull_request_review_id,
      message: "Spec accepted and stored",
    });
  }

  /**
   * Extract spec from comment body
   * @param {string} commentBody - Comment body
   * @returns {Object} Extracted spec
   */
  extractSpecFromComment(commentBody) {
    // Parse the comment to extract spec details
    const lines = commentBody.split("\n");
    const spec = {
      functionName: "",
      preconditions: [],
      postconditions: [],
      invariants: [],
      confidence: 0,
      reasoning: "",
    };

    let currentSection = "";

    for (const line of lines) {
      if (line.includes("Specification for")) {
        spec.functionName = line.match(/`([^`]+)`/)?.[1] || "";
      } else if (line.includes("Confidence:")) {
        spec.confidence = parseInt(line.match(/(\d+)%/)?.[1] || "0");
      } else if (line.includes("### 📋 Preconditions")) {
        currentSection = "preconditions";
      } else if (line.includes("### ✅ Postconditions")) {
        currentSection = "postconditions";
      } else if (line.includes("### 🔒 Invariants")) {
        currentSection = "invariants";
      } else if (line.includes("### 💭 Reasoning")) {
        currentSection = "reasoning";
      } else if (line.startsWith("- ") && currentSection !== "reasoning") {
        const item = line.substring(2);
        if (currentSection === "preconditions") {
          spec.preconditions.push(item);
        } else if (currentSection === "postconditions") {
          spec.postconditions.push(item);
        } else if (currentSection === "invariants") {
          spec.invariants.push(item);
        }
      } else if (currentSection === "reasoning" && line.trim() && !line.startsWith("---")) {
        spec.reasoning += line + "\n";
      }
    }

    return spec;
  }

  /**
   * Store accepted spec
   * @param {Object} spec - Spec object
   * @param {Object} context - GitHub context
   */
  async storeAcceptedSpec(spec, context) {
    // Store in database or file system
    const { SpecAnalyzer } = require("./spec-analyzer");
    const specAnalyzer = new SpecAnalyzer();

    const functionKey = `${context.payload.repository.full_name}:${spec.functionName}`;
    await specAnalyzer.storeSpec(functionKey, spec);
  }

  /**
   * Handle edit action
   * @param {Object} context - GitHub context
   * @param {Object} comment - Comment object
   */
  async handleEditAction(context, comment) {
    // Create an editable version of the spec
    const spec = this.extractSpecFromComment(comment.body);

    // Generate edit form
    const editForm = this.generateEditForm(spec);

    await this.octokit.issues.createComment({
      owner: context.payload.repository.owner.login,
      repo: context.payload.repository.name,
      issue_number: context.payload.pull_request.number,
      body: editForm,
    });
  }

  /**
   * Generate edit form for spec
   * @param {Object} spec - Spec object
   * @returns {string} Edit form HTML
   */
  generateEditForm(spec) {
    return `## ✏️ Edit Specification for \`${spec.functionName}\`

<form method="POST" action="/specsync/edit">
  <input type="hidden" name="functionName" value="${spec.functionName}">
  
  <h3>Preconditions</h3>
  <textarea name="preconditions" rows="3">${spec.preconditions.join("\n")}</textarea>
  
  <h3>Postconditions</h3>
  <textarea name="postconditions" rows="3">${spec.postconditions.join("\n")}</textarea>
  
  <h3>Invariants</h3>
  <textarea name="invariants" rows="3">${spec.invariants.join("\n")}</textarea>
  
  <h3>Reasoning</h3>
  <textarea name="reasoning" rows="3">${spec.reasoning}</textarea>
  
  <button type="submit">Save Changes</button>
</form>`;
  }

  /**
   * Handle ignore action
   * @param {Object} context - GitHub context
   * @param {Object} comment - Comment object
   */
  async handleIgnoreAction(context, comment) {
    // Mark comment as resolved without storing spec
    const { payload } = context;
    const { repository } = payload;

    await this.octokit.pulls.dismissReview({
      owner: repository.owner.login,
      repo: repository.name,
      pull_number: payload.pull_request.number,
      review_id: comment.pull_request_review_id,
      message: "Spec suggestion ignored",
    });
  }

  /**
   * Handle review action
   * @param {Object} context - GitHub context
   * @param {Object} comment - Comment object
   */
  async handleReviewAction(context, comment) {
    // Create a review request
    const { payload } = context;
    const { repository } = payload;

    await this.octokit.issues.createComment({
      owner: repository.owner.login,
      repo: repository.name,
      issue_number: payload.pull_request.number,
      body: `## 🔍 Manual Review Requested

A manual review has been requested for the specification suggestion.

**Function:** ${this.extractSpecFromComment(comment.body).functionName}

Please review the suggested specification and provide feedback.`,
    });
  }
}