)]}'
{
  "commit": "5c2bbb76aebed1af1c75ae0c04ec32836e2efd8b",
  "tree": "979c3c108468e6bde21f839874d02f19be10c8b4",
  "parents": [
    "26c0252f6cd46334d0ad792cc0032ef0029b3f0d"
  ],
  "author": {
    "name": "Thomas Lively",
    "email": "tlively@google.com",
    "time": "Fri Dec 20 06:24:57 2024"
  },
  "committer": {
    "name": "Thomas Lively",
    "email": "tlively@google.com",
    "time": "Fri Dec 20 06:24:57 2024"
  },
  "message": "Super-minimal POC for bounded translation validation\n\nGiven a source and target module, validate that the functions in the\ntarget module are refinements of the corresponding functions in the\nsource module by translating the function bodies to SMT expressions and\nhaving Z3 either prove that they are equal for all inputs or find a\ncounterexample showing that they are not.\n\nThis minimal proof-of-concept can already prove that this source module:\n\n```\n(func $test (param $x i32) (result i32)\n  (i32.mul\n    (local.get 0)\n    (i32.const 2)\n  )\n)\n```\n\nIs refined by this target module:\n\n```\n(func $test (param $x i32) (result i32)\n  (i32.shl\n    (local.get 0)\n    (i32.const 1)\n  )\n)\n```\n\nBut not by this target module:\n\n```\n(func $test (param $x i32) (result i32)\n  (i32.shl\n    (local.get 0)\n    (i32.const 2)\n  )\n)\n```\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "d02096fa06e9c6604c71c98abbada0800d24b5cc",
      "old_mode": 33188,
      "old_path": "CMakeLists.txt",
      "new_id": "08e458f5c5abdde1ac3d9911a0670fb133de4cab",
      "new_mode": 33188,
      "new_path": "CMakeLists.txt"
    },
    {
      "type": "modify",
      "old_id": "c73797f54c22e7978f5bb2a442167cd24cd25788",
      "old_mode": 33188,
      "old_path": "src/tools/CMakeLists.txt",
      "new_id": "105ad3d011c0b1be735ccb9901c81970463ea701",
      "new_mode": 33188,
      "new_path": "src/tools/CMakeLists.txt"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "07d1507048eab32a52c289b187a4caf8e1821bd8",
      "new_mode": 33188,
      "new_path": "src/tools/wasm-validate-refinement.cpp"
    }
  ]
}